I am trying to learn basics of lambda calculus by following the tutorial by Raul Rojas, called A Tutorial Introduction to Lambda Calculus. In it, I have reached the Arithmetic section. We defined Church numerals. For example
$$\lambda sz.s(s(z))=2$$
I realized $2$ is just a name for this function and we represent natural numbers as functions. We also defined a successor function called $S$. I am sure you are familiar with it. Basically $S3=4$ as an example. We also showed something like $3fa = f(f(f(a)))$, so applying function $f$ three times to argument $a$. Now, addition was defined as
$$+ \ a \ b = aSb$$
I can understand this as well, applying successor $a$ times to $b$.
Now, I know we actually have anonymous functions in $\lambda$-calculus and these names like $1,3,S \ldots$ are just symbolic convenience for us but still, working with them makes things a lot easier. And since $\alpha$ and $\beta$ reduction are just symbolic rewrites, I can be sure that I can work with names.
To this end, I wanted to define myself multiplication. I wanted to devise it as follows:
- $\lambda x.aSx$ is a function that increments its argument by $a$
- $a \times b$ means applying increment-by-a $b$ times to $0$.
- Thus, $\lambda ab.b (\lambda x.aSx) 0$ should give $a \times b$.
- Put $0$ in in the first $\lambda$ to get $\lambda ab.baS0$
- So, $a \times b = \lambda ab.ba1$.
In the notes, multiplication is defined as
$$\lambda abx.a(bx)$$
I can't see how this can give the same result as the one I described above, namely $\lambda ab.ba1$. In which step I am doing a mistake? If am not, how this is equivalent to definition given at the tutorial?
Overture: First, the fact the term $\lambda abx.a(bx)$ represents multiplication does not exclude the possibility that other terms can represent multiplication as well.
Notational interlude: Given $n \in \mathbb{N}$ and two terms $R$ and $T$, we set \begin{align} R^nT := \overbrace{R(R \dots(R}^{n \text{ times } R}T) \dots). \end{align} For all $n \in \mathbb{N}$, we set the numeral $\underline{n} := \lambda fx. f^nx$. For instance, $\underline{0} = \lambda fx.x$, and $\underline{3} = \lambda fx.f(f(fx))$. Note that $\underline{n}RT$ reduces to $R^nT$: intuitively, a numeral $\underline{n}$ is a function of two arguments, say $R$ and $T$, that iterates $n$ times the function $R$ and apply it to $T$.
Answer: Your term $\lambda ab.b (\lambda x.aSx) \underline{0}$ is almost right, your only mistake is the way you parenthesize that term. Actually, the term $\lambda ab. \big(b (\lambda x.aSx) \big) \underline{0}$ represents multiplication as well (this means that you cannot apply $0$ to $\lambda x$). Indeed, if you apply this term to two numerals $\underline{m}$ and $\underline{n}$, you obtain the reduction: \begin{align} \Big(\lambda ab.\big(b (\lambda x.aSx)\big) \underline{0}\Big) \underline{m}\,\underline{n} &\to^* \big(\underline{n} (\lambda x. \underline{m}Sx) \big)\underline{0} \to^* (\lambda x. \underline{m}Sx)^n\underline{0} \\ &\to (\lambda x. \underline{m}Sx)^{n-1}(\underline{m}S\underline{0}) \to^* (\lambda x. \underline{m}Sx)^{n-1}\underline{m} \to^* \underline{n\cdot m}\,. \end{align}
You can check all the steps by yourself. To have an intuition of the reason why it works, consider the term $\big(\underline{n} (\lambda x. \underline{m}Sx) \big)\underline{0}$: it iterates $n$ times the function $(\lambda x. \underline{m}Sx)$ (which increments its argument by $m$) and then applies this $n$-iterated incrementation by $m$ to $0$. This is exactly what multiplication $m \cdot n$ is supposed to do.