Ο λογισμός λάμδα είναι ένα επίσημο σύστημα στη μαθηματική λογική για την έκφραση υπολογισμών που βασίζονται σε αφαίρεση και την εφαρμογή συναρτήσεων χρησιμοποιώντας δέσμευση και αντικατάσταση μεταβλητών. Αυτό είναι ένα καθολικό μοντέλο που μπορεί να εφαρμοστεί στη σχεδίαση οποιασδήποτε μηχανής Turing. Ο λογισμός λάμδα εισήχθη για πρώτη φορά από τον Church, έναν διάσημο μαθηματικό, τη δεκαετία του 1930.
Το σύστημα αποτελείται από την κατασκευή μελών λάμδα και την εκτέλεση εργασιών μείωσης σε αυτά.
Επεξηγήσεις και Εφαρμογές
Το ελληνικό γράμμα λάμδα (λ) χρησιμοποιείται σε εκφράσεις λάμδα και όρους λάμδα για να υποδηλώσει τη σύνδεση μιας μεταβλητής σε μια συνάρτηση.
Ο λογισμός λάμδα μπορεί να είναι μη πληκτρολογημένος ή πληκτρολογημένος. Στην πρώτη παραλλαγή, οι συναρτήσεις μπορούν να χρησιμοποιηθούν μόνο εάν είναι σε θέση να λαμβάνουν δεδομένα αυτού του τύπου. Οι πληκτρολογημένοι λίθοι λάμδα είναι πιο αδύναμοι, μπορούν να εκφράσουν μικρότερη τιμή. Αλλά, από την άλλη, σου επιτρέπουν να αποδείξεις περισσότερα πράγματα.
Ένας λόγος που υπάρχουν τόσοι πολλοί διαφορετικοί τύποι είναι η επιθυμία των επιστημόνων να κάνουν περισσότερα χωρίς να εγκαταλείψουν την ευκαιρία να αποδείξουν ισχυρά θεωρήματα λογισμού λάμδα.
Το σύστημα έχει εφαρμογές σε πολλούς διαφορετικούς τομείς των μαθηματικών, της φιλοσοφίας, της γλωσσολογίας και της επιστήμης των υπολογιστών. Πρώτα απ 'όλα, ο λογισμός λάμδα είναι ένας λογισμός που έπαιξε σημαντικό ρόλο στην ανάπτυξη της θεωρίας των γλωσσών προγραμματισμού. Είναι τα στυλ λειτουργικής δημιουργίας που εφαρμόζουν τα συστήματα. Αποτελούν επίσης ένα καυτό θέμα έρευνας στη θεωρία αυτών των κατηγοριών.
Για ανδρείκελα
Ο λογισμός λάμδα εισήχθη από τον μαθηματικό Alonzo Church τη δεκαετία του 1930 ως μέρος της έρευνάς του στα θεμέλια της επιστήμης. Το αρχικό σύστημα αποδείχθηκε ότι ήταν λογικά ασυνεπές το 1935 όταν οι Stephen Kleen και J. B. Rosser ανέπτυξαν το παράδοξο Kleene-Rosser.
Αργότερα, το 1936, ο Church ξεχώρισε και δημοσίευσε μόνο το μέρος που σχετίζεται με τους υπολογισμούς, αυτό που σήμερα ονομάζεται άτυπος λογισμός λάμδα. Το 1940 εισήγαγε επίσης μια πιο αδύναμη αλλά λογικά συνεπή θεωρία γνωστή ως σύστημα πρώτων τύπων. Στο έργο του, εξηγεί ολόκληρη τη θεωρία με απλά λόγια, επομένως μπορεί να ειπωθεί ότι ο Church δημοσίευσε τον λογισμό λάμδα για τα ανδρείκελα.
Μέχρι τη δεκαετία του 1960, όταν η σχέση του με τις γλώσσες προγραμματισμού έγινε ξεκάθαρη, το λ ήταν απλώς ένας φορμαλισμός. Χάρη στις εφαρμογές του Richard Montagu και άλλων γλωσσολόγων στη σημασιολογία της φυσικής γλώσσας, ο λογισμός έχει πάρει υπερήφανη θέση τόσο στη γλωσσολογία όσο και στην επιστήμη των υπολογιστών.
Προέλευση του συμβόλου
Το Λάμδα δεν σημαίνει λέξη ή αρκτικόλεξο, προέρχεται από μια αναφορά στα Κύρια Μαθηματικά του Russell ακολουθούμενη από δύο τυπογραφικές αλλαγές. Παράδειγμα σημειογραφίας: για μια συνάρτηση f με f (y)=2y + 1 είναι 2ŷ + 1. Και εδώ χρησιμοποιούμε ένα καρέ («καπέλο») πάνω από το y για να επισημάνουμε τη μεταβλητή εισόδου.
Η εκκλησία αρχικά σκόπευε να χρησιμοποιήσει παρόμοια σύμβολα, αλλά οι στοιχειοθέτες δεν μπόρεσαν να τοποθετήσουν το σύμβολο "καπέλο" πάνω από τα γράμματα. Αντίθετα, το τύπωσαν αρχικά ως "/\y.2y+1". Στο επόμενο επεισόδιο επεξεργασίας, οι δακτυλογράφοι αντικατέστησαν το "/ \" με έναν οπτικά παρόμοιο χαρακτήρα.
Εισαγωγή στον λογισμό λάμδα
Το σύστημα αποτελείται από μια γλώσσα όρων, οι οποίοι επιλέγονται από μια ορισμένη επίσημη σύνταξη, και ένα σύνολο κανόνων μετασχηματισμού που επιτρέπουν τον χειρισμό τους. Το τελευταίο σημείο μπορεί να θεωρηθεί ως θεωρία εξισώσεων ή ως λειτουργικός ορισμός.
Όλες οι συναρτήσεις στον λογισμό λάμδα είναι ανώνυμες, που σημαίνει ότι δεν έχουν ονόματα. Λαμβάνουν μόνο μία μεταβλητή εισόδου και το currying χρησιμοποιείται για την υλοποίηση γραφικών με πολλές μεταβλητές.
Όροι λάμδα
Η σύνταξη του λογισμού ορίζει ορισμένες εκφράσεις ως έγκυρες και άλλες ως μη έγκυρες. Ακριβώς όπως διαφορετικές σειρές χαρακτήρων είναι έγκυρα προγράμματα C και μερικά όχι. Η πραγματική έκφραση του λογισμού λάμδα ονομάζεται "όρος λάμδα".
Οι ακόλουθοι τρεις κανόνες παρέχουν έναν επαγωγικό ορισμό που μπορεί να είναιισχύει για την κατασκευή όλων των συντακτικά έγκυρων εννοιών:
Η ίδια η μεταβλητή x είναι έγκυρος όρος λάμδα:
- αν το T είναι LT και το x είναι μη σταθερό, τότε το (λάμδα xt) ονομάζεται αφαίρεση.
- αν το T καθώς και το s είναι έννοιες, τότε το (TS) ονομάζεται εφαρμογή.
Τίποτα άλλο δεν είναι όρος λάμδα. Έτσι, μια έννοια είναι έγκυρη εάν και μόνο εάν μπορεί να αποκτηθεί με επαναλαμβανόμενη εφαρμογή αυτών των τριών κανόνων. Ωστόσο, ορισμένες αγκύλες ενδέχεται να παραληφθούν σύμφωνα με άλλα κριτήρια.
Ορισμός
Οι εκφράσεις λάμδα αποτελούνται από:
- variables v 1, v 2, …, v n, …
- σύμβολα αφαίρεσης 'λ' και τελείας '.'
- αγκύλες ().
Το σύνολο Λ μπορεί να οριστεί επαγωγικά:
- Αν το x είναι μεταβλητή, τότε x ∈ Λ;
- Το x δεν είναι σταθερό και το M ∈ Λ, τότε (λx. M) ∈ Λ;
- M, N ∈ Λ, στη συνέχεια (MN) ∈ Λ.
Ονομασία
Για να διατηρηθεί η σημείωση των εκφράσεων λάμδα, χρησιμοποιούνται συνήθως οι ακόλουθες συμβάσεις:
- Εξωτερικές αγκύλες παραλείφθηκαν: MN αντί για (MN).
- Οι εφαρμογές θεωρείται ότι παραμένουν συσχετιστικές: μπορεί κανείς να γράψει MNP αντί για ((MN) P).
- Το σώμα της αφαίρεσης εκτείνεται πιο δεξιά: λx. MN σημαίνει λx. (MN), όχι (λx. M) N.
- Η ακολουθία των αφαιρέσεων μειώνεται: λx.λy.λz. N μπορεί να είναι λxyz. N.
Ελεύθερες και δεσμευμένες μεταβλητές
Ο τελεστής λ συνδέει τη μη σταθερά του όπου κι αν βρίσκεται στο σώμα της αφαίρεσης. Οι μεταβλητές που εμπίπτουν στο πεδίο εφαρμογής ονομάζονται δεσμευμένες. Στην έκφραση λ x. M, το τμήμα λ x αναφέρεται συχνά ως συνδετικό υλικό. Σαν να υπαινίσσεται ότι οι μεταβλητές γίνονται μια ομάδα με την προσθήκη του X x στο M. Όλες οι άλλες ασταθείς ονομάζονται ελεύθερες.
Για παράδειγμα, στην έκφραση λ y. x x y, y - δεσμευμένο μη μόνιμο και x - δωρεάν. Και αξίζει επίσης να σημειωθεί ότι η μεταβλητή ομαδοποιείται με βάση την "πλησιέστερη" αφαίρεση της. Στο ακόλουθο παράδειγμα, η λύση του λογισμού λάμδα αντιπροσωπεύεται από μια μοναδική εμφάνιση του x, η οποία σχετίζεται με τον δεύτερο όρο:
λ x. y (λ x. z x)
Το σύνολο των ελεύθερων μεταβλητών M συμβολίζεται ως FV (M) και ορίζεται με αναδρομή στη δομή των όρων ως εξής:
- FV (x)={x}, όπου x είναι μια μεταβλητή.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Ένας τύπος που δεν περιέχει ελεύθερες μεταβλητές ονομάζεται κλειστός. Οι κλειστές εκφράσεις λάμδα είναι επίσης γνωστές ως συνδυαστές και είναι ισοδύναμοι με όρους στη συνδυαστική λογική.
Συντομογραφία
Η σημασία των εκφράσεων λάμδα καθορίζεται από το πώς μπορούν να συντομευθούν.
Υπάρχουν τρεις τύποι περικοπών:
- α-μετατροπή: αλλαγή δεσμευμένων μεταβλητών (άλφα).
- β-αναγωγή: εφαρμογή συναρτήσεων στα ορίσματά τους (beta).
- η-transform: καλύπτει την έννοια της επέκτασης.
Εδώ είναι επίσηςΜιλάμε για τις ισοδυναμίες που προκύπτουν: δύο εκφράσεις είναι β-ισοδύναμες αν μπορούν να β-μετασχηματιστούν στην ίδια συνιστώσα και η α / η-ισοδυναμία ορίζεται παρόμοια.
Ο όρος redex, συντομογραφία του μειωμένου κύκλου εργασιών, αναφέρεται σε υποθέματα που μπορούν να μειωθούν με έναν από τους κανόνες. Λογισμός λάμδα για ανδρείκελα, παραδείγματα:
(λ x. M) Το N είναι μια beta redex στην έκφραση για την αντικατάσταση του N με x στο M. Η συνιστώσα στην οποία μειώνεται μια redex ονομάζεται αναγωγή της. Η αναγωγή (λ x. M) N είναι M [x:=N].
Αν το x δεν είναι ελεύθερο στο M, λ x. M x επίσης em-REDEX με ρυθμιστή M.
α-μετασχηματισμός
Οι μετονομασίες Alpha σάς επιτρέπουν να αλλάξετε τα ονόματα των δεσμευμένων μεταβλητών. Για παράδειγμα, x. Το x μπορεί να δώσει λ y. y. Οι όροι που διαφέρουν μόνο στον άλφα μετασχηματισμό λέγονται α-ισοδύναμοι. Συχνά, όταν χρησιμοποιείται ο λογισμός λάμδα, τα α-ισοδύναμα θεωρούνται αμοιβαία.
Οι ακριβείς κανόνες για τη μετατροπή άλφα δεν είναι εντελώς ασήμαντοι. Πρώτον, με αυτήν την αφαίρεση, μετονομάζονται μόνο εκείνες οι μεταβλητές που σχετίζονται με το ίδιο σύστημα. Για παράδειγμα, ο μετασχηματισμός άλφα λ x.λ x. Το x μπορεί να οδηγήσει σε λ y.λ x. x, αλλά αυτό μπορεί να μην οδηγεί σε λy.λx.y Το τελευταίο έχει διαφορετική σημασία από το πρωτότυπο. Αυτό είναι ανάλογο με την έννοια του προγραμματισμού μεταβλητής σκίασης.
Δεύτερον, ένας μετασχηματισμός άλφα δεν είναι δυνατός εάν θα είχε ως αποτέλεσμα να συλληφθεί από μια μη μόνιμη άλλη αφαίρεση. Για παράδειγμα, αν αντικαταστήσετε το x με το y στο λ x.λ y. x, τότε μπορείτε να πάρετελy.λy. u, που δεν είναι καθόλου το ίδιο.
Σε γλώσσες προγραμματισμού με στατικό εύρος, η μετατροπή άλφα μπορεί να χρησιμοποιηθεί για την απλοποίηση της ανάλυσης ονόματος. Ταυτόχρονα, φροντίζοντας ώστε η έννοια της μεταβλητής να μην καλύπτει τον προσδιορισμό στην περιοχή που περιέχει.
Στο συμβολισμό ευρετηρίου De Bruyne, οποιοιδήποτε δύο όροι ισοδύναμοι με άλφα είναι συντακτικά πανομοιότυποι.
Αντικατάσταση
Οι αλλαγές που γράφτηκαν από το E [V:=R] είναι η διαδικασία αντικατάστασης όλων των ελεύθερων εμφανίσεων της μεταβλητής V στην έκφραση Ε με τον κύκλο εργασιών R. Η υποκατάσταση ως προς το λ ορίζεται από το λάμδα της αναδρομής λογισμός στη δομή της έννοιας ως εξής (σημείωση: x και y - μόνο μεταβλητές, και M και N - οποιαδήποτε λ-έκφραση).
x [x:=N] ≡ N
y [x:=N] ≡ y εάν x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) εάν x ≠ y, με την προϋπόθεση ότι y ∉ FV (N).
Για αντικατάσταση σε αφαίρεση λάμδα, μερικές φορές είναι απαραίτητο να α-μετασχηματιστεί μια έκφραση. Για παράδειγμα, δεν είναι αλήθεια ότι το (λ x. Y) [y:=x] έχει ως αποτέλεσμα (λ x. X) επειδή το x που αντικατέστησε θα έπρεπε να ήταν ελεύθερο, αλλά κατέληξε να είναι δεσμευμένο. Η σωστή αντικατάσταση σε αυτή την περίπτωση είναι (λ z. X) μέχρι α-ισοδυναμίας. Σημειώστε ότι η αντικατάσταση ορίζεται μοναδικά μέχρι το λάμδα.
β-μείωση
Η μείωση beta αντανακλά την ιδέα της εφαρμογής μιας συνάρτησης. Το βήτα-αναγωγικό ορίζεται με όρουςαντικατάσταση: ((X V. E) E ') είναι E [V:=E'].
Για παράδειγμα, υποθέτοντας κάποια κωδικοποίηση 2, 7, ×, υπάρχει η ακόλουθη β-αναγωγή: ((λ n. N × 2) 7) → 7 × 2.
Η Η μείωση βήτα μπορεί να θεωρηθεί ως η ίδια με την έννοια της τοπικής αναγωγιμότητας υπό φυσική έκπτωση μέσω του ισομορφισμού Curry-Howard.
η-transform
Αυτή η μετατροπή εκφράζει την ιδέα της επέκτασης, η οποία σε αυτό το πλαίσιο είναι ότι δύο συναρτήσεις είναι ίσες όταν δίνουν το ίδιο αποτέλεσμα για όλα τα ορίσματα. Αυτή η μετατροπή ανταλλάσσεται μεταξύ λ x. (F x) και f όποτε το x δεν φαίνεται ελεύθερο στο f.
Αυτή η ενέργεια μπορεί να θεωρηθεί ίδια με την έννοια της τοπικής πληρότητας στη φυσική έκπτωση μέσω του ισομορφισμού Curry-Howard.
Κανονικές μορφές και σύντηξη
Για έναν μη τυποποιημένο λογισμό λάμδα, ο κανόνας της β-αναγωγής δεν είναι γενικά ούτε ισχυρός ούτε ασθενής κανονικοποιητικός.
Ωστόσο, μπορεί να αποδειχθεί ότι η β-αναγωγή συγχωνεύεται όταν τρέχει πριν από τον α-μετασχηματισμό (δηλαδή, δύο κανονικές μορφές μπορούν να θεωρηθούν ίσες εάν είναι δυνατός ένας μετασχηματισμός α από τη μία στην άλλη).
Ως εκ τούτου, τόσο οι ισχυροί κανονικοποιούμενοι όροι όσο και οι ασθενώς προσαρμοζόμενοι όροι έχουν μια ενιαία κανονική μορφή. Για τους πρώτους όρους, οποιαδήποτε στρατηγική μείωσης είναι εγγυημένο ότι θα οδηγήσει σε μια τυπική διαμόρφωση. Ενώ για συνθήκες ασθενούς ομαλοποίησης, ορισμένες στρατηγικές μείωσης μπορεί να μην το βρουν.
Πρόσθετες μέθοδοι προγραμματισμού
Υπάρχουν πολλά ιδιώματα δημιουργίας για τον λογισμό λάμδα. Πολλά από αυτά αναπτύχθηκαν αρχικά στο πλαίσιο της χρήσης συστημάτων ως βάσης για τη σημασιολογία μιας γλώσσας προγραμματισμού, εφαρμόζοντάς τα αποτελεσματικά ως κατασκευή χαμηλού επιπέδου. Δεδομένου ότι ορισμένα στυλ περιλαμβάνουν έναν λογισμό λάμδα (ή κάτι πολύ παρόμοιο) ως απόσπασμα, αυτές οι τεχνικές βρίσκουν επίσης χρήση στην πρακτική δημιουργία, αλλά μπορεί στη συνέχεια να εκληφθούν ως ασαφείς ή ξένοι.
Ονομασμένες σταθερές
Στον λογισμό λάμδα, μια βιβλιοθήκη παίρνει τη μορφή ενός συνόλου προκαθορισμένων συναρτήσεων, όπου οι όροι είναι απλώς συγκεκριμένες σταθερές. Ο καθαρός λογισμός δεν έχει την έννοια των ονομασμένων αμετάβλητων αφού όλοι οι ατομικοί όροι λάμδα είναι μεταβλητοί. Αλλά μπορούν επίσης να μιμηθούν παίρνοντας το μεταβλητό ως όνομα της σταθεράς, χρησιμοποιώντας μια αφαίρεση λάμδα για να δεσμεύσουμε αυτό το πτητικό στο σώμα και εφαρμόζοντας αυτήν την αφαίρεση στον επιδιωκόμενο ορισμό. Έτσι, αν χρησιμοποιείτε το f για να αναπαραστήσετε το M στο Ν, θα μπορούσατε να πείτε
(λ στ. N) M.
Οι συγγραφείς συχνά εισάγουν μια συντακτική έννοια, όπως αφήστε για να επιτρέψετε στα πράγματα να γράφονται με πιο διαισθητικό τρόπο.
f=M έως N
Με την αλυσίδα τέτοιων ορισμών, μπορεί κανείς να γράψει ένα "πρόγραμμα" λογισμού λάμδα ως μηδενικούς ή περισσότερους ορισμούς συναρτήσεων ακολουθούμενο από ένα μεμονωμένο μέλος λάμδα, χρησιμοποιώντας εκείνους τους ορισμούς που αποτελούν το μεγαλύτερο μέρος του προγράμματος.
Ένας αξιοσημείωτος περιορισμός αυτού είναι ότι το όνομα f δεν ορίζεται στο M,αφού το M είναι έξω από το δεσμευτικό πεδίο της αφαίρεσης λάμδα f. Αυτό σημαίνει ότι ένα χαρακτηριστικό αναδρομικής συνάρτησης δεν μπορεί να χρησιμοποιηθεί ως M με let. Η πιο προηγμένη σύνταξη letrec, η οποία σας επιτρέπει να γράφετε αναδρομικούς ορισμούς συναρτήσεων σε αυτό το στυλ, χρησιμοποιεί επιπλέον συνδυαστές σταθερού σημείου.
Τυπωμένα ανάλογα
Αυτός ο τύπος είναι ένας τυποποιημένος φορμαλισμός που χρησιμοποιεί ένα σύμβολο για να αναπαραστήσει μια ανώνυμη αφαίρεση συνάρτησης. Σε αυτό το πλαίσιο, οι τύποι είναι συνήθως αντικείμενα συντακτικής φύσης που αποδίδονται σε όρους λάμδα. Η ακριβής φύση εξαρτάται από τον εν λόγω λογισμό. Από μια ορισμένη άποψη, το τυποποιημένο LI μπορεί να θεωρηθεί ως βελτιώσεις του μη τυποποιημένου LI. Αλλά από την άλλη πλευρά, μπορούν επίσης να θεωρηθούν μια πιο θεμελιώδη θεωρία, και ο άτυπος λογισμός λάμδα είναι μια ειδική περίπτωση με έναν μόνο τύπο.
Το Typed LI είναι το θεμέλιο των γλωσσών προγραμματισμού και η ραχοκοκαλιά λειτουργικών γλωσσών όπως η ML και η Haskell. Και, πιο έμμεσα, επιτακτικά στυλ δημιουργίας. Οι δακτυλογραφημένοι υπολογισμοί λάμδα παίζουν σημαντικό ρόλο στην ανάπτυξη συστημάτων τύπων για γλώσσες προγραμματισμού. Εδώ, η δυνατότητα πληκτρολόγησης συνήθως καταγράφει τις επιθυμητές ιδιότητες του προγράμματος, για παράδειγμα, δεν προκαλεί παραβίαση πρόσβασης στη μνήμη.
Οι υπολογισμοί λάμδα συνδέονται στενά με τη μαθηματική λογική και τη θεωρία αποδείξεων μέσω του ισομορφισμού Curry–Howard και μπορούν να θεωρηθούν ως εσωτερική γλώσσα των κατηγοριών, για παράδειγμα, η οποίααπλά είναι το στυλ των καρτεσιανών κλεισίματος.
