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$

  • $\begingroup$ The Church numerals in your starting term aren't right. 2 is represented by $\lambda s. \lambda z. s (s z)$, not $\lambda s. \lambda z. s s z$. $\endgroup$
    – Uday Reddy
    Apr 15 '12 at 20:29

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)))))$.

  • $\begingroup$ As far as your paragraph goes, you are right and I was aware of this. It just striked me that applying rightly associative did yield the right result. As far as the second paragraph: you are right. Using no braces was erroneous of me, again because of the application's left associativity. I will reduce the whole thing again now and see if my lack of braces did cause my error! $\endgroup$
    – codd
    Apr 14 '12 at 0:37
  • $\begingroup$ It did. You noting that my notation implied wrong order of application solved the problem! Accepting your answer. $\endgroup$
    – codd
    Apr 14 '12 at 0:51

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.