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…