<p>Church coding is really bad if you want to use <code>pred</code>.
I would advise you to use some more efficient coding in Peano style:</p>

<pre>
// 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
...
</pre>

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

<p>I'm not really sure you would obtain better results for <code>fac</code> though.</p>

CC BY-SA 3.0
2011-07-25T02:41:43.073Z
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
CC BY-SA 3.0
2011-07-25T13:37:34.523Z
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
CC BY-SA 3.0
2011-07-25T13:52:29.970Z
Just curious, what about 4!, 5!, 6! ?
Stéphane Gimenez
CC BY-SA 3.0
2011-07-25T16:22:44.030Z
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
CC BY-SA 3.0
2011-07-25T19:35:22.693Z
There are also the Scott numerals.
Andrej Bauer
CC BY-SA 3.0
2011-07-25T20:19:33.783Z
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
CC BY-SA 3.0
2011-07-26T15:52:15.950Z
I was about to say that from what I've seen, Scott numerals should be equivalent to Peano numerals in terms of the number of reduction steps, as the definition I took was identical except that s and z (WRT to the notation above) were swapped. So with de Bruijn indexes, from the definition above, zero = λλ2 and succ = λλλ23, whereas in the one I found of Scott numerals, zero = λλ1 and succ = λλλ13.
Nowhere man
CC BY-SA 3.0
2011-07-30T04:18:50.583Z
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.
Kaveh
CC BY-SA 3.0
2011-07-23T20:14:06.583Z
2011-07-25T14:10:19.050Z
2011-07-25T14:10:19.050Z
Stéphane Gimenez
<p>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.</p>

CC BY-SA 3.0
2011-07-29T19:41:38.313Z
2011-07-29T19:41:38.313Z
Andrej Bauer
<p>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 <code>Y fac 3</code> in normal-order reduction, it takes 619 steps, which seemed a bit much.</p>

<p>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:</p>

<pre><code>fac = λfac.λn.if (= n 0) 1 (* n (fac (- n 1)))
</code></pre>

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

<p>But in my evaluator, I used the following:</p>

<pre><code>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)
</code></pre>

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

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

<p>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…</p>

<lo.logic><lambda-calculus>
Are a few hundred reduction steps too many to get the normal form of Y fac ⌜3⌝?
Nowhere man
# Are a few hundred reduction steps too many to get the normal form of Y fac ⌜3⌝?

(Asked by: username_0 on 2011-07-23)

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…

**Tags:** lo.logic, lambda-calculus


---

## 2 answers

### Answer by username_1 on 2011-07-23. Score: 11

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.

> **Comments:**
> **username_0**: 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…  
> **username_1**: 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.  
> **username_1**: Just curious, what about 4!, 5!, 6! ?  
> **username_0**: 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.  
> **username_2**: There are also the Scott numerals.  
> **username_1**: 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).  
> **username_0**: I was about to say that from what I've seen, Scott numerals should be equivalent to Peano numerals in terms of the number of reduction steps, as the definition I took was identical except that s and z (WRT to the notation above) were swapped. So with de Bruijn indexes, from the definition above, zero = λλ2 and succ = λλλ23, whereas in the one I found of Scott numerals, zero = λλ1 and succ = λλλ13.  
> **username_3**: 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.  

---

### Answer by username_2 on 2011-07-29. Score: 2

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.


---

