Θεωρία τύπων

Στα Μαθηματικά, στη Λογική και στη Επιστήμη των Υπολογιστών, η Θεωρία Τύπων είναι ένα από τα τυπικά συστήματα τα οποία χρησιμοποιούνται στην Απλοϊκή Θεωρία Συνόλων, ή στη μελέτη τέτοιων φορμαλισμών γενικότερα. Στη Θεωρία των Γλωσσών Προγραμματισμού, ενός κλάδου της Επιστήμης των Υπολογιστών, η Θεωρία Τύπων μπορεί να αναφέρεται στο σχεδιασμό, στην ανάλυση και στη μελέτη των Συστημάτων Τύπων, παρόλο που κάποιοι επιστήμονες της Πληροφορικής περιορίζουν τη σημασία του όρου στη μελέτη των αφηρημένων φορμαλισμών όπως ο λ-λογισμός με τύπους.

Ο Μπέρτραντ Ράσελ εφηύρε την πρώτη θεωρία τύπων μετά την ανακάλυψή του πως η εκδοχή της Απλοϊκής Θεωρίας Συνόλων του Γκότλομπ Φρέγκε υπόκειντο στο Παράδοξο του Ράσελ. Αυτή η θεωρία τύπων βρίσκεται σε περίοπτη θέση στο Principia Mathematica των Άλφρεντ Νορθ Γουάιτχεντ και Ράσελ. Αποφεύγει το Παράδοξο του Ράσελ με το να δημιουργεί πρώτα μία ιεραρχία τύπων, και κατόπιν να αναθέτει κάθε μαθηματική (και πιθανώς άλλη) οντότητα σε έναν τύπο. Τα αντικείμενα ενός δοσμένου τύπου δημιουργούνται αποκλειστικά από αντικείμενα προηγούμενων τύπων (αυτών που είναι χαμηλότερα στην ιεραρχία), αποφεύγοντας έτσι τις επαναλήψεις.

Ο Αλόνσο Τσερτς, εφευρέτης του λ-λογισμού, ανέπτυξε μια Λογική Υψηλής Τάξης γνωστότερη ως Θεωρία Τύπων του Τσερτς, με σκοπό να αποφύγει το Παράδοξο Κλέινι-Ρόσερ που ταλαιπωρούσε τον αρχικό αμιγή λ-λογισμό. Η θεωρία τύπων του Τσερτς είναι μια παραλλαγή του λ-λογισμού στην οποία οι εκφράσεις (που επίσης καλούνται φόρμουλες ή λ-όροι) κατηγοριοποιούνται σε τύπους, και οι τύποι των εκφράσεων περιορίζουν τους τρόπους με τους οποίους μπορούν να συνδυαστούν. Με άλλα λόγια, είναι ένας λ-λογισμός με τύπους.

Το άρθρο Η Θεωρία Τύπων του Church στην Εγκυκλοπαίδεια την Φιλοσοφίας του Στάνφορντ είναι αφιερωμένο σε αυτό το θέμα.

Σήμερα χρησιμοποιούνται πολλοί άλλοι παρόμοιοι λογισμοί, συμπεριλαμβανομένης της Ιντουισιονιστικής θεωρίας τύπων του Περ Μάρτιν-Λέφ , του Συστήματος F του Ζαν-Ιβ Ζιράρ και του Λογισμoύ των κατασκευών. Στον λ-λογισμό με τύπους, οι τύποι παίζουν ένα ρόλο παρόμοιο με αυτό των συνόλων στη Θεωρία Συνόλων.

Ιστορία

1900 - 1927

Η Προέλευση της Θεωρίας Τύπων του Ράσελ: Σε ένα γράμμα του προς τον Γκότλομπ Φρέγκε (1902) ο Ράσελ ανακοίνωσε την ανακάλυψη του παραδόξου στο Begriffsschrift του Φρέγκε. Ο Φρέγκε απάντησε τάχιστα, αναγνωρίζοντας το πρόβλημα και προτείνοντας μια λύση σε μια τεχνική συζήτηση επιπέδων (levels). Παραθέτοντας τον Φρέγκε:

Παρεμπιπτόντως, μου φαίνεται ότι η έκφραση «ένα κατηγόρημα δηλώνει τον εαυτό του» δεν είναι ακριβής. Ένα κατηγόρημα είναι κατά κανόνα μια συνάρτηση πρώτου επιπέδου, και αυτή η συνάρτηση χρειάζεται ένα αντικείμενο ως παράμετρο και δεν μπορεί να έχει τον εαυτό της ως παράμετρο (subject). Συνεπώς, θα προτιμούσα να πω «μια έννοια δηλώνεται από την έκτασή της».

Συνεχίζει δείχνοντας πως θα μπορούσε αυτό να δουλέψει αλλά φαίνεται πως τελικά κάνει πίσω. (Σε μια υποσημείωση, ο φαν Χάιενορτ (van Heijenoort) σημειώνει πως ο Φρέγκε είχε χρησιμοποιήσει ένα σύμβολο (horseshoe) «για την αναγωγή συναρτήσεων δεύτερου επιπέδου σε συναρτήσεις πρώτου επιπέδου»). Ως συνέπεια αυτού που έχει γίνει γνωστό ως το Παράδοξο του Ράσελ τόσο ο Frege όσο και ο Ράσελ έπρεπε να διορθώσουν γρήγορα τα έργα τους που είχαν προς εκτύπωση. Στο Παράρτημα Β που ο Ράσελ πρόσθεσε στο βιβλίο του Principles of Mathematics του 1903, μπορεί κανείς να βρει την «διστακτική» του «θεωρία τύπων».

Το θέμα στοίχειωνε τον Ράσελ για περίπου πέντε χρόνια (1903–1908). Ο Γουίλαρντ Κιν (Willard Quine) στον πρόλογό του για το Η Μαθηματική λογική βασισμένη στην θεωρία των τύπων (1908) του Ράσελ παρουσιάζει μια ιστορική σύνοψη για την προέλευση της θεωρίας των τύπων και της «διακλαδιζόμενης» θεωρίας των τύπων. Ο Ράσελ πρότεινε με σειρά του κάποιες εναλλακτικές: (i) εγκαταλείποντας την θεωρία των τύπων (1905) και προτείνοντας τρεις θεωρίες το 1905: (ii.1) την θεωρία ζιγκ ζαγκ (zigzag theory), (ii.2) την θεωρία του περιορισμού του μεγέθους (theory of limitation of size), (ii.3) την θεωρία χωρίς κλάσεις (no-class theory) (1905–1906), και κατόπιν (iii) επανέφερε την θεωρία των τύπων (1908).

Ο Κιν παρατηρεί ότι η εισαγωγή της έννοιας της «προφανούς μεταβλητής» από τον Ράσελ είχε το ακόλουθο αποτέλεσμα: «η διάκριση μεταξύ του 'όλα' ('all') και του 'κάποιο' ('any'): Το 'όλα' εκφράζεται από την δεσμευμένη ('προφανή') μεταβλητή της καθολικής ποσοτικοποίησης, που εκτείνεται πάνω σε έναν τύπο, και το 'κάποιο' εκφράζεται από την ελεύθερη ('πραγματική') μεταβλητή που αναφέρεται σχηματικά σε οτιδήποτε ανεξαρτήτως τύπου». Ο Κιν απορρίπτει αυτή την ιδέα της «δεσμευμένης μεταβλητής» ως «άσκοπη εκτός μια συγκεκριμένη πτυχή της θεωρίας των τύπων».

Η «διακλαδιζόμενη» θεωρία τύπων του 1908

Ο Κιν εξηγεί την διακλαδιζόμενη θεωρία ως εξής: «Ονομάζεται έτσι επειδή ο τύπος μιας συνάρτησης εξαρτάται τόσο από τους τύπους των παραμέτρων της όσο και από τους τύπους των προφανών μεταβλητών που περιέχονται σε αυτήν (ή στην έκφρασή της), σε περίπτωση που αυτές υπερβαίνουν τους τύπους των παραμέτρων». Ο Στίβεν Κλέινι στο βιβλίο του Εισαγωγή στα Μετα-Μαθηματικά του 1952 περιγράφει την διακλαδιζόμενη θεωρία τύπων ως εξής:

Τα πρωτογενή αντικείμενα ή άτομα (δηλ. τα δοσμένα αντικείμενα που δεν υποβάλλονται σε λογική ανάλυση) αποδίδονται σε έναν τύπο (π.χ. τύπο 0), οι ιδιότητες των ατόμων στον τύπο 1, οι ιδιότητες των ιδιοτήτων των ατόμων στον τύπο 2, κλπ. Και δεν αναγνωρίζονται ιδιότητες που δεν εμπίπτουν σε έναν από αυτούς τους λογικούς τύπους (π.χ. αυτό βάζει τις ιδιότητες 'προβλέψιμο' και 'μη προβλέψιμο' ... εκτός του πεδίου της λογικής). Μία πιο λεπτομερής έκθεση θα περιέγραφε τους αποδεκτούς τύπους για άλλα αντικείμενα ως σχέσεις και κλάσεις. Στη συνέχεια για να αποκλείσει μη κατηγορηματικές δηλώσεις μέσα σε έναν τύπο, οι τύποι πάνω από τον τύπο 0 διαχωρίζονται περαιτέρω σε τάξεις. Συνεπώς για τον τύπο 1, οι ιδιότητες που ορίζονται χωρίς την αναφορά πληρότητας ανήκουν στον τύπο 0 και ιδιότητες που ορίζονται χρησιμοποιώντας όλες τις ιδιότητες μιας τάξης ανήκουν στην επόμενη μεγαλύτερη τάξη. Αλλά αυτός ο διαχωρισμός σε τάξεις κάνει αδύνατη την οικεία ανάλυση, η οποία όπως είδαμε περιέχει μη κατηγορηματικούς ορισμούς. Για να αποφύγουμε το παραπάνω αποτέλεσμα ο Ράσελ εισήγαγε το αξίωμα της αναγωγής το οποίο λέει ότι για κάθε ιδιότητα που ανήκει σε τάξη μεγαλύτερη της μηδενικής υπάρχει μια συνεκτατική (coextensive) ιδιότητα (που ανήκει στα ίδια αντικείμενα) τάξης 0. Αν υποθέσουμε ότι υπάρχουν μόνο ιδιότητες που μπορούν να οριστούν, τότε το αξίωμα ουσιαστικά λέει ότι για κάθε μη κατηγορηματικό ορισμό μέσα σε ένα τύπο υπάρχει ένας ισοδύναμος κατηγορηματικός (Kleene 1952:44-45)

Το αξίωμα της αναγωγής και η ιδέα της «μήτρας»

Αλλά επειδή οι παραδοχές της διακλαδιζόμενης θεωρίας θα αποδεικνύονταν (παραθέτοντας τον Κιν) «επαχθείς», ο Ράσελ το 1908 στο έργο του Η Μαθηματική λογική βασισμένη στην θεωρία των τύπων θα πρότεινε επίσης το αξίωμα της αναγωγής. Ως το 1910, οι Ουάιτχεντ και ο Ράσελ στο έργο τους Principia Mathematica θα επαύξαναν περαιτέρω αυτό το αξίωμα με την ιδέα μιας μήτρας, η οποία ήταν μια πλήρως επεκτάσιμη προδιαγραφή μιας συνάρτησης. Από την μήτρα της μια συνάρτηση θα μπορούσε να παραχθεί μέσω της διαδικασίας της «γενίκευσης» και αντίστροφα, δηλ. οι δύο διεργασίες είναι αντιστρέψιμες -- (i) γενίκευση από μήτρα σε συνάρτηση (με χρήση προφανών μεταβλητών) και (ii) η αντίστροφη διαδικασία της αναγωγής τύπου με κλάσεις-τιμών αντικατάσταση των ορισμάτων για την προφανή μεταβλητή. Με αυτή τη μέθοδο αποφεύγουμε το να είμαστε μη κατηγορηματικοί.

Πίνακες Αλήθειας

Τελικά ο Έμιλ Ποστ (1921) θα έβαζε τέλος στην προβληματική θεωρία τύπων του Ράσελ με τις «συναρτήσεις αλήθειας» και τους αντίστοιχους πίνακες αληθείας. Στην «Εισαγωγή» του κατηγορεί την έννοια της προφανούς μεταβλητής του Ράσελ. Αν και η πλήρης θεωρία [των Ουάιτχεντ και Ράσελ (1910, 1912, 1913)] απαιτεί για την έκφραση των λημμάτων τις πραγματικές και προφανείς μεταβλητές οι οποίες αναπαριστούν ατομικές και προτασιακές συναρτήσεις διαφορετικών ειδών, οπότε απαιτεί την προβληματική θεωρία των τύπων, αυτή η υποθεωρία χρησιμοποιεί μόνο πραγματικές μεταβλητές οι οποίες αναπαριστούν μόνο μία οντότητα την οποία οι συγγραφείς ονομάζουν βασικές προτάσεις.

Περίπου τον ίδιο καιρό ο Λούντβιχ Βιτγκενστάιν το 1922 έκανε μια σύντομη εργασία στη θεωρία των τύπων στο έργο του Tractatus Logico-Philosophicus στην οποία σημειώνει τα ακόλουθα στα μέρη 3.331–3.333:

3.331 Από αυτή την παρατήρηση αποκτούμε μια καλύτερη εικόνα – της Θεωρίας Τύπων του Ράσελ. Το λάθος του Ράσελ φαίνεται από το γεγονός ότι σχεδιάζοντας τους συμβολικούς του κανόνες πρέπει να μιλήσει για τη σημασία των συμβόλων αυτών.

3.332 Καμία πρόταση δεν μπορεί να πει κάτι για τον εαυτό της, επειδή το σύμβολο της πρότασης δεν μπορεί να εμπεριέχεται στον εαυτό του (αυτή είναι όλη η «θεωρία των τύπων»).

3.333 Μια συνάρτηση δεν μπορεί να είναι παράμετρός της, επειδή το σύμβολο της συνάρτησης περιέχει ήδη το πρωτότυπο της παραμέτρου του και δεν μπορεί να περιέχει τον εαυτό του...

Ο Βιτγκενστάιν επίσης πρότεινε τη μέθοδο του πίνακα αλήθειας. Από το 4.3 έως το 5.101, ο Βιτγκενστάιν υιοθετεί μια μη δεσμευμένη μολυβιά του Σέφερ (Sheffer stroke στα αγγλικά, η μολυβιά του Σέφερ είναι ο χαρακτήρας '|') ως τη θεμελιώδη λογική οντότητά του και κατόπιν καταγράφει όλες τις 16 συναρτήσεις δύο μεταβλητών (5.101).

Η ιδέα της μήτρας ως πίνακα αλήθειας εμφανίζεται στα 1940-1950 στο έργο του Τάρσκι, π.χ. στα ευρετήριά του το 1946 «Μήτρα, βλέπε: Πίνακας αλήθειας»

Οι αμφιβολίες του Ράσελ

Ο Ράσελ στην Εισαγωγή στη Μαθηματική Φιλοσοφία (1920) αφιερώνει ένα κεφάλαιο στο «Αξίωμα του Απείρου και των λογικών τύπων» στο οποίο λέει τα εξής:

Πλέον η θεωρία τύπων δεν ανήκει στο τελειωμένο και βέβαιο κομμάτι της δουλειάς μας: μεγάλο μέρος της θεωρίας είναι ακόμη ελλιπές, μπερδεμένο και θολό. Αλλά η ανάγκη για κάποια αρχή των τύπων είναι λιγότερο αμφισβητήσιμη από την ακριβή μορφή που θα πάρει αυτή η αρχή. Και σε σύνδεση με το αξίωμα του απείρου είναι ιδιαίτερα εύκολο να δούμε την αναγκαιότητα μια τέτοιας αρχής.

Ο Ράσελ εγκαταλείπει το αξίωμα της αναγωγής: Στη δεύτερη έκδοση του Principia Mathematica (1927) αναγνωρίζει το επιχείρημα του Βιτγκενστάιν. Στην αρχή της εισαγωγής παραδέχεται: «δεν υπάρχει αμφιβολία... ότι δε χρειάζεται η διαφοροποίηση των εννοιών πραγματική και προφανής μεταβλητή». Οικειοποιείται την έννοια της μήτρας και δηλώνει «Μια συνάρτηση μπορεί να εμφανιστεί σε μια μήτρα μόνο μέσω των τιμών της» (αλλά συμπληρώνει σε μια υποσημείωση: «Αντικαθιστά (όχι αρκετά ικανοποιητικά) το αξίωμα της αναγωγής.») Επιπλέον εισάγει τη νέα (συντομευμένη, γενική) έννοια της «μήτρας», αυτή της «λογικής μήτρας .. που δεν περιέχει σταθερές. Επομένως το p|q είναι μια λογική μήτρα». Βλέπουμε ότι ο Ράσελ εγκατέλειψε την ιδέα του αξιώματος της αναγωγής αλλά στις τελευταίες παραγράφους δηλώνει ότι «από τις παρούσες πρωταρχικές έννοιες» δεν μπορεί να παράγει «σχέσεις του Ντέντεκιντ και σχέσεις καλώς διατεταγμένες» και παρατηρεί ότι αν υπάρχει κάποιο καινούριο αξίωμα να αντικαταστήσει το αξίωμα της αναγωγής «μένει να ανακαλυφθεί».

Θεωρία των απλών τύπων

Στη δεκαετία του 20 οι Λέον Τσβίστεκ και Φρανκ Π. Ράμσεϊ παρατήρησαν ότι αν κάποιος θέλει να εγκαταλείψει την αρχή του φαύλου κύκλου, η ιεραρχία των επιπέδων των τύπων στην «διακλαδιζόμενη θεωρία των τύπων» (δείτε το ιστορικό σημείωμα πριν) μπορεί να καταρρεύσει.

Η προϊούσα περιορισμένη λογική ονομάζεται θεωρία των απλών τύπων ή πιο απλά θεωρία των τύπων. Λεπτομερείς εκθέσεις της απλής θεωρίας των τύπων εκδόθηκαν στα τέλη του 1920 και στις αρχές του 30 από τους Ρ. Κάρναπ, Φ. Ράμσεϊ, Ου.Β.Ο. Κιν και Α. Τάρσκι. Το 1940 ο Αλόνσο Τσέρτς την επανασχεδίασε ως λ-λογισμό με απλούς τύπους. και εξετάστηκε και από τον Γκέντελ το 1944.

1940s - σήμερα

Ο Κιν αναφέρει ότι ο Ράμσεϊ το 1931 παρότρυνε την «πτώση του διακλαδισμού και του αξιώματος της αναγωγής». Ο Κιν είναι της γνώμης ότι «η αποτυχία του Ράσελ ήταν εξαιτίας αυτής της αποτυχίας της διακρίσεως ανάμεσα στις προτασιακές συναρτήσεις ως συμβολισμούς και τις προτασιακές συναρτήσεις ως ιδιότητες και σχέσεις [Ο σχολιασμός του Κιν στο Ράσελ 1908 στο φαν Χάιενορτ 1967:151-152].»<!

Γκέντελ 1944

Ο Κουρτ Γκέντελ στην Μαθηματική Λογική του Ράσελ του το 1944 έδωσε σε μια υποσημείωση τον ακόλουθο ορισμό της «θεωρίας των απλών τύπων»:

Ως θεωρία των απλών τύπων εννοώ το δόγμα που λέει ότι τα αντικείμενα της σκέψης (ή, κατά μια άλλη ερμηνεία, οι συμβολικές εκφράσεις) είναι διαχωρισμένα σε τύπους, ήτοι: άτομα, ιδιότητες ατόμων, σχέσεις μεταξύ ατόμων, ιδιότητες τέτοιων σχέσεων, κλπ. (με μια παρόμοια ιεραρχία για επεκτάσεις), και ότι οι προτάσεις της μορφής: «Το a έχει τη ιδιότητα φ», «το b έχει τη σχέση R με το c», κλπ. είναι δίχως νόημα, αν τα a, b, c, R, φ δεν είναι τύποι συμβατοί μεταξύ τους. Εξαιρούνται οι μικτοί τύποι (όπως οι κλάσεις που περιέχουν άτομα και κλάσεις ως στοιχεία) και συνεπώς και οι υπερπεπερασμένοι τύποι (όπως η κλάση όλων των κλάσεων από πεπερασμένους τύπους). Το ότι αυτή η θεωρία των απλών τύπων αρκεί για την αποφυγή επίσης των επιστημονικών παραδόξων φαίνεται μετά από μια ενδελεχέστερη ανάλυση αυτών (Cf. Ramsey 1926 και Tarski 1935, σελ. 399).

Κατέληξε ότι η Θεωρία των Απλών Τύπων και η Αξιωματική Θεωρία Συνόλων, «επιτρέπουν την παραγωγή των σύγχρονων μαθηματικών και ταυτόχρονα αποφεύγουν όλα τα γνωστά παράδοξα» (Γκέντελ 1944:126). Επιπροσθέτως, η θεωρία των απλών τύπων «είναι το σύστημα του ''Principia Mathematica'' σε μια κατάλληλη ερμηνεία... Ωστόσο, πολλά από τα συμπτώματα δείχνουν ξεκάθαρα ότι οι βασικές έννοιες χρειάζονται περαιτέρω διευκρίνιση» (Γκέντελ 1944:126).

Φορμαλισμοί της θεωρίας τύπων

Σύστημα ST του Μέντελσον

Το ακόλουθο σύστημα είναι το ST του Μέντελσον (1997, 289–293). To ST είναι ισοδύναμο με τη διακλαδιζόμενη θεωρία του Ράσελ σε συνδυασμό με το αξίωμα της αναγωγής. Το πεδίο ποσοτικοποίησης χωρίζεται σε μια αύξουσα ιεραρχία τύπων , όπου όλα τα άτομα έχουν ένα τύπο. Οι ποσοτικές μεταβλητές έχουν μόνο ένα τύπο. Αυτό σημαίνει ότι η λογική είναι λογική πρώτης-τάξης. Το ST είναι «απλό» (σε σχέση με τη θεωρία τύπων του Principia Mathematica) κυρίως γιατί όλα τα μέλη του πεδίου και του συμπληρωματικού πεδίου (co-domain) μιας σχέσης πρέπει να είναι του ίδιου τύπου. Υπάρχει ένας ελάχιστος τύπος του οποίου τα άτομα δεν έχουν μέλη και είναι μέλη του δεύτερου χαμηλότερου τύπου. Τα άτομα του ελάχιστου τύπου αντιστοιχούν στα άτομα άλλων συνολοθεωριών. Κάθε τύπος έχει έναν αμέσως μεγαλύτερο τύπο, παρόμοια με την έννοια του διαδόχου στην αριθμητική Πεάνο. Αν και το ST δε μας λέει αν υπάρχει ένας μέγιστος τύπος ένας υπερπεπερασμένος αριθμός τύπων δεν παρουσιάζει δυσκολία. Αυτά τα στοιχεία, που θυμίζουν τα αξιώματα Πεάνο, κάνουν βολική την ανάθεση ενός φυσικού αριθμού σε κάθε τύπο αρχίζοντας από το 0 για τον ελάχιστο τύπο. Αλλά η θεωρία τύπων δεν απαιτεί τον προηγούμενο ορισμό των φυσικών αριθμών.

Τα συμβατά σύμβολα με την ST είναι οι μεταβλητές με τόνο και το πρόθεμα $\in$. Σε οποιαδήποτε φόρμουλα οι μεταβλητές χωρίς τόνο έχουν όλες τον ίδιο τύπο ενώ οι μεταβλητές με τόνο ($x'$) έχουν τον αμέσως μεγαλύτερο τύπο. Οι ατομικές φόρμουλες της ST έχουν δύο μορφές, $x=y$ (ταυτότητα) και $y\in x'$. Το πρόθεμα $\in$ δηλώνει την προτιθέμενη ερμηνεία, την σχέση μέλους συνόλου.

Όλες οι μεταβλητές που εμφανίζονται στον ορισμό της ταυτότητας και στα αξιώματα της Εκτασιμότητας και Κατανόησης προέρχονται από άτομα από ένα εκ των δύο συνεχόμενων τύπων. Μόνο οι μεταβλητές χωρίς τόνο (που προέρχονται από τον «χαμηλότερο» τύπο) μπορούν να εμφανιστούν στα αριστερα του '$\in$', ενώ τα δεξιά μόνο μεταβλητές με τόνο (που προέρχονται από «υψηλότερο» τύπο) μπορούν να εμφανιστούν. Ο πρώτης-τάξης φορμαλισμός του ST αποκλείει την ποσοτικοποίηση προς όφελος των τύπων. Ως συνέπεια κάθε ζευγάρι από συνεχόμενους τύπους απαιτεί το δικό του αξίωμα της Εκτασιμότητας και Κατανόησης, το οποίο είναι πιθανό αν η Εκτασιμότητα και η Κατανόηση παρακάτω θεωρούνται σαν σχήματα αξιωμάτων που εφαρμόζονται σε τύπους.

• Ταυτότητα, ορίζεται ως $x=y\leftrightarrow \forall z'[x\in z'\leftrightarrow y\in z']$.

• Επεκτασιμότητα. Ένα αξιωματικό σχήμα. $\forall x[x\in y'\leftrightarrow x\in z']\rightarrow [y'=z']$.

Αν $\Phi (x)$ είναι οποιαδήποτε φόρμουλα πρώτης τάξης που περιέχει την ελεύθερη μεταβλητή $x$.

• Κατανόηση. Ένα αξιωματικό σχήμα. $\exists z'\forall x[x\in z'\leftrightarrow \Phi (x)]$.

Σημείωση. Κάθε συλλογή αντικειμένων του ίδιου τύπου αποτελούν ένα αντικείμενο με επόμενης τάξης τύπο. Η Κατανόηση είναι σχηματική όσον αφορά το $\Phi (x)$ όπως επίσης και τους τύπους.

• Άπειρο. Υπάρχει μια μη κενή δυαδική σχέση $R$ στα άτομα του χαμηλότερου τύπου, που είναι μη ανακλαστική, ματαβατική, και ισχυρά συνδεδεμένη: $\forall x,y[x\neq y\rightarrow [xRy\vee yRx]]$.

Σημείωση. Το άπειρο είναι το μοναδικό πραγματικό αξίωμα τoυ ST που είναι καθαρά μαθηματικό στη φύση του. Μας βεβαιώνει ότι το $R$ είναι μια αυστηρά ολική διάταξη, με ένα πεδίο ταυτόσημο με το συμπληρωματικό πεδίο. Αν αναθέσουμε 0 στο χαμηλότερο τύπο το $R$ έχει τύπο 3. Το άπειρο μπορεί να ικανοποιηθεί αν ο (συμπληρωματικό) τομέας του $R$ είναι άπειρο, οπότε απαιτεί την ύπαρξη ενός άπειρου συνόλου. Αν οι σχέσεις ορίζονται σε σχέση με διατεταγμένα ζεύγη, το αξίωμα απαιτεί τον προηγούμενο ορισμό του διατεταγμένου ζεύγους. Ο ορισμός του Κουρατόφσκι, προσαρμοσμένος στο ST, είναι αυτό που χρειάζεται. Στη βιβλιογραφία δεν εξηγείται γιατί το σύνηθες αξίωμα του απείρου (υπάρχει άλλες συνολοθεωρίες δεν μπορεί να ταιριάξει με το ST.

Το ST αποκαλύπτει πως η θεωρία τύπων μπορεί να αναχθεί στην αξιωματική θεωρία συνόλων. Επιπλέον η πιο λεπτομερής οντολογία του ST, περιορισμένη σε αυτό που τώρα ονομάζεται «επαναλαμβανόμενη σύλληψη του συνόλου» (αγγλικά: iterative conception of set), περιέχει αξιώματα που είναι πολύ απλούστερα των συμβατικών συνολοθεωριών, όπως της ZFC. Συνολοθεωρίες των οποίων σημείο εκκίνησης είναι η θεωρία τύπων αλλά τα αξιώματά τους, η Οντολογία και η ορολογία διαφέρουν από αυτή περιλαμβάνουν τη Νέα Θεμέλια και Συνολοθεωρία των Σκοτ-Πότερ.

Φόρμουλες βασισμένες στην ισότητα

Η θεωρία τύπων του Τσερτς έχει μελετηθεί εκτενώς από δύο μαθητές του, τον Λέον Χένκιν και τον Πίτερ Μπρους Άντριους. Καθώς η ST είναι μια λογική υψηλής τάξης, και στις λογικές υψηλής τάξης μπορεί κανείς να ορίσει προτασιακούς συνδέσμους από την άποψη της λογικής ισοδυναμίας και των ποσοδεικτών, το 1963 ο Χένκιν ανέπτυξε μια μορφοποίηση της ST βασισμένη στην ισότητα, αλλά στην οποία περιόρισε την προσοχή του στους κατηγορηματικούς τύπους. Το παραπάνω απλοποιήθηκε αργότερα τον ίδιο χρόνο από τον Άντριους στη θεωρία Q₀. Κάτω από αυτό το πρίσμα η ST μπορεί να θεωρηθεί ως ένα είδος λογικής υψηλής τάξης, η οποία χαρακτηρίστηκε από τον Π.Τ. Τζόνστον στο Sketches of an Elephant ότι έχει μια λάμδα-υπογραφή η οποία είναι μια υψηλής-τάξης υπογραφή που δεν περιέχει σχέσεις και χρησιμοποιεί μόνο γινόμενα και βέλη (τύποι συναρτήσεων) ως κατασκευαστές τύπων. Επιπλέον, όπως το έθεσε ο Τζόντστον η ST είναι «χωρίς λογική» με την έννοια ότι δεν περιέχει λογικές συνδέσεις ή ποσοδείκετες στον ορισμό της.

Επεκτάσεις

Πολυμορφισμός τύπων

Ο Πολυμορφισμός είναι ένα χαρακτηριστικό των γλωσσών προγραμματισμού που μας επιτρέπει να χειριστούμε τιμές διαφορετικών δομών δεδομένων χρησιμοποιώντας μία ομοιόμορφη διεπαφή. Η έννοια του παραμετρικού πολυμορφισμού ισχύει τόσο για τις δομές δεδομένων όσο και για τις συναρτήσεις. Μια συνάρτηση που μπορεί να αποτιμήσει ή να εφαρμοστεί σε τιμές διαφορετικών τύπων είναι γνωστή ως πολυμορφική συνάρτηση. Ένας τύπος δεδομένων που μπορεί να φαίνεται γενικευμένου τύπου (π.χ. μία λίστα με στοιχεία αόριστου τύπου) χαρακτηρίζεται ως πολυμορφικός τύπος δεδομένων όπως ο γενικευμένος τύπος από τον οποίο γίνονται αυτές οι εξειδικεύσεις.

Εξαρτώμενοι τύποι

Ο εξαρτώμενος τύπος είναι ένας τύπος που εξαρτάται από μία τιμή. Οι εξαρτώμενοι τύποι παίζουν ένα κεντρικό ρόλο στην Ιντουισιονιστική θεωρία τύπων και στον σχεδιασμό των συναρτησιακών γλωσσών προγραμματισμού όπως η ATS, η Agda και η Epigram.

Ένα παράδειγμα είναι ο τύπος της n-πλειάδας πραγματικών αριθμών. Αυτός είναι ένας εξαρτώμενο τύπος διότι ο τύπος εξαρτάται από την τιμή n.

Πρακτικές συνέπειες

Πληροφορική

Η πιο προφανής εφαρμογή της Θεωρίας Τύπων είναι στην κατασκευή αλγορίθμων ελέγχου τύπων στην φάση της σημασιολογικής ανάλυσης των μεταγλωττιστών των γλωσσών προγραμματισμού. Οι ορισμοί του συστήματος τύπων ποικίλλουν, αλλά ο επόμενος χάρη στον Μπέντζαμιν Κρόφορντ Πιρς αντιστοιχεί χονδρικά στη σημερινή ομοφωνία της κοινότητας της θεωρίας των γλωσσών προγραμματισμού:

Ένα σύστημα τύπων είναι μία ευεπίλυτη (πολυωνυμικού χρόνου) συντακτική μέθοδος για την απόδειξη της μη ύπαρξης συγκεκριμένων συμπεριφορών του προγράμματος κατατάσσοντας τις φράσεις σύμφωνα με το είδος των τιμών που υπολογίζουν.

— Μπέντζαμιν Κρόφορντ Πιρς, Εκδόσεις του Τεχνολογικού Ινστιτούτου της Μασαχουσέτης (The MIT Press), Κέιμπριτζ Μασαχουσέτης (2002)

Με άλλα λόγια, ένα σύστημα τύπων χωρίζει τις τιμές του προγράμματος σε σύνολα που ονομάζονται τύποι - αυτό ονομάζεται ανάθεση τύπων - και καθιστά ορισμένες συμπεριφορές του προγράμματος μη έγκυρες με βάση τους τύπους που έχουν ανατεθεί. Για παράδειγμα, ένα σύστημα τύπων μπορεί να κατηγοριοποιήσει την τιμή "hello" ως συμβολοσειρά και την τιμή 5 ως αριθμό, και να απαγορεύσει στον προγραμματιστή να προσθέσει το "hello" με το 5 βάσει αυτής της ανάθεσης τύπων. Σε αυτό το σύστημα τύπων, το πρόγραμμα

"hello" + 5

θα ήταν μη έγκυρο. Ως εκ τούτου, κάθε πρόγραμμα που περνάει από το σύστημα τύπων αποδεδειγμένα δεν θα εμφανίζει την εσφαλμένη συμπεριφορά της πρόσθεσης συμβολοσειρών με αριθμούς.

Ο σχεδιασμός και η υλοποίηση των συστημάτων τύπων είναι ένα θέμα σχεδόν τόσο ευρύ όσο και το θέμα των γλωσσών προγραμματισμού καθαυτό. Στην πραγματικότητα, οι υποστηρικτές της θεωρίας τύπων διακηρύσσουν ότι ο σχεδιασμός των συστημάτων τύπων είναι η ουσία του σχεδιασμού των γλωσσών προγραμματισμού: «Σχεδίασε σωστά το σύστημα τύπων, και η γλώσσα θα σχεδιάσει τον εαυτό της.»

Γλωσσολογία

Η θεωρία τύπων χρησιμοποιείται ευρέως στις τυπικές θεωρίες της σημασιολογίας των φυσικών γλωσσών, ειδικότερα της γραμματικής Μόνταγκιου και των απογόνων της. Η πιο κοινή κατασκευή παίρνει τους βασικούς τύπους $e$ και $t$ για άτομα και αληθοτιμές, αντίστοιχα, και ορίζει το σύνολο των τύπων ως εξής:

• Εάν $a$ και $b$ είναι τύποι, τότε τύπος είναι και ο $\langle a,b\rangle$.
• Τύποι είναι μόνο οι βασικοί τύποι και ό,τι μπορεί να κατασκευαστεί από αυτούς μέσω της παραπάνω πρότασης.

Ένας σύνθετος τύπος $\langle a,b\rangle$ είναι ο τύπος των συναρτήσεων συναρτήσεων από οντότητες τύπου $a$ σε οντότητες τύπου $b$. Έτσι κάποιος έχει τύπους όπως $\langle e,t\rangle$ που ερμηνεύονται ως στοιχεία του συνόλου των συναρτήσεων από οντότητες σε αληθοτιμές, δηλ. χαρακτηριστικές συναρτήσεις του συνόλου των οντοτήτων. Μια συνάρτηση τύπου $\langle \langle e,t\rangle ,t\rangle$ είναι μια συνάρτηση από οντότητες σε αληθοτιμές, δηλ. μια χαρακτηριστική συνάρτηση ενός συνόλου από σύνολα. Αυτός ο τελευταίος τύπος συχνά θεωρείται ο τύπος των ποσοδεικτών των φυσικών γλωσσών, όπως οι όλοι ή κανένας (Μόνταγκιου 1973, Μπάρουαϊς και Κούπερ 1981).

Κοινωνικές επιστήμες

Ο Gregory Bateson εισήγαγε μια θεωρία λογικών τύπων στις κοινωνικές επιστήμες; οι ιδέες του της διπλής δέσμευσης και των λογικών επιπέδων βασίζονται στη θεωρία τύπων του Ράσελ.

Δείτε επίσης

• Θεωρία κατηγοριών
• Θεωρία μοντέλων
• Θεωρία πεδίων
• Σύστημα Τύπων για μια πιο πρακτική συζήτηση των συστημάτων τύπων για γλώσσες προγραμματισμού
• Τύπος (θεωρία μοντέλων)
• Τύπος δεδομένων για συμπαγείς τύπους δεδομένων στον προγραμματισμό

Αναφορές

• Mendelson, Elliot, 1997. Εισαγωγή στην Μαθηματική Λογική, 4η έκδοση. Chapman & Hall.
• W. Farmer, Οι 7 αρετές της απλή θεωρίας τύπων, Περιοδικό της Εφαρμοσμένης Λογικής, Vol. 6, No. 3. (Σεπτέμβριος 2008), σελ. 267–286.

Επιπλέον διάβασμα

• Constable, Robert L., 2002, "Απλοϊκή θεωρία τύπων υπολογισμού," στο Απόδειξη και Αξιοπιστία του συστήματος: των H. Schwichtenberg και R. Steinbruggen (eds.), 213–259. Προορισμένο ως ομόλογο του Naive Set Theory του Πολ Χάλμος (1960) σχετικά με τη θεωρία τύπων
• Andrews B., Peter (2002). Μια Εισαγωγή στη Μαθηματική Λογική και τη Θεωρία Τύπων: Στην Αλήθεια μέσω της Απόδειξης, 2η έκδοση. Kluwer Academic Publishers. ISBN 978-1-4020-0763-7. 
• Jacobs, Bart (1999). Κατηγορηματική Λογική και Θεωρία Τύπων. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3.  Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
• Collins, Jordan E. (2012). Μια Ιστορία της Θεωρίας Τύπων: Εξελίξεις μετά την δεύτερη έκδοση της 'Principia Mathematica'. LAP Lambert Academic Publishing. ISBN 978-3-8473-2963-3.  Παρέχει μια ιστορική έρευνα των εξελίξεων της θεωρίας των τύπων με εστίαση στην άρνηση της θεωρίας ως ένα θεμέλιο των μαθηματικών διαμέσου των τεσσάρων δεκαετιών που ακολούθησαν την δημοσιοποίηση της 2ης έκδοσης της 'Principia Mathematica'.
• Cardelli, Luca, 1997, "Συστήματα Τύπων, Αρχειοθετήθηκε 2008-04-10 στο Wayback Machine." in Allen B. Tucker, ed., Η Πληροφορική και το Εγχειρίδιο του Μηχανικού. CRC Press: 2208–2236.
• Thompson, Simon, 1991. Θεωρία Τύπων και Συναρτησιακός Προγραμματισμός. Addison-Wesley. ISBN 0-201-41667-0.
• J. Roger Hindley, Βασική Απλή Θεωρια Τύπων, Cambridge University Press, 2008, ISBN 0521054222 (also 1995, 1997). Μια καλή εισαγωγή στη θεωρία τύπων για επιστήμονες της Πληροφορικής. Το σύστημα που περιγράφεται δεν είναι ακριβώς το STT του Church όμως. Book review
• Stanford Encyclopedia of Philosophy: Θεωρία Τύπων" – από τον Τιερί Κοκάντ.
• Fairouz D. Kamareddine, Twan Laan, Rob P. Nederpelt, Μια σύγχρονη προοπτική στη θεωρία τύπων: από τις καταβολές της ως σήμερα, Springer, 2004, ISBN 1402023340
• Jose Ferreiros, Jose Ferreiros Dominguez, Λαβύρινθος σκέψεων: μια ιστορία της θεωρίας συνόλων και τον ρόλο της στα σύγχρονα μαθηματικά, 2η Έκδοση, Springer, 2007, ISBN 3764383496, Κεφάλαιο X "Λογική και Θεωρία Τύπων κατά τη διάρκεια του Μεσοπολέμου"

Πηγές για το τμήμα της Ιστορίας

• Μπέρτραντ Ράσελ (1903) Οι αρχές των Μαθηματικών: Τόμος 1, Cambridge at the University Press, Cambridge, UK, επανεκτυπωμένο ως googlebook.
• Μπέρτραντ Ράσελ (1920) Εισαγωγή στην Μαθηματική Φιλοσοφία (2η έκδοση), Dover Publishing Inc., New York NY, ISBN 0-486-27724-0 (pbk).
• Άλφρεντ Τάρσκι (1946) Εισαγωγή στη Λογική και στις Επιστήμες Εξαγωγής Συμπερασμάτων, επανεκτυπωμένο το 1995 από την Dover Publications, Inc., New York, NY ISBN 0-486-28462-x
• Jean van Heijenoort (1967, 3η εκτύπωση 1976), Από τον Frege στον Godel: Ένα βασικό βιβλίο στη Μαθηματική Λογική, 1879-1931, Harvard University Press, Cambridge, MA, ISBN 0-674-32449-8 (pbk)
  • Μπέρτραντ Ράσελ (1902) Γράμμα στον Frege με σχολιασμό από τον van Heijenoort, σελίδες 124-125. Όπου ο Ράσελ ανακοινώνει την ανακάλυψή του ενός "παραδόξου" στην εργασία του Frege.
  • Gottlob Frege (1902) Γράμμα στον Ράσελ με σχολιασμό από τον van Heijenoort, σελίδες 126-128.
  • Μπέρτραντ Ράσελ (1908a) Η μαθηματική λογική βασιμένη στη θεωρία των τύπων, με σχολιασμό από τον Γουίλαρντ Κιν, σελίδες 150-182.
  • Emil Post (1921) Εισαγωγή σε μια γενική θεωρία βασικών προτάσεων, με σχολιασμό από τον van Heijenoort, σελίδες 264-283.
• Alfred North Whitehead και Μπέρτραντ Ράσελ (1910–1913, 1927 2η έκδοση επανεκτυπωμένη το 1962), Principia Mathematica to *56, Cambridge at the University Press, London UK, χωρίς ISBN ή US card αριθμό καταλόγου.
• Λούντβιχ Βιτγκενστάιν (επανεκτυπωμένο 2009) Μεγάλα έργα: Επιλεγμένα φιλοσοφικά έργα", HarperCollins, New York. ISBN 978-0-06-155024-9. Το Tractatus Logico-Philosophicus του Βιτγκενστάιν (1921 στα Αγγλικά) σελίδες 1–82.

Εξωτερικοί Σύνδεσμοι

• Types Project lecture notes των θερινών μαθημάτων 2005-2008
  • The 2005 summer school έχει εισαγωγικές διαλέξεις
• The Nuprl Book: "Εισαγωγή στη Θεωρία Τύπων."