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

Ο λ-λογισμός με απλούς τύπους ($\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$

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