ein von A.Church entwickelter Kalkül, der eine Sprache zur systematischen Definition von Funktionen darstellt.

Der Kalkül ist typenfrei, d. h. es wird syntaktisch nicht zwischen Funktionen und deren Argumenten unterschieden. Der λ-Operator ist hierbei der wesentliche syntaktische Baustein, um Funktionen aufzubauen, wobei λx.T die Funktion x ↦ T bedeutet. Dabei ist T ein Term, der normalerweise x als freie Variable enthält.

Formal wird der λ-Kalkül aufgebaut aus den folgenden syntaktischen Komponenten: Variablen x₀, x₁, …; dem Abstraktionsoperator λ; den Klammern „(“ und „)“; und dem Punkt „. “.

Hieraus baut man λ-Terme induktiv wie folgt auf: Eine Variable x ist bereits ein λ-Term, und zwar kommt x hierin freivor. Wenn M, N bereits λ-Terme sind, so ist auch die Anwendung von M auf N, (MN), ein λ-Term. Die Variablenvorkommen in M bzw. N, die jeweils frei oder gebunden sind, bleiben in (MN) jeweils frei oder gebunden. Wenn M ein λ-Term ist und x eine Variable, dann ist die Anwendung des λ-Operators auf M, die λ-Abstraktion von M, (λx.M), ebenfalls ein λ-Term. Die Variablenvorkommen von x in M sind dann gebunden, während alle anderen Variablenvorkommen frei oder gebunden bleiben, wie sie es zuvor in M waren.

Mit Hilfe der α- und β-Regeln kann eine Transformationstheorie für λ-Terme aufgebaut werden.

α-Regel: Gebundene Variablen können umbenannt werden: \begin{eqnarray}\lambda x.M\mathop{\to }\limits^{\alpha }\lambda y.M[x/y],\end{eqnarray}

sofern y in M nicht vorkommt. Hierbei bedeutet M[x/y], daß jedes Vorkommen von x in M durch y ersetzt wird.

β-Regel (oder λ-Konversion): Man kann eine Funktion λx.M auf ein Argument N anwenden: \begin{eqnarray}(\lambda x.M)N\mathop{\to }\limits^{\beta }M[x/N].\end{eqnarray}

Man schreibt \({t}_{1}\mathop{=}\limits^{\beta }{t}_{2}\), wenn die λ-Terme t₁ und t₂ mittels der α- und β-Regeln in denselben λ-Term überführt werden können.

In der Kombinatortheorie werden einige wenige λ-Terme, die Kombinatoren, als Primitive betrachtet, und alle anderen λ-Terme mit Hilfe dieser Kombinatoren aufgebaut. Es genügt, die folgenden beiden Kombinatoren zu wählen: \begin{eqnarray}\begin{array}{cc}S=\lambda xyz.xz(yz), & K=\lambda xy.x\end{array}.\end{eqnarray}

Dann ergibt sich z. B. die identische Abbildung λx.x mittels SKK.

Mit Hilfe der λ-Terme lassen sich die natürlichen Zahlen und gewisse arithmetische Funktionen wie folgt definieren. Der Zahl n ∈ ℕ₀ wird der λ-Term \begin{eqnarray}\bar{n}=\lambda xy.\mathop{\underbrace{xx\ldots x}}\limits_{n-\text{mal}}y\end{eqnarray}

zugeordnet. Eine k-stellige arithmetische Funktion \(f:{{\mathbb{N}}}_{0}^{k}\to {{\mathbb{N}}}_{0}\) heißt λ-definierbar, falls es einen λ-Term M gibt, so daß f(a₁,…,a_k) = b genau dann gilt, wenn \begin{eqnarray}M\overline{{a}_{1}}\ \overline{{a}_{2}}\ldots \overline{{a}_{k}}\mathop{=}\limits^{\beta }\overline{b}.\end{eqnarray}

Wie Kleene 1936 zeigte, ist eine Funktion λ-definierbar genau dann, wenn sie μ-rekursiv ist (μ-rekursive Funktion, Churchsche These).

Der λ-Kalkül bildet die Grundlage für die Programmiersprache LISP, und damit für den gesamten Bereich der funktionalen Programmiersprachen.

[1] Oberschelp, A.: Rekursionstheorie. BI-Wissenschaftsverlag Mannheim, 1993.