Church-Kodierung

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

Unter Church-Kodierung versteht man die Einbettung von Daten und Operatoren in den Lambda-Kalkül. Die bekannteste Form sind die Church-Numerale, welche die natürlichen Zahlen repräsentieren. Benannt sind sie nach Alonzo Church, der Daten als Erster auf diese Weise modellierte.

Church-Numerale[Bearbeiten]

Definition[Bearbeiten]

Die Grundidee zur Kodierung beruht auf den Peano-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

Rechnen mit Church-Numeralen[Bearbeiten]

Im Lambda-Kalkül sind arithmetische Funktionen durch korrespondierende Funktionen über Church-Numerale darstellbar. Diese Funktionen können in funktionalen 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 n und m ist die m-malige Anwendung der Nachfolger-Funktion auf n:

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

Die Multiplikation zweier Zahlen n und m ist die m-malige Anwendung der Addition (+n) auf n:

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

Die Vorgänger-Funktion:

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

Boolesche Ausdrücke[Bearbeiten]

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 einfache Kontrollstruktur (IF THEN ELSE) ableiten:

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

Dabei ist die Variable b als Bedingung zu verstehen, x als „THEN“ und y als „ELSE“.