Consulta Booleans en cálculo lambda

Question

Esta es la representación lambda cálculo para el operador AND:

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

Puede alguien me ayuda en la comprensión de esta representación?

Answer 1

Para entender cómo representar booleanos en el cálculo lambda, que ayuda a pensar en un IF expresión, "si A entonces B otra cosa c". Esta es una expresión que elige la primera rama, b, si bien es cierto, y el segundo, c, si es falso. Las expresiones lambda pueden hacerlo muy fácilmente:

lambda(x).lambda(y).x

le dará la primera de sus argumentos, y

lambda(x).lambda(y).y

le da la segunda. Así que si a es una de esas expresiones, a continuación,

a b c

da ya sea b o c, que es justo lo que queremos que el SI a hacer. Así definir

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

y a b c se comportará como if a then b else c.

Mirando dentro de su expresión en (n a b), que los medios if n then a else b. Luego medios m (n a b) b

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

Esta expresión se evalúa como a si ambos m y n son true, y para b lo contrario. Desde a es el primer argumento de la función y b es el segundo, y true se ha definido como una función que da la primera de sus dos argumentos, entonces si m y n son tanto true, también lo es toda la expresión. De lo contrario, es false. Y eso es sólo la definición de and!

Todo esto fue inventado por Alonzo Church, quien inventó el cálculo lambda.

Answer 2

En el cálculo lambda, un booleano está representada por una función que toma dos argumentos, uno para el éxito y uno para el fracaso. Los argumentos se llaman continuaciones , debido a que continúan con el resto de la computación; las llamadas booleanos verdaderos de continuación del éxito y las booleanas falsas llamadas de continuación del fallo. Esta codificación se llama la codificación Iglesia, y la idea es que un booleano es muy parecido a una "función if-then-else".

Así que podemos decir

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

donde s es sinónimo de éxito, f es sinónimo de fracaso, y la barra invertida es un lambda ASCII.

Ahora espero que pueda ver dónde va esto. ¿Cómo podemos código and? Bueno, en C podríamos ampliarlo a

n && m = n ? m : false

Sólo se trata de funciones, por lo que

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

Pero, el constructo ternario, cuando codificado en el cálculo lambda, es la aplicación simplemente función, por lo que tenemos

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

Así que finalmente llegamos a

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

Y si renombramos las continuaciones de éxito y fracaso a a y b volvemos a el original

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

Al igual que con otros cálculos en el cálculo lambda, especialmente cuando se utilizan codificaciones Iglesia, a menudo es más fácil de resolver las cosas con las leyes algebraicas y el razonamiento ecuacional, a continuación, convertir a lambdas al final.

Answer 3

En realidad es un poco más que el operador AND. Es la versión del cálculo lambda de if m and n then a else b. Aquí está la explicación:

En lambda cálculo verdadero se representa como una función de tomar dos argumentos * y devolver la primera. Falsa se representa como función tomar dos argumentos * y devolver el segundo.

La función que mostró anteriormente tiene cuatro argumentos *. Desde el aspecto de que M y N se supone que son booleanos y a y b algunos otros valores. Si m es cierto, se evaluará a su primer argumento que es n a b. Esto a su vez evaluar a un si n es verdadera y b si n es falsa. Si m es falsa, se evaluará a su segundo argumento b.

Así que, básicamente, la función devuelve un tanto si myn son verdaderas y B lo contrario.

(*) Donde "tomar dos argumentos" significa "que toman un argumento y que vuelven una función de tomar otro argumento".

Editar en respuesta a su comentario:

and true false como se ve en la página wiki funciona así:

El primer paso es simplemente para reemplazar cada identificador con su definición, es decir (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Ahora se aplica la (λm.λn. m n m) función. Esto significa que cada aparición de m en m n m se reemplaza con el primer argumento ((λa.λb. a)) y cada ocurrencia de N se sustituye con el segundo argumento ((λa.λb. b)). Por lo que tenemos (λa.λb. a) (λa.λb. b) (λa.λb. a). Ahora simplemente aplicamos el (λa.λb. a) función. Puesto que el cuerpo de esta función es simplemente una, es decir, el primer argumento, este evalúa a (λa.λb. b), es decir false (como medios λx.λy. y false).