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

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

Οι λ-λογισμοί με τύπους είναι θεμελιώδεις γλώσσες προγραμματισμού και αποτελούν τη βάση των γλωσσών συναρτησιακού προγραμματισμού με τύπους όπως η ML και η Haskell, και κάπως γενικότερα των γλωσσών προστακτικού προγραμματισμού. Οι λ-λογισμοί με τύπους παίζουν σημαντικό ρόλο στη σχεδίαση των συστημάτων τύπων των γλωσσών προγραμματισμού, όπου η τυποποιησιμότητα συνήθως εκφράζει επιθυμητές ιδιότητες του προγράμματος, όπως π.χ. ότι το πρόγραμμα δε θα προκαλέσει κάποιο σφάλμα μνήμης.

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

## Είδη των λ-λογισμών με τύπους
Έχουν μελετηθεί πολλοί λ-λογισμοί με τύπους: οι τύποι του λ-λογισμού με απλούς τύπους είναι μόνο βασικοί τύποι (ή μεταβλητές τύπων) και τύποι συναρτήσεων \sigma\to\tau. Το Σύστημα T επεκτείνει το λ-λογισμό με απλούς τύπους με έναν τύπο φυσικών αριθμών και πρωτογενή αναδρομή ανώτερης τάξης - σε αυτό το σύστημα μπορούν να οριστούν όλες οι συναρτήσεις που αποδεικνύεται ότι είναι πρωτογενώς αναδρομικές στην αριθμητική Πεάνο. Το Σύστημα F επιτρέπει τον πολυμορφισμό χρησιμοποιώντας καθολικούς ποσοδείκτες πάνω σε όλους τους τύπους - από λογικής απόψεως μπορεί να περιγράψει όλες τις συναρτήσεις που μπορεί να αποδειχθεί ότι είναι πλήρεις στη λογική δεύτερης τάξης. Οι λ-λογισμοί με εξαρτώμενους τύπους είναι η βάση της ιντουισιονιστικής θεωρίας τύπων, του λογισμού των κατασκευών και του LF, ενός αμιγούς λ-λογισμού με εξαρτώμενους τύπους. Βασισμένος σε δουλειά του Μπεράρντι πάνω στα αμιγή συστήματα τύπων (pure type systems), ο Μπάρεντρεγκτ πρότεινε τον λ-κύβο για τη συστηματοποίηση των σχέσεων μεταξύ των αμιγών λ-λογισμών με τύπους (συμπεριλαμβανομένων του λ-λογισμού με απλούς τύπους, του Συστήματος F, του LF και του λογισμού των κατασκευών).

Κάποιοι λ-λογισμοί με τύπους περιλαμβάνουν την έννοια του *[[υποτύπος|υποτύπου]]*, δηλ. αν ο A είναι ένας υπότυπος του B, τότε όλοι οι όροι τύπου A έχουν επίσης τύπο B. Οι λ-λογισμοί με τύπους και υπότυπους είναι ο λ-λογισμός με απλούς τύπους και τύπους συζεύξεως (conjunctive types) και το Σύστημα F.

Όλα τα παραπάνω συστήματα, εκτός του λ-λογισμού χωρίς τύπους, είναι *ισχυρά κανονικοποιήσιμα*: όλοι οι υπολογισμοί τερματίζουν. Αυτό έχει ως αποτέλεσμα να είναι συνεπή σαν λογικές, δηλ. δεν υπάρχουν κενοί τύποι. Υπάρχουν όμως λ-λογισμοί με τύπους που δεν είναι ισχυρά κανονικοποιήσιμοι. Για παράδειγμα ο λ-λογισμός με εξαρτώμενους τύπους που περιέχει ένα τύπο όλων των τύπων (Τύπος : Τύπος) δεν είναι κανονικοποιήσιμος λόγω του παραδόξου του Ζιράρ. Το σύστημα αυτό είναι επίσης το πιο απλό αμιγές σύστημα τύπων, ενός φορμαλισμού που γενικεύει τον λ-κύβο. Τα συστήματα με ρητούς συνδυαστές αναδρομής (recursion combinators), όπως το PCF του Πλότκιν, δεν είναι κανονικοποιήσιμα, αλλά δεν προορίζονται να ερμηνευτούν σαν λογικές. Η PCF (*Programming language for Computable Functions*) είναι μια πρωτότυπη γλώσσα συναρτησιακού προγραμματισμού με τύπους, στην οποία οι τύποι χρησιμοποιούνται για να βεβαιωθεί ότι τα προγράμματα συμπεριφέρονται σωστά, αλλά δεν είναι απαραίτητο να τερματίζουν.

## Εφαρμογές στις γλώσσες προγραμματισμού
Στον προγραμματισμό, οι ρουτίνες (συναρτήσεις, διαδικασίες, μέθοδοι) των γλωσσών προγραμματισμού με ισχυρούς τύπους έχουν σχέση με τις λ-εκφράσεις με τύπους. Η Eiffel έχει την έννοια του "ένθετου πράκτορα" ("inline agent") που επιτρέπει τον ορισμό και το χειρισμό απευθείας λ-εκφράσεων με τύπους, μέσω εκφράσεων όπως **agent** (p: PERSON): STRING **do Result** := p.spouse.name **end**, που σημαίνει ένα αντικείμενο που αναπαριστά μια συνάρτηση που επιστρέφει το όνομα της συζύγου ενός ατόμου.

## Παραπομπές

* Henk Barendregt, [ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps Lambda Calculi with Types], Handbook of Logic in Computer Science, Volume II, Oxford University Press.

Κατηγορία:Λ-λογισμός
Κατηγορία:Θεωρία τύπων