Me estoy quedando atrapado con la descripción de Wikipedia de la función predecesora en cálculo lambda.Función predecesora de cálculo lambda pasos de reducción
Lo que dice la Wikipedia es la siguiente:
PRED: = λnfx.n (λgh.h (gf)) (λu.x) (λu.u)
Puede alguien explicar los procesos de reducción de paso- ¿Por paso?
Gracias.
Ok, entonces la idea de Números de la Iglesia es codificar "datos" usando funciones, ¿verdad? La forma en que funciona es mediante la representación de un valor mediante alguna operación genérica que realizaría con él. Por lo tanto, podemos ir en la otra dirección, lo que a veces puede aclarar las cosas.
Los numerales de las iglesias son una representación unaria de los números naturales. Entonces, usemos Z para significar cero y Sn para representar al sucesor de n. Ahora podemos contar de esta manera: Z, SZ, SSZ, SSSZ ... El número equivalente Iglesia toma dos argumentos - la primera corresponde a S, y la segunda a Z --¡entonces los utiliza para construir el patrón anterior. Así que da argumentos f y x, podemos contar de esta manera: x, f x, f (f x), f (f (f x)) ...
Veamos lo que hace PRED.
En primer lugar, se crea un lambda teniendo tres arguments-- n está el numeral Iglesia cuyo predecesor que queremos, por supuesto, lo que significa que f y x son los argumentos a la cifra resultante, que de este modo significa que el cuerpo de esa lambda será f aplicado a x una vez menos que n.
A continuación, se aplica n a tres argumentos. Esta es la parte difícil.
El segundo argumento, que corresponde a Z de antes, es λu.x --una función constante que ignora un argumento y devuelve x.
El primer argumento, que corresponde a S de antes, es λgh.h (g f). Podemos reescribir esto como λg. (λh.h (g f)) para reflejar el hecho de que solo se está aplicando el lambda externo n veces. Lo que hace esta función es tomar el resultado acumulado hasta g y devolver una nueva función tomando un argumento, que aplica ese argumento al g aplicado a f. Lo cual es absolutamente desconcertante, por supuesto.
Entonces ... ¿qué está pasando aquí? Considere la sustitución directa con S y Z. En un número distinto de cero Sn, el n corresponde al argumento vinculado a g. Así, recordando que f y x están unidos en un ámbito exterior, podemos contar de esta manera: λu.x, λh. h ((λu.x) f), λh'. h' ((λh. h ((λu.x) f)) f) ... Realización de las reducciones evidentes, obtenemos lo siguiente: λu.x, λh. h x, λh'. h' (f x) ...El patrón aquí es que una función se pasa "hacia adentro" una capa, en cuyo punto se aplicará un S, mientras que Z la ignorará. Entonces obtenemos una aplicación de f para cada Sexcepto la más externa.
El tercer argumento es simplemente la función identidad, que se aplica debidamente por la más externa S, devolviendo el result-- final de f aplica uno menos veces que el número de capas Sn corresponde a.
+1 por la importante percepción de que "el cuerpo de esa lambda será 'f' aplicado a' x' una vez menos que 'n' would." Pero cómo logra este objetivo todavía está más allá de mi descripción. Probablemente sería útil agregar algunas más abstracciones a esta fórmula, resumiendo las ideas en un nivel un poco más alto. Por ejemplo, reemplazando ese 'Lu.u' con' I', la función de Identidad. Y tal vez algunos otros también. Vi una explicación interesante aquí: http://www.mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/index.html que descifra estas lambdas como operaciones de lista (contras, auto, cdr). – SasQ
Creo que la versión de la lista termina siendo una implementación diferente y más elaborada, aunque más fácil de entender. La definición del predecesor aquí es realmente difícil de comprender, y la mejor manera de ver cómo funciona podría ser hacer un recorrido por la evaluación de forma manual para tener una idea de lo que está sucediendo. –
La respuesta de McCann lo explica bastante bien. Tomemos un ejemplo concreto para Pred 3 = 2:
Considere la expresión: n (λgh.h (g f)) (λu.x). Sea K = (λgh.h (g f))
Para n = 0, codificamos 0 = λfx.x, así que cuando se aplica la reducción beta para (λfx.x)(λgh.h(gf)) significa (λgh.h(gf)) se sustituye 0 veces. Después de una nueva beta-reducción se obtiene:
λfx.(λu.x)(λu.u)
reduce a
λfx.x
donde λfx.x = 0, como se esperaba.
Para n = 1, aplicamos K para 1 veces:
(λgh.h (g f)) (λu.x) => λh. h((λu.x) f) => λh. h x
Para n = 2, aplicamos K por 2 veces:
(λgh.h (g f)) (λh. h x) => λh. h ((λh. h x) f) => λh. h (f x)
Para n = 3 , aplicamos K por 3 veces:
(λgh.h (g f)) (λh. h (f x)) => λh.h ((λh. h (f x)) f) => λh.h (f (f x))
Por último, tomamos este resultado y aplicar una función de identificación a la misma, llegamos
λh.h (f (f x)) (λu.u) => (λu.u)(f (f x)) => f (f x)
Ésta es la definición del número 2.
La lista implementación basada podría ser más fácil de entender, pero toma muchos pasos intermedios. Por lo tanto, no es tan agradable como la OMI de implementación original de la Iglesia.
No entiendo cómo se obtiene de "Para n = tantas veces aplicamos K tantas y tantas veces" a cada una de las primeras líneas de las derivaciones. – Zelphir
Sí, no está explícitamente indicado; pero viene del término 'f' en un numeral. Por ejemplo, 2 se define como 'λfx.f (fx)'. Entonces eso significa que cuando la reducción beta se realiza para '(λfx.f (fx)) (λgh.h (g f))' la función '(λgh.h (g f))' se aplica dos veces. – Greg
Puede intentar comprender esta definición de la función predecesora (no mi favorita) en términos de continuación.
Para simplificar el asunto un poco, consideremos el siguiente variante
PRED := λn.n (λgh.h (g S)) (λu.0) (λu.u)
a continuación, se puede reemplazar con S f, y 0 con x.
El cuerpo de la función itera n veces una transformación M sobre un argumento N. El argumento N es una función de tipo (nat -> nat) -> nat que espera una continuación para nat y devuelve un nat. Inicialmente, N = λu.0, es decir, ignora la continuación y simplemente devuelve 0. Llamemos N al cálculo actual.
La función M: (nat -> nat) -> nat) -> (nat -> nat) -> nat modifica el cálculo g: (nat -> nat) -> nat de la siguiente manera. Se toma en entrada una continuación h, y la aplica al resultado de continuar el cálculo g actual con S.
Desde el cálculo inicial ignoró la continuación, después de una aplicación de M obtenemos el cálculo (λh.h 0), luego (λh.h (S 0)), y así sucesivamente.
Al final, aplicamos el cálculo a la continuación de identidad para extraer el resultado.
Después de leer las respuestas anteriores (buenas), me gustaría dar mi propia visión del asunto con la esperanza de que ayude a alguien (las correcciones son bienvenidas). Voy a usar un ejemplo.
En primer lugar, me gustaría agregar algunos paréntesis a la definición que me aclararon todo. Vamos a redifine la fórmula dada a:
PRED := λn λf λx.(n (λgλh.h (g f)) (λu.x)) (λu.u)
También vamos a definir tres números de la Iglesia que le ayudarán con el ejemplo:
Zero := λfλx.x
One := λfλx. f (Zero f x)
Two := λfλx. f (One f x)
Three := λfλx. f (Two f x)
Con el fin de entender cómo funciona esto, vamos a centrarnos en primer lugar en esta parte de la fórmula:
n (λgλh.h (g f)) (λu.x)
a partir de aquí, podemos extraer estas conclusiones: n es un número Iglesia, la función que debe aplicarse es λgλh.h (g f) y los datos de partida es λu.x
Con esto en mente, vamos a probar un ejemplo:
PRED Three := λf λx.(Three (λgλh.h (g f)) (λu.x)) (λu.u)
Vamos a centrarnos primero en la reducción del número (la parte explicamos anteriormente):
Three (λgλh.h (g f)) (λu.x)
que se reduce a:
(λgλh.h (g f)) (Two (λgλh.h (g f)) (λu.x))
(λgλh.h (g f)) ((λgλh.h (g f)) (One (λgλh.h (g f)) (λu.x)))
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (Zero (λgλh.h (g f)) (λu.x))))
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) ((λfλx.x) (λgλh.h (g f)) (λu.x)))) -- Here we lose one application of f
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (λu.x)))
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h ((λu.x) f)))
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h x))
(λgλh.h (g f)) (λh.h ((λh.h x) f))
(λgλh.h (g f)) (λh.h (f x))
(λh.h ((λh.h (f x) f)))
Terminar el ingenio h:
λh.h f (f x)
Así, tenemos:
PRED Three := λf λx.(λh.h (f (f x))) (λu.u)
Reducción de nuevo:
PRED Three := λf λx.((λu.u) (f (f x)))
PRED Three := λf λx.f (f x)
Como se puede ver en las reducciones, que terminan aplicando la función de una sola vez menos gracias a una forma inteligente de usar funciones.
Uso add1 como f y 0 como x, obtenemos:
PRED Three add1 0 := add1 (add1 0) = 2
Espero que esto ayude.
La notación lambda es difícil de seguir, así que he hecho reducciones paso a paso con las expresiones S utilizando Clojure para '(pred zero)', '(pred one)' y '(pred two)' y [lo publicó en Github.] (https://github.com/abiro/church-encoding/blob/master/src/church_encoding/pred_reductions.clj) –