¿Son demasiados cientos de pasos de reducción demasiados para obtener la forma normal de Y fac ⌜3⌝?

9

Como he estado enseñando la base del cálculo λ últimamente, he implementado un simple evaluador de cálculo λ en Common Lisp. Cuando pregunto la forma Y fac 3normal de reducción de orden normal, se requieren 619 pasos, lo que me pareció un poco demasiado.

Por supuesto, cada vez que hice reducciones similares en el papel, nunca usé el cálculo λ sin tipo, pero agregué números y funciones que operan en ellos. En este caso, fac se define como tal:

fac = λfac.λn.if (= n 0) 1 (* n (fac (- n 1)))

En este caso, teniendo en cuenta =, *y -como currying funciones, sólo toma unos 50 escalones para llegar Y fac 3a su forma normal 6.

Pero en mi evaluador, utilicé lo siguiente:

true = λx.λy.x
false = λx.λy.y
⌜0⌝ = λf.λx.x
succ = λn.λf.λx.f n f x
⌜n+1⌝ = succ ⌜n⌝
zero? = λn.n (λx.false) true
mult = λm.λn.λf.m (n f)
pred = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
fac = λfac.λn.(zero? n) ⌜1⌝ (* n (fac (pred n)))
Y = λf.(λf.λx.f (x x)) f ((λf.λx.f (x x)) f)

En 619 pasos, llego Y fac ⌜3⌝a la forma normal de ⌜6⌝, a saber λf.λx.f (f (f (f (f (f x))))).

Supongo que es una definición rápida de los muchos pasos, lo predque justifica una reducción tan larga, pero aún me pregunto si puede ser un gran error desagradable en mi implementación ...

EDITAR: Inicialmente pregunté acerca de mil pasos, algunos de los cuales de hecho causaron una implementación incorrecta del orden normal, así que obtuve 2/3 del número inicial de pasos. Como se comenta a continuación, con mi implementación actual, cambiar de la aritmética de Church a Peano en realidad aumenta el número de pasos ...

Hombre de ningún lado
fuente

Respuestas:

11

La codificación de la iglesia es realmente mala si quieres usarla pred. Le aconsejaría que use una codificación más eficiente en estilo Peano:

// aritmética

: p_zero = λs.λz.z
: p_one = λs.λz.s p_zero
: p_succ = λn.λs.λz.sn
: p_null = λn.n (λx. ff) tt
: p_pred = λn.n (λp.p) p_zero
: p_plus = μ! f.λn.λm.n (λp. p_succ (! fpm)) m
: p_subs = μ! f.λn.λm.n (λp. p_pred (! fpm)) m
: p_eq = μ! f.λm.λn. m (λp. n (λq.! fpq) ff) (n (λx.ff) tt)
: p_mult = μ! f.λm.λn. m (λp. p_plus n (! fpn)) p_zero
: p_exp = μ! f.λm.λn. m (λp. p_mult n (! fpn)) p_one
: p_even = μ! f.λm. m (λp. no (! fp)) tt

// números

: p_0 = λs.λz.z
: p_1 = λs.λz.s p_0
: p_2 = λs.λz.s p_1
: p_3 = λs.λz.s p_2
...

Este es un código tomado de una de mis viejas bibliotecas, y μ!f. …fue solo una construcción optimizada para Y (λf. …). (Y tt, ff, notson booleanos.)

Sin facembargo, no estoy realmente seguro de que obtenga mejores resultados .

Stéphane Gimenez
fuente
Gracias por el consejo, trabajar con esta codificación alternativa me ayudó a encontrar algunos errores en mi implementación. En realidad, no ayuda para la cantidad de pasos, porque después de arreglarlo, ¡encuentra la forma normal de 3! da 619 pasos con números de la Iglesia y 687 con números de Peano ...
Nowhere man
Sí, eso es lo que pensé, porque usar alguna regla de reducción especial Yparece crucial aquí (especialmente para los números de Peano) para obtener reducciones cortas.
Stéphane Gimenez
Por curiosidad, ¿qué pasa con 4 !, 5 !, 6! ?
Stéphane Gimenez
1
Por extraño que parezca, después de 3 !, la codificación de Peano se vuelve más eficiente que la codificación de Church. Para obtener la forma normal de respectivamente 1 !, 2 !, 3 !, 4! y 5! con Peano / Church, toma 10/10, 40/33, 157/134, 685/667, 3541/3956 y 21629/27311 pasos. ¡Aproximando el número de pasos para 6! al interpolar a partir de los datos anteriores se deja como ejercicio para el lector.
Nowhere man
1
Parece que los mencionados anteriormente son precisamente los números de Scott "Peano + λ = Scott". Otra cosa que valdría la pena probar son sus variantes binarias (tanto para Church como para <strike> Peano </strike> Scott).
Stéphane Gimenez
2

Si pienso en cuántas cosas hace una CPU para calcular el factorial de 3, digamos en Python, entonces unos cientos de reducciones no son un gran problema.

Andrej Bauer
fuente