lambda calculus - que - Pasos de reducción de la función predecesora del cálculo lambda
lambda significado (4)
Me estoy quedando estancado con la descripción de Wikipedia de la función predecesora en el cálculo lambda.
Lo que Wikipedia dice es lo siguiente:
PRED: = λnfx.n (λgh.h (gf)) (λu.x) (λu.u)
¿Puede alguien explicar los procesos de reducción paso a paso?
Gracias.
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). Usaré un ejemplo.
En primer lugar, me gustaría agregar algunos paréntesis a la definición que me aclaró todo. Vamos a redefinir la fórmula dada para:
PRED := λn λf λx.(n (λgλh.h (g f)) (λu.x)) (λu.u)
También definamos tres números de la Iglesia que 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)
Para entender cómo funciona esto, concentrémonos primero 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 de Iglesia, la función a aplicar es λgλh.h (gf) y los datos iniciales son λu.x
Con esto en mente, probemos un ejemplo:
PRED Three := λf λx.(Three (λgλh.h (g f)) (λu.x)) (λu.u)
Centrémonos primero en la reducción del número (la parte que explicamos antes):
Three (λgλh.h (g f)) (λu.x)
Lo 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)))
Terminando con:
λh.h f (f x)
Entonces tenemos:
PRED Three := λf λx.(λh.h (f (f x))) (λu.u)
Reduciendo de nuevo:
PRED Three := λf λx.((λu.u) (f (f x)))
PRED Three := λf λx.f (f x)
Como puede ver en las reducciones, terminamos aplicando la función una vez menos gracias a una forma inteligente de usar las funciones.
Usando add1 como f y 0 como x , obtenemos:
PRED Three add1 0 := add1 (add1 0) = 2
Espero que esto ayude.
La respuesta de McCann lo explica bastante bien. Tomemos un ejemplo concreto para Pred 3 = 2:
Considere la expresión: n (λgh.h (gf)) (λu.x). Sea K = (λgh.h (gf))
Para n = 0, codificamos 0 = λfx.x , de modo que cuando aplicamos la reducción beta para (λfx.x)(λgh.h(gf)) medios (λgh.h(gf)) se reemplazan 0 veces. Después de una mayor reducción beta obtenemos:
λfx.(λu.x)(λu.u)
reduce a
λfx.x
donde λfx.x = 0 , como se esperaba.
Para n = 1, aplicamos K por 1 vez:
(λgh.h (gf)) (λu.x) => λh. h((λu.x) f) => λh. hx
Para n = 2, aplicamos K por 2 veces:
(λgh.h (gf)) (λh. hx) => λh. h ((λh. hx) f) => λh. h (fx)
Para n = 3, aplicamos K por 3 veces:
(λgh.h (gf)) (λh. h (fx)) => λh.h ((λh. h (fx)) f) => λh.h (f (fx))
Finalmente, tomamos este resultado y le aplicamos una función de identificación, obtenemos
λh.h (f (fx)) (λu.u) => (λu.u)(f (fx)) => f (fx)
Esta es la definición del número 2.
La implementación basada en listas puede ser más fácil de entender, pero toma muchos pasos intermedios. Por lo tanto, no es tan agradable como la implementación original de la Iglesia, IMO.
Ok, entonces la idea de los números de la Iglesia es codificar "datos" usando funciones, ¿verdad? La forma en que funciona es representando un valor por alguna operación genérica que realizarías con él. Por lo tanto, también podemos ir en la otra dirección, lo que a veces puede aclarar las cosas.
Los números de la iglesia son una representación unaria de los números naturales. Entonces, usemos Z para significar cero y Sn para representar el sucesor de n . Ahora podemos contar de esta manera: Z , SZ , SSZ , SSSZ ... El número equivalente de Iglesia toma dos argumentos: el primero corresponde a S y el segundo a Z usa para construir el patrón anterior. Entonces, dados los argumentos f y x , podemos contar de esta manera: x , fx , f (fx) , f (f (fx)) ...
Veamos lo que hace PRED.
Primero, crea un lambda tomando tres argumentos: n es el número de la Iglesia cuyo predecesor queremos, por supuesto, lo que significa que f y x son los argumentos del número resultante, lo que 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 (gf) . Podemos reescribir esto como λg. (λh.h (gf)) λg. (λh.h (gf)) para reflejar el hecho de que solo la lambda más externa se aplica n veces. Lo que hace esta función es llevar el resultado acumulado hasta g y devolver una nueva función tomando un argumento, que aplica ese argumento a g aplicado a f . Lo que es absolutamente desconcertante, por supuesto.
Entonces ... ¿qué está pasando aquí? Considere la sustitución directa con S y Z En un número no nulo Sn , la n corresponde al argumento vinculado a g . Entonces, recordando que f y x están vinculados en un ámbito externo, podemos contar de esta manera: λu.x , λh. h ((λu.x) f) λh. h ((λu.x) f) , λh''. h'' ((λh. h ((λu.x) f)) f) λh''. h'' ((λh. h ((λu.x) f)) f) ... Realizando las reducciones obvias, obtenemos esto: λu.x , λh. hx λh. hx , λh''. h'' (fx) λh''. h'' (fx) ... El patrón aquí es que una función se está pasando "hacia adentro" de una capa, en cuyo punto una S aplicará, mientras que una Z ignorará. Entonces obtenemos una aplicación de f para cada S excepto la más externa.
El tercer argumento es simplemente la función de identidad, que se aplica diligentemente por la S más externa, devolviendo el resultado final: se aplica una vez menos que la cantidad de S capas a las que corresponde n .
Puede intentar comprender esta definición de la función predecesora (no la mía favorita) en términos de continuaciones.
Para simplificar un poco el tema, consideremos la siguiente variante
PRED := λn.n (λgh.h (g S)) (λu.0) (λu.u)
entonces, puedes reemplazar S con 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 solo devuelve 0. Llamemos a N el 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. Toma en la entrada una continuación h, y la aplica al resultado de continuar el cálculo actual g con S.
Como 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.