Church Encodings - Booleans und Zahlen

Beschreibung

Nebst den bekannten Lambda-Kombinatoren gibt es noch die Church-Booleans und Church-Zahlen. Mit den Church-Booleans werden boolesche Logik mit Funktionen ausgedrückt und die Church-Zahlen sind die bekannteste Form, mit welche die natürlichen Zahlen repräsentiert werden. Benannt sind sie nach Alonzo Church, Mathematiker und einer der Begründer der theoretischen Informatik.

Church-Boolean

True & False

True kann durch die Funktion Kestrel ausgedrückt werden. False kann durch die Funktion Kite ausgedrückt werden.

Implementation

const True  = K;
const False = KI;

Not

Der boolesche not Operator kann mit der Funktion Cardinal ausgedrückt werden.

Implementation & Beispiele:

const not = C;

not(True);         // False (Function)
not(False);        // True  (Function)
not(not(True));    // True  (Function)

And

Die And-Funktion nimmt zwei Church-Booleans entgegen und liefert ein Church-Boolean zurück. Die Funktion funktioniert genau gleich wie der and-Operator in der mathematischen Logik.

Implementation:

const and = p => q => p(q)(False);

Beispiele:

and(True)(True)         // True
and(False)(True)        // False
and(True)(False)        // False
and(False)(False)       // False

Or

Die Or-Funktion nimmt zwei Church-Booleans entgegen und liefert ein Church-Boolean zurück. Die Funktion funktioniert genau gleich wie der or-Operator in der mathematischen Logik.

Implementation:

const or = p => q => p(True)(q);

Beispiele:

or(True)(True)         // True
or(False)(True)        // True
or(True)(False)        // True
or(False)(False)       // False

Boolean Equality

Diese Funktion nimmt zwei Church-Booleans entgegen und vergleicht diese miteinander. Nur wenn beide gleich sind, gibt die Funktion ein Church-True zurück, sonst ein Church-False.

Implementation:

const beq = p => q => p(q)(not(q));

Beispiele:

beq(True)(True)         // True
beq(False)(True)        // False
beq(True)(False)        // False
beq(False)(False)       // True

Show Boolean

Die Funktion showBoolean ist eine Helferfunktion um eine String Repräsentation, eines Church-Boolean zu erhalten. Die Funktion nimmt ein Church-Boolean entgegen und gibt die String Repräsentation davon zurück.

Implementation:

const showBoolean = b => b("True")("False");

Beispiele:

showBoolean(True);        // 'True'
showBoolean(False);       // 'False'

Connvert to js Bool

Die Funktion convertToJsBool nimmt ein Church-Boolean entgegen und liefert die JavaScript Representation davon zurück.

Implementation:

const convertToJsBool = b => b(true)(false);

Beispiele:

convertToJsBool(True)        // true
convertToJsBool(False)       // false

Church-Zahlen

Die Church-Zahlen sind keine "echte" Zahlen, sondern eine Funktionen wird n-Mal auf ein Argument angewendet. Um die Zahl Eins als eine Church-Zahl ( n1) zu repräsentieren muss es eine Funktion geben die einmal auf das Argument angewendet wird.

Implementation der Church-Zahl n1 (Eins):

// Implementation n1
const n1 = f => a => f(a);

// Demonstration
n1(x => x + 1)(0)      // 1

n1(x => x + '!')('λ')  // 'λ!'

Das gleiche mit den Zahlen von Zwei bis Neun, welche jeweils n-Mal auf ein Argument angewendet werden.

// Implementation n2...n9
const n2 = f => a => f(f(a));
const n3 = f => a => f(f(f(a)));
const n4 = f => a => f(f(f(f(a))));
const n5 = f => a => f(f(f(f(f(a)))));
const n6 = f => a => f(f(f(f(f(f(a))))));
const n7 = f => a => f(f(f(f(f(f(f(a)))))));
const n8 = f => a => f(f(f(f(f(f(f(f(a))))))));
const n9 = f => a => f(f(f(f(f(f(f(f(f(a)))))))));

// Demonstration
n2(x => x + 1)(0)      // 2
n3(x => x + 1)(0)      // 3
n4(x => x + 1)(0)      // 4

n3(x => x + '!')('λ')  // 'λ!!!'

Die Zahl Null n0 wird in den Church-Zahlen als Funktion die keinmal auf das Argument angewendet wird. Somit wird die Funktion f ignoriert.

Implementation der Church-Zahl n0 (Null):

// Implementation n0
const n0 = f => a => a;

// Demonstration
n0(x => x + 1)(0)      // 0

n0(x => x + '!')('λ')  // 'λ'

n0 nimmt zwei Parameter und gibt den zweiten zurück. Gleich wie die Funktion: Kite (n0 === KI).

jsNum

Um eine Church-Zahl in eine JavaScript-Zahl zu transferiere, evaluiert die Funktion jsNum die Church-Zahl n-Mal den Funktionsaufruf und zählt dabei die Aufrufe.

// Implementaion
const jsNum = n => n(x => x + 1)(0);

// Anwendung
jsNum(n0)     // 0
jsNum(n1)     // 1
jsNum(n2)     // 2

churchNum

Um aus einer JavaScript-Zahl eine Church-Zahl zu kreieren, wird mit der Funktion churchNum rekursiv n-Mal mit der Nachfolger-Funktion successor eine Church-Zahl gebaut.

// Implementaion
const churchNum = n => n === 0 ? n0 : successor(churchNum(n - 1));

// Anwendung
jsNum(0)     // n0
jsNum(1)     // n1
jsNum(2)     // n2

Mathematische Operationen mit Church-Zahlen

Successor (Nachfolger)

Der Successor nimmt eine Church-Zahl und gibt dessen Nachfolger zurück.

Implementation:

const successor = n => f => a => f(n(f)(a));

Beispiel:

successor(n0)        // n1
successor(n5)        // n6

Phi (-Kombinator)

Der Phi-Kombinator nimmt eine Pair und gibt ein neues Pair zurück. Der erste Wert entspricht dem zweiten des alten Pairs. Der zweite Wert ist der Nachfolger des zweiten Wertes vom alten Pair.

Implementation:

const phi = p => pair(p(snd))(succ(p(snd)));

Beispiel:

const testPair  = pair(n1)(n2);
const testPhi   = phi(testPair);

testPhiPair(fst)    // n2
testPhiPair(snd)    // n3

Predecessor (Vorgänger)

Der Predecessor nimmt eine Church-Zahl und gibt dessen Vorgänger zurück.

Der Phi-Kombinator ist dabei eine unterstützende Funktion um den Vorgänger der Church-Zahl zu definieren.

Implementation:

const pred = n => n(phi)(pair(n0)(n0))(fst);

Beispiel:

 pred(n0)   // n0
 pred(n1)   // n0
 pred(n2)   // n1
 pred(n9)   // n8

Church-Addition (Addieren)

ChurchAddition nimmt zwei Church-Zahlen und gibt den addierten Wert als Church-Zahl zurück.

Der Successor ist dabei unterstützende Funktion. Die erste Church-Zahl ruft dabei n-Mal den successorauf und nimmt die zweite Church-Zahl als Summand.

Implementation:

const churchAddition = n => k => n(successor)(k);

Beispiel:

churchAddition(n0)(n0)     //  0
churchAddition(n1)(n0)     //  1
churchAddition(n2)(n5)     //  7
churchAddition(n9)(n9)     // 18

Church-Substraction (Substrahieren)

ChurchSubstraction nimmt zwei Church-Zahlen und gibt den subtrahierten Wert als Church-Zahl zurück.

Der Predecessor ist dabei eine unterstützende Funktion. Die zweite Church-Zahl ruft dabei n-Mal den pred als Subtrahend und nimmt die erste Church-Zahl als Minuend.

Implementation:

const churchSubtraction = n => k => k(pred)(n);

Beispiel:

churchSubtraction(n2)(n1)     // 1
churchSubtraction(n2)(n0)     // 2
churchSubtraction(n2)(n5)     // 0
churchSubtraction(n9)(n4)     // 5

Church-Multiplication (Multiplizieren)

ChurchMultiplication nimmt zwei Church-Zahlen und gibt den multiplizierten Wert als Church-Zahl zurück.

Die ChurchMultiplication entspricht exakt dem Bluebird !

Implementation:

const churchMultiplication = B;    // Bluebird

Beispiel:

churchMultiplication(n2)(n1)     //  1
churchMultiplication(n2)(n0)     //  0
churchMultiplication(n2)(n5)     // 10
churchMultiplication(n9)(n4)     // 36

Church-Potency (Potenzieren)

ChurchPotency nimmt zwei Church-Zahlen und gibt den potenzierende Wert als Church-Zahl zurück.

Die ChurchPotency entspricht exakt dem Thrush !

Implementation:

const churchPotency = T;    // Thrush

Beispiel:

churchPotency(n2)(n1)     //    2
churchPotency(n2)(n0)     //    1
churchPotency(n2)(n5)     //   32
churchPotency(n9)(n4)     // 6561

isZero

isZero nimmt eine Church-Zahlen und gibt ein Church-Boolean zurück. Wenn die Church-Zahl n0 ist gibt die Funktion ein Church-Boolean True, ansonsten False zurück.

Beachte den Kestrel k in der Funktion, der nur zum Zug kommt, wenn die Church-Zahl nicht n0 ist und somit den ersten Wert bzw. False zurück gibt.

Implementation:

const is0 = n => n(K(False))(True);

Beispiel:

is0(n0)     // True
is0(n1)     // False
is0(n2)     // False
is0(n7)     // False

leq (less-than-or-equal)

leq nimmt zwei Church-Zahlen und gibt ein Church-Boolean zurück. Wenn der erste Wert kleiner oder gleich dem zweiten Wert ist gibt die Funktion ein Church-Boolean True, ansonsten False zurück.

isZero und churchSubstraction sind dabei die benötigten Funktionen um Leq zu implementieren. churchSubstraction substrahiert die erste Church-Zahl mit der zweiten Church-Zahl. Der substrahierte Wert ist n0 , wenn die zweite Church-Zahl grösser oder gleich der ersten Church-Zahl ist. Wenn dies stimmt, gibt isZero ein True zurück.

Implementation:

const leq = n => k => is0(churchSubtraction(n)(k));

Beispiel:

leq(n0)(n0)     // True
leq(n0)(n3)     // True
leq(n5)(n5)     // True
leq(n5)(n1)     // False

eq (equality-to)

eq nimmt zwei Church-Zahlen und gibt ein Church-Boolean zurück. Wenn die beiden Church-Zahlen gleich sind, gibt die Funktion das Church-Boolean True, ansonsten False zurück.

And und Leq sind dabei die unterstützende Funktionen. Mit a_nd_ und leq werden die Church-Zahlen auf ihre Äquivalenz geprüft. Wenn dies Stimmt, erhält a_nd_ zwei True-Werte von leq zurück.

Implementation:

const eq = n => k => and(leq(n)(k))(leq(k)(n));

Beispiel:

 eq(n0)(n0)  // True
 eq(n0)(n1)  // False
 eq(n1)(n1)  // True
 eq(n2)(n1)  // False

gt (greater-than)

gt nimmt zwei Church-Zahlen und gibt ein Church-Boolean zurück. Wenn der erste Wert grösser als der zweite Wert ist, gibt die Funktion ein Church-Boolean True, ansonsten False zurück.

Blackbird, Not und Leq sind dabei die unterstützende Funktionen. Der Blackbird handelt die not und leq-Funktion (not(leq(n)(k) ). Dabei wird nichts andere als der Output bzw. die Church-Boolean der leq-Funktion von der not-Funktion negiert.

Implementation:

const gt = Blackbird(not)(leq);

Beispiel:

gt(n0)(n0)     // False
gt(n0)(n1)     // False
gt(n1)(n1)     // False
gt(n2)(n1)     // True