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 3
normal 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 3
a 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 pred
que 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 ...
fuente
Y
parece crucial aquí (especialmente para los números de Peano) para obtener reducciones cortas.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.
fuente