A logic for intersection and union types

Abstract

We investigate the logical foundation of the type system with intersection and union types IUT in the perspective of the Curry-Howard isomorphism. In particular, we seek a logical system corresponding to IUT through a ''decoration'' with untyped terms that simulate the terms in IUT. The thesis consists of the following chapters. Chapter 1: A chapter that refers to the already established results in the field in question up until the strart of the thesis. We historically present the issue of defining a logic corresponding to the type system with intersection types IT by citing the basic points of the articles "Intersection Logic'' (by S. Ronchi Della Rocca and L. Roversi) and “Intersection Types from a Proof-theoretic Perspective” (by E. Pimentel, S. Ronchi Della Rocca and L. Roversi). Chapter 2: A chapter that presents the type system with intersection and union types IUT in natural deduction style and also in sequent calculus style. We describe and prove properties of the system, like subject reduction (under a notion of ''parallel'' reduction) and cut elimination. Furthermore, we prove four theorems that characterize λ-terms according to their typings in the type system. Chapter 3: A chapter that records the early research results on the logical foundation of the type system IUT in natural deduction style. We present the logical systems IULk and IULm (with implication, intersection, and union connectives) and prove theorems corresponding each of them to IUT through a decoration with λ-terms that simulate the terms in IUT. We explain how the substitution term in the union elimination rule hinders the proof of inverse theorems from IUT to the logical systems. We prove the equivalence of the two logical systems and discuss the advantages of the fornalism of IULm over the formalism of IULk. Chapter 4: A chapter that introduces a modified version of the logical system IULm (with respect to its structural chatacteristics and its rules) in natural deduction style and also presents anew the type system IUT in natural deduction style. We state and prove basic properties of the two systems and examine their relation through decoration. Chapter 5: A chapter that investigates the correspondence between IULm and IUT in natural deduction style. We define the notion ''tree of implications and union eliminations with terms'' for both the decorated logic and the type system, and prove theorems of correspondence through this notion. We show that non-compatible derivations in IUT (ie. derivations that do not share the same tree of implications and union eliminations with terms) cannot always be transformed, leaving the roots unaltered, to compatible derivations in IUT, which accounts for the fact that we cannot have theorems of correspondence without the notion of trees, solely on transformation grounds. Chapter 6: A chapter that examines the correspondence between the restricted-to-intersection systems ILm and IT in natural deduction style. We adjust the notion of tree, introduced in the previous chapter, to the restricted systems and prove theorems of correspondence through the adjusted notion. We also compare and contrast the correspondences IULm-IUT and ILm-IT. Chapter 7: A chapter that presents the (modified) logical system IULm and the type system IUT in sequent calculus style. The basic properties of the two systems are transferred and proved in the sequent calculus context. We also prove the equivalence of the two presentations (ie. in natural deduction and sequent calculus styles) for both systems. Finally, we relate the logic to the type system (through decoration) in the new context and state the correspondence between the two systems by adjusting the method of trees to the new context.

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 σε φορμαλισμό ακολουθητών. Οι βασικές ιδιότητες των δύο συστημάτων μεταφέρονται και αποδεικνύονται στο πλαίσιο του φορμαλισμού των ακολουθητών. Αποδεικνύεται επίσης η ισοδυναμία των δύο διαφορετικών παρουσιάσεων (σε φορμαλισμό φυσικής απαγωγής και σε φορμαλισμό ακολουθητών) και για τα δύο συστήματα. Τέλος, εξετάζεται η σχέση λογικής και συστήματος τύπων (μέσω διακόσμησης) στο νέο πλαίσιο και παρουσιάζονται τα θεωρήματα αντιστοιχίας τους με προσαρμογή της μεθόδου των δέντρων στο πλαίσιο αυτό.