Lambda-Kalkül

formale Sprache zur Untersuchung von Funktionen

Der Lambda-Kalkül ist eine formale Sprache zur Untersuchung von Funktionen. Er beschreibt die Definition von Funktionen und gebundenen Parametern und wurde in den 1930er Jahren von Alonzo Church und Stephen Cole Kleene eingeführt. Heute ist er ein wichtiges Konstrukt für die Theoretische Informatik, Logik höherer Stufe und Linguistik.

Als Symbol für den Lambda-Kalkül wird das kleine Lambda, der elfte Buchstabe des griechischen Alphabets, benutzt

Geschichte

Bearbeiten

Alonzo Church benutzte den Lambda-Kalkül, um 1936 sowohl eine negative Antwort auf das Entscheidungsproblem zu geben als auch eine Fundierung eines logischen Systems zu finden, wie es den Principia Mathematica von Bertrand Russell und Alfred North Whitehead zugrunde lag. Mittels des untypisierten Lambda-Kalküls kann man klar definieren, was eine berechenbare Funktion ist. Die Frage, ob zwei Lambda-Ausdrücke (s. u.) äquivalent sind, kann im Allgemeinen nicht algorithmisch entschieden werden. In seiner typisierten Form kann der Kalkül benutzt werden, um Logik höherer Stufe darzustellen. Der Lambda-Kalkül hat die Entwicklung funktionaler Programmiersprachen, die Forschung um Typsysteme von Programmiersprachen im Allgemeinen sowie moderne Teildisziplinen in der Logik wie die Typtheorie wesentlich beeinflusst.

Meilensteine der Entwicklung waren im Einzelnen:

  • Nach der Einführung die frühe Entdeckung, dass sich mit dem Lambda-Kalkül alles ausdrücken lässt, was man mit einer Turingmaschine ausdrücken kann. Anders formuliert: Im Sinne des Konzepts der Berechenbarkeit sind beide gleich mächtig.
  • Konrad Zuse hat Ideen aus dem Lambda-Kalkül 1942 bis 1946 in seinen Plankalkül einfließen lassen.
  • John McCarthy hat sie Ende der 1950er Jahre verwendet und damit die minimalen Funktionen der Programmiersprache Lisp definiert.
  • Die typisierten Varianten des Lambda-Kalküls führten zu modernen Programmiersprachen wie ML oder Haskell.
  • Als überaus fruchtbar erwies sich die Idee, Ausdrücke des typisierten Lambda-Kalküls zur Repräsentation von Termen einer Logik zugrunde zu legen, den Lambda-Kalkül also als Meta-Logik zu verwenden. Erstmals von Church 1940 in seiner Theory of Simple Types präsentiert, führte sie einerseits zu modernen Theorembeweisern für Logiken höherer Stufe und …
  • andererseits in den 1970er und 1980er Jahren zu Logiken mit immer mächtigeren Typsystemen, in denen sich z. B. logische Beweise an sich als Lambda-Ausdruck darstellen lassen.
  • In Anlehnung an den Lambda-Kalkül wurde für die Beschreibung nebenläufiger Prozesse der Pi-Kalkül von Robin Milner in den 1990er Jahren entwickelt.

Der untypisierte Lambda-Kalkül

Bearbeiten

Motivation

Bearbeiten

Ausgehend von einem mathematischen Term, wie beispielsweise  , lässt sich eine Funktion bilden, die   auf   abbildet. Man schreibt auch  . Beim Lambda-Kalkül geht es zunächst darum, solche Funktionsbildungen sprachlich zu formalisieren. Im Lambda-Kalkül würde man statt   den Term

  •  

schreiben. Man sagt, dass die freie Variable   durch λ-Abstraktion gebunden wird. Die Variablen-Bindung kommt in der Mathematik auch in anderen Bereichen vor:

  • Mengenlehre:  
  • Logik:   und  
  • Analysis:  

Die abstrahierte Variable muss nicht notwendigerweise im Term vorkommen, z. B.   . Dieser λ-Ausdruck bezeichnet dann die Funktion, die jedes   auf   abbildet. Etwas allgemeiner ist   die Funktion, die konstant   ist. Wird nachträglich noch nach   abstrahiert, so erhält man mit   eine Formalisierung der Funktion, die jedem Wert   die Funktion zuordnet, die konstant   ist. Der Ausdruck   repräsentiert also eine funktionswertige Funktion. Im Lambda-Kalkül lassen sich aber auch Funktionen ausdrücken, deren Argumente bereits Funktionen sind. Nimmt man bspw. die Funktion, die jeder Funktion   eine andere Funktion   zuordnet, die so entsteht, dass   zweimal angewandt wird, so wird   durch den λ-Term   dargestellt und die Zuordnung   durch  .

Da λ-Terme als Funktionen gesehen werden, kann man sie auf ein Argument anwenden. Man spricht von Applikation und schreibt im Lambda-Kalkül eher   statt  . Klammern können Terme gruppieren. Die Applikation als Verbindungsprinzip von Termen ist definitionsgemäß linksassoziativ, d. h.   bedeutet  . In der üblichen mathematischen Notation würde man hier   schreiben. Wendet man nun einen Lambda-Term   auf ein Argument   an, also  , so berechnet sich das Ergebnis dadurch, dass in dem Term   jedes Vorkommen der Variablen   durch   ersetzt wird. Diese Ableitungsregel nennt man β-Konversion.

λ-Terme formulieren eher allgemeine Prinzipien der Mathematik und bezeichnen nicht so sehr Objekte des üblichen mathematischen Universums. Beispielsweise formuliert   das Zuordnungsprinzip der identischen Abbildung, doch diese ist immer auf eine gegebene Menge als Definitionsmenge bezogen. Eine universelle Identität als Funktion ist in der mengentheoretischen Formulierung der Mathematik nicht definiert. Der Lambda-Kalkül im strengen Sinne ist daher eher als ein Neuentwurf der Mathematik zu sehen, in dem die Grundobjekte als universelle Funktionen verstanden werden, im Gegensatz zur axiomatischen Mengenlehre, deren Grundobjekte Mengen sind.

Zahlen und Terme wie   sind zunächst nicht Bestandteil eines reinen Lambda-Kalküls. Ähnlich wie in der Mengenlehre, in der man Zahlen und Arithmetik allein aus dem Mengenbegriff heraus konstruieren kann, ist es aber auch im Lambda-Kalkül möglich, auf der Basis von λ-Abstraktion und Applikation die Arithmetik zu definieren. Da im Lambda-Kalkül jeder Term als einstellige Funktion verstanden wird, muss eine Addition als die Funktion verstanden werden, die jeder Zahl   diejenige (einstellige) Funktion zuordnet, die zu jeder Zahl   den Wert   addiert (s. Currying).

Lambda-Terme ohne freie Variablen werden auch als Kombinatoren bezeichnet. Die Kombinatorische Logik (oder Kombinator-Kalkül) kann als alternativer Ansatz zum Lambda-Kalkül gesehen werden.

Formale Definition

Bearbeiten

In seiner einfachsten, dennoch vollständigen Form gibt es im Lambda-Kalkül drei Sorten von Termen, hier in Backus-Naur-Form:

Term ::= a (Variable) | (Term Term) (Applikation) | λa. Term (Abstraktion)

wobei   für ein beliebiges Symbol aus einer mindestens abzählbar-unendlichen Menge von Variablensymbolen (kurz: Variablen) steht. Für praktische Zwecke wird der Lambda-Kalkül üblicherweise noch um eine weitere Sorte von Termen, die Konstantensymbole, erweitert.

Die Menge der freien Variablen   kann induktiv über der Struktur eines λ-Terms   wie folgt definiert werden:

  1.  , falls der Term eine Variable   ist
  2.   für Applikationen, und
  3.  , falls der Term eine Abstraktion ist, sind seine freien Variablen die freien Variablen von   außer  .

Die Menge der gebundenen Variablen   eines Terms   errechnet sich auch induktiv:

  1.  , falls der Term eine Variable   ist
  2.   für Applikationen, und
  3.  , falls der Term eine Abstraktion ist, sind seine gebundenen Variablen die gebundenen Variablen von   vereinigt  .

Mittels der Definition von freien und gebundenen Variablen kann nun der Begriff der (freien) Variablensubstitution (Einsetzung) induktiv definiert werden durch:

  1.   falls Variable   ungleich  
  2.  
  3.  
  4.  
  5.   falls Variable   ungleich   und falls   disjunkt von  .

Hinweis:   steht für:  , in dem die freie Variable   durch   ersetzt wurde (falls   nicht in   vorhanden ist, wird auch nichts ersetzt).

Man beachte, dass die Substitution nur partiell definiert ist; ggf. müssen gebundene Variablen geeignet umbenannt werden (siehe α-Kongruenz im Folgenden), so dass niemals eine freie Variable in einem Substitut durch Einsetzung für eine Variable gebunden wird.

Über der Menge der λ-Terme können nun Kongruenzregeln (hier ≡ geschrieben) definiert werden, die die Intuition formal fassen, dass zwei Ausdrücke dieselbe Funktion beschreiben. Diese Relationen sind durch die sogenannte α-Konversion, die β-Konversion sowie die η-Konversion erfasst.

Kongruenzregeln

Bearbeiten

α-Konversion

Bearbeiten

Die α-Konversionsregel formalisiert die Idee, dass die Namen von gebundenen Variablen „Schall und Rauch“ sind; z. B. beschreiben   und   dieselbe Funktion. Allerdings sind die Details nicht ganz so einfach wie es zunächst erscheint: Eine Reihe von Einschränkungen müssen beachtet werden, wenn gebundene Variablen durch andere gebundene Variablen ersetzt werden.

Formal lautet die Regel wie folgt:

 

falls   in   nirgends frei vorkommt und   in   dort nicht gebunden ist, wo es ein   ersetzt. Da eine Kongruenzregel in jedem Teilterm anwendbar ist, erlaubt sie die Ableitung, dass   gleich   ist.

β-Konversion

Bearbeiten

Die β-Konversionsregel formalisiert das Konzept der „Funktionsanwendung“. Wird sie ausschließlich von links nach rechts angewandt, spricht man auch von β-Reduktion. Formal lässt sie sich durch

 

beschreiben, wobei alle freien Variablen in   in   frei bleiben müssen (siehe Nebenbedingung bei der Substitutionsdefinition).

Ein Term heißt in β-Normalform, wenn keine β-Reduktion mehr anwendbar ist (nicht für alle Terme existiert eine β-Normalform; siehe unten). Ein tiefes Resultat von Church und Rosser über den λ-Kalkül besagt, dass die Reihenfolgen von α-Konversionen und β-Reduktionen in gewissem Sinn keine Rolle spielt: wenn man einen Term zu zwei Termen   und   ableitet, gibt es immer eine Möglichkeit,   und   jeweils zu einem gemeinsamen Term   abzuleiten.

η-Konversion

Bearbeiten

Die η-Konversion kann optional zum Kalkül hinzugefügt werden. Sie formalisiert das Konzept der Extensionalität, d. h., dass zwei Funktionen genau dann gleich sind, wenn sie für alle Argumente dasselbe Resultat liefern. Formal ist die η-Konversion beschrieben durch:

 , wenn   nicht freie Variable von   ist.

Anmerkungen

Bearbeiten
  • Nicht für alle Terme existiert eine β-Normalform. Beispielsweise kann man auf den Term   zwar β-Reduktion anwenden, doch man erhält wieder den gleichen Term als Ergebnis zurück.
  • Jeder Term, der die Bedingung der β-Regel erfüllt, wird β-reduzibel genannt.
  • Die β-Reduktion ist im Allgemeinen nicht eindeutig; es kann mehrere Ansatzpunkte (sog. β-Redexe, von englisch reducible expression, reduzibler Ausdruck) für die Anwendung der β-Regel geben, weil die Regelanwendung in allen Teiltermen möglich ist.
  • Wenn mehrere Folgen von β-Reduktionen möglich sind und mehrere davon zu einem nicht-β-reduziblen Term führen, so sind diese Terme bis auf α-Kongruenz gleich.
  • Wenn jedoch eine Reihenfolge der β zu einem nicht-β-reduziblen Term (einem Ergebnis) führt, so tut dies auch die Standard Reduction Order, bei der das im Term erste Lambda zuerst verwendet wird.
  • In einer alternativen Notation werden die Variablennamen durch De-Bruijn-Indizes ersetzt. Diese Indizes entsprechen der Anzahl der Lambda-Terme zwischen der Variablen und ihrem bindenden Lambda-Ausdruck. Diese Darstellung wird oft in Computerprogrammen verwendet, da sie die α-Konversion obsolet macht und β-Reduktion deutlich vereinfacht.

Weitere Beispiele

Bearbeiten
  • Der Term   ist eine Möglichkeit von vielen, die logische Funktion   darzustellen. Hierzu versteht man   als Abkürzung für   und   als Abkürzung für  . Der Term erfüllt alle Forderungen, die man an die Funktion   stellt.
    •  
    •  
    •  
    •  
  • Man kann in ähnlicher Weise Zahlen, Tupel und Listen in λ-Ausdrücken codieren (z. B. durch sogenannte Church-Numerale)
  • Man kann beliebige rekursive Funktionen durch den Fixpunkt-Kombinator   darstellen.

Typisierter Lambda-Kalkül

Bearbeiten

Die zentrale Idee des typisierten Lambda-Kalküls ist es, nur noch Lambda-Ausdrücke zu betrachten, denen sich ein Typ durch ein System von Typinferenzregeln zuordnen lässt. Das einfachste Typsystem, das von Church in seiner Theory of Simple Types vorgestellt wurde, sieht die Typen vor, die durch folgende Grammatik in Backus-Naur-Form generiert werden:

TT ::= I (Individuen) | O (Wahrheitswerte) | (TT → TT) (Funktionstypen)

Den Typ   kann man sich als Zahlen vorstellen,   wird für boolesche Werte wie Wahr und Falsch verwendet.

Zusätzlich wird eine Umgebung   definiert; dies ist eine Funktion, die Variablensymbolen Typen   zuordnet.

Ein Tripel aus einer Umgebung  , einem Ausdruck   und einem Typ  , geschrieben   wird ein Typurteil genannt.

Nun können die Inferenzregeln Beziehungen zwischen Ausdrücken, ihren Typen und Typurteilen herstellen:  

 

 

Hierbei ist   diejenige Funktion, die an der Stelle   den Typ   zuordnet, und ansonsten die Funktion   ist. (Anders ausgedrückt: Der Parameter   der Funktion ist vom Typ   und genau diese Information wird der Umgebung hinzugefügt.)

Durch Einführung einer zweiten Umgebung sind auch Konstantensymbole behandelbar; eine weitere wichtige Erweiterung besteht darin, in Typen auch die Kategorie der Typvariablen   etc. oder Typkonstruktoren wie  ,   etc. zuzulassen: so entstehen schon sehr mächtige funktionale oder logische Kernsprachen.   ist beispielsweise eine Funktion, die den beliebigen Typen   auf den Typ „Menge, deren Elemente vom Typ   sind“ abbildet;   analog; geschrieben   und  , wobei auch wie gehabt die Klammern fehlen dürfen. Das Konzept kann leicht weiter abstrahiert werden, indem statt eines konkreten Typkonstruktors auch eine Variable verwendet wird, z. B.  . Typkonstruktoren dürfen allgemein auch mehrere Argumente besitzen, wie beispielsweise der Pfeil: Der Typ   ist nichts anderes als  , zeigt aber besser, dass der Pfeil ein Typkonstruktor in zwei Variablen ist. Insbesondere ist auch bei Typkonstruktoren Currying möglich, und   ist ein Typkonstruktor in einer Variablen.

Es ist entscheidbar, ob ein untypisierter Term sich typisieren lässt, selbst wenn die Umgebung   unbekannt ist (eine Variante mit Typvariablen und Typkonstruktoren ist der Algorithmus nach Hindley-Milner).

Die Menge der typisierbaren Ausdrücke ist eine echte Teilmenge des untypisierten Lambda-Kalküls; z. B. lässt sich der Y-Kombinator nicht typisieren. Andererseits ist für typisierte Ausdrücke die Gleichheit zwischen zwei Funktionen modulo α- und β-Konversionen entscheidbar. Es ist bekannt, dass das Matching-Problem auf Lambda-Ausdrücken bis zur vierten Ordnung entscheidbar ist. Das Unifikationsproblem ist unentscheidbar; allerdings gibt es praktisch brauchbare approximative Algorithmen.

Anwendung in der Semantik

Bearbeiten

Die Semantik ist dasjenige Teilgebiet der Linguistik, welches die Bedeutung natürlichsprachlicher Ausdrücke analysiert. Die formale Semantik nutzt dazu zunächst einfache Mittel der Prädikatenlogik und Mengenlehre. Diese erweitert man um Grundlagen des Lambda-Kalküls, etwa um mittels Lambda-Abstraktion Propositionen als Eigenschaften zu repräsentieren und komplexere Nominalphrasen, Adjektivphrasen und einige Verbalphrasen darstellen zu können. Grundlage ist etwa eine modelltheoretische semantische Interpretation der intensionalen Logik Richard Montagues.

Anwendung in der Informatik

Bearbeiten

Der Lambda-Kalkül ist auch die formale Grundlage für viele Programmiersprachen, wie z. B. Scheme oder Lisp. Einige Programmiersprachen bieten Konzepte wie anonyme Funktionen an, auf die sich einige der Regeln des Lambda-Kalküls anwenden lassen. Die Programmiersprachen erlauben jedoch meist mehr als der reine Lambda-Kalkül wie beispielsweise Nebeneffekte.

Siehe auch

Bearbeiten

Literatur

Bearbeiten
  • Stephen Kleene: A theory of positive integers in formal logic. In: American Journal of Mathematics. 57, 1935, ISSN 0002-9327, S. 153–173 und 219–244.
  • Alonzo Church: An unsolvable problem of elementary number theory. In: American Journal of Mathematics. 58, 1936, S. 345–363.
  • Alonzo Church: The Calculi of Lambda-Conversion[1]
  • Henk P. Barendregt: The lambda calculus. Its syntax and semantics. Revised edition. North-Holland, Amsterdam u. a. 1984, ISBN 0-444-87508-5 (Studies in logic and the foundations of mathematics 103).
  • Guo-Qiang Zhang: Logic of Domains. Birkhäuser, Boston u. a. 1991, ISBN 0-8176-3570-X (Progress in theoretical computer science 4), (Zugleich: Cambridge, Univ., Diss., 1989).
  • Roberto M. Amadio, Pierre-Louis Curien: Domains and Lambda-Calculi. Cambridge University Press, Cambridge u. a. 1998, ISBN 0-521-62277-8 (Cambridge tracts in theoretical computer science 46).
  • Samson Abramsky (Hrsg.): Typed Lambda Calculi and Applications. 5th international conference, Kraków, Poland, May 2 – 5, 2001. Proceedings. Springer, Berlin u. a. 2001, ISBN 3-540-41960-8 (Lecture notes in computer science 2044).
Bearbeiten

Einzelnachweise

Bearbeiten
  1. Alonzo Church: The Calculi of Lambda-Conversion. Princeton University Press, Princeton 1941 (englisch, archive.org [abgerufen am 14. April 2020]).