Query booleani in lambda calcolo

Question

Questa è la rappresentazione lambda calcolo per l'operatore:

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

Qualcuno mi può aiutare a capire questa rappresentazione?

Answer 1

Per capire come rappresentare le booleane nel calcolo lambda, è utile pensare a un'espressione IF, "se a then b else c". Questa è un'espressione che sceglie il primo ramo, b, se è vero, e il secondo, c, se è falso. espressioni lambda possono farlo molto facilmente:

lambda(x).lambda(y).x 

vi darà il primo dei suoi argomenti, e

lambda(x).lambda(y).y 

ti dà la seconda. Quindi, se a è una di quelle espressioni, quindi

a b c 

dà sia b o c, che è proprio quello che vogliamo l'IF da fare. Quindi definire

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

e a b c si comporterà come if a then b else c.

Guardare dentro la tua espressione a (n a b), che significa if n then a else b. Poi m (n a b) b significa

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

Questa espressione restituisce a se entrambi m e n sono true, e b altrimenti. Poiché a è il primo argomento della funzione e b è il secondo e true è stato definito come una funzione che fornisce il primo dei suoi due argomenti, quindi se m e n sono entrambi true, quindi è l'intera espressione. Altrimenti è false. E questa è solo la definizione di and!

Tutto questo è stato inventato da Alonzo Church, che ha inventato il calcolo lambda.

Answer 2

In realtà è poco più che l'operatore AND. È la versione di lambda calcolo di if m and n then a else b. Ecco la spiegazione:

Nel calcolo lambda true è rappresentato come una funzione che accetta due argomenti * e restituisce il primo. False è rappresentato come funzione che prende due argomenti * e restituisce il secondo.

La funzione visualizzata sopra richiede quattro argomenti *. Dagli sguardi di m e n si suppone che siano booleani e aeb altri valori. Se m è vero, valuterà il suo primo argomento che è n a b. Questo a sua volta valuterà a se n è vero e b se n è falso. Se m è falso, valuterà il suo secondo argomento b.

Quindi in sostanza la funzione restituisce a se sia m che n sono true e b altrimenti.

(*) Dove "prendere due argomenti" significa "prendere un argomento e restituire una funzione prendendo un altro argomento".

Modifica in risposta al tuo commento:

and true false come si vede nella pagina wiki funziona così:

Il primo passo è semplicemente quello di sostituire ogni identificativo con la sua definizione, vale a dire (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Ora viene applicata la funzione (λm.λn. m n m). Ciò significa che ogni occorrenza di m in m n m viene sostituita con il primo argomento ((λa.λb. a)) e ogni occorrenza di n viene sostituita con il secondo argomento ((λa.λb. b)). Quindi otteniamo (λa.λb. a) (λa.λb. b) (λa.λb. a). Ora applichiamo semplicemente la funzione (λa.λb. a). Poiché il corpo di questa funzione è semplicemente un, ovvero il primo argomento, questo viene valutato a (λa.λb. b), ad esempio false (come λx.λy. y significa false).

Answer 3

Nel calcolo lambda, un booleano è rappresentato da una funzione che accetta due argomenti, uno per il successo e uno per il fallimento. Gli argomenti sono chiamati continuazioni , perché continuano con il resto del calcolo; il valore booleano True chiama la prosecuzione del successo e il Falso booleano chiama la continuazione dell'errore. Questa codifica è chiamata codifica della Chiesa, e l'idea è che un booleano sia molto simile a una "funzione if-then-else".

Quindi possiamo dire

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

dove s sinonimo di successo, f stand per il fallimento, e la barra rovesciata è un lambda ASCII.

Ora spero che tu possa vedere dove sta andando. Come si codifica and? Ebbene, in C potremmo espanderla per

n && m = n ? m : false 

Solo questi sono funzioni, così

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

MA, il costrutto ternario, quando codificata nel lambda calcolo, è solo un'applicazione funzionamento, quindi abbiamo

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

Così alla fine si arriva al

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

E se rinominare il continuazioni successo e il fallimento di a e b torniamo al tuo originale

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

Come con altri calcoli in lambda calcolo, soprattutto quando si utilizzano codifiche Chiesa, spesso è più facile far funzionare le cose con le leggi algebriche e ragionamento equo, quindi convertire in lambda alla fine.