Problem Detail: 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$
Asked By : codd
Answered By : Gilles
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)))))$.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/1259 Ask a Question Download Related Notes/Documents
