UnterChurch-Kodierung versteht man die Einbettung von Daten und Operatoren in denLambda-Kalkül. Die bekannteste Form sind dieChurch-Numerale, welche dienatürlichen Zahlen repräsentieren. Benannt sind sie nachAlonzo Church, der Daten als Erster auf diese Weise modellierte.

Die Grundidee zur Kodierung beruht auf denPeano-Axiomen, wonach die natürlichen Zahlen durch einen Startwert – die 0 – und einer Nachfolger-Funktion definiert sind. Demnach sind die Church-Numerale wie folgt definiert:

0 ≡λf.λx. x

1 ≡λf.λx. f x

2 ≡λf.λx. f (f x)

3 ≡λf.λx. f (f (f x))

...

n ≡λf.λx. fn x

In der obigen Liste istf die Nachfolger-Funktion undx der Startwert, beides sind Parameter der Definition. Die Definition ist unabhängig von der Ausprägung des Startwertes oder der Nachfolger-Funktion. Somit sind die Numerale nur repräsentativ. Jedes einzelne Numeral benutzt die beiden Parameter für seine Implementation. Solange man sich aber nicht festlegt, worin genau der Startwert und die Nachfolger-Funktion besteht, ist auch nicht festgelegt, was die Numerale schlussendlich machen. Die Definition basiert lediglich auf den Annahme, dass es so etwas wie einen Startwert und eine dazu passende Nachfolger-Funktion geben mag, wie immer die auch aussehen mögen. Unter dieser Annahme machen die Numerale das Folgende:

• Das Numeral0 benutzt die Nachfolger-Funktion gar nicht, weil es nur den Startwert zurückgibt.
• Das Numeral1 benutzt sowohl Nachfolger-Funktion als auch Startwert, indem es die Nachfolge-Funktion genau einmal auf den Startwert anwendet.
• Das Numeral2 benutzt wie Numeral 1 und alle folgenden Numerale ebenfalls Nachfolger-Funktion und Startwert, wendet die Nachfolger-Funktion aber zweimal auf den Startwert an.
• Das Numeral3 macht das gleiche wie Numeral 2, nur wendet es die Nachfolger-Funktion diesmal dreimal auf den Startwert an.
• Das Numeraln folgt der Regel und wendet die Nachfolger-Funktion n mal auf den Startwert an.

Im Lambda-Kalkül sind arithmetische Funktionen durch korrespondierende Funktionen über Church-Numerale darstellbar. Diese Funktionen können infunktionalen Programmiersprachen direkt durch Übertragen der Lambda-Ausdrücke implementiert werden.

Die Nachfolger-Funktion wird wie folgt definiert:

succ ≡λn.λf.λx. f (n f x)

Die Addition zweier Zahlen${\displaystyle n}$ und${\displaystyle m}$ ist die${\displaystyle m}$-malige Anwendung der Nachfolger-Funktion auf${\displaystyle n}$:

plus ≡λm.λn.λf.λx. m f (n f x)

Die Multiplikation zweier Zahlen${\displaystyle n}$ und${\displaystyle m}$ ist die${\displaystyle m}$-malige Anwendung der Addition${\displaystyle (+n)}$ auf${\displaystyle n}$:

mult ≡λm.λn.λf.λx. m (n f) x

Die Vorgänger-Funktion:

pred ≡λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

Analog zu den natürlichen Zahlen lassen sich auch (zweiwertige)Wahrheitswerte im Lambda-Kalkül modellieren.

true ≡λx.λy. x

false ≡λx.λy. y

Daraus lässt sich auch eine einfacheKontrollstruktur (IF THEN ELSE) ableiten:

ifthenelse ≡λb.λx.λy.b x y

Dabei ist die Variable${\displaystyle b}$ als Bedingung zu verstehen,${\displaystyle x}$ als „THEN“ und${\displaystyle y}$ als „ELSE“.

• Mathematische Logik
• Berechenbarkeitstheorie
• Mathematische Notation