Σύστημα F

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

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

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

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

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

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

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

$\mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x$

$\mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y$

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

$\mathrm {AND} =\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,y\,\mathbf {F}$

$\mathrm {OR} =\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {T} \,y$

$\mathrm {NOT} =\lambda x^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {F} \,\mathbf {T}$

Απουσιάζει η ανάγκη για μια IFTHENELSE συνάρτηση καθώς οι ίδιοι οι όροι τύπου $\scriptstyle {\mathsf {Boolean}}$ μπορούν να χρησιμοποιηθούν ως συναρτήσεις απόφασης. Μολοταύτα, αν ζητηθεί γράφεται ως:

$\mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz$

Ένα κατηγόρημα είναι συνάρτηση που επιστρέφει μια τιμή τύπου $\scriptstyle {\mathsf {Boolean}}$. Το θεμελιωδέστερο κατηγόρημα είναι το ISZERO που επιστρέφει $\scriptstyle \mathbf {T}$ αν και μόνο αν το όρισμά του είναι ο αριθμός Τσερτς 0:

$\mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T}$

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

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

$K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S$.

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

$\forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha$

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

${\mathit {zero}}:\mathrm {N}$

${\mathit {succ}}:\mathrm {N} \rightarrow \mathrm {N}$

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

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

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

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

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

Αντιστρέφοντας τη σειρά των ορισμάτων (i.e., $\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \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 }={\underset {1\leq i}{\bigcup }}F_{i}$

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

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

Δείτε επίσης

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

Αναφορές

• Girard, Jean-Yves (1971). «Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types». Proceedings of the Second Scandinavian Logic Symposium. Amsterdam, pp. 63–92. 
• Reynolds, John (1974). «Towards a Theory of Type Structure». Colloque sur la Programmation. Paris, France, pp. 408–425. ftp://ftp.cs.cmu.edu/user/jcr/theotypestr.pdf. Ανακτήθηκε στις 6 Apr 2010. 
• 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]

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

• Pierce, Benjamin (2002). Types and Programming Languages. MIT Press. ISBN 0-262-16209-1.  Chapter 23: Universal Types, and Chapter 25: An ML Implementation of System F.

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

• Summary of System F by Franck Binard.