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
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
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?