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

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

Στη μαθηματική λογική και στην επιστήμη υπολογιστών, λογισμός λάμδα ή λ-λογισμός (αγγλ. 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. Αν και δεν είναι μέρος του τυπικού ορισμού της γλώσσας, η

λ x1 x2xn. έκφραση

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

λ x1. λ x2. … λ xn. έκφραση

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

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))  ως Ω2, κλπ.

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

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

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

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

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

λ z. zx. y).

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

Τυπικός ορισμός[Επεξεργασία | επεξεργασία κώδικα]

Ορισμός[Επεξεργασία | επεξεργασία κώδικα]

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

μεταβλητές v1, v2, . . . vn
τα σύμβολα αφαίρεσης λ και .
παρενθέσεις ( )

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

  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 . Συχνά, σε πολλές χρήσεις του λογισμού λάμδα, όροι που διαφέρουν μόνο κατά μια α-μετατροπή θεωρούνται ισοδύναμοι.

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

Δεύτερον, η μετατροπή άλφα δεν είναι δυνατή αν θα προκαλούσε τη δέσμευση μιας μεταβλητής από διαφορετική αφαίρεση. Για παράδειγμα, αν αντικαταστήσουμε το x με y στην έκφραση λxy.x, παίρνουμε λyy.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
(M1 M2)[x := N]  ≡ (M1[x := N]) (M2[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(n)x. Τονίζεται ότι η έκφραση f(n) από μόνη της δεν αποτελεί λ-όρο[1]. Στην αρχική διατύπωση του λογισμού λάμδα από τον Τσερτς, η τυπική παράμετρος μιας έκφρασης λάμδα έπρεπε απαραίτητα να εμφανίζεται τουλάχιστον μια φορά στο σώμα της συνάρτησης, πράγμα που έκανε τον παραπάνω ορισμό του 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. ng h. h (g f)) (λ u. x) (λ u. u

μπορεί να επαληθευτεί δείχνοντας επαγωγικά ότι αν το T αναπαριστά το g h. h (g f)), τότε T(n)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. nx. FALSE) TRUE

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

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

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

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

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

το οποίο μπορεί να επαληθευτεί δείχνοντας επαγωγικά ότι το ng 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))

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

  1. Jean-Louis Krivine, Lambda-Calculus, Types and Models, σελ. 31.

Δείτε επίσης[Επεξεργασία | επεξεργασία κώδικα]

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

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