Σύστημα F

Πρότυπο:Χωρίς παραπομπές To Σύστημα F, επίσης γνωστό ως πολυμορφικός λ-λογισμός των Ζιράρ-Ρέινολντς και λ-λογισμός δευτέρας τάξης, είναι ένας λ-λογισμός με τύπους που επεκτείνει τον λ-λογισμό με απλούς τύπους εισάγοντας ένα μηχανισμό καθολικής ποσόδειξης επί των τύπων. Ως εκ τούτου, το Σύστημα F αποτελεί φορμαλισμό της έννοιας του παραμετρικού πολυμορφισμού στις γλώσσες προγραμματισμού, και μια θεωρητική βάση γλωσσών όπως η Haskell και η ML. Το Σύστημα F επινοήθηκε ανεξάρτητα από τον λογικολόγο Ζαν-Υβ Ζιράρ και τον επιστήμονα υπολογιστών Τζον Σ. Ρέινολντς.

Επεκτείνοντας το λ-λογισμό με απλούς τύπους που έχει μεταβλητές επί των όρων, το Σύστημα F έχει επιπρόσθετα μεταβλητές επί των τύπων. Για παράδειγμα, το γεγονός ότι η ταυτοτική συνάρτηση μπορεί να έχει οιονδήποτε τύπο της μορφής A→ A γράφεται στο Σύστημα F ως

$⊢\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x:\mathrm{\forall }\alpha .\alpha \to \alpha$

όπου α είναι μεταβλητή τύπου. Το κεφαλαίο $\mathrm{\Lambda }$ χρησιμοποιείται συνήθως για να εκφράσει συναρτήσεις στο επίπεδο των τύπων, σε αντιπαραβολή με το πεζό $\lambda$ που χρησιμοποιείται για συναρτήσεις στο επίπεδο των όρων.

Ως ένα σύστημα αναγωγής όρων, το Σύστημα F είναι ισχυρά κανονικοποιήσιμο. Η εξαγωγή τύπων στο Σύστημα F χωρίς ρητές επισημειώσεις τύπων είναι ωστόσο μη αποφάνσιμη. Με τον ισομορφισμό Κάρι-Χάουαρντ το Σύστημα F αντιστοιχίζεται στην διαισθητική λογική δευτέρας τάξης με μόνη την καθολική ποσόδειξη. Το Σύστημα F μπορεί να θεωρηθεί τμήμα του λ-κύβου, μαζί με εκφραστικότερους λ-λογισμούς με τύπους, συμπεριλαμβανομένων αυτών με εξαρτώμενους τύπους.

Λογική και Κατηγορήματα

Ο τύπος του Μπουλ ορίζεται ως: $\mathrm{\forall }\alpha .\alpha \to \alpha \to \alpha$, όπου $\alpha$ είναι μεταβλητή τύπου. Αυτός συνεπάγεται τους ακόλουθους ορισμούς για τις αληθοτιμές $𝐓$ και $𝐅$:

$𝐓=\mathrm{\Lambda }\alpha .\lambda x^{\alpha }\lambda y^{\alpha }.x$

$𝐅=\mathrm{\Lambda }\alpha .\lambda x^{\alpha }\lambda y^{\alpha }.y$

Εν συνεχεία, με αυτούς τους δύο $\lambda$-όρους, μπορούμε να ορίσουμε μερικούς λογικούς τελεστές:

$\mathrm{A}\mathrm{N}\mathrm{D}=\lambda x^{𝖡𝗈𝗈𝗅𝖾𝖺𝗇}\lambda y^{𝖡𝗈𝗈𝗅𝖾𝖺𝗇}.x𝖡𝗈𝗈𝗅𝖾𝖺𝗇y𝐅$

$\mathrm{O}\mathrm{R}=\lambda x^{𝖡𝗈𝗈𝗅𝖾𝖺𝗇}\lambda y^{𝖡𝗈𝗈𝗅𝖾𝖺𝗇}.x𝖡𝗈𝗈𝗅𝖾𝖺𝗇𝐓y$

$\mathrm{N}\mathrm{O}\mathrm{T}=\lambda x^{𝖡𝗈𝗈𝗅𝖾𝖺𝗇}.x𝖡𝗈𝗈𝗅𝖾𝖺𝗇𝐅𝐓$

Απουσιάζει η ανάγκη για μια IFTHENELSE συνάρτηση καθώς οι ίδιοι οι όροι τύπου $𝖡𝗈𝗈𝗅𝖾𝖺𝗇$ μπορούν να χρησιμοποιηθούν ως συναρτήσεις απόφασης. Μολοταύτα, αν ζητηθεί γράφεται ως:

$\mathrm{I}\mathrm{F}\mathrm{T}\mathrm{H}\mathrm{E}\mathrm{N}\mathrm{E}\mathrm{L}\mathrm{S}\mathrm{E}=\mathrm{\Lambda }\alpha .\lambda x^{𝖡𝗈𝗈𝗅𝖾𝖺𝗇}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz$

Ένα κατηγόρημα είναι συνάρτηση που επιστρέφει μια τιμή τύπου $𝖡𝗈𝗈𝗅𝖾𝖺𝗇$. Το θεμελιωδέστερο κατηγόρημα είναι το ISZERO που επιστρέφει $𝐓$ αν και μόνο αν το όρισμά του είναι ο αριθμός Τσερτς 0:

$\mathrm{I}\mathrm{S}\mathrm{Z}\mathrm{E}\mathrm{R}\mathrm{O}=\lambda n^{\mathrm{\forall }\alpha .(\alpha \to \alpha )\to \alpha \to \alpha }.n𝖡𝗈𝗈𝗅𝖾𝖺𝗇(\lambda x^{𝖡𝗈𝗈𝗅𝖾𝖺𝗇}.𝐅)𝐓$

Δομές του Συστήματος F

Το Σύστημα F επιτρέπει την φυσική ενσωμάτωση αναδρομικών κατασκευών, σε σχέση με τη θεωρία τύπων του Μάρτιν-Λεφ. Οι αφηρημένες δομές (S) δημιουργούνται με τη χρήση κατασκευαστών, δηλαδή συναρτήσεων με τύπο:

$K_1\to K_2\to \dots \to S$.

Η αναδρομικότητα εμφανίζεται όταν το ίδιο το $S$ παρουσιάζεται μεταξύ κάποιου εκ των τύπων $K_i$. Δοθέντων $m$ τέτοιων κατασκευαστών, ο τύπος του $S$ ορίζεται ως:

$\mathrm{\forall }\alpha .(K_1^1[\alpha /S]\to \dots \to \alpha )\dots \to (K_1^m[\alpha /S]\to \dots \to \alpha )\to \alpha$

Για παράδειγμα, οι φυσικοί αριθμοί μπορούν να ορισθούν ως ο επαγωγικός τύπων δεδομένων $N$ με κατασκευαστές

$𝑧𝑒𝑟𝑜:\mathrm{N}$

$𝑠𝑢𝑐𝑐:\mathrm{N}\to \mathrm{N}$

Ο αντίστοιχος τύπος στο Σύστημα F είναι $\mathrm{\forall }\alpha .\alpha \to (\alpha \to \alpha )\to \alpha$. Οι όροι αυτού του τύπου συνιστούν μια τυποποιημένη εκδοχή των αριθμών Τσερτς, μερικοί εκ των οποίων είναι:

0 := $\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x$

1 := $\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx$

2 := $\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)$

3 := $\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))$

Αντιστρέφοντας τη σειρά των ορισμάτων (i.e., $\mathrm{\forall }\alpha .(\alpha \to \alpha )\to \alpha \to \alpha$) ο αριθμός Τσερτς για το $n$ είναι μια συνάρτηση που δέχεται μια συνάρτηση f ως όρισμα και επιστρέφει την $n$-ιοστή δύναμη του f. Με άλλα λόγια, ένας αριθμός Τσερτς είναι μια συνάρτηση υψηλής τάξης – δέχεται μια συνάρτηση f ενός ορίσματος και επιστρέφει μια άλλη συνάρτηση ενός ορίσματος.

Χρήση στις γλώσσες προγραμματισμού

Η εκδοχή του Συστήματος F που χρησιμοποιήθηκε στο παρόν άρθρο είναι τύπου Τσερτς (οι τύποι επισημειώνονται ρητώς). Η πληροφορία τυποποίησης που εμπεριέχεται στους λ-όρους κάνει τον έλεγχο τύπων ευθύ. Για μια παραλλαγή τύπου Κάρι (χωρίς ρητή επισημείωση τύπων) του Συστήματος F ο Τζο Ουέλς (1994) περιέγραψε ένα "ντροπιαστικό ανοιχτό πρόβλημα" αποδεικνύοντας ότι ο έλεγχος τύπων είναι μη αποφάνσιμος.

Το αποτέλεσμα του Ουέλς υπονοεί ότι η εξαγωγή τύπων για το Σύστημα F είναι αδύνατη. Ένας περιορισμός του Συστήματος F, γνωστός ως "Χίντλεϊ-Μίλνερ", ή απλά "HM", έχει ένα εύκολο αλγόριθμο εξαγωγής τύπων και χρησιμοποιείται για πολλές συναρτησιακές γλώσσες προγραμματισμού όπως η Haskell 98 και η ML. Προϊόντος του χρόνου, καθώς οι περιορισμοί των συστημάτων τύπου Χίντλεϊ-Μίλνερ έγιναν εμφανείς, οι γλώσσες σταθερά κινούνταν προς εκφραστικότερες λογικές για τα συστήματα τύπων τους. Για παράδειγμα, από το 2008 ο GHC, ένας μεταγλωττιστής της Haskell, υπερέβη το HM, και τώρα χρησιμοποιεί το Σύστημα F επεκτεταμένο με μη συντακτική ισότητα τύπων.

Σύστημα F_ω

Ενώ το Σύστημα F αντιστοιχίζεται με τον πρώτο άξονα του λ-κύβου του Μπάρεντρεγκτ, το Σύστημα F_ω συνδυάζει τον πρώτο άξονα (πολυμορφισμό) με το δεύτερο άξονα (τελεστές τύπων) αποτελώντας ένα διαφορετικό, πολυπλοκότερο σύστημα.

Το Σύστημα F_ω μπορεί να οριστεί επαγωγικά σε μια οικογένεια συστημάτων, όπου η επαγωγή βασίζεται στα είδη που επιτρέπονται σε κάθε σύστημα:

• Το $F_n$ επιτρέπει τα είδη:
  • $\star$ (είδος των τύπων) και
  • $J\Rightarrow K$ όπου $J\in F_{n-1}$ και $K\in F_n$ (είδος των συναρτήσεων από τύπους σε τύπους, όπου ο τύπος όρισμα είναι κατώτερης τάξης)

Στο όριο μπορεί να ορισθεί το $F_{\omega }$ ως

• $F_{\omega }=\bigcup _{1\le i}{F}_i$

Δηλαδή το F_ω είναι το σύστημα που επιτρέπει συναρτήσεις από τύπους σε τύπους όπου το όρισμα και το αποτέλεσμα μπορούν να είναι οιασδήποτε τάξης.

Σημειώνεται ότι τα ορίσματα αυτών των απεικονίσεων στο F_ω παρά την απουσία περιορισμών στην τάξη τους, προέρχονται από ένα περιορισμένο σύμπαν: πρέπει να είναι τύποι και όχι τιμές. Το Σύστημα F_ω δεν επιτρέπει απεικονίσεις από τιμές σε τύπους (εξαρτώμενοι τύποι), αλλά επιτρέπει απεικονίσεις από τιμές σε τιμές ($\lambda$ αφαίρεση), από τύπους σε τιμές ($\mathrm{\Lambda }$ αφαίρεση, εμφανίζεται και ως $\mathrm{\forall }$) και από τύπους σε τύπους ($\lambda$ αφαίρεση στο επίπεδο των τύπων).

Δείτε επίσης

• Οι υπαρξιακοί τύποι είναι το υπαρξιακώς ποσοδειγμένο αντίστοιχο των καθολικών τύπων.
• Το System F_<: επεκτείνει το Σύστημα F με υποτύπους, προσεγγίζοντας πολύ περισσότερο πραγματικές γλώσσες προγραμματισμού της οικογένειας ML.

Αναφορές

• Πρότυπο:Cite conference
• Πρότυπο:Cite conferenceΠρότυπο:Dead link
• Girard, Lafont and Taylor, Proofs and Types. Cambridge University Press, 1989, ISBN 0 521 37181 3.
• J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994. [1]

Πρόσθετες Πηγές

• Πρότυπο:Cite book Chapter 23: Universal Types, and Chapter 25: An ML Implementation of System F.

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

• Summary of System F by Franck Binard.