1
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.