Exkurs: Zahlen nach Church
Dieses Kapitel und auch diese Ausarbeitung enden mit einem Ausflug in die theoretische Phantasie. Dieses Material
wird für den weiteren Verlauf der Veranstaltung nicht benötigt, soll aber dennoch kurz angesprochen
werden.
Es wurde bereits gezeigt, dass es nicht notwendig ist, Datentypen als bereits im System implementiert anzunehmen. Sie
können ebenso jeweils durch eigene Deklarationen eingeführt werden.
Nun soll zusätzlich gezeigt werden, dass auch diese eigenen Datentypen-Deklarationen überflüssig sind,
denn alles kann auch alleine durch Funktionen bewerkstelligt werden.
Dies war Teil des Programms, welches Alonzo Church (1903-1995) in den 40er Jahren entwickelte, als er am
Lamda-Kalkül arbeitete. Als Professor für Philosophie und Mathematik forschte er u.a. im Bereich der
Logik und Rekursion. Das Lamda-Kalkül ist dabei ein formales mathematisches System, auf dem viele Ansätze
der heutigen Forschung zur funktionalen Programmierung basieren. Vergleichbar ist der Status des Kalküls mit dem
der Turingmaschine für imperative Programmiersprachen wie Pascal oder C.
Zur Einführung in dieses Thema dienen die booleschen Wahrheitswerte True und False.
Frage: Wofür werden diese Wahrheitswerte benötigt?
Antwort: Es gibt sie, um eine Entscheidung zwischen zwei Alternativen zu treffen.
Dies kann als Funktion dargestellt werden:
true, false :: α -> α -> α
true x y = x
false x y = y
|
Dabei wählt die Funktion true die erste Alternative und die Funktion false die zweite. So sind
diese Wahrheitswerte nach Church ein Synonym für einen bestimmten Typ von Funktionen:
type Cbool α = α -> α -> α
|
Negation:
not :: Cbool(Cbool α) -> Cbool α
not x = x false true
|
Konjunktion und Disjunktion:
and, or :: Cbool(Cbool α) -> Cbool α -> Cbool α
and x y = x y false
or x y = x true y
|
In jedem der Fälle wählt das x die passende Alternative. Diese Funktion nimmt das "Church-boolean"
als Argument, was auch die Signatur von not, and und or erklärt.
Ebenso kann gefragt werden, für was die natürlichen Zahlen gebraucht werden. Natürliche Zahlen
werden z.B. benötigt, um zu zählen. Somit auch für die Kontrolle, wie oft etwas ausgeführt
wird.
Wie schon bei bool, so können auch die natürlichen Zahlen durch Funktionen definiert werden:
zero, one, two :: (α -> α) -> α -> α
zero f = id
one f = f
two f = f · f
...
|
Die Funktion zero f wendet f nie auf ihre Argumente an. Die Funktion one f dagegen einmal und
die Funktion two f zweimal. Somit sind Church-Zahlen ebenso ein synonymer Typ, wie schon Bool:
type Cnum α = (α -> α) -> (α -> α)
|
Anstatt jede Zahl einzeln explizit schreiben zu müssen, kann die Nachfolger-Funktion Succ verwendet
werden. Diese Funktion ist wie folgt definiert:
succ :: Cnum α -> Cnum α
succ cn f = f · cn f
|
Es lässt sich erkennen, dass succ cn f erst cn mal nutzt und dann ein weiteres Mal.
An dieser Stelle ist ein Programm beschrieben, das natürliche Zahlen in Church-Zahlen umwandelt und
umgekehrt:
church :: Int -> Cnum Int
church = foldn succ zero
natural :: Cnum Int -> Int
natural cn = cn (+1) 0
|
Die Funktion foldn für Nat wurde bereits in einem früheren Abschnitt vorgestellt.
Der Wert natural cn wird berechnet, indem cn genutzt wird, um die Funktion (+1) exakt cn-
mal auf die Zahl 0 anzuwenden. Zu beachten sind die Typen church und natural. Der Quelltyp für
natural muss Cnum Int sein, da seine Argumente rechts auf eine int -> int-Funktion angewendet
werden. Der Zieltyp für church ist der selbe. Dadurch wird sichergestellt, dass sich church und
natural invers verhalten.
Ebenso ist es möglich, arithmetische Operationen mit diesen Church-Nummern durchzuführen. Tatsächlich
gibt es mehrere Wege, um die einfachen arithmetischen Operationen zu implementieren, obwohl nicht alle von ihnen
durch Cnum α -> Cnum α -> Cnum α bestimmt werden können.
Eine legitime Definition für plus ist:
plus1 :: Cnum α -> Cnum α -> Cnum α
plus1 cn dn f = cn f · dn f
|
Dadurch wird für plus1 cn dn definiert, dass es das Ergebnis der dn-maligen Ausführung
von f und der dann folgenden cn-maligen Durchführung ist.
Eine kürzere Definition für plus ist:
plus2 :: Cnum(Cnum α) -> Cnum α -> Cnum α
plus2 cn = cn succ
|
Die Funktion plus2 cn dn wendet succ genau cn-mal auf dn an. Das erste Argument von
plus2 ist eine Church-Nummer, die succ :: Cnum α -> Cnum α als Argument nimmt. Das
beschreibt die Typänderung.
Für die Multiplikation kann ebenfalls eine kurze Definition gegeben werden:
times1 :: Cnum α -> Cnum α -> Cnum α
times1 cn dn = cn · dn
|
Die Funktion times1 cn dn f wendet dn f exakt cn-mal an.
Eine alternative Definition für die Multiplikation ist:
times2 :: Cnum(Cnum α) -> Cnum α -> Cnum (α -> α)
times2 cn = cn · plus1
|
Die Funktion times2 cn dn verwendet plus1 dn genau cn-mal. Wird plus1 durch plus2
ersetzt, so ergibt sich eine dritte Version für die Multiplikation.
Die Typsignaturen dieser Funktionen werden immer komplizierter und es soll an dieser Stelle nicht versucht
werden, sie zu belegen. Tatsächlich werden sie mit Hilfe eines Haskell-eigenen Systems abgeleitet.
Als letzes Beispiel (dieser Ausarbeitung) wird nun noch eine Version der Exponentialrechnung ohne Signatur vorgestellt:
Bei dieser Funktion werden die Argumente vertauscht, dabei steht der Ausdruck arrow1 m n für
n^m. Die Funktion arrow1 cn dn verwendet dabei times1 dn exakt cn-mal.