I think the following encoding also works.

ZERO := λf. λx. x
ONE  := λf. f
TWO  := λf. f f
THREE:= λf. f (f f)

Note: the original encoding is

ZERO := λf. λx. x
ONE  := λf. λx. f x
TWO  := λf. λx. f (f x)
THREE:= λf. λx. f (f (f x))

Why is the original one better?

  • $\begingroup$ Your ZERO is the same as the original, your ONE is equivalent to the original. Can you explain what your TWO and THREE do? $\endgroup$
    – Bergi
    Oct 20, 2017 at 3:39
  • $\begingroup$ The original encoding actually is TWO := λf. λx. f (f x) and THREE := λf. λx. f (f (f x)). Notice the difference? If you want to write it without parenthesis, you need to use an infix composition operator. $\endgroup$
    – Bergi
    Oct 20, 2017 at 3:40
  • $\begingroup$ @Bergi thx for pointing out that. I omitted the parenthesis in the original post. I revised the formula. $\endgroup$
    – czheo
    Oct 20, 2017 at 4:33
  • $\begingroup$ @czheo My lambda calculus is a bit rusty, but did you consider any type system for this code? What would the type of f be in your version? $\endgroup$
    – Bergi
    Oct 20, 2017 at 5:10

4 Answers 4


I think what you really are asking for are criteria for judging correctness of coding. Once you have got these, you can answer your question on your own.

Correctness of coding of some structure always originates from the structure itself. The structure of natural numbers $\mathbb{N}$ is:

  1. A constant $0$,
  2. A unary operation $S$,
  3. For each set $A$, a recursion operator $\mathsf{rec}_A : A \to (\mathbb{N} \to A \to A) \to \mathbb{N} \to A$, subject to equations: $$\mathsf{rec}_A \; x \; f \; 0 = x$$ and $$\mathsf{rec}_A \; x \; f \; (S n) = f \; n \; (\mathsf{rec}_A \; x \; f \; n).$$

So whatever your coding of natural numbers is, it has to have $0$, $S$ and $\mathsf{rec}$ (only one will do in the untyped $\lambda$-calculus as there are no types to worry about) such that the above equations are satisfied for all suitable $x$, $f$ and $n$.

You can ask yourself:

Does your coding allow you write down $0$, $S$ and $\mathsf{rec}$ which satisfy the desired equations?

If it does, then it's a valid coding. There are many codings of natural numbers.


I am the guy who posted this question. I somehow figure this out.

In the original form, consider the succ operation is defined as below (+1).

succ = λn.λf.λx. f (n f x)


succ ONE
= (λn.λf.λx. f (n f x)) (λf. λx. f x)
= λf.λx. f ((λf. λx. f x) f x)
= λf.λx. f ((λx. f x) x)
= λf.λx. f (f x)

Same to succ TWO, succ THREE ...

In my form, let us define succ like following.

succ = λn.λf. f (n f)


succ ONE
= (λn.λf. f (n f)) (λf. f)
= λf. f ((λf. f) f)
= λf. f f

This also works.

However, the pattern breaks when we try to do succ ZERO

In the original form,

succ ZERO
= (λn.λf.λx. f (n f x)) (λf. λx. x)
= λf.λx. f ((λf. λx. x) f x)
= λf.λx. f ((λx. x) x)
= λf.λx. f x

But in my form,

succ ZERO
= (λn.λf. f (n f)) (λf. λx. x)
= λf. f ((λf. λx. x) f)
= λf. f (λx. x)

If we really want my new form holds, we have to define ZERO = λf._ where _ is something like NULL or empty, which is not supported by the syntax.

Alternatively, I think we can define:

ZERO  := λf. f
ONE   := λf. f f
TWO   := λf. f (f f)

So that the newly defined succ operation may still hold. However, other things/rules can break. For example, in the original form, the boolean FALSE (λx.λy.y) encoding is as same as ZERO. But in my form, this property will no longer hold. ... There may be better explanations. But finally, I've somehow convinced myself that Church's design is a piece of art!

  • $\begingroup$ You need $0$, successor and recursion, satisfying some equations, see my answer. $\endgroup$ Oct 29, 2017 at 18:57
TWO  := λf. f f
THREE:= λf. f (f f)

This looks like a type error to me. TWO and THREE should have the same type - regardless which one exactly. That would imply that f and (f f) had the same generic type as well, which is impossible however (without a recursive infinite type) or requires f to be the identity function (with type ∀a. a -> a), which would be pretty useless and makes the numbers indistinguishable.

In the original version, the number type is (a -> a) -> a -> a.

  • 3
    $\begingroup$ There is no type error in the untyped lambda calculus. Thus a combinator like TWO above is not only perfectly valid, it is also famous and has its own name: Omega combinator. (Note, I'm not saying anything about that proposed number encoding.) $\endgroup$
    – Ingo
    Oct 20, 2017 at 22:11

You're breaking the η-reduction rule

M := λx. N x
Μ := N

Note the parentheses in TWO – you cannot do η-reduction here

TWO := λf. λx. f (f x)

To demonstrate, as you propose

TWO := λf. f (f f)

Would result in a problem

TWO g x
= (λf. f (f f)) g x
= g (g g) x

But in Church's definition we get

TWO g x
= (λf. λx. f (f x)) g x
= (λx. g (g x)) x
= g (g x)

Your proposed g (g g) x is not equivalent to g (g x)

To remove x, use B — its not exactly what you’re asking for but shows that there’s room in the definition for change, while simultaneously keeping everything the same

B := λf. λg. λx. f (g x)

 ZERO := λf. λx. x
  ONE := λx. x
  TWO := λf. B (ONE f) (ONE f)
THREE := λf. B (TWO f) (ONE f)
 FOUR := λf. B (TWO f) (TWO f) 
 FIVE := λf. B (TWO f) (THREE f) 

Let's evaluate THREE h z to see it work

= (λf. B (TWO f) (ONE f)) h z
=      B (TWO h) (ONE h) z
= (λf. λg. λx. f (g x)) (TWO h) (ONE h) z
= (λg. λx. TWO h (g x)) (ONE h) z
= (λx. TWO h (ONE h x)) z
= TWO h (ONE h z)
= (λf. B (ONE f) (ONE f)) h (ONE h z)
= B (ONE h) (ONE h) (ONE h z)
= (λf. λg. λx. f (g x)) (ONE h) (ONE h) (ONE h z)
= (λg. λx. ONE h (g x)) (ONE h) (ONE h z)
= (λx. ONE h (ONE h x)) (ONE h z)
= ONE h (ONE h (ONE h z))
= (λx. x) h (ONE h (ONE h z))
= h (ONE h (ONE h z))
= h ((λx. x) h (ONE h z))
= h (h (ONE h z))
= h (h ((λx. x) h z))
= h (h (h z))
= THREE h z

Or the expression in this waterfall-style formatting - may help readability for some

=                                                      (λf. B (TWO f) (ONE f)) h z
=                                                           B (TWO h) (ONE h)    z
=                               (λf. λg. λx. f     (g     x)) (TWO h) (ONE h)    z
=                                   (λg. λx. TWO h (g     x))         (ONE h)    z
=                                       (λx. TWO h (ONE h x))                    z
=                                            TWO h (ONE h z)
=                        (λf. B (ONE f) (ONE f)) h (ONE h z)
=                             B (ONE h) (ONE h)    (ONE h z)
= (λf. λg. λx. f     (g     x)) (ONE h) (ONE h)    (ONE h z)
=     (λg. λx. ONE h (g     x))         (ONE h)    (ONE h z)
=         (λx. ONE h (ONE h x))                    (ONE h z)
=              ONE h (ONE h (ONE h z))
=          (λx. x) h (ONE h (ONE h z))
=                  h (ONE h (ONE h z))
=              h ((λx. x) h (ONE h z))
=              h (h         (ONE h z))
=              h (h     ((λx. x) h z))
=              h (h     (h         z))
= h (h (h z))
= THREE h z
  • $\begingroup$ Although you TWO is not defined as the same as mine, I understand your points. This makes sense. Thx a lot! $\endgroup$
    – czheo
    Oct 20, 2017 at 5:20
  • $\begingroup$ @czheo see my updated answer re B – it's somewhat related to what Bergi was talking about $\endgroup$
    – user43109
    Oct 20, 2017 at 5:38

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.