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$
A lambda calculus evaluation involving Church numerals
lambda calculus;church numerals
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)))))$.