λ-λογισμός με απλούς τύπους

Ο λ-λογισμός με απλούς τύπους ($\lambda ^{\to }$) είναι μια θεωρίας τύπων, είναι μια ερμηνεία τύπων του λ-λογισμού με ένα μοναδικό κατασκευαστή τύπων (type constructor): $\to$, ο οποίος κατασκευάζει τύπους συναρτήσεων. Είναι το κανονικό και το πιο απλό παράδειγμα λ-λογισμού με τύπους, και εμφανίζει πολλές επιθυμητές και ενδιαφέρουσες ιδιότητες.

Ο όρος απλός τύπος χρησιμοποιείται επίσης για επεκτάσεις του λ-λογισμού με απλούς τύπους όπως τα γινόμενα, τα συγγινόμενα, και οι φυσικοί αριθμοί (Σύστημα Τ) ή ακόμη και με πλήρη αναδρομή. Αντίθετα, συστήματα που εισάγουν πολυμορφικούς τύπους (όπως το Σύστημα F) ή εξαρτώμενους τύπους όπως το Logical Framework δεν θεωρούνται με απλούς τύπους. Τα πρώτα θεωρούνται απλά επειδή μπορεί να γίνει κωδικοποίηση Τσερτς τέτοιων δομών χρησιμοποιώντας μόνο $\to$ και κατάλληλες μεταβλητές τύπων, ενώ δεν μπορούν να κωδικοποιηθούν αντίστοιχα ο πολυμορφισμός και η εξάρτηση τύπων.

Συντακτικό

Για να οριστούν οι τύποι, ορίζουμε ένα σύνολο βασικών τύπων, $B$. Αυτοί λέγονται και ατομικοί τύποι ή σταθερές τύπων. Με ορισμένο το σύνολο σταθερών, το συντακτικό των τύπων είναι:

$\tau =\tau \to \tau \mid T\quad \mathrm {where} \;T\in B$.

Στο παρόν άρθρο τα $\sigma$ και $\tau$ αναπαριστούν τύπους. Πρακτικά, ο τύπος συνάρτησης $\sigma \to \tau$ αναφέρεται στο σύνολο από συναρτήσεις δέχονται είσοδο τύπου $\sigma$ και παράγουν έξοδο τύπου $\tau$. Κατα σύμβαση, ο τελεστής $\to$ έχει προτεραιότητα στα δεξιά: το $\sigma \to \tau \to \rho$ διαβάζεται ως $\sigma \to (\tau \to \rho )$.

Ορίζουμε ακόμη ένα σύνολο από σταθερές όρων για τους βασικούς τύπους. Για παράδειγμα, για το βασικός τύπο nat οι σταθερές όρων θα ήταν οι φυσικοί αριθμοί. Στην αρχική παρουσίασή του, ο Τσερτς χρησιμοποίησε μόνο δύο βασικούς τύπους: $o$ για τον "τύπο των προτάσεων" και $\iota$ για τον "τύπο των ατόμων". Ο τύπος $o$ δεν έχει σταθερές όρων, ενώ ο τύπος $\iota$ έχει μια σταθερά όρων. Συχνότερα θεωρείται ο λ-λογισμός με ένα μόνο βασικό τύπο, συνήθως $o$.

Το συντακτικό του λ-λογισμού με απλούς τύπους είναι βασικά το ίδιο με το συντακτικό του λ-λογισμού. Το συντακτικό όρων που χρησιμοποιεί το παρόν άρθρο είναι:

$e=x\mid \lambda x\!:\!\tau .e\mid e\,e\mid c$

όπου $c$ είναι σταθερά όρων.

δηλαδή, αναφορά σε μεταβλητή, αφαίρεση, εφαρμογή, και σταθερά. Μια αναφορά σε μεταβλητή $x$ είναι δεσμευμένη αν βρίσκεται μέσα σε μια αφαίρεση που δεσμεύει το $x$. Ένας όρος είναι κλειστός αν δεν περιέχει μη-δεσμευμένες μεταβλητές.

Συγκριτικά, το συντακτικό του λ-λογισμού χωρίς τύπους είναι:

$e=x\mid \lambda x.e\mid e\,e$

Φαίνεται ότι στο λ-λογισμό με τύπους κάθε συνάρτηση (αφαίρεση) πρέπει να καθορίζει τον τύπο του ορίσματός της.

Κανόνες τύπων

Για να οριστεί το σύνολο των όρων με καλά ορισμένο τύπο, για κάθε τύπο, ορίζεται μια σχέση αντιστοίχησης μεταξύ όρων και τύπων. Αρχικά, θεωρούμε τα πλαίσια τύπων (typing contexts) $\Gamma ,\Delta ,\dots$, τα οποία είναι σύνολα από υποθέσεις αντιστοίχησης τύπων σε μεταβλητές. Μια υπόθεση αντιστοίχησης τύπου έχει τη μορφή $x:\sigma$, που σημαίνει ότι η μεταβλητή $x$ έχει τύπο $\sigma$.

Η σχέση αντιστοίχησης τύπων $\Gamma \vdash e:\sigma$ εκφράζει ότι ο όρος $e$ είναι τύπου $\sigma$ στο πλαίσιο $\Gamma$. Λέγεται λοιπόν ότι το "$e$ έχει καλά ορισμένο τύπο (στο $\sigma$)". Παραδείγματα τέτοιων σχέσεων αντιστοίχησης τύπων λέγονται κρίσεις αντιστοίχησης τύπων (typing judgments). Η ορθότητα μιας τέτοιας κρίσης τύπων δείχνεται παρέχοντας μια αναγωγή τύπων (typing derivation), η οποία κατασκευάζεται με τους ακόλουθους κανόνες τύπων. Οι προυποθέσεις που βρίσκονται πάνω από τη γραμμή επιτρέπουν την αναγωγή του συμπεράσματος που βρίσκεται κάτω από τη γραμμή.

${x:\sigma \in \Gamma } \over {\Gamma \vdash x:\sigma }$ (1)      ${c{\textrm {~is~a~constant~of~type~}}T} \over {\Gamma \vdash c:T}$ (2)

${\Gamma ,x:\sigma \vdash e:\tau } \over {\Gamma \vdash \lambda x:\sigma .~e:\sigma \to \tau }$ (3)      ${\Gamma \vdash e_{1}:\sigma \to \tau \quad \Gamma \vdash e_{2}:\sigma } \over {\Gamma \vdash e_{1}~e_{2}:\tau }$ (4)

Με άλλα λόγια,

1. Αν το $x$ έχει τύπο $\sigma$ στο πλαίσιο, γνωρίζουμε ότι το $x$ έχει τύπο $\sigma$.
2. Οι σταθερές όρων έχουν τον αντίστοιχο βασικό τύπο.
3. Αν, σε κάποιο πλάισιο όπου το $x$ έχει τύπο $\sigma$, το $e$ έχει τύπο $\tau$, τότε, στο ίδιο πλαίσιο χωρίς το $x$, ο όρος $\lambda x:\sigma .~e$ έχει τύπο $\sigma \to \tau$.
4. Αν σε κάποιο πλαίσιο το $e_{1}$ έχει τύπο $\sigma \to \tau$, και το $e_{2}$ έχει τύπο $\sigma$, τότε ο όρος $e_{1}~e_{2}$ έχει τύπο $\tau$.

Παραδείγματα κλειστών όρων, δηλαδή όρων που έχουν τύπο σε κενό πλαίσιο, είναι:

• Για κάθε τύπο $\tau$, ο όρος $\lambda x:\tau .x:\tau \to \tau$ (ο συνδυαστής I, ή ταυτοτική συνάρτηση),
• Για κάθε τύπο $\sigma ,\tau$, ο όρος $\lambda x:\sigma .\lambda y:\tau .x:\sigma \to \tau \to \sigma$ (ο συνδυαστής K), και
• Για κάθε τύπο $\tau ,\tau ',\tau ''$, ο όρος $\lambda x:\tau \to \tau '\to \tau ''.\lambda y:\tau \to \tau '.\lambda z:\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''$ (ο συνδυαστής S).

Αυτές είναι οι αναπαραστάσεις σε λ-λογισμό των βασικών συνδυαστών της συνδυαστικής λογικής.

Σε κάθε τύπο $\tau$ αντιστοιχεί ένας βαθμός, ένας αριθμός $o(\tau )$. Για τους βασικούς τύπους $o(T)=0$; για τύπους συνάρτησης, $o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))$. Δηλαδή, ο βαθμός ενός τύπου μετράει το βάθος του πιο φωλιασμένου βέλους. Έτσι,

$o(\iota \to \iota \to \iota )=1$

$o((\iota \to \iota )\to \iota )=2$

Σημασιολογία

Σημασιολογία θεωρίας αποδείξεων

Ο λ-λογισμός με απλούς τύπους σχετίζεται πολύ με το επαγωγικό κομμάτι της προτασιακής ιντουισιονιστικής λογικής (δηλ. ελάχιστης λογικής) μέσω του ισομορφισμού Κάρυ-Χάουαρντ: οι όροι αντιστοιχούν ακριβώς σε αποδείξεις στην φυσική αναγωγή, και οι μη-κενοί (ή κατοικημένοι) τύποι είναι ταυτολογίες της ελάχιστης λογικής.

Σημαντικά αποτελέσματα

• Ο Τέιτ έδειξε το 1967 ότι η $\beta$-αναγωγή είναι ισχυρά κανονικοποιητική. Ως επακόλουθο, η $\beta \eta$-ισοδυναμία είναι αποφασίσιμη. Ο Στάτμαν έδειξε το 1977 ότι το πρόβλημα κανονικοποίησης δεν είναι στοιχειωδώς αναδρομικό. Μια αμιγώς σημασιολογική απόδειξη κανονικοποίησης (βλ. κανονικοποίηση με υπολογισμό) δόθηκε από τους Μπέργκερ και Σβιχτενμπεργκ το 1991.
• Το πρόβλημα ενοποίησης για την $\beta \eta$-ισοδυναμία είναι μη-αποφασίσιμο. Ο Υ (Huet) έδειξε το 1973 ότι η ενοποίηση 3ου βαθμού είναι μη αποφασίσιμη, και αυτό βελτιώθηκε από τον Μπάξτερ το 1978, και τον Γκόλντφαρμπ το 1981 δείχνοντας ότι η ενοποίηση 2ου βαθμού είναι ήδη μη-αποφασίσιμη. Το αν η αντιστοιχία ανώτερου βαθμού (ενοποίηση, όπου μόνο ένας όρος περιέχει υπαρξιακές μεταβλητές) είναι αποφασίσιμο, είναι ακόμη ανοικτό πρόβλημα.
• Οι φυσικός αριθμός φυσικοί αριθμοί μπορούν να κωδικοποιηθούν από όρους του τύπου $(o\to o)\to (o\to o)$ (Αριθμητικά Τσερτς). Ο Σβιχτενμπεργκ έδειξε το 1976 ότι στο $\lambda ^{\to }$ ακριβώς τα επεκτεταμένα πολυώνυμα μπορούν να αναπαρασταθούν ως συναρτήσεις πάνω σε αριθμητικά Τσερτς. Αυτά είναι περίπου τα πολυώνυμα που είναι κλειστά υπο υποθετικό τελεστή.
• Ένα πλήρες μοντέλο του $\lambda ^{\to }$ δείνεται ερμηνεύοντας τους βασικούς τύπους ως σύνολα και τους τύπους συνάρτησης με το συνολοθεωρητικό χώρο συναρτήσεων. Ο Φρίντμαν έδειξε το 1975 ότι αυτή η ερμηνεία είναι πλήρης για $\beta \eta$-ισοδυναμία, αν οι βασικοί τύποι ερμηνευθούν ως άπειρα σύνολα. Ο Στάτμαν έδειξε το 1983 ότι η $\beta \eta$-ισοδυναμία είναι η μέγιστη ισοδυναμία που είναι τυπικά ασαφής, δηλαδή κλειστή υπό την αντικατάσταση τύπων (Θεώρημα τυπικής ασάφειας του Στάτμαν). Συνέπεια αυτού είναι ότι η ιδιότητα πεπερασμένου μοντέλου ισχύει, δηλαδή τα πεπερασμένα σύνολα είναι αρκετά για να διαχωριστούν όροι που δεν ταυτοποιούνται από τη $\beta \eta$-ισοδυναμία.
• Ο Πλότκιν εισήγαγε τις λογικές σχέσεις το 1973 για να χαρακτηρίσει τα στοιχεία ενός μοντέλου που είναι ορίσιμα από όρους λ-λογισμού. Το 1993 οι Γιούνγκ και Τιουρίν έδειξαν ότι μια γενική μορφή λογικής σχέσης (Λογικές σχέσεις Κρίπκε με μεταβλητό εύρος (arity)) χαρακτηρίζει ακριβώς την ορισιμότητα λ. Οι Πλότκιν και Στάτμαν διατύπωσαν την εικασία ότι είναι αποφασίσιμο αν ένα δεδομένο στοιχείο ενός μοντέλου που παράγεται από πεπερασμένα σύνολα είναι ορίσιμο από ένα όρο λ-λογισμού (Εικασία Πλότκιν-Στάτμαν). Η εικασία αυτή καταρρίφθηκε από τον Λόντερ το 1993.

Αναφορές

• A. Church: A Formulation of the Simple Theory of Types, JSL 5, 1940
• W.W.Tait: Intensional Interpretations of Functionals of Finite Type I, JSL 32(2), 1967
• G.D. Plotkin: Lambda-definability and logical relations, Technical report, 1973
• G.P. Huet: The Undecidability of Unification in Third Order Logic Information and Control 22(3): 257-267 (1973)
• H. Friedman: Equality between functionals. LogicColl. '73, pages 22-37, LNM 453, 1975.
• H. Schwichtenberg: Functions definable in the simply-typed lambda calculus, Arch. Math Logik 17 (1976) 113-114.
• R. Statman: The Typed lambda-Calculus Is not Elementary Recursive FOCS 1977: 90-94
• W. D. Goldfarb: The undecidability of the 2nd order unification problem, TCS (1981), no. 13, 225- 230.
• R. Statman. $\lambda$-definable functionals and $\beta \eta$ conversion. Arch. Math. Logik, 23:21–26, 1983.
• J. Lambek: Cartesian Closed Categories and Typed Lambda-calculi. Combinators and Functional Programming Languages 1985: 136-175
• U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus LICS 1991: 203-211
• Jung, A.,Tiuryn, J.:A New Characterization of Lambda Definability, TLCA 1993
• R. Loader: The Undecidability of λ-definability, appeared in the Church Festschrift, 2001
• H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN 0-19-853761-1.
• L. Baxter: The undecidability of the third order dyadic unification problem, Information and Control 38(2), 170-178 (1978)

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

• Article Church's Type Theory in the Stanford Encyclopedia of Philosophy.
• Loader, Ralph (1998). «Notes on Simply Typed Lambda Calculus».