1

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?

MJD
  • 65,394
  • 39
  • 298
  • 580
Kartik
  • 1,413
  • 1
    The usual definition of $0$ is $\lambda f. \lambda x. x$. What is your definition of $0$? – user21929 Sep 13 '14 at 11:11
  • This is not a lambda-term. – user21929 Sep 13 '14 at 11:13
  • @user21929 Then we can decrease all numbers by 1. – Kartik Sep 13 '14 at 11:14
  • @user21929 So then 0=$\lambda x.x$ and 1=$\lambda x.xx$ – Kartik Sep 13 '14 at 11:14
  • Could you define the usual functions on the integers? For instance, the multiplication? – user21929 Sep 13 '14 at 11:16
  • @user21929 I can define successor and plus operations. I have not tried to define multiplications because of lack of time. – Kartik Sep 13 '14 at 11:18
  • One thing: Your definition of $3 \equiv \lambda x.xxx$ is more explicitly $\lambda x.(xx)x$ since application is left-associative. Even if you define $3 \equiv \lambda x.x(xx)$ this is not equivalent to $3$-fold composition, which is what's happening with $f$ in $\lambda fx.f(f(fx))$. – joseville Jan 08 '22 at 21:28

2 Answers2

2

  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.

MJD
  • 65,394
  • 39
  • 298
  • 580
  • The linked-list representation of numerals was discussed as early as 1976: Barendregt, H. “A global representation of the recursive functions in the lambda calculus” Theoretical Computer Science 3, pp. 225–242 – MJD Nov 22 '21 at 20:41
1

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.

user21929
  • 607