Lambda-Kalkül ist ein formales System in der mathematischen Logik zum Ausdrücken abstraktionsbasierter Berechnungen und Anwenden von Funktionen unter Verwendung von Bindung und Variablensubstitution. Dies ist ein universelles Modell, das auf das Design jeder Turing-Maschine angewendet werden kann. Der Lambda-Kalkül wurde erstmals in den 1930er Jahren von Church, einem berühmten Mathematiker, eingeführt.
Das System besteht aus dem Erstellen von Lambda-Mitgliedern und der Durchführung von Reduktionsoperationen an ihnen.
Erklärungen und Anwendungen
Der griechische Buchstabe Lambda (λ) wird in Lambda-Ausdrücken und Lambda-Begriffen verwendet, um die Bindung einer Variablen in einer Funktion zu bezeichnen.
Der Lambda-Kalkül kann untypisiert oder typisiert sein. Bei der ersten Variante können Funktionen nur verwendet werden, wenn sie in der Lage sind, Daten dieses Typs zu empfangen. Typisierte Lambda-Kalküle sind schwächer, können einen kleineren Wert ausdrücken. Aber andererseits erlauben sie dir, mehr Dinge zu beweisen.
Ein Grund dafür, dass es so viele verschiedene Typen gibt, ist der Wunsch von Wissenschaftlern, mehr zu tun, ohne die Möglichkeit aufzugeben, starke Lambda-Kalkül-Theoreme zu beweisen.
Das System findet Anwendung in vielen verschiedenen Bereichen der Mathematik, Philosophie, Linguistik und Informatik. Zunächst einmal ist der Lambda-Kalkül ein Kalkül, der eine wichtige Rolle bei der Entwicklung der Theorie der Programmiersprachen gespielt hat. Es sind die Stile der funktionalen Erstellung, die Systeme implementieren. Sie sind auch ein heißes Forschungsthema in der Theorie dieser Kategorien.
Für Dummies
Der Lambda-Kalkül wurde von dem Mathematiker Alonzo Church in den 1930er Jahren im Rahmen seiner Grundlagenforschung eingeführt. Das ursprüngliche System erwies sich 1935 als logisch inkonsistent, als Stephen Kleen und J. B. Rosser das Kleene-Rosser-Paradoxon entwickelten.
Später, im Jahr 1936, hat Church nur den Teil herausgegriffen und veröffentlicht, der für Berechnungen relevant ist, was heute als untypisierter Lambda-Kalkül bezeichnet wird. 1940 führte er auch eine schwächere, aber logisch konsistente Theorie ein, die als Primzahlensystem bekannt ist. In seiner Arbeit erklärt er die ganze Theorie in einfachen Worten, so dass man sagen kann, dass Church den Kalkül Lambda für Dummies veröffentlicht hat.
Bis in die 1960er Jahre, als seine Beziehung zu Programmiersprachen klar wurde, war λ nur ein Formalismus. Dank der Anwendungen von Richard Montagu und anderen Linguisten in der Semantik der natürlichen Sprache hat die Infinitesimalrechnung sowohl in der Linguistik als auch in der Informatik einen Ehrenplatz eingenommen.
Ursprung des Symbols
Lambda steht nicht für ein Wort oder Akronym, es kommt von einer Referenz in Russells Hauptmathematik, gefolgt von zwei typografischen Änderungen. Notationsbeispiel: für eine Funktion f mit f (y)=2y + 1 ist 2ŷ + 1. Und hier verwenden wir ein Caret („Hut“) über y, um die Eingabevariable zu beschriften.
Die Kirche beabsichtigte ursprünglich, ähnliche Symbole zu verwenden, aber die Schriftsetzer waren nicht in der Lage, das "Hut"-Symbol über den Buchstaben zu platzieren. Stattdessen druckten sie es ursprünglich als "/\y.2y+1". In der nächsten Folge der Bearbeitung ersetzten Schreibkräfte „/ \“durch ein optisch ähnliches Zeichen.
Einführung in die Lambda-Kalküle
Das System besteht aus einer Sprache von Begriffen, die durch eine bestimmte formale Syntax ausgewählt werden, und einem Satz von Transformationsregeln, die es erlauben, sie zu manipulieren. Der letzte Punkt kann als Gleichungstheorie oder als operationale Definition betrachtet werden.
Alle Funktionen im Lambda-Kalkül sind anonym, dh sie haben keine Namen. Sie nehmen nur eine Eingabevariable und Currying wird verwendet, um Diagramme mit mehreren Variablen zu implementieren.
Lambda-Terme
Die Analysis-Syntax definiert einige Ausdrücke als gültig und andere als ungültig. Genauso wie verschiedene Zeichenfolgen gültige C-Programme sind und manche nicht. Der eigentliche Ausdruck des Lambda-Kalküls wird "Lambda-Term" genannt.
Die folgenden drei Regeln liefern eine induktive Definition, die sein kanngelten für die Konstruktion aller syntaktisch gültigen Konzepte:
Die x-Variable selbst ist ein gültiger Lambda-Term:
- wenn T LT und x nicht konstant ist, dann heißt (lambda xt) eine Abstraktion.
- wenn sowohl T als auch s Konzepte sind, dann heißt (TS) eine Anwendung.
Nichts anderes ist ein Lambda-Term. Ein Konzept ist also genau dann gültig, wenn es durch wiederholte Anwendung dieser drei Regeln gewonnen werden kann. Einige Klammern können jedoch nach anderen Kriterien weggelassen werden.
Definition
Lambda-Ausdrücke bestehen aus:
- Variablen v 1, v 2, …, v n, …
- Abstraktionszeichen 'λ' und Punkt '.'
- Klammern ().
Die Menge Λ kann induktiv definiert werden:
- Wenn x eine Variable ist, dann ist x ∈ Λ;
- x nicht konstant und M ∈ Λ, dann (λx. M) ∈ Λ;
- M, N ∈ Λ, dann (MN) ∈ Λ.
Bezeichnung
Um die Schreibweise von Lambda-Ausdrücken übersichtlich zu h alten, werden üblicherweise die folgenden Konventionen verwendet:
- Äußere Klammern weggelassen: MN statt (MN).
- Anwendungen bleiben assoziativ: man kann MNP statt ((MN) P) schreiben.
- Der Abstraktionskörper erstreckt sich weiter nach rechts: λx. MN bedeutet λx. (MN), nicht (λx. M) N.
- Die Folge der Abstraktionen wird reduziert: λx.λy.λz. N kann λxyz. N sein.
Freie und gebundene Variablen
Der Operator λ verbindet seine Nichtkonstante, wo immer sie sich im Abstraktionskörper befindet. Variablen, die in den Geltungsbereich fallen, werden als gebunden bezeichnet. Im Ausdruck λ x. M, der λ x -Teil wird oft als Binder bezeichnet. Als wolle man andeuten, dass die Variablen durch die Addition von X x zu M zu einer Gruppe werden. Alle anderen instabilen werden als frei bezeichnet.
Zum Beispiel im Ausdruck λ y. x x y, y - gebunden nicht permanent und x - frei. Und es ist auch erwähnenswert, dass die Variable nach ihrer "nächstgelegenen" Abstraktion gruppiert ist. Im folgenden Beispiel wird die Lösung des Lambda-Kalküls durch ein einzelnes Vorkommen von x dargestellt, das sich auf den zweiten Term bezieht:
λ x. y (λ x. z x)
Die Menge der freien Variablen M wird als FV (M) bezeichnet und ist durch Rekursion über die Termstruktur wie folgt definiert:
- FV (x)={x}, wobei x eine Variable ist.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Eine Formel, die keine freien Variablen enthält, heißt geschlossen. Geschlossene Lambda-Ausdrücke werden auch als Kombinatoren bezeichnet und sind äquivalent zu Begriffen in der kombinatorischen Logik.
Abkürzung
Die Bedeutung von Lambda-Ausdrücken wird dadurch bestimmt, wie sie verkürzt werden können.
Es gibt drei Arten von Schnitten:
- α-Transformation: Gebundene Variablen ändern (Alpha).
- β-Reduktion: Anwenden von Funktionen auf ihre Argumente (Beta).
- η-transform: deckt den Begriff der Extensionalität ab.
Hier ist es auchwir sprechen von den resultierenden Äquivalenzen: Zwei Ausdrücke sind β-äquivalent, wenn sie in dieselbe Komponente β-transformiert werden können, und α / η-Äquivalenz ist ähnlich definiert.
Der Begriff Redex, kurz für reduzierbarer Umsatz, bezieht sich auf Unterthemen, die durch eine der Regeln reduziert werden können. Lambda-Kalkül für Dummies, Beispiele:
(λ x. M) N ist ein Beta-Redex im Ausdruck zum Ersetzen von N durch x in M. Die Komponente, auf die ein Redex reduziert wird, heißt sein Redukt. Die Reduktion (λ x. M) N ist M [x:=N].
Wenn x in M nicht frei ist, ist λ x. M x auch em-REDEX mit Regler M.
α-Umwandlung
Alpha-Umbenennungen erlauben Ihnen, die Namen gebundener Variablen zu ändern. Zum Beispiel x. x kann λ y ergeben. j. Terme, die sich nur in der Alpha-Transformation unterscheiden, werden als α-äquivalent bezeichnet. Bei der Verwendung des Lambda-Kalküls werden α-Äquivalente häufig als reziprok betrachtet.
Die genauen Regeln für die Alpha-Konvertierung sind nicht ganz trivial. Erstens werden bei dieser Abstraktion nur diejenigen Variablen umbenannt, die demselben System zugeordnet sind. Beispielsweise die Alpha-Transformation λ x.λ x. x kann zu λ y.λ x führen. x, aber das darf nicht zu λy.λx.y führen. Letzteres hat eine andere Bedeutung als das Original. Dies ist analog zum Konzept der variablen Shadowing-Programmierung.
Zweitens ist eine Alpha-Transformation nicht möglich, wenn sie dazu führen würde, dass sie von einer nicht-permanenten anderen Abstraktion erfasst wird. Zum Beispiel, wenn Sie in λ x.λ y x durch y ersetzen. x, dann können Sie bekommenλy.λy. u, was überhaupt nicht dasselbe ist.
In Programmiersprachen mit statischem Gültigkeitsbereich kann die Alpha-Konvertierung verwendet werden, um die Namensauflösung zu vereinfachen. Dabei ist darauf zu achten, dass der Begriff einer Variablen nicht die Bezeichnung im umgebenden Bereich verdeckt.
In der Indexnotation von De Bruyne sind zwei beliebige alphaäquivalente Begriffe syntaktisch identisch.
Ersatz
Die durch E [V:=R] geschriebenen Änderungen sind der Vorgang des Ersetzens aller freien Vorkommen der Variablen V im Ausdruck E durch den Umsatz R. Die Substitution in Bezug auf λ wird durch das Lambda der Rekursion definiert Kalkül auf der Konzeptstruktur wie folgt (Anmerkung: x und y - nur Variablen, und M und N - irgendein λ-Ausdruck).
x [x:=N] ≡ N
y [x:=N] ≡ y wenn 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]) falls x ≠ y, sofern y ∉ FV (N).
Für die Substitution in eine Lambda-Abstraktion ist es manchmal notwendig, einen Ausdruck zu α-transformieren. Zum Beispiel ist es nicht wahr, dass (λ x. Y) [y:=x] zu (λ x. X) führt, weil das ersetzte x frei hätte sein sollen, aber am Ende gebunden war. Die korrekte Ersetzung ist in diesem Fall (λ z. X) bis auf α-Äquivalenz. Beachten Sie, dass die Substitution bis zu Lambda eindeutig definiert ist.
β-Reduktion
Beta-Reduktion spiegelt die Idee wider, eine Funktion anzuwenden. Beta-reduktiv ist in Begriffen definiertSubstitution: ((X V. E) E ') ist E [V:=E'].
Wenn man zum Beispiel eine Codierung 2, 7, × annimmt, gibt es die folgende β-Reduktion: ((λ n. N × 2) 7) → 7 × 2.
Beta-Reduktion kann als dasselbe angesehen werden wie das Konzept der lokalen Reduzierbarkeit unter natürlicher Deduktion über den Curry-Howard-Isomorphismus.
η-transformieren
Diese Umwandlung drückt die Idee der Extensionalität aus, was in diesem Zusammenhang bedeutet, dass zwei Funktionen gleich sind, wenn sie für alle Argumente das gleiche Ergebnis liefern. Diese Umwandlung tauscht zwischen λ x aus. (F x) und f, wenn x in f nicht frei erscheint.
Diese Aktion kann als dasselbe betrachtet werden wie das Konzept der lokalen Vollständigkeit in der natürlichen Deduktion durch den Curry-Howard-Isomorphismus.
Normalformen und Fusion
Für einen untypisierten Lambda-Kalkül ist die β-Reduktionsregel im Allgemeinen weder stark noch schwach normalisierend.
Dennoch kann gezeigt werden, dass die β-Reduktion verschmilzt, wenn sie vor der α-Transformation läuft (d.h. zwei Normalformen können als gleich angesehen werden, wenn eine α-Transformation von einer in die andere möglich ist).
Daher haben sowohl stark normalisierende Terme als auch schwach anpassende Terme eine einzige Normalform. Für die ersten Terme führt jede Reduktionsstrategie garantiert zu einer typischen Konfiguration. Während bei schwach normalisierenden Bedingungen einige Reduktionsstrategien es möglicherweise nicht finden.
Zusätzliche Programmiermethoden
Es gibt viele schöpferische Redewendungen für den Lambda-Kalkül. Viele von ihnen wurden ursprünglich im Zusammenhang mit der Verwendung von Systemen als Grundlage für die Semantik einer Programmiersprache entwickelt und praktisch als Konstrukt auf niedriger Ebene angewendet. Da einige Stile einen Lambda-Kalkül (oder etwas sehr ähnliches) als Schnipsel enth alten, finden diese Techniken auch in der praktischen Erstellung Anwendung, können dann aber als obskur oder fremd wahrgenommen werden.
Benannte Konstanten
In der Lambda-Rechnung nimmt eine Bibliothek die Form einer Menge zuvor definierter Funktionen an, wobei die Terme nur konkrete Konstanten sind. Reine Kalküle haben kein Konzept von benannten Unveränderlichen, da alle atomaren Lambda-Terme Variablen sind. Sie können aber auch nachgeahmt werden, indem man das Veränderliche als Namen der Konstanten nimmt, eine Lambda-Abstraktion verwendet, um dieses Flüchtige im Körper zu binden, und diese Abstraktion auf die beabsichtigte Definition anwendet. Wenn Sie also f verwenden, um M in N darzustellen, könnten Siesagen
(λ f. N) M.
Autoren führen oft ein syntaktisches Konzept wie let ein, damit Dinge auf intuitivere Weise geschrieben werden können.
f=M bis N
Indem man solche Definitionen verkettet, kann man ein Lambda-Kalkül-"Programm" als null oder mehr Funktionsdefinitionen schreiben, gefolgt von einem einzelnen Lambda-Element, wobei man die Definitionen verwendet, die den Großteil des Programms ausmachen.
Eine bemerkenswerte Einschränkung dieses let ist, dass der Name f nicht in M definiert ist,da M außerhalb des Bindungsbereichs der Lambda-Abstraktion f liegt. Das bedeutet, dass ein rekursives Funktionsattribut nicht als M mit let verwendet werden kann. Die fortgeschrittenere letrec-Syntax, mit der Sie rekursive Funktionsdefinitionen in diesem Stil schreiben können, verwendet stattdessen stattdessen Festkomma-Kombinatoren.
Gedruckte Analoga
Dieser Typ ist ein typisierter Formalismus, der ein Symbol verwendet, um eine anonyme Funktionsabstraktion darzustellen. Typen sind dabei meist Objekte syntaktischer Natur, die Lambda-Termen zugeordnet sind. Die genaue Natur hängt von dem betreffenden Kalkül ab. Unter einem bestimmten Gesichtspunkt können typisierte LI als Verfeinerungen von untypisiertem LI betrachtet werden. Aber andererseits können sie auch als eine grundlegendere Theorie angesehen werden, und der untypisierte Lambda-Kalkül ist ein Spezialfall mit nur einem Typ.
Typed LI sind die Grundlage von Programmiersprachen und das Rückgrat funktionaler Sprachen wie ML und Haskell. Und, indirekter, imperative Gest altungsstile. Typisierte Lambda-Kalküle spielen eine wichtige Rolle bei der Entwicklung von Typsystemen für Programmiersprachen. Hier erfasst die Tippbarkeit normalerweise die gewünschten Eigenschaften des Programms, z. B. verursacht sie keine Speicherzugriffsverletzung.
Typisierte Lambda-Kalküle sind durch den Curry-Howard-Isomorphismus eng mit der mathematischen Logik und der Beweistheorie verwandt und können beispielsweise als interne Sprache von Kategorieklassen betrachtet werden, dieist einfach der Stil kartesischer Schließungen.
