consulta en Booleanos en cálculo lambda

Question

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

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

¿Alguien puede ayudar a comprender esta representación?

Answer 1

Para comprender cómo representar booleanos en cálculo lambda, ayuda pensar en una expresión IF, "if a then b else c". Esta es una expresión que elige la primera rama, b, si es verdadera, y la segunda, c, si es falsa. 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 al (n a b), que significa if n then a else b. Entonces m (n a b) b significa

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

Esta expresión se evalúa a a si tanto m y n son true, y para b lo contrario. Desde a es el primer argumento de su función y b es el segundo, y true se ha definido como una función que proporciona el primero de sus dos argumentos, entonces si m y n son ambos true, también lo es la expresión completa. De lo contrario, es false. ¡Y esa es solo la definición de and!

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

Answer 2

Actualmente 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 cálculo lambda true se representa como una función tomando dos argumentos * y devolviendo el primero. False se representa como función tomando dos argumentos * y devolviendo el segundo.

La función que mostró anteriormente tiene cuatro argumentos *. Por lo que se ve, m y n se supone que son booleanos y a y b algunos otros valores. Si m es verdadero, evaluará su primer argumento que es n a b. Esto a su vez evaluará aa si n es verdadero yb si n es falso. Si m es falso, evaluará su segundo argumento b.

Así que, básicamente, la función devuelve a si tanto m como n son verdaderas yb de lo contrario.

(*) Donde "tomar dos argumentos" significa "tomar un argumento y devolver una función tomando 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 función (λm.λn. m n m). Esto significa que cada ocurrencia de m en m n m se reemplaza con el primer argumento ((λa.λb. a)) y cada aparición de n se reemplaza con el segundo argumento ((λa.λb. b)). Entonces obtenemos (λa.λb. a) (λa.λb. b) (λa.λb. a). Ahora simplemente aplicamos la función (λa.λb. a). Como el cuerpo de esta función es simplemente a, es decir, el primer argumento, se evalúa como (λa.λb. b), es decir, false (como λx.λy. y significa false).

Answer 3

En el cálculo lambda, un booleano está representado por una función que toma dos argumentos, uno para el éxito y el otro para el fracaso. Los argumentos se llaman continuaciones, porque continúan con el resto del cálculo; el booleano True llama a la continuación del éxito y Boolean False llama a la continuación del error. Esta codificación se llama codificación Church, y la idea es que un Boolean 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 gradas para el fracaso, y la barra invertida es un lambda ASCII.

Ahora espero que puedan ver a dónde va esto. ¿Cómo codificamos and? Bueno, en C podríamos extenderlo a

n && m = n ? m : false 

Sólo se trata de funciones, por lo

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

PERO, la construcción ternaria, cuando se codifica en el cálculo lambda, es sólo función de la aplicació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 razonamiento ecuacional, luego conviértase en lambdas al final.