Σύστημα 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 y z 
Ένα *κατηγόρημα* είναι συνάρτηση που επιστρέφει μια τιμή τύπου \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} . f x
: 2 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f x)
: 3 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x))

Αντιστρέφοντας τη σειρά των ορισμάτων (*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<sub>ω</sub>
Ενώ το Σύστημα 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<sub><:</sub> επεκτείνει το Σύστημα F με υποτύπους, προσεγγίζοντας πολύ περισσότερο πραγματικές γλώσσες προγραμματισμού της οικογένειας ML.

## Αναφορές


*
*
*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. http://www.macs.hw.ac.uk/~jbw/papers/Wells:Typability-and-Type-Checking-in-the-Second-Order-Lambda-Calculus-Are-Equivalent-and-Undecidable:LICS-1994.ps.gz

## Πρόσθετες Πηγές
*  Chapter 23: Universal Types, and Chapter 25: An ML Implementation of System F.

## Εξωτερικοί σύνδεσμοι
*Summary of System F by Franck Binard.

Κατηγορία:Λ-λογισμός
Κατηγορία:Θεωρία τύπων
Κατηγορία:Πολυμορφισμός (υπολογιστές)