Ειδικά Θέματα Λογικής: Θεωρία Τύπων τού Martin-Löf
Νικόλαος Ρήγας
Από τη δεκαετία τού '70 ο Per Martin-Löf έχει αναπτύξει, σε μία σειρά διαδοχικών παραλλαγών, μία κατασκευαστική θεωρία τύπων. Η θεωρία αυτή προέκυψε αρχικά ως προϊόν τής αναζήτησης του κατάλληλου πλαισίου για κατασκευαστικά μαθηματικά. Σε αντίθεση με τις περισσότερες άλλες τυποποιήσεις των μαθηματικών, η θεωρία τύπων τού Martin-Löf δεν βασίζεται στην κατηγορηματική λογική. Αντίθετα, οι λογικές σταθερές ερμηνεύονται μέσα στη θεωρία τύπων μέσω τής αντιστοιχίας Curry-Howard μεταξύ προτάσεων και τύπων: μία πρόταση ερμηνεύεται ως ένας τύπος, τα στοιχεία τού οποίου αντιπροσωπεύουν τις αποδείξεις τής πρότασης.
Ένας τύπος είναι επίσης δυνατό να θεωρηθεί περιγραφή κάποιου προβλήματος με τρόπο παρόμοιο με την εξήγηση του Kolmogorov για τον ιντουισιονιστικό προτασιακό λογισμό. Συγκεκριμένα, ένας τύπος μπορεί να θεωρηθεί προδιαγραφή ενός προβλήματος προγραμματισμού· τα στοιχεία του τύπου είναι τότε τα προγράμματα που ικανοποιούν την προδιαγραφή.
Ένα πλεονέκτημα της χρήσης τής θεωρίας τύπων για την κατασκευή προγραμμάτων είναι ότι είναι δυνατόν να εκφράσουμε τόσο τις προδιαγραφές όσο και τα προγράμματα μέσα στον ίδιο φορμαλισμό. Επιπλέον, οι απoδεικτικοί κανόνες μπορούν να χρησιμοποιηθούν για την εξαγωγή ενός ορθού προγράμματος από μια προδιαγραφή καθώς και για την επαλήθευση ότι ένα συγκεκριμένο πρόγραμμα έχει μια συγκεκριμένη ιδιότητα. Ως γλώσσα προγραμματισμού, η θεωρία τύπων είναι παρόμοια με συναρτησιακές γλώσσες όπως η ML και η Haskell, με τη σημαντική διαφορά ότι η εκτέλεση ενός καλά συντεταγμένου προγράμματος τερματίζει πάντα.
Πιο πρόσφατα, μέσα από τη δουλειά των Martin Hofmann και Thomas Streicher, αλλά κυρίως του Vladimir Voevodsky, προέκυψε ότι οι τύποι μπορούν επίσης να θεωρηθούν αφηρημένοι τοπολογικοί χώροι. Αυτή η θεώρηση περιλαμβάνει μία νέα ανάγνωση της ισότητας, που είναι ένα από τα πιο μυστηριώδη συστατικά τής θεωρίας τύπων τού Martin-Löf, ως του τύπου/χώρου των μονοπατιών μέσα σε έναν τοπολογικό χώρο, καθώς και μία νέα τυποθεωρητική αρχή, η οποία φέρει το όνομα univalence, και αποτελεί αντικείμενο τρέχουσας έρευνας.
ΛιγότεραΑπό τη δεκαετία τού '70 ο Per Martin-Löf έχει αναπτύξει, σε μία σειρά διαδοχικών παραλλαγών, μία κατασκευαστική θεωρία τύπων. Η θεωρία αυτή προέκυψε αρχικά ως προϊόν τής αναζήτησης του κατάλληλου πλαισίου για κατασκευαστικά μαθηματικά. Σε αντίθεση με τις περισσότερες άλλες τυποποιήσεις των μαθηματικών, η θεωρία τύπων τού Martin-Löf δεν βασίζεται στην κατηγορηματική λογική. Αντίθετα, οι λογικές σταθερές ερμηνεύονται μέσα στη θεωρία τύπων μέσω τής αντιστοιχίας Curry-Howard μεταξύ προτάσεων και τύπων: μία πρόταση ερμηνεύεται ως ένας τύπος, τα στοιχεία τού οποίου αντιπροσωπεύουν τις αποδείξεις τής πρότασης.
Ένας τύπος είναι επίσης δυνατό να θεωρηθεί περιγραφή κάποιου προβλήματος με τρόπο παρόμοιο με την εξήγηση του Kolmogorov για τον ιντουισιονιστικό προτασιακό λογισμό. Συγκεκριμένα, ένας τύπος μπορεί να θεωρηθεί προδιαγραφή ενός προβλήματος προγραμματισμού· τα στοιχεία του τύπου είναι τότε τα προγράμματα που ικανοποιούν την προδιαγραφή.
Ένα πλεονέκτημα της χρήσης τής θεωρίας τύπων για την
Από τη δεκαετία τού '70 ο Per Martin-Löf έχει αναπτύξει, σε μία σειρά διαδοχικών παραλλαγών, μία κατασκευαστική θεωρία τύπων. Η θεωρία αυτή προέκυψε αρχικά ως προϊόν τής αναζήτησης του κατάλληλου πλαισίου για κατασκευαστικά μαθηματικά. Σε αντίθεση με τις περισσότερες άλλες τυποποιήσεις των μαθηματικών, η θεωρία τύπων τού Martin-Löf δεν βασίζεται στην κατηγορηματική λογική. Αντίθετα, οι λογικές σταθερές ερμηνεύονται μέσα στη θεωρία τύπων μέσω τής αντιστοιχίας Curry-Howard μεταξύ προτάσεων και τύπων: μία πρόταση ερμηνεύεται ως ένας τύπος, τα στοιχεία τού οποίου αντιπροσωπεύουν τις αποδείξεις τής πρότασης.
Ένας τύπος είναι επίσης δυνατό να θεωρηθεί περιγραφή κάποιου προβλήματος με τρόπο παρόμοιο με την εξήγηση του Kolmogorov για τον ιντουισιονιστικό προτασιακό λογισμό. Συγκεκριμένα, ένας τύπος μπορεί να θεωρηθεί προδιαγραφή ενός προβλήματος προγραμματισμού· τα στοιχεία του τύπου είναι τότε τα προγράμματα που ικανοποιούν την προδιαγραφή.
Ένα πλεονέκτημα της χρήσης τής θεωρίας τύπων για την
Περίγραμμα
Προτάσεις για θέματα εργασιών
Γενικού ενδιαφέροντος
- HoTT 11.3 Μόνο η κατασκευή τού τύπου Rc των Cauchy reals ως του ελεύθερου πλήρους μετρικού χώρου επί τού Q, και, ενδεχομένως, η αρχή επαγωγής τού Rc. (3-4/5)
Αλγεβροτοπολογικού ενδιαφέροντος
- HoTT 8.1 Η θεμελιώδης ομάδα τού κύκλου. Απαιτητικό. (4-5/5)
Κατηγορικού ενδιαφέροντος
- M. Hofmann "Syntax and semantics of dependent types",
S. Castellan, P. Clairambault, P. Dybjer "Categories with Families: Unityped, Simply Typed, and Dependently Typed",
categorical model of dependent types in nLab,
Κατηγορική ερμηνεία τής MLTT. (4/5)
- HoTT 9.1 Θεωρία κατηγοριών εντός τής HoTT. (2/5)
- HoTT 10.1 Ιδιότητες της εσωτερικής κατηγορίας των συνόλων. (3-5/5)
Συνολοθεωρητικού ενδιαφέροντος
- P. Martin-Löf "100 years of Zermelo’s axiom of choice: What was the problem with it?" (2/5)
- HoTT Το θεώρημα του Diaconescu (θεώρημα 10.1.14). (2/5)
- HoTT 10.2: Ορισμός πληθικών αριθμών, πράξεις, διάταξη, ενδεχομένως το θεώρημα Schröder-Bernstein, θεώρημα Cantor. (2/5)
- HoTT 10.3: Accessibility, καλά θεμελιωμένες σχέσεις, διατακτικοί. Μεγάλο θέμα, για δύο ή περισσότερους. (4-5/5)
- HoTT 10.5: Η συσσωρευτική ιεραρχία. Απαιτητικό. (4-5/5)
Τυποθεωρητικού-λογικού ενδιαφέροντος
- HoTT Το θεώρημα του Hedberg (θεώρημα 7.2.5). (1-2/5)
- HoTT Τύποι W και επαγωγή. Επιλογή από το κεφάλαιο 5. (3/5)
- HoTT 4.9: "Univalence implies function extensionality". (3/5)
Μεταμαθηματικού ενδιαφέροντος
- J. Smith, "The Independence of Peano's Fourth Axiom from Martin-Löf's Type Theory Without Universes" (2/5)
- Κανονικοποίηση για την MLTT. (4/5)
Η βαθμολόγηση της δυσκολίας είναι καθαρά ενδεικτική.
Πληροφορίες σχετικά με τις εργασίες
Οι ενδιαφερόμενοι καλούνται να προετοιμάσουν και να παρουσιάσουν ένα θέμα (από τα παραπάνω ή κάποιο άλλο δικής τους επιλογής). Η προβλεπόμενη διάρκεια της παρουσίασης είναι 30-45 λεπτά. Εάν ο φοιτητής το επιθυμεί, ο χρόνος αυτός μπορεί να αυξηθεί (εφ' όσον κάτι τέτοιο δικαιολογείται και από το περιεχόμενο της παρουσίασης).
Η βαθμολογία θα βασιστεί στα ακόλουθα κριτήρια:
- Προσπάθεια που καταβλήθηκε για την διεκπεραίωση της εργασίας
- Αρτιότητα της παρουσίασης
- Γενική γνώση τού αντικειμένου τού μαθήματος
Οι ημερομηνίες των παρουσιάσεων μένει να προσδιοριστούν.
Γενικού ενδιαφέροντος
- HoTT 11.3 Μόνο η κατασκευή τού τύπου Rc των Cauchy reals ως του ελεύθερου πλήρους μετρικού χώρου επί τού Q, και, ενδεχομένως, η αρχή επαγωγής τού Rc. (3-4/5)
Αλγεβροτοπολογικού ενδιαφέροντος
- HoTT 8.1 Η θεμελιώδης ομάδα τού κύκλου. Απαιτητικό. (4-5/5)
Κατηγορικού ενδιαφέροντος
- M. Hofmann "Syntax and semantics of dependent types",
S. Castellan, P. Clairambault, P. Dybjer "Categories with Families: Unityped, Simply Typed, and Dependently Typed",
categorical model of dependent types in nLab,
Κατηγορική ερμηνεία τής MLTT. (4/5)
- HoTT 9.1 Θεωρία κατηγοριών εντός τής HoTT. (2/5)
- HoTT 10.1 Ιδιότητες της εσωτερικής κατηγορίας των συνόλων. (3-5/5)
Συνολοθεωρητικού ενδιαφέροντος
- P. Martin-Löf "100 years of Zermelo’s axiom of choice: What was the problem with it?" (2/5)
- HoTT Το θεώρημα του Diaconescu (θεώρημα 10.1.14). (2/5)
- HoTT 10.2: Ορισμός πληθικών αριθμών, πράξεις, διάταξη, ενδεχομένως το θεώρημα Schröder-Bernstein, θεώρημα Cantor. (2/5)
- HoTT 10.3: Accessibility, καλά θεμελιωμένες σχέσεις, διατακτικοί. Μεγάλο θέμα, για δύο ή περισσότερους. (4-5/5)
- HoTT 10.5: Η συσσωρευτική ιεραρχία. Απαιτητικό. (4-5/5)
Τυποθεωρητικού-λογικού ενδιαφέροντος
- HoTT Το θεώρημα του Hedberg (θεώρημα 7.2.5). (1-2/5)
- HoTT Τύποι W και επαγωγή. Επιλογή από το κεφάλαιο 5. (3/5)
- HoTT 4.9: "Univalence implies function extensionality". (3/5)
Μεταμαθηματικού ενδιαφέροντος
- J. Smith, "The Independence of Peano's Fourth Axiom from Martin-Löf's Type Theory Without Universes" (2/5)
- Κανονικοποίηση για την MLTT. (4/5)
Η βαθμολόγηση της δυσκολίας είναι καθαρά ενδεικτική.
Οι ενδιαφερόμενοι καλούνται να προετοιμάσουν και να παρουσιάσουν ένα θέμα (από τα παραπάνω ή κάποιο άλλο δικής τους επιλογής). Η προβλεπόμενη διάρκεια της παρουσίασης είναι 30-45 λεπτά. Εάν ο φοιτητής το επιθυμεί, ο χρόνος αυτός μπορεί να αυξηθεί (εφ' όσον κάτι τέτοιο δικαιολογείται και από το περιεχόμενο της παρουσίασης).
Η βαθμολογία θα βασιστεί στα ακόλουθα κριτήρια:
- Προσπάθεια που καταβλήθηκε για την διεκπεραίωση της εργασίας
- Αρτιότητα της παρουσίασης
- Γενική γνώση τού αντικειμένου τού μαθήματος
Οι ημερομηνίες των παρουσιάσεων μένει να προσδιοριστούν.
