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, 2015 at 11:34

1 Answer 1

(λ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, 2015 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$ Jan 30, 2015 at 13:02
  • 4
    $\begingroup$ $\lambda x.x$ and $1$ are equivalent under $\eta$-expansion $\endgroup$
    – mercio
    Jan 30, 2015 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$ Jan 30, 2015 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, 2015 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.