In Church encoding of the natural numbers in lambda calculus raising zero to the power zero gives the answer zero. Does anybody know of an encoding where the answer is 1?

  • $\begingroup$ no, it gives $1$ as the answer. $\endgroup$ – mercio Jan 30 '15 at 11:34
(λm.λn.n m) (λf.λx.x) (λf.λx.x)
⇒   (λn.n (λf.λx.x)) (λf.λx.x)
⇒   (λf.λx.x) (λf.λx.x)
⇒   λx.x

Another different calculation ((\m.\n. ((n (\m.\n.\f. (m (n f)))) f x))(\f.\x.x)(\f.\x.x)):

(λm.λn.n (λi0.λi1.λi2.i0 [i1 i2]) f x) (λi0.λi1.i1) (λi0.λi1.i1)
⇒   (λn.n (λm.λi0.λi1.m [i0 i1]) f x) (λi0.λi1.i1)
⇒   (λi0.λi1.i1) (λm.λn.λi0.m (n i0)) f x
⇒   (λi0.i0) f x
⇒   f x

Calculations done using: http://www.cburch.com/lambda/index.html

  • 1
    $\begingroup$ Which is not a Church numeral at all, is it? So, can we conclude that $0^0$ is undefined in the context of Church encoding? $\endgroup$ – Daniel R Jan 30 '15 at 12:59
  • $\begingroup$ @DanielR I am slightly confused by it myself now. I calculated it again using a different approach, which does indeed result in 1. $\endgroup$ – Loreno Heer Jan 30 '15 at 13:02
  • 4
    $\begingroup$ $\lambda x.x$ and $1$ are equivalent under $\eta$-expansion $\endgroup$ – mercio Jan 30 '15 at 13:03
  • 2
    $\begingroup$ I'm confused. In "Constructive Foundations for Functional Languages" academia.edu/456528/… it says λx.x is the zero object $\endgroup$ – William Pearson Jan 30 '15 at 13:18
  • 3
    $\begingroup$ the zero object is $\lambda f. \lambda x. x$. Meanwhile, $\lambda x. x =_\alpha \lambda f.f =_\eta \lambda f. (\lambda x. f x) = 1$ $\endgroup$ – mercio Jan 30 '15 at 15:36

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.