Wie in Lambda-Kalkül zu kodieren

Question

Ich lerne Lambda-Kalkül in Haskell und während dieser, ich stoße auf diese Frage.

Und die Lösung dieser Frage ist:

Aber ich bin nicht in der Lage zu verstehen, wie sie die Antwort schließen. Wie für eq, ich verstehe nicht, wie sie dazu kommen: λab.a b (b (λxy.y) (λxy.x)) und das gleiche für nand. Es wird wirklich toll sein, wenn jemand es erklärt und mir hilft, diese Frage zu verstehen.

Vielen Dank.

Answer 1

Ich benutze die Haskell Konvention von Schreiben & Lambda; als \.

Aus den Kommentaren sieht es aus wie Sie sind speziell mit diesem Teil Schwierigkeiten mit:

eq = \a b. a b (b (\x y. y) (\x y. x)) 

Also werde ich auf diese konzentrieren sich nur.

Unsere Codierung von Booleans ist als Funktionen, die zwei Argumente nehmen. True gibt das erste Argument zurück, False gibt das zweite Argument zurück. Der erste Absatz gibt die Codierung direkt:

True = \x y. x 
False = \x y. y 

Wir werden die Namen anstelle der Lambda-Ausdrücke, bis zum Ende.

Wir wissen, dass zwei Argumente, die zwei booleans zu vergleichen sind.(Die Codierung von booleans selbst nimmt zwei Argumente, aber das ist anders - eq zwei Argumente nehmen soll, egal wie booleans codiert werden), so wissen wir, es sollte wie folgt aussehen:

eq = \a b. _________________ 

An dieser Stelle so ziemlich die einzige Was wir tun können, ist eines der Argumente zu überprüfen, ob es True oder False ist. ist symmetrisch, so dass es nicht wirklich wichtig ist, nach welchem ​​wir fragen; Lassen Sie uns a ohne Grund wählen. Die Art, wie wir nach der Codierung fragen, besteht darin, zwei Argumente an die Sache zu übergeben, die wir herausfinden wollen.

eq = \a b. a ____ ____ 

Wo haben wir noch nicht herausgefunden, was in den "Löchern" noch geht. Das erste Loch wird zurückgegeben, wenn aTrue ist, das zweite ist, was zurückgegeben wird, wenn es False wird.

Um herauszufinden, wie diese Löcher zu füllen, lassen Sie uns die Wahrheitstabelle für schreiben, was wir versuchen zu definieren:

a  | b | eq a b 
------+-------+--------- 
True | True | True 
True | False | False 
False | True | False 
False | False | True 

Beachten Sie, dass an den beiden Zeilen, in denen aTrue ist, die a == b Spalte das ist genau wie die b Spalte. Wenn also aTrue ist, geben wir einfach b zurück. So können wir in einem der Löcher füllen:

eq = \a b. a b ____ 

nun in der Tabelle feststellen, dass, wenn aFalse ist, a == b ist das Gegenteil der b Säule, so dass in diesem Fall wir b umkehren sollte, und es zurückgeben.

Um b zu invertieren, wollen wir, dass es False ist, wenn bTrue ist und umgekehrt. Bei der Codierung, das heißt:

b False True 

Und das ist, was wir zurückkommen sollen, wenn aFalse ist, so füllen wir in dem anderen Loch:

eq = \a b. a b (b False True) 

Jetzt nur entrollen wir die Definitionen von False und True

eq = \a b. a b (b (\x y. y) (\x y. x)) 

Und da haben Sie es.

Answer 2

Lassen Sie uns zunächst die betreffenden Funktionen mit den tatsächlichen Datentypen schreiben (aber keine Pattern-Matching: nur if/then/else):

data Bool = False | True -- recall this definition 
not a = if a then False else True 
eq a b = if a then (if b then True else False) 
       else (if b then False else True) 
nand a b = if a then (if b then False else True) 
       else (if b then True else True) 

Wenn Sie diese Definitionen kaufen - die ganz einfach sind, Listen Sie nur die Wahrheitstabellen der Funktionen auf - dann können wir anfangen, einige Schlussfolgerungen zu ziehen.

eq a b = if a then b else not b 
nand a b = if a then not b else True 

Und jetzt sind wir im Grunde getan: Erstens können wir die äußeren Zweige der eq und nand Funktionen ein wenig vereinfachen. Wir ersetzen nur jeden False und True mit ihrem if/then/else Verhalten und jeden if/then/else mit Funktionsanwendung ersetzen:

type Bool a = a -> a -> a 
false a b = a -- `if False then a else b` becomes `false a b` 
true a b = b -- `if True then a else b` becomes `true a b` 

not a = a false true -- from `if a then False else True` 
eq a b = a b (not b) -- from `if a then b else not b` 
nand a b = a (not b) true -- from `if a then not b else True` 

Dies sind die in Ihren Lösungen Definitionen, obwohl zugegebenermaßen in Haskell Syntax eher als Lambda-Kalkül-Syntax.