In lambda calculus, why do we define $n=\lambda f.\lambda x.f^n(x)$ instead of $n=\lambda f.f^n$?

Question

I just started learning lambda calculus and I understood most of it but i was thinking that why do we define $n=\lambda f.\lambda x.f^n(x)$ instead of $n=\lambda f.f^n$? I think it would be more simple in that way?

Eg.:

$$0\equiv\lambda f.\;\lambda x.x$$ $$1\equiv\lambda f.\;\lambda x.\; f(x)$$ $$2\equiv\lambda f.\;\lambda x.\; f(f(x))$$ $$3\equiv\lambda f.\;\lambda x.\; f(f(f(x)))$$ in normal lambda calculus but I think it would be better if $$0\equiv\lambda x.\,x$$ $$1\equiv\lambda x.\,xx$$ $$2\equiv\lambda x.\,xxx$$ $$3\equiv\lambda x.\,xxxx$$

I can define the usual successor function and the addition function with this definition but I have not tried to implement multiplication. But it is quite similar to addition and I will be able to do it. It seems that this definition is also valid.

Please provide some reason for using the standard definition?

Answer 1

1. Even more important than addition is the ability to recognize the number 0; if someone gives you a numeral $n$, can you test whether $n=0$?

   With the standard (Church) numerals, one just uses:

   $$\def\iz{\operatorname{isZero}}\iz n \equiv \lambda n. n (\lambda a. \def\F{\operatorname{false}}\F) \def\T{\operatorname{true}}\T$$

   and then one has $$\begin{align} \iz 0 &\Rightarrow \T \\ \iz n & \Rightarrow \F \text{(when $n>0$)} \end{align} $$ the reductions requiring only two steps in each case.

   It is difficult to see how one would build $\iz$ this with your suggested definition of the numerals.

2. You claim to have a definition for addition, but you didn't show it, and I wonder if it works as well as you think it will. With Church numerals the definition of addition is very simple, and multiplication and exponentiation ever more so, which is a decided advantage, and the main reason why these definitions are used.

3. The forms $\lambda x.xx, \lambda x. xxx,\ldots$ are often associated with terms that have no normal form. One would have to worry, for every computation involving any number other than 0, whether the computation would reduce to a normal form. Even when it did, the reduction order might make a difference. This is an unneeded complication.

4. To go the way you want to go, I think a better choice would be the following:

   $$\begin{align} \def\pair{\operatorname{pair}}\pair a\, b &\equiv \lambda x. x\, a\, b\\ \operatorname{first} p & \equiv p\, (\lambda a\,b.a) \\ \operatorname{second} p & \equiv p\, (\lambda a\,b.b) \end{align}$$

   This defines an ordered pair type from which we can extract the first or second component; we have for example $\operatorname{first}(\pair a\, b) \Rightarrow a$. Then the numeral $n$ is defined as a linked list of length $n+1$:

   $$\begin{align} 0 & \equiv \pair \T \T \\ \operatorname{succ} & \equiv \lambda n. \pair \F n \\ n &\equiv \operatorname{succ}^n 0 \\ \iz &\equiv \operatorname{first} \\ \operatorname{pred} & \equiv \operatorname{second} \\ + &\equiv \lambda a b.Y(\lambda s.(\iz a)\,b\,(s (\operatorname{pred} a)\,(\operatorname{succ} b))\\ &\text{(etc.)} \end{align}$$

   The addition and multiplication are more complicated than the Church numeral definitions, since they require a fixed-point combinator $Y$, but in some ways more perspicuous. The definition of $\operatorname{pred}$ is simpler.

Answer 2

Your $0$ is the usual $1$ (up to $\eta$-equivalence) and is the identity. It seems to me more natural that $1$ is the identity and that $0$ erases something (as in the usual definition of the $0$, which erases the argument), but maybe it is subjective.

You did not try to define the multiplication. If you try, maybe you will have an answer to your question. The usual definition of multiplication is $M = \lambda n. \lambda p. \lambda f. (n)(p)f$. If you apply $M$ to the identity, you obtain the identity (up to $\eta$-equivalence); in your case, you sould have that $M'$ (your lambda-term for the multiplication) applied to the identity gives $\lambda p. \lambda x. x$, so, of course, you have to find another lambda-term.

Moreover, the usual encoding of integer is typeable, not your encoding.