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 può aiutarmi a capire questa rappresentazione?

Answer 1

Per capire come rappresentare Booleans in lambda calcolo, aiuta a pensare ad un IF espressione, "se un altro allora b 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.

Guardando dentro la vostra espressione a (n a b), la disponibilità di mezzi if n then a else b. Poi mezzi m (n a b) b

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 è stata definita come una funzione che dà il primo dei suoi due argomenti, quindi se m e n sono entrambi true, così è l'intera espressione. Altrimenti è false. E questo è solo la definizione di and!

Il tutto è stato inventato da Alonzo Church, che ha inventato il lambda calcolo.

Answer 2

Nel lambda calcolo, un booleano è rappresentato da una funzione che prende due argomenti, uno per il successo ed uno per il fallimento. Gli argomenti sono chiamate continuazioni , perché continuano con il resto del calcolo; i booleani veri chiamate la continuazione successo e le booleane false chiamate la continuazione fallimento. Questa codifica è chiamata la codifica Chiesa, e l'idea è che un valore booleano è 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 è sinonimo di fallimento, e il backslash è un lambda ASCII.

Ora spero si può vedere dove questo sta andando. Come facciamo a codice and? Ebbene, in C si potrebbe estendere a

n && m = n ? m : false

Solo questi sono funzioni, in modo da

(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, è l'applicazione solo funzione, così abbiamo

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

Così finalmente arriviamo a

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

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

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

Come per altri calcoli in lambda calcolo, soprattutto quando si utilizza codifiche della Chiesa, è spesso più facile per le cose funzionano con le leggi algebriche e il ragionamento equazionale, poi convertire lambda alla fine.

Answer 3

In realtà è un po 'più di un semplice l'operatore AND. E 'la versione del lambda calcolo di if m and n then a else b. Ecco la spiegazione:

In lambda calcolo vero è rappresentato come una funzione prendendo due argomenti * e restituendo il primo. Falso è rappresentata come funzione di prendere due argomenti * e restituendo il secondo.

La funzione che avete mostrato sopra prende quattro argomenti *. Dagli sguardi di esso M e N dovrebbero essere booleani e A e B alcuni altri valori. Se m è vero, valuterà al suo primo argomento che è n a b. Questo a sua volta restituisce una se n è vero e B se n è falsa. Se m è falso, si valuterà al suo secondo argomento b.

Quindi, in pratica la funzione restituisce un se entrambi m e n sono vere e b altrimenti.

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

Modifica in risposta al tuo commento:

and true false come si vede nella pagina wiki funziona in questo modo:

Il primo passo è semplicemente quello di sostituire ogni identificatore con la sua definizione, cioè (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Ora la funzione (λm.λn. m n m) viene applicata. Ciò significa che ogni occorrenza di m m n m viene sostituito con il primo argomento ((λa.λb. a)) e le sequenze di tipo n è sostituito con il secondo argomento ((λa.λb. b)). Così otteniamo (λa.λb. a) (λa.λb. b) (λa.λb. a). Ora abbiamo semplicemente applicare la funzione (λa.λb. a). Poiché il corpo di questa funzione è semplicemente una, cioè il primo argomento, questo restituisce (λa.λb. b), cioè false (come mezzo λx.λy. y false).