Are a few hundred reduction steps too many to get the normal form of Y fac ⌜3⌝? As I have been teaching the basis of λ-calculus lately, I have implemented a simple λ-calculus evaluator in Common Lisp. When I ask the normal form of Y fac 3 in normal-order reduction, it takes 619 steps, which seemed a bit much.

Of course, each time I did similar reductions on paper, I never used the untyped λ-calculus, but added numbers and functions operating on them. In this case, fac is defined as such:

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


In this case, considering =, * and - as currying functions, it only take approximately 50 steps to get Y fac 3 to its normal form 6.

But in my evaluator, I used the following:

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)


In 619 steps, I get from Y fac ⌜3⌝ to the normal form of ⌜6⌝, namely λf.λx.f (f (f (f (f (f x))))).

From a quick skimming of the many steps, I guess it's the definition of pred that warrants such a long reduction, but I still wonder if it just may be a big nasty bug in my implementation...

EDIT: I initially asked about a thousand steps, some of a which were indeed caused a incorrect implementation of the normal order, so I got down to 2/3 of the initial number of steps. As commented below, with my current implementation, switching from Church to Peano arithmetic actually increases the number of steps…
Church coding is really bad if you want to use pred.
I would advise you to use some more efficient coding in Peano style:


// arithmetics

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

// numbers

: 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
...


This is some code taken from one of my old libraries, and μ!f. … was just an optimized construction for Y (λf. …). (And tt, ff, not are booleans.)

I'm not really sure you would obtain better results for fac though.