Abfrage Boolesche Werte in Lambda-Kalkül

Question

Dies ist die Lambda-Kalkül Darstellung für den AND-Operator:

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b

Kann mir jemand helfen diese Darstellung zu verstehen?

Answer 1

Um zu verstehen, wie darzustellen Boolesche Werte in Lambda-Kalkül, hilft es, über eine IF-Ausdruck zu denken, „wenn ein dann b sonst c“. Dies ist ein Ausdruck, der den ersten Zweig, b wählt, wenn es wahr ist, und die zweite, c, wenn es falsch ist. Lambda-Ausdrücke kann das tun sehr einfach:

lambda(x).lambda(y).x

wird Ihnen das erste seiner Argumente und

lambda(x).lambda(y).y

haben Sie die zweite. Also, wenn ein ist einer jener Ausdrücke, dann

a b c

gibt entweder b oder c, die genau das, was wir die IF tun wollen. So definieren

 true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y

und a b c wird wie if a then b else c verhalten.

Suchen Sie in Ihrem Ausdruck bei (n a b), dass Mittel if n then a else b. Dann m (n a b) b Mittel

if m then (if n then a else b) else b

Dieser Ausdruck ergibt a wenn beide m und n true sind, und sonst b. Da a das erste Argument Ihrer Funktion und b ist, ist die zweite, und true als Funktion definiert, die die erste ihrer zwei Argumente gibt, dann, wenn m und n beide true sind, so dass der ganze Ausdruck ist. Ansonsten ist es false. Und das ist nur die Definition von and!

All dies wurde erfunden von Alonzo Church, der das Lambda-Kalkül erfunden.

Answer 2

In dem Lambda-Kalkül wird ein Boolean durch eine Funktion dargestellt, die zwei Argumente übernehmen, einen für Erfolg und einen für das Scheitern. Die Argumente werden genannt Fortsetzungen , weil sie mit dem Rest der Berechnung fortzusetzen; die boolean True, fordert der Erfolg Fortsetzung und die Booleschen falsche Anrufe der Ausfall Fortsetzung. Diese Codierung ist die Kirche Codierung genannt, und die Idee ist, dass ein Boolean ist sehr ähnlich wie eine „if-then-else-Funktion“.

So können wir sagen,

true  = \s.\f.s
false = \s.\f.f

Dabei gilt s für Erfolg steht, f für das Scheitern steht, und der Backslash ist eine ASCII-Lambda.

Jetzt hoffe ich, man kann sehen, wohin dieses geht. Wie können wir Code and? Nun, in C konnten wir es zu

erweitern

n && m = n ? m : false

Nur diese sind Funktionen, so

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f

ABER, das ternäre Konstrukt, wenn es in der Lambda-Kalkül codiert, ist nur Funktionsanwendung, also haben wir

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f

So endlich kommen wir zu

&& = \n . \m . \s . \f . n (m s f) f

Und wenn wir die Erfolge und Misserfolge Fortsetzungen zu a umbenennen und b wir zu Ihrem ursprünglichen zurückkehren

&& = \n . \m . \a . \b . n (m a b) b

Wie bei anderen Berechnungen in Lambda-Kalkül, vor allem, wenn Kirche Kodierungen verwenden, ist es oft einfacher, Arbeit Dinge mit algebraischen Gesetzen und equational Argumentation, wandelt dann lambdas am Ende.

Answer 3

Eigentlich ist es ein wenig mehr als nur der AND-Operator. Es ist die Version von if m and n then a else b Lambda-Kalkül. Hier ist die Erklärung:

In Lambda-Kalkül wahr als eine Funktion nimmt zwei Argumente dargestellt wird * und die erste Rückkehr. Falsch wird dargestellt als Funktion nimmt zwei Argumente * und Rückführen der zweiten.

Die Funktion, die Sie oben zeigte nimmt vier Argumente *. Von den Blicken von ihm m und n soll booleans und a und b einige andere Werte. Wenn m wahr ist, wird es das erste Argument zu bewerten, die n a b ist. Dies wiederum wird zu einem bewerten, wenn n wahr und b ist, wenn n falsch ist. Wenn m falsch ist, wird es in seinem zweiten Argumente b bewerten.

Also im Grunde die Funktion gibt ein, wenn sowohl m und n wahr und b sonst.

(*) Wo „nimmt zwei Argumente“ bedeutet „ein Argument zu nehmen und eine Funktion, die ein anderes Argument zurückkehrt“.

In Antwort auf Ihren Kommentar:

and true false wie auf der Wiki-Seite gesehen funktioniert wie folgt:

Der erste Schritt ist einfach jede Kennung mit ihrer Definition zu ersetzen, d.h. (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Nun wird die Funktion (λm.λn. m n m) angewendet. Dies bedeutet, dass jedes Vorkommen von m in m n m mit dem ersten Argumente ((λa.λb. a)) und jedes Auftreten von n ersetzt wird, wird mit dem zweiten Argumente ((λa.λb. b)) ersetzt. So bekommen wir (λa.λb. a) (λa.λb. b) (λa.λb. a). Nun wenden wir einfach die Funktion (λa.λb. a). Da der Körper dieser Funktion ist einfach ein, das heißt das erste Argument, diese auswertet, um (λa.λb. b), d.h. false (als λx.λy. y Mittel false).