Definition of success function

Question

In church numerals, if we have:

# (define zero (lambda (f) (lambda (x) x)))
zero = lambda f: lambda x: x

Then the successor function can be defined as:

# (define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
succ = lambda n: lambda f: lambda x: f(n(f)(x))

Maybe this is a silly question, but if the successor essentially adds one more wrapper f(...) to the previous equation, why couldn't this just be defined as f(n)? Is this more for consistency of definition, or why can't that shorter form be used?

(Note: using python definitions here as well as scheme as it makes it a bit simpler for me to test with.)

Answer 1

The numeral n is defined as n applications of the function f to some argument x.

Thus,

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f (x))
...

Note that 1 is not the same as λf.λx.f 0, so succ 0 can't be, either. (The same is true for the other numerals.)

Your definition, λn.λf.λx.(f n) would give

succ 0 = (λn.λf.λx.(f n)) (λg.λy.y)
       = λf.λx.f (λg.λy.y)

which is not the same as 1, but

 (λn.λf.λx.f (n f x)) (λg.λy.y)
= λf.λx.f ((λg.λy.y) f x)
= λf.λx.f ((λy.y) x)
= λf.λx.f x
= 1