Quelltext der Seite Church-Kodierung

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ürliche Zahl|natürlichen Zahlen]] repräsentieren. Benannt sind sie nach [[Alonzo Church]], der Daten als Erster auf diese Weise modellierte.

== Church-Numerale ==

=== Definition ===

Die Grundidee zur Kodierung beruht auf den [[Peano-Axiome]]n, 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''' ≡ <code>λf.λx. x</code>
: '''1''' ≡ <code>λf.λx. f x</code>
: '''2''' ≡ <code>λf.λx. f (f x)</code>
: '''3''' ≡ <code>λf.λx. f (f (f x))</code>
: ...
: '''n''' ≡ <code>λf.λx. f<sup>''n''</sup> x</code>
In der obigen Liste ist <code>f</code> die Nachfolger-Funktion und <code>x</code> 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 Numeral '''0''' benutzt die Nachfolger-Funktion gar nicht, weil es nur den Startwert zurückgibt.
* Das Numeral '''1''' benutzt sowohl Nachfolger-Funktion als auch Startwert, indem es die Nachfolge-Funktion genau einmal auf den Startwert anwendet.
* Das Numeral '''2''' benutzt wie Numeral 1 und alle folgenden Numerale ebenfalls Nachfolger-Funktion und Startwert, wendet die Nachfolger-Funktion aber zweimal auf den Startwert an.
* Das Numeral '''3''' macht das gleiche wie Numeral 2, nur wendet es die Nachfolger-Funktion diesmal dreimal auf den Startwert an.
* Das Numeral '''n''' folgt der Regel und wendet die Nachfolger-Funktion n mal auf den Startwert an.

=== Rechnen mit Church-Numeralen ===

Im Lambda-Kalkül sind arithmetische Funktionen durch korrespondierende Funktionen über Church-Numerale darstellbar. Diese Funktionen können in [[Funktionale Programmierung|funktionalen Programmiersprachen]] direkt durch Übertragen der Lambda-Ausdrücke implementiert werden. 

Die Nachfolger-Funktion wird wie folgt definiert:
: '''succ''' ≡ <code>λn.λf.λx. f (n f x)</code> 

Die Addition zweier Zahlen <math>n</math> und <math>m</math> ist die <math>m</math>-malige Anwendung der Nachfolger-Funktion auf <math>n</math>:
: '''plus''' ≡ <code>λm.λn.λf.λx. m f (n f x)</code>

Die Multiplikation zweier Zahlen <math>n</math> und <math>m</math> ist die <math>m</math>-malige Anwendung der Addition <math>(+n)</math> auf <math>n</math>:
: '''mult''' ≡ <code>λm.λn.λf.λx. m (n f) x</code>

Die Vorgänger-Funktion:
: '''pred''' ≡ <code>λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)</code>

== Boolesche Ausdrücke ==

Analog zu den natürlichen Zahlen lassen sich auch (zweiwertige) [[Wahrheitswert]]e im Lambda-Kalkül modellieren.
: '''true''' ≡ <code>λx.λy. x</code>
: '''false''' ≡ <code>λx.λy. y</code>

Daraus lässt sich auch eine einfache [[Kontrollstruktur]] ([[Verzweigung (Programmierung)|IF THEN ELSE]]) ableiten:
: '''ifthenelse''' ≡ <code>λb.λx.λy.b x y</code>

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

[[Kategorie:Mathematische Logik]]
[[Kategorie:Berechenbarkeitstheorie]]
[[Kategorie:Mathematische Notation]]