5
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Pseudonym Nov 10 '15 at 0:24
  • $\begingroup$ η-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? $\endgroup$ – aioobe Nov 10 '15 at 7:55
  • $\begingroup$ Take (λf.f) and replace the f with (λx.f x). If it helps, ((λf.f) x) can be β-reduced to x. $\endgroup$ – Pseudonym Nov 10 '15 at 13:46
  • 1
    $\begingroup$ 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$. $\endgroup$ – aioobe Nov 10 '15 at 14:57
1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ "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$? $\endgroup$ – aioobe Nov 9 '15 at 22:02
  • $\begingroup$ Would you edit your question to reflect that, please? $\endgroup$ – Pseudonym Nov 10 '15 at 0:26
  • $\begingroup$ Question updated. $\endgroup$ – aioobe Nov 10 '15 at 7:45
  • $\begingroup$ Answer updated. $\endgroup$ – Anton Trunov Nov 10 '15 at 9:16
  • $\begingroup$ 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. $\endgroup$ – aioobe Nov 10 '15 at 14:33

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.