¿Es el cálculo lambda fundamentalmente imposible de explicar clara y completamente?

Answer 1

Dependiendo de lo completo que lo desee, el cálculo lambda podría explicarse con un ejemplo en unos minutos a cualquiera que haya usado la notación f (x):

Normalmente dirías algo como: [math] f (x) = x ^ 2 + x + 1 [/ math]
Saque esos corchetes: [math] f \ x = x ^ 2 + x + 1 [/ math]
Mueva la x como un parámetro lambda (no se ha explicado aún): [math] f = \ lambda xx ^ 2 + x + 1 [/ math]
[math] f [/ math] es una función, también lo es [math] \ lambda xx ^ 2 + x + 1 [/ math]
Haz un ejemplo: [math] f \ 6 [/ math]
Sustituye en [math] f = \ lambda xx ^ 2 + x + 1 [/ math], dando: [math] (\ lambda xx ^ 2 + x + 1) \ 6 [/ math]
Para evaluar, mire a la izquierda [math] \ lambda [/ math] y la variable a su lado ([math] x [/ math]).
Reemplace [math] x [/ math] con [math] 6 [/ math], y elimine la parte [math] \ lambda [/ math]: [math] 6 ^ 2 + 6 + 1 = 43 [/ math]

Eso es todo lo que necesita saber para usar el cálculo lambda mecánicamente. En el bit sin explicación, envolvimos ambos lados en una abstracción lambda ([math] \ lambda xf \ x = \ lambda xx ^ 2 + x + 1 [/ math]), luego notamos que [math] \ lambda xf \ x = f [/ math]. Esto se puede ver aplicando, digamos, [math] y [/ math] a ambos lados: [math] (\ lambda xf \ x) \ y = f \ y [/ math].

Alguna terminología innecesaria: el último punto habla de la eta-equivalencia: poder envolver [math] f [/ math] en [math] \ lambda xf \ x [/ math], y desempaquetar iff [math] f [/ math La definición de] no depende de [math] x [/ math]. “Aplicar los argumentos”, o “reemplazar [math] x [/ math]”, se llama beta-equivalencia. Finalmente, la equivalencia alfa es simplemente “una rosa con cualquier otro nombre …”: [math] \ lambda xf \ x = \ lambda yf \ y [/ math], iff [math] f [/ math] no es la definición depende de [math] x [/ math] o [math] y [/ math].

Explicación de por qué es Turing-complete es más difícil, pero para cualquier persona familiarizada con Turing-completitud, la existencia de [math] irreducible (\ lambda xx \ x) \ (\ lambda xx \ x) [/ math] (prueba fuera!) hace que se vea lo suficientemente plausible. La codificación de la iglesia (que representa números en el cálculo lambda) hace que se vea aún más plausible.

Answer 2

Todo lo contrario, en realidad: se trata de una estructura simple como vienen. De hecho, diría que es una de las pocas cosas interesantes en CS que puede explicar clara y completamente en una sola hoja de papel.

El cálculo Lambda solo tiene tres construcciones: variables (como x o y ), aplicaciones de función (como E₁E₂ ) y lambdas: λx.E. Aquí E es cualquier expresión de cálculo lamba. En última instancia, lo único que podemos hacer es escribir o aplicar funciones.

Dada una expresión compuesta de estas construcciones, tenemos algunas “reglas de reducción”, por lo que podemos simplificar una expresión.

La regla más importante es que podemos aplicar lambdas a otras expresiones. Si vemos (λx.E) E ‘ –a lambda aplicada a una expresión, podemos simplificarla a E con cada aparición de x reemplazada por E’ .

Como ejemplo simple, si tenemos (λx.xx) (λy.y) , podemos aplicar la función para obtener: (λy.y) (λy.y) y luego aplicarla para obtener solo λy.y. Y eso es todo lo que podemos hacer.

Hay un par de otras reglas. Una de ellas es que el nombre real de una variable no importa: puede cambiar el nombre de una variable dentro de una función sin cambiarla siempre y cuando no oculte ninguna variable existente.

La regla final es que puede “cancelar” un lambda si todo lo que está haciendo es llamar a otra función. Es decir, λx. (Fx) es exactamente lo mismo que f siempre y cuando f no dependa de x .

El único bit difícil es tratar con nombres que se superponen, e incluso eso es sencillo: cuando introduces dos variables con el mismo nombre, la interna tiene prioridad. Así que en λx. (Λx.x) , la tercera x se refiere a la segunda.