A lambda calculus evaluation involving Church numerals

Question

I understand that a Church numeral $c_n$ looks like $\lambda s. \lambda z. s$ (... n times ...) $s\;z$. This means nothing more than "the function $s$ applied $n$ times to the function $z$".

A possible definition of the $\mathtt{times}$ function is the following: $\mathtt{times} = \lambda m. \lambda n. \lambda s. m \; (n\; s)$. Looking at the body, I understand the logic behind the function. However, when I start evaluating, I get stuck. I will illustrate it with an example:

$$\begin{align*} (\lambda m. \lambda n. \lambda s. m \; (n\; s))(\lambda s.\lambda z.s\;s\;z)(\lambda s.\lambda z.s\;s\;s\;z) \mspace{-4em} \\ \to^*& \lambda s. (\lambda s.\lambda z.s\;s\;z) \; ((\lambda s.\lambda z.s\;s\;s\;z)\; s)) \\ \to^*& \lambda s. (\lambda s.\lambda z.s\;s\;z) \; (\lambda z.s\;s\;s\;z) \\ \to^*& \lambda s. \lambda z.(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)\;z \end{align*}$$

Now in this situation, if I first apply $(\lambda z.s\;s\;s\;z)\;z$, I get to the desired result. However, if I apply $(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)$ first, as I should because application is associative from the left, I get a wrong result:

$\lambda s. \lambda z.(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)\;z \to \lambda s. \lambda z.(s\;s\;s\;(\lambda z.s\;s\;s\;z))\;\;z$

I can no longer reduce this. What am I doing wrong? The result should be $\lambda s. \lambda z.s\;s\;s\;s\;s\;s\;z$

Answer 1

I think your reduction is correct (I've only eyeballed it, though). At the end, you can't apply $(\lambda z. s s s z)$ to $z$, this never appears in the term. $\lambda z. f f z$ is $\lambda z. (f f) z$, not $\lambda z. f (f z)$. Functions in the lambda-calculus take a single argument; they are effectively curried: a two-argument function is implemented as a one-argument function that takes the first argument and returns a new one-argument function that takes the second argument and returns the result.

You made the same mistake when defining Church numerals. The Church numeral for $n$ is based on composing a function $n$ times. “The function $s$ applied $n$ times to the function $z$” $\lambda s. \lambda z. s (s ( … s \: z) … ))$. What you wrote is the function $s$ applied $n-1$ times to the function $s$ and finally to $z$, which doesn't strike me as a useful term.

$2 \times 3$ is thus $(\lambda m n s. m (n s)) (\lambda s z. s (s \: z)) (\lambda s z. s (s (s \: z)))$. I'll let you check that it does reduce to $\lambda s z. s (s (s (s (s (s \: z)))))$.