A logic for intersection and union types
Authors: Βενέτη Αναστασία 
Published: August 2021

Eρευνούμε τη λογική θεμελίωση του συστήματος τύπων τομής και ένωσης IUT υπό το πρίσμα του ισομορφισμού Curry-Howard. Πιο συγκεκριμένα, αναζητούμε ένα λογικό σύστημα που να αντιστοιχεί στο IUT μέσω ''διακόσμησης'' των αποδείξεών του με όρους του καθαρού λ-λογισμού που προσομοιώνουν τους όρους στο IUT. Η διατριβή απαρτίζεται από τα ακόλουθα κεφάλαια. Κεφάλαιο 1: Ένα κεφάλαιο που αναφέρεται στο διαμορφωμένο πεδίο έρευνας πριν την έναρξη της διατριβής. Παρουσιάζεται ιστορικά το θέμα του ορισμού μιας λογικής που να αντιστοιχεί στο σύστημα τύπων τομής IT και παρατίθενται τα βασικότερα σημεία των θεμελιωδών άρθρων “Intersection Logic” (των S. Ronchi Della Rocca και L. Roversi) και “Intersection Types from a Proof-theoretic Perspective” (των E. Pimentel, S. Ronchi Della Rocca και L. Roversi). Κεφάλαιο 2: 'Ενα κεφάλαιο που παρουσιαζει το σύστημα τύπων τομής και ένωσης IUT σε φορμαλισμό φυσικής απαγωγής, αλλά και σε φορμαλισμό ακολουθητών. Περιγράφονται και αποδεικνύονται ιδιότητες του συτήματος, όπως η αναγωγή υποκειμένου (υπό μία έννοια ''παράλληλης'' αναγωγής) και η απαλοιφή της τομής. Επίσης, αποδεικνύονται τέσσερα θεωρήματα που αποδίδουν ιδιότητες σε λ-όρους ανάλογα με τις τυποποιησεις που αυτοί έχουν στο σύστημα τύπων. Κεφάλαιο 3: Ένα κεφάλαιο που καταγράφει τα πρώιμα αποτελέσματα της έρευνας ως προς τη λογική θεμελίωση του συστήματος τύπων IUT σε φορμαλισμό φυσικής απαγωγής. Παρουσιάζονται τα λογικά συστήματα IULk και IULm (με συνδέσμους συνεπαγωγής, τομής και ένωσης) και αποδεικνύονται θεωρήματα που αντιστοιχιζουν το καθένα από αυτά με το IUT μέσω διακόσμησης με λ-όρους που προσομοιώνουν τους όρους στο IUT. Εξηγείται με ποιό τρόπο ο όρος αντικατάστασης, ο οποίος εμφανίζεται στον κανόνα απαλοιφής της ένωσης, εμποδίζει την απόδειξη αντίστροφων θεωρημάτων από το IUT στα λογικά συστήματα. Αποδεικνύεται η ισοδυναμία των δύο λογικών συστημάτων και επισημαίνονται τα συγκριτικά πλεονεκτήματα του φορμαλισμού του IULm σε σχέση με αυτόν του IULk. Κεφάλαιο 4: Ένα κεφάλαιο που παρουσιάζει μια τροποιημένη εκδοχή του λογικού συστήματος IULm (ως προς τα δομικα χαρακτηριστικά του και τους κανόνες του) σε φορμαλισμό φυσικής απαγωγής, αλλά και εκ νέου το σύστημα τύπων IUT σε φορμαλισμό φυσικής απαγωγής. Διατυπώνονται και αποδεικνύονται βασικές ιδιότητες των δύο συστημάτων και εξετάζεται η μεταξύ τους σχέση μέσω διακόσμησης. Κεφάλαιο 5: Ένα κεφάλαιο που μελετά την αντιστοιχία μεταξύ IULm και IUT σε φορμαλισμό φυσικής απαγωγής. Εισάγεται η έννοια ''δέντρο συνεπαγωγών και απαλοιφών της ένωσης με όρους'' για τη διακοσμημένη λογική και για το σύστημα τύπων, και αποδεικνύονται θεωρήματα αντιστοιχίας με χρήση της έννοιας αυτής. Δίνεται αντιπαράδειγμα μετασχηματισμού μη συμβατών αποδείξεων του IUT (δλδ. αποδείξεων που δεν έχουν ταυτόσημα δεντρα συνεπαγωγών και απαλοιφών της ένωσης με όρους) σε συμβατές και με αμετάβλητες ρίζες αποδείξεις του IUT, μέσω του οποίου δικαιολογείται η μη ευστάθεια θεωρημάτων αντιστοιχίας χωρίς τη χρήση της εν λόγω έννοιας και μόνο στη βάση μετασχηματισμού. Κεφάλαιο 6: Ένα κεφάλαιο που μελετά την αντιστοιχία μεταξύ των περιορισμένων-στην-τομή συστημάτων ILm και IT σε φορμαλισμό φυσικής απαγωγής. Προσαρμόζεται η έννοια του δέντρου, που εισήχθη στο προηγούμενο κεφάλαιο, στα περιορισμένα συστήματα και αποδεικνύονται θεωρήματα αντιστοιχίας με χρήση της προσαρμοσμένης πλέον έννοιας. Επίσης, συζητώνται συγκριτικά οι αντιστοιχίες IULm-IUT και ILm-IT. Κεφάλαιο 7: Ένα κεφάλαιο που παρουσιάζει το (τροποποιημένο) λογικό σύστημα IULm και το σύστημα τύπων IUT σε φορμαλισμό ακολουθητών. Οι βασικές ιδιότητες των δύο συστημάτων μεταφέρονται και αποδεικνύονται στο πλαίσιο του φορμαλισμού των ακολουθητών. Αποδεικνύεται επίσης η ισοδυναμία των δύο διαφορετικών παρουσιάσεων (σε φορμαλισμό φυσικής απαγωγής και σε φορμαλισμό ακολουθητών) και για τα δύο συστήματα. Τέλος, εξετάζεται η σχέση λογικής και συστήματος τύπων (μέσω διακόσμησης) στο νέο πλαίσιο και παρουσιάζονται τα θεωρήματα αντιστοιχίας τους με προσαρμογή της μεθόδου των δέντρων στο πλαίσιο αυτό.