Error in solution in Types and Programming Languages?

I'm reading Types and Programming Languages and trying to understand the solution to exercise 5.2.4 on untyped lambda calculus / Church numerals:

Define a term for raising one number to the power of another.

The proposed solution says:

$\textrm{power2} = \lambda m. \lambda n. m~n$

In an attempt to understand how this solution works, I tried it on 01 as follows:

$$\begin{array}{ll} & \textrm{power2}~c_0~c_1 \\ \rightarrow & c_0~c_1 \\ = & (\lambda s.\lambda z.z)~c_1 \\ \rightarrow & \lambda z.z \end{array}$$

The result doesn't look like a Church numeral to me. Is it an error in the solution, or have I misunderstood something?

• Anton is right that you got the order wrong; it's (λm.λn.n m). If (λz.z) doesn't look like a Church numeral to you, (λf.λx.f x) can be "simplified" to (λf.f) via η-conversion. – Pseudonym Nov 10 '15 at 0:24
• η-conversion says that f and λx.(f x) are equivalent. As far as I can tell, that means (λf.f) is equivalent to λx.((λf.f) x), and not (λf.λx.f x). Right? – aioobe Nov 10 '15 at 7:55
• Take (λf.f) and replace the f with (λx.f x). If it helps, ((λf.f) x) can be β-reduced to x. – Pseudonym Nov 10 '15 at 13:46
• Ok. I think I get it. Replacing the second f in λf.f with (the behaviourally equivalent term) (λx.f x) yields (λf.λx.f x). So λz.z is behaviourally equivalent to (λs.λz.s z) which is the good old c$_1$. – aioobe Nov 10 '15 at 14:57

If $power2~m~n$ stands for $m^n$, then it should be

$$power2=λm.λn.n~m$$

Let's try it on $0^1$: $$\begin{array}{ll} & power2~c_0~c_1 \\ = & (λm.λn.n~m)~c_0~c_1 \\ \rightarrow & c_1~c_0 \\ = & (λs.λz.s~z)~c_0 \\ \rightarrow & λz.c_0~z \\ = & λz.(λs.λz.z)~z \\ \rightarrow & λs.λz.z \\ = & c_0 \end{array}$$ Works fine.

Let's try it on $1^0$: $$\begin{array}{ll} & power2~c_1~c_0 \\ = & (λm.λn.n~m)~c_1~c_0 \\ \rightarrow & c_0~c_1 \\ = & (λs.λz.z)~c_1 \\ \rightarrow & λz.z \end{array}$$

Wait, we should have got $c_1$.

Although syntactically $λz. z$ is different from it, but it has the same behavior as $c_1$. In fact, you can use the function $equal$ (ex. 5.2.7) to prove it: $$equal = λm. λn.~and~(iszro~(m~prd~n))~~~(iszro~(n~prd~m))$$

By the way, another form of the power function, given in the solution to this exercise have the arguments swapped:

$$power1 = λm. λn. m~(times~n)~c_1$$.

• "What you got is $0^1 = 0$" $-$ No, 0 ($c_0$) is represented by $\lambda s. \lambda z. z$, and not $\lambda z.z$. Assuming I did swap the arguments, my question still stands, though slightly reformulated: Why doesn't $0^1$ result in $c_0$? – aioobe Nov 9 '15 at 22:02
• Would you edit your question to reflect that, please? – Pseudonym Nov 10 '15 at 0:26
• Question updated. – aioobe Nov 10 '15 at 7:45
• Answer updated. – Anton Trunov Nov 10 '15 at 9:16
• Thanks. Yes, the first thing I checked was the errata which indeed says that the arguments are swapped. So I tried both ways before even posting the question. What puzzles me is that in one of the cases I get $\lambda z.z$ which doesn't even look like a church numeral to me. – aioobe Nov 10 '15 at 14:33