Funktionale Programmierung - Lambda-Berechnung
Der Lambda-Kalkül ist ein Rahmen, der von der Alonzo-Kirche in den 1930er Jahren entwickelt wurde, um Berechnungen mit Funktionen zu untersuchen.
Function creation - Die Kirche führte die Notation ein λx.Eeine Funktion zu bezeichnen, in der 'x' ein formales Argument und 'E' der funktionale Körper ist. Diese Funktionen können ohne Namen und einzelne Argumente sein.
Function application - Church benutzte die Notation E1.E2 die Anwendung der Funktion zu bezeichnen E1 zum eigentlichen Argument E2. Und alle Funktionen basieren auf einem einzigen Argument.
Syntax der Lambda-Rechnung
Der Lamdba-Kalkül enthält drei verschiedene Arten von Ausdrücken, dh
E :: = x (Variablen)
| E 1 E 2 (Funktionsanwendung)
| λx.E (Funktionserstellung)
Wo λx.E heißt Lambda-Abstraktion und E ist als λ-Ausdrücke bekannt.
Bewertung der Lambda-Rechnung
Reine Lambda-Rechnung hat keine eingebauten Funktionen. Lassen Sie uns den folgenden Ausdruck bewerten -
(+ (* 5 6) (* 8 3))
Hier können wir nicht mit '+' beginnen, da es nur mit Zahlen arbeitet. Es gibt zwei reduzierbare Ausdrücke: (* 5 6) und (* 8 3).
Wir können beide zuerst reduzieren. Zum Beispiel -
(+ (* 5 6) (* 8 3))
(+ 30 (* 8 3))
(+ 30 24)
= 54
β-Reduktionsregel
Wir brauchen eine Reduktionsregel, um mit λs umgehen zu können
(λx . * 2 x) 4
(* 2 4)
= 8
Dies wird als β-Reduktion bezeichnet.
Der formale Parameter kann mehrmals verwendet werden -
(λx . + x x) 4
(+ 4 4)
= 8
Wenn es mehrere Begriffe gibt, können wir sie wie folgt behandeln:
(λx . (λx . + (− x 1)) x 3) 9
Das Innere x gehört zum Inneren λ und das äußere x gehört zum äußeren.
(λx . + (− x 1)) 9 3
+ (− 9 1) 3
+ 8 3
= 11
Freie und gebundene Variablen
In einem Ausdruck ist jedes Auftreten einer Variablen entweder "frei" (an λ) oder "gebunden" (an λ).
β-Reduktion von (λx . E) y ersetzt jeden x das kommt frei vor E mit y. Zum Beispiel -
Alpha-Reduktion
Die Alpha-Reduktion ist sehr einfach und kann durchgeführt werden, ohne die Bedeutung eines Lambda-Ausdrucks zu ändern.
λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)
Zum Beispiel -
(λx . (λx . + (− x 1)) x 3) 9
(λx . (λy . + (− y 1)) x 3) 9
(λy . + (− y 1)) 9 3
+ (− 9 1) 3
+ 8 3
11
Church-Rosser-Theorem
Der Church-Rosser-Satz besagt Folgendes:
Wenn E1 ↔ E2 ist, gibt es ein E, so dass E1 → E und E2 → E. „Eine Reduktion in irgendeiner Weise kann schließlich zu demselben Ergebnis führen.“
Wenn E1 → E2 und E2 Normalform ist, gibt es eine Reduktion normaler Ordnung von E1 auf E2. "Eine Reduzierung normaler Ordnung erzeugt immer eine normale Form, falls vorhanden."