Σύστημα F

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

To Σύστημα F, επίσης γνωστό ως πολυμορφικός λ-λογισμός των (Girard–Reynolds) και λ-λογισμός δευτέρας τάξης, είναι ένας λ-λογισμός με τύπους που επεκτείνει τον λ-λογισμό με απλούς τύπους εισάγοντας ένα μηχανισμό καθολικής ποσοδεικτοδότησης επί των τύπων. Ως εκ τούτου, το Σύστημα F αποτελεί φορμαλισμό της έννοιας του παραμετρικού πολυμορφισμού στις γλώσσες προγραμματισμού, και μια θεωρητική βάση γλωσσών όπως η Haskell και η ML. Το Σύστημα F επινοήθηκε ανεξάρτητα από τον λογικολόγο Jean-Yves Girard και τον επιστήμονα υπολογιστών John C. Reynolds.

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

\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha

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

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

Λογική και Κατηγορήματα[Επεξεργασία | επεξεργασία κώδικα]

Ο τύπος Boolean ορίζεται ως: \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} αν και μόνο αν το όρισμά του είναι ο Church αριθμός 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 επιτρέπει την φυσική ενσωμάτωση αναδρομικών κατασκευών, σε σχέση με τη θεωρία τύπων του Martin-Lö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. Οι όροι αυτού του τύπου συνιστούν μια τυποποιημένη εκδοχή των αριθμών Church, μερικοί εκ των οποίων είναι:

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))

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

Χρήση στις γλώσσες προγραμματισμού[Επεξεργασία | επεξεργασία κώδικα]

Η εκδοχή του Συστήματος F που χρησιμοποιήθηκε στο παρόν άρθρο είναι Church-style (οι τύποι επισημειώνονται ρητώς). Η πληροφορία τυποποίησης που εμπεριέχεται στους λ-όρους κάνει τον έλεγχο τύπων ευθύ. Για μια Curry-style (χωρίς ρητή επισημείωση τύπων) παραλλαγή του Συστήματος F ο Joe Wells (1994) περιέγραψε ένα "ντροπιαστικό ανοιχτό πρόβλημα" αποδεικνύοντας ότι ο έλεγχος τύπων είναι ένα μη αποφάνσιμος.[1][2]

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

Σύστημα Fω[Επεξεργασία | επεξεργασία κώδικα]

Ενώ το Σύστημα F αντιστοιχίζεται με τον πρώτο άξονα του λ-κύβου του Barendregt, το Σύστημα 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.

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

Πρόσθετες Πηγές[Επεξεργασία | επεξεργασία κώδικα]

  • 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.

Εξωτερικοί Σύνδεσμοι[Επεξεργασία | επεξεργασία κώδικα]

Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα System F της Αγγλικής Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).