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

• Thanks for the tip, working with this alternate encoding helped me find a few bugs in my implementation. Actually, it doesn't help for the number of steps, because after fixing, finding the normal form of 3! takes 619 steps with Church numerals and 687 with Peano numerals… – Nowhere man Jul 25 '11 at 2:41
• Yes, that's what I thought, because using some special reduction rule for Y seems crucial here (especially for Peano numerals) to obtain short reductions. – Stéphane Gimenez Jul 25 '11 at 13:37
• Just curious, what about 4!, 5!, 6! ? – Stéphane Gimenez Jul 25 '11 at 13:52
• Strangely enough, after 3!, Peano encoding becomes more efficient that Church encoding. To get the normal form of respectively 1!, 2!, 3!, 4! and 5! with Peano/Church, it takes 10/10, 40/33, 157/134, 685/667, 3541/3956 and 21629/27311 steps. Approximating the number of steps for 6! by interpolating from the previous data is left as an exercise for the reader. – Nowhere man Jul 25 '11 at 16:22
• It seems that the above-mentioned are precisely the Scott numerals "Peano+λ=Scott". Something else that would be worth trying is their binary variants (both for Church and <strike>Peano</strike> Scott). – Stéphane Gimenez Jul 25 '11 at 20:19

If I think about how many things a CPU does to compute the factorial of 3, say in Python, then a few hundred reductions are not a big deal at all.