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:
In der obigen Liste ist f die Nachfolger-Funktion und x 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 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:
Die Addition zweier Zahlen und ist die -malige Anwendung der Nachfolger-Funktion auf :
Die Multiplikation zweier Zahlen und ist die -malige Anwendung der Addition auf :
Die Vorgänger-Funktion:
Boolesche Ausdrücke Bearbeiten
Analog zu den natürlichen Zahlen lassen sich auch (zweiwertige) Wahrheitswerte im Lambda-Kalkül modellieren.
Daraus lässt sich auch eine einfache Kontrollstruktur (IF THEN ELSE) ableiten:
Dabei ist die Variable als Bedingung zu verstehen, als „THEN“ und als „ELSE“.