# Why don't we encode church numerals like this?

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?

• Your ZERO is the same as the original, your ONE is equivalent to the original. Can you explain what your TWO and THREE do? – Bergi Oct 20 '17 at 3:39
• 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. – Bergi Oct 20 '17 at 3:40
• @Bergi thx for pointing out that. I omitted the parenthesis in the original post. I revised the formula. – czheo Oct 20 '17 at 4:33
• @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? – Bergi Oct 20 '17 at 5:10

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$.

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)


Thus,

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)
= TWO


Same to succ TWO, succ THREE ...

In my form, let us define succ like following.

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


Here,

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


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
= ONE


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!

• You need $0$, successor and recursion, satisfying some equations, see my answer. – Andrej Bauer Oct 29 '17 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.

• 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.) – Ingo Oct 20 '17 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

THREE h z
= (λ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

THREE h z
=                                                      (λ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

• Although you TWO is not defined as the same as mine, I understand your points. This makes sense. Thx a lot! – czheo Oct 20 '17 at 5:20
• @czheo see my updated answer re B – it's somewhat related to what Bergi was talking about – Thank you Oct 20 '17 at 5:38