# zero raised to power zero in Church encoding

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?

• no, it gives $1$ as the answer. Jan 30, 2015 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

• 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? Jan 30, 2015 at 12:59
• @DanielR I am slightly confused by it myself now. I calculated it again using a different approach, which does indeed result in 1. Jan 30, 2015 at 13:02
• $\lambda x.x$ and $1$ are equivalent under $\eta$-expansion Jan 30, 2015 at 13:03
• I'm confused. In "Constructive Foundations for Functional Languages" academia.edu/456528/… it says λx.x is the zero object Jan 30, 2015 at 13:18
• 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$ Jan 30, 2015 at 15:36