zero raised to power zero in Church encoding

608 Views Asked by At

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?

1

There are 1 best solutions below

9
On
(λ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