9
$\begingroup$

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…

$\endgroup$

2 Answers 2

11
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ 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… $\endgroup$ Jul 25, 2011 at 2:41
  • $\begingroup$ 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. $\endgroup$ Jul 25, 2011 at 13:37
  • 1
    $\begingroup$ 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. $\endgroup$ Jul 25, 2011 at 16:22
  • 1
    $\begingroup$ 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). $\endgroup$ Jul 25, 2011 at 20:19
  • 1
    $\begingroup$ computing factorial when numbers are encoded as unary is probably going to take exponentially more steps than when they are coded as binary, recursion on binary notation is exponentially faster than usual unary recursion. $\endgroup$
    – Kaveh
    Jul 30, 2011 at 4:18
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.