6
$\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?

Improve this question
$\endgroup$
4
  • $\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, 2015 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, 2015 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, 2015 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, 2015 at 14:57

1 Answer 1

Reset to default
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$$.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.