Algumas centenas de etapas de redução são demais para obter a forma normal de Y fac ⌜3⌝?

Como tenho ensinado as bases do cálculo λ ultimamente, implementei um avaliador simples do cálculo λ no Common Lisp. Quando pergunto a forma Y fac 3normal de redução na ordem normal, são necessários 619 passos, o que parecia um pouco demais.

Obviamente, toda vez que fazia reduções semelhantes no papel, nunca usava o cálculo λ não tipado, mas adicionava números e funções operando neles. Nesse caso, fac é definido como tal:

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

Neste caso, considerando-se =, *e -como currying funções, só demorar cerca de 50 passos para chegar Y fac 3à sua forma normal 6.

Mas no meu avaliador, usei o seguinte:

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)

Em 619 etapas, chego Y fac ⌜3⌝à forma normal de ⌜6⌝, a saber λf.λx.f (f (f (f (f (f x))))).

A partir de uma rápida verificação das muitas etapas, acho que é a definição predque justifica uma redução tão longa, mas ainda me pergunto se isso pode ser um grande bug desagradável na minha implementação ...

EDIT: Inicialmente, perguntei cerca de mil etapas, algumas das quais realmente causaram uma implementação incorreta da ordem normal, então reduzi para 2/3 do número inicial de etapas. Como comentado abaixo, com minha implementação atual, a mudança da aritmética da Igreja para a Peano realmente aumenta o número de etapas…

A codificação da igreja é muito ruim se você quiser usar pred. Aconselho você a usar uma codificação mais eficiente no 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. não (! 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 é um código retirado de uma das minhas bibliotecas antigas e μ!f. …foi apenas uma construção otimizada para Y (λf. …). (E tt, ff, notsão booleans.)

Não tenho muita certeza de que você obteria melhores resultados para isso fac.

Se eu pensar em quantas coisas uma CPU faz para calcular o fatorial de 3, digamos em Python, então algumas centenas de reduções não são um grande problema.