Λογισμός λάμδα

Στη μαθηματική λογική, την πληροφορική και την υπολογιστική γλωσσολογία, λογισμός λάμδα ή λ-λογισμός (αγγλ. lambda calculus ή λ-calculus), είναι ένα τυπικό σύστημα (formal system) σχεδιασμένο για τη διερεύνηση ορισμών, εφαρμογών συναρτήσεων και αναδρομής συναρτήσεων. Δημιουργήθηκε από τους Αλόνζο Τσερτς και Στίβεν Κλέινι τη δεκαετία 1930. Ο Τσερτς χρησιμοποίησε το λογισμό λάμδα για να δώσει αρνητική απάντηση στο πρόβλημα απόφασης (Entscheidungsproblem) του Ντάβιντ Χίλμπερτ. Ο λογισμός λάμδα μπορεί να χρησιμοποιηθεί για να ορίσει τι είναι μια υπολογίσιμη συνάρτηση. Η ερώτηση αν δύο όροι του λογισμού λάμδα είναι ισοδύναμοι (πρόβλημα λέξης, word problem) δε μπορεί να απαντηθεί με ένα γενικό αλγόριθμο. Αυτό ήταν το πρώτο πρόβλημα, πριν ακόμα το πρόβλημα τερματισμού (halting problem) για το οποίο μπορούσε να αποδειχθεί η μη αποφασισιμότητα.

Ο λογισμός λάμδα είναι η μικρότερη δυνατή καθολική γλώσσα προγραμματισμού. Αποτελείται από ένα μοναδικό κανόνα μετασχηματισμού (αντικατάσταση μεταβλητών) και ένα μοναδικό τρόπο ορισμού συνάρτησης. Ο λογισμός λάμδα είναι καθολικός με την έννοια ότι οποιαδήποτε υπολογίσιμη συνάρτηση μπορεί να εκφραστεί και να υπολογιστεί χρησιμοποιώντας αυτό το σύστημα. Έτσι, είναι ισοδύναμος με τη μηχανή Τούρινγκ. Παρόλα αυτά, ο λογισμός λάμδα είναι τυποποίηση της υπολογισιμότητας που δίνει έμφαση στη χρήση κανόνων μετασχηματισμού, και δεν ενδιαφέρεται για τη μηχανή που τους υλοποιεί —σχετίζεται περισσότερο με το λογισμικό παρά με το υλικό— και ως τέτοια έχει αποτελέσει τη βάση του λεγόμενου συναρτησιακού προγραμματισμού.

Ανεπίσημος ορισμός

Στο λογισμό λάμδα, κάθε έκφραση είναι μια μοναδιαία συνάρτηση, δηλαδή συνάρτηση με μόνο ένα όρισμα. Όταν μία έκφραση εφαρμόζεται σε μία άλλη (λέμε ότι "καλείται" η συνάρτηση με όρισμα την άλλη έκφραση), επιστρέφει μία μοναδική τιμή, που λέγεται το αποτέλεσμά της.

Μια και κάθε έκφραση είναι μία μοναδιαία συνάρτηση, και κάθε όρισμα και αποτέλεσμα είναι κι αυτά συναρτήσεις, ο λογισμός λάμδα παρουσιάζει ενδιαφέρον τόσο ως προς τον υπολογισμό όσο και τα μαθηματικά.

Μια συνάρτηση ορίζεται χωρίς να της δοθεί όνομα από μια έκφραση λάμδα, που εκφράζει την πράξη που εφαρμόζει πάνω στο όρισμά της. Για παράδειγμα, η συνάρτηση "πρόσθεσε δύο" f έτσι ώστε  f(x) = x + 2  εκφράζεται στο λογισμό λάμδα ως  λ x. x + 2  (ή ισοδύναμα ως  λ y. y + 2;  το όνομα της παραμέτρου δεν έχει σημασία) και η εφαρμογή της συνάρτησης f(3) θα γραφόταν ως  (λ x. x + 2) 3.  Αυτό που κάνει αυτή την έκφραση "ανεπίσημη", είναι ότι η έκφραση x + 2 (ή ακόμα και ο αριθμός 2) δεν είναι μέρος του λογισμού λάμδα. Η εφαρμογή συνάρτησης ακολουθεί συσχέτιση προς τα αριστερά:  f x y = (f x) y.  Έστω η συνάρτηση που παίρνει μία συνάρτηση ως όρισμα και την εφαρμόζει στον αριθμό 3 ως εξής: λ f. f 3.  Η τελευταία αυτή συνάρτηση μπορεί να εφαρμοστεί στην προηγούμενη "πρόσθεσε δύο" ως εξής:  (λ f. f 3) (λ x. x + 2).  Οι τρεις εκφράσεις:

• (λ f. f 3) (λ x. x + 2)
• (λ x. x + 2) 3
• 3 + 2

είναι ισοδύναμες.

Μία συνάρτηση δύο μεταβλητών εκφράζεται στο λογισμό λάμδα ως μία συνάρτηση με ένα όρισμα, που επιστρέφει μία συνάρτηση με ένα όρισμα (καρρύωση, currying). Για παράδειγμα, η συνάρτηση  f(x, y) = x - y  γράφεται  λ x. λ y. x - y. Συνηθίζεται να συντομογραφούνται αυτές οι συναρτήσεις. Για παράδειγμα, η προηγούμενη γράφεται  λ x y. x - y. Αν και δεν είναι μέρος του τυπικού ορισμού της γλώσσας, η

λ x₁ x₂ … x_n. έκφραση

χρησιμοποιείται ως συντομογραφία για την

λ x₁. λ x₂. … λ x_n. έκφραση

Δεν μπορούν όλες οι εκφράσεις λάμδα να αναχθούν σε μία συγκεκριμένη τιμή όπως οι παραπάνω. Για παράδειγμα, μπορεί κανείς να υποθέσει

(λ x. x x) (λ x. x x)

ή

(λ x. x x x) (λ x. x x x)

και να προσπαθήσει να εφαρμόσει την πρώτη συνάρτηση στο όρισμά της. Η έκφραση  (λ x. x x)  είναι γνωστή ως συνδυαστής (combinator) ω, η  ((λ x. x x) (λ x. x x))  είναι γνωστή ως Ω, η  ((λ x. x x x) (λ x. x x x))  ως Ω₂, κλπ.

Οι εκφράσεις στον λογισμό λάμδα μπορεί να περιέχουν ελεύθερες μεταβλητές, δηλαδή μεταβλητές που δε δεσμεύονται από κάποιο λ. Για παράδειγμα, η μεταβλητή  y  είναι ελεύθερη στην έκφραση  (λ x. y) , που αναπαριστά μία συνάρτηση που παράγει πάντα το αποτέλεσμα y. Ορισμένες φορές αυτό καθιστά αναγκαία τη μετονομασία κάποιων τυπικών παραμέτρων. Για παράδειγμα, στον παρακάτω τύπο, το γράμμα y χρησιμοποιείται πρώτα σαν τυπική παράμετρος, και μετά σαν ελεύθερη μεταβλητή:

(λ x y. y x) (λ x. y).

Για να υπολογίσουμε αυτή την έκφραση, μετονομάζουμε την πρώτη ως z έτσι ώστε η αναγωγή να μην μπερδέψει τα ονόματα:

(λ x z. z x) (λ x. y)

και η αναγωγή είναι

λ z. z (λ x. y).

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

Τυπικός ορισμός

Ορισμός

Οι εκφράσεις (expressions) στο λογισμό λάμδα αποτελούνται από:

μεταβλητές v₁, v₂, . . . v_n

τα σύμβολα αφαίρεσης λ και .

παρενθέσεις ( )

Το σύνολο των εκφράσεων λάμδα, Λ, μπορεί να οριστεί αναδρομικά:

1. Αν x είναι μεταβλητή, τότε x $\in$ Λ
2. Αν x είναι μεταβλητή και M $\in$ Λ, τότε ( λ x . M ) $\in$ Λ
3. Αν M, N $\in$ Λ, τότε ( M N ) $\in$ Λ

Οι εκφράσεις που παράγονται από το 2 λέγονται αφαιρέσεις ή αποσπάσεις (abstractions) και από το 3 λέγονται εφαρμογές.

Συμβολισμός

Για να διατηρηθεί ο συμβολισμός των εκφράσεων λάμδα συμπαγής, ακολουθούνται κατά σύμβαση οι ακόλουθοι κανόνες:

Οι εξωτερικές παρενθέσεις παραλείπονται: M N αντί για (M N).

Οι εφαρμογές υποθέτουμε ότι συσχετίζονται προς τα αριστερά: M N P σημαίνει (M N) P.

Η ακτίνα επίδρασης μίας αφαίρεσης εκτείνεται όσο είναι δυνατόν προς τα δεξιά: λ x. M N σημαίνει (λ x.M N) και όχι (λ x. M) N

Σειρές από αφαιρέσεις συμπτύσσονται: λ x λ y λ z. N γράφεται συμπτυγμένα λ x y z . N

Ελεύθερες και δεσμευμένες μεταβλητές

Ο τελεστής αφαίρεσης, λ, λέγεται ότι δεσμεύει τη μεταβλητή του οπουδήποτε αυτή υπάρχει στην ακτίνα επίδρασης της αφαίρεσης. Μεταβλητές που εμπίπτουν εντός της επίδρασης ενός τελεστή λ λέγονται δεσμευμένες. Όλες οι άλλες μεταβλητές λέγονται ελεύθερες. Για παράδειγμα, στην ακόλουθη έκφραση το y είναι δεσμευμένη μεταβλητή και το x είναι ελεύθερη:

λ y . xxy

Παρατηρήστε ότι κάθε μεταβλητή δεσμεύεται από το "κοντινότερο" λάμδα. Στην ακόλουθη έκφραση η (μόνη) εμφάνιση του x δεσμεύεται από το δεύτερο λάμδα:

λ x . y (λ x . z x)

Το σύνολο των ελεύθερων μεταβλητών μιας έκφρασης λάμδα, M, συμβολίζεται με FV(M) και ορίζεται αναδρομικά ως:

1. FV( x ) = {x}, όπου x είναι μεταβλητή
2. FV ( λ x . M ) = FV ( M ) - {x}
3. FV ( M N ) = FV ( M ) $\cup$ FV ( N )

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

Αναγωγή

α-μετατροπή

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

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

Δεύτερον, η μετατροπή άλφα δεν είναι δυνατή αν θα προκαλούσε τη δέσμευση μίας μεταβλητής από διαφορετική αφαίρεση. Για παράδειγμα, αν αντικαταστήσουμε το x με y στην έκφραση λx.λy.x, παίρνουμε λy.λy.y, που δεν είναι καθόλου το ίδιο.

Αντικατάσταση

Η αντικατάσταση (substitution), η οποία συμβολίζεται με E[V := E′], αντικαθιστά μία μεταβλητή V από την έκφραση E′ σε κάθε σημείο που η V είναι ελεύθερη στην E. Ο ακριβής ορισμός χρειάζεται προσοχή, για να αποφευχθεί η κατά λάθος δέσμευση άλλων μεταβλητών. Για παράδειγμα, δεν είναι σωστή η αντικατάσταση (λ x.y)[y := x] να δώσει (λ x.x), αφού η μεταβλητή x που αντικαθιστά το y θα έπρεπε να ήταν ελεύθερη, αλλά καταλήγει να είναι δεσμευμένη. Η σωστή λύση για αυτή την περίπτωση είναι η (λ z.x), έως την α-ισοδυναμία.

Η αντικατάσταση σε όρους του λογισμού λάμδα ορίζεται αναδρομικά στη δομή των όρων, ως εξής:

x[x := N]        ≡ N

y[x := N]        ≡ y, αν x ≠ y

(M₁ M₂)[x := N]  ≡ (M₁[x := N]) (M₂[x := N])

(λ y. M)[x := N] ≡ λ y. (M[x := N]), if x ≠ y και y∉fv(N)

Μπορεί κανείς να παρατηρήσει ότι η αντικατάσταση ορίζεται μοναδικά κατά προσέγγιση α-ισοδυναμίας.

β-αναγωγή

Η αναγωγή βήτα εκφράζει την έννοια της εφαρμογής συνάρτησης. Η αναγωγή βήτα της έκφρασης  ((λ V. E) E′)  είναι απλά  E[V := E′].

η-μετατροπή

Η μετατροπή ήτα εκφράζει την έννοια της εκτατικότητας, που σ'αυτό το πλαίσιο είναι ότι δύο συναρτήσεις είναι ίδιες αν και μόνο αν δίνουν το ίδιο αποτέλεσμα για όλα τα ορίσματα. Η μετατροπή ήτα μετατρέπει την έκφραση  λ x. f x  σε  f  και αντίστροφα, όταν η μεταβλητή x δεν εμφανίζεται ελεύθερη μέσα στην f.

Η μετατροπή αυτή δεν επιτρέπεται πάντα όταν οι εκφράσεις λάμδα ερμηνεύονται ως προγράμματα. Η αποτίμηση της  λ x. f x  θα μπορούσε να τερματίζει ακόμα και αν η αποτίμηση της f δεν τερματίζει [ΨΕΥΔΕΣ!!! ένας λ-όρος είναι β-κανονικοποιήσιμος αν και μόνο αν είναι βη-κανονικοποιήσιμος].

Κωδικοποίηση τύπων δεδομένων

Αριθμητική στο λογισμό λάμδα

Υπάρχουν διάφοροι τρόποι να οριστούν οι φυσικοί αριθμοί στο λογισμό λάμδα, αλλά ο πιο κοινός είναι τα αριθμητικά του Τσερτς (Church numerals), που ορίζονται ως εξής:

0 := λ f x. x

1 := λ f x. f x

2 := λ f x. f (f x)

3 := λ f x. f (f (f x))

και ούτω καθεξής. Κάθε αριθμός είναι μία συνάρτηση υψηλού τύπου, παίρνει ως όρισμα μία συνάρτηση με ένα όρισμα, και επιστρέφει μία άλλη. Το αριθμητικό Τσερτς n είναι μία συνάρτηση, που δέχεται ως ορίσματα μία άλλη συνάρτηση f και ένα λ-όρο x και επιστρέφει την f, εφαρμοσμένη στο x, n φορές. Αυτό γράφεται f⁽ⁿ⁾x. Τονίζεται ότι η έκφραση f⁽ⁿ⁾ από μόνη της δεν αποτελεί λ-όρο. Στην αρχική διατύπωση του λογισμού λάμδα από τον Τσερτς, η τυπική παράμετρος μίας έκφρασης λάμδα έπρεπε απαραίτητα να εμφανίζεται τουλάχιστον μία φορά στο σώμα της συνάρτησης, πράγμα που έκανε τον παραπάνω ορισμό του 0 αδύνατο.

Μπορούμε να ορίσουμε τη συνάρτηση διαδοχής, που δέχεται έναν αριθμό n και επιστρέφει n + 1 προσθέτοντας μία επιπλέον εφαρμογή της f:

SUCC := λ n f x. f (n f x)

Επειδή η m-οστή σύνθεση της f, σε σύνθεση με τη n-οστή σύνθεση της f δίνει τη m+n-οστή σύνθεση της f, η πρόσθεση μπορεί να οριστεί ως εξής:

PLUS := λ m n f x. n f (m f x)

Το PLUS μπορεί να θεωρηθεί ως μία συνάρτηση που παίρνει δύο φυσικούς αριθμούς ως ορίσματα και επιστρέφει ένα φυσικό αριθμό. Μπορεί κανείς να ελέγξει ότι το

PLUS 2 3    και το    5

είναι ισοδύναμες εκφράσεις στο λογισμό λάμδα. Δεδομένου ότι η πρόσθεση του m σε έναν αριθμό n μπορεί να επιτευχθεί προσθέτοντας το 1 m φορές, ένας ισοδύναμος ορισμός είναι:

PLUS := λ n m. m SUCC n

Ομοίως, ο πολλαπλασιασμός μπορεί να οριστεί ως εξής:

MULT := λ m n f . m (n f)

Εναλλακτικά

MULT := λ m n. m (PLUS n) 0,

αφού ο πολλαπλασιασμός του m και n είναι το ίδιο με την επανάληψη της συνάρτησης "πρόσθεσε n", για m φορές, και στη συνέχεια την εφαρμογή της στο μηδέν. Η συνάρτηση προκατόχου, που ορίζεται ως  PRED n = n - 1  για ένα θετικό ακέραιο n και  PRED 0 = 0  είναι αρκετά πιο δύσκολη. Ο τύπος

PRED := λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u) 

μπορεί να επαληθευτεί δείχνοντας επαγωγικά ότι αν το T αναπαριστά το (λ g h. h (g f)), τότε T⁽ⁿ⁾(λ u. x) = (λ h. h(f^(n-1)(x)) ) για n > 0. Άλλοι δυο ορισμοί του PRED δίνονται παρακάτω, ο ένας με χρήση υποθετικών και ο άλλος με χρήση ζευγών. Με την συνάρτηση προκατόχου, η αφαίρεση γίνεται εύκολη. Ορίζοντας

SUB := λ m n. n PRED m,

το SUB m n δίνει m - n όταν m > n και 0 αλλιώς.

Λογική και κατηγορούμενα

Κατά σύμβαση, οι ακόλουθοι δύο ορισμοί (γνωστοί ως λογικές τιμές του Τσερτς) χρησιμοποιούνται για τις λογικές τιμές TRUE και FALSE:

TRUE := λ x y. x

FALSE := λ x y. y

(Παρατηρήστε ότι το FALSE είναι ισοδύναμο με το αριθμητικό Τσερτς για το μηδέν που ορίζεται παραπάνω)

Έτσι, με αυτούς τους δύο όρους λάμδα, μπορούμε να ορίσουμε κάποιους λογικούς τελεστές (αυτοί είναι απλά πιθανές διατυπώσεις, άλλες εκφράσεις μπορεί να είναι εξίσου σωστές):

AND := λ p q. p q p

OR := λ p q. p p q

NOT := λ p a b. p b a

IFTHENELSE := λ p a b. p a b

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

AND TRUE FALSE

≡ (λ p q. p q p) TRUE FALSE →_β TRUE FALSE TRUE

≡ (λ x y. x) FALSE TRUE →_β FALSE

και βλέπουμε ότι το AND TRUE FALSE είναι ισοδύναμο με το FALSE.

Ένα κατηγόρημα είναι μια συνάρτηση που επιστρέφει μια λογική τιμή. Το βασικότερο κατηγόρημα είναι το ISZERO, το οποίο επιστρέφει TRUE αν το όρισμά του είναι το αριθμητικό Τσερτς για το μηδέν, και FALSE αν το όρισμά του είναι οποιοδήποτε άλλο αριθμητικό Τσερτς:

ISZERO := λ n. n (λ x. FALSE) TRUE

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

LEQ := λ m n. ISZERO (SUB m n),

και αφού m = n αν και μόνο αν LEQ m n και LEQ n m, είναι απλό να κατασκευαστεί ένα κατηγόρημα για αριθμητική ισότητα.

Χρησιμοποιώντας τα κατηγορήματα και τους παραπάνω ορισμούς των TRUE και FALSE, γίνεται εύκολο να γράψουμε εκφράσεις "if-then-else" στο λογισμό λάμδα. Για παράδειγμα, η συνάρτηση προκατόχου μπορεί να οριστεί ως εξής:

PRED := λ n. n (λ g k. ISZERO (g 1) k (PLUS (g k) 1) ) (λ v. 0) 0

το οποίο μπορεί να επαληθευτεί δείχνοντας επαγωγικά ότι το n (λ g k. ISZERO (g 1) k (PLUS (g k) 1) ) (λ v. 0) είναι η συνάρτηση "n - 1" για n > 0.

Ζεύγη

Ένα ζεύγος μπορεί να οριστεί με βάση τα TRUE και FALSE, χρησιμοποιώντας την κωδικοποίηση ζευγών κατά Τσερτς. Για παράδειγμα, το PAIR ενσωματώνει το ζεύγος (x,y), το FIRST επιστρέφει το πρώτο στοιχείο του ζεύγους, και το SECOND επιστρέφει το δεύτερο.

PAIR := λ x y f. f x y

FIRST := λ p. p TRUE

SECOND := λ p. p FALSE

NIL := λ x. TRUE

NULL := λp. p (λx y.FALSE)

Μια συνδεδεμένη λίστα μπορεί να οριστεί επαγωγικά είτε ως NIL για την άδεια λίστα, είτε ως PAIR ενός στοιχείου ή κεφαλής και μιας μικρότερης λίστας ή ουράς. Το κατηγόρημα NULL ελέγχει για την τιμή NIL. (Εναλλακτικά, με NIL := FALSE και με την κατασκευή l (λh t z. περίπτωση_κεφαλής_h_και_ουράς_t) (περίπτωση_nil), δεν υπάρχει ανάγκη για ορισμό του NULL).

Ως παράδειγμα για τη χρήση των ζευγών, η συνάρτηση shift-and-increment που αντιστοιχεί (m, n) στο (n, n+1) μπορεί να οριστεί ως εξής:

Φ := λ x. PAIR (SECOND x) (SUCC (SECOND x))

η οποία μας επιτρέπει να ορίσουμε ίσως την πιο προφανή παραλλαγή της συνάρτησης προκατόχου:

PRED := λ n. FIRST (n Φ (PAIR 0 0))

Δείτε επίσης

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

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

• λ-λογισμός (Λ14), Γ. Κολέτσος, Γ. Σταυρινός, ΕΜΠ.
• Λογική και λ-λογισμός Αρχειοθετήθηκε 2015-09-08 στο Wayback Machine., Γ. Μαΐστρος, Σ. Μαρκαντωνάτου, ΕΜΠ.
• Λάμβδα λογισμός, Π. Ροντογιάννης, ΕΚΠΑ.