lambdalambda-calculuscomputation-theoryexponentiationchurch-encoding

m to the power of 0 in Church’s Numerals


A topic on undergraduate level computer science.
I came upon a bothering problem about (0 m) in terms of exponentiation of church’s numerals in lambda calculus when reviewing the theory.
As far as I know, (0 m) when reduced results in λx. x, which is not 1 (= m^0) as expected and even not within church’s numerals.

I adopt n of a natural number in lambda calculus encoded by church’s encodings usually as below

n := λfx. (f^n x) = (f ... (f x))

Many literatures say that

EXP(m, n) := λmn. (n m)

returns m^n for given m and n of church’s numerals, and I understand the function responds correctly in most cases. But this is not the case when n = 0 since

(0 m) = ((λfx. x) m) → λx. x

In mathematics, 1 is an identity element of natural numbers regarded as a multiplicative group, i.e. x * 1 = 1 * x for any x in N. So if I set EXP function in the form of

EXP’(m, n) := λmn. (n (MUL m) 1)

for MUL(m, n) = m * n, this appears to work fine, coinciding the fact m^0 is often defined as 1 in mathematics. Also this seems straightforward in the sense of hyperoperation.

HYPEROPERATION: https://en.m.wikipedia.org/wiki/Hyperoperation

I expect some criticisms like m^0 is not necessarily 1 in math, and rigid mathematical guys would say it all depends on definitions. But then is there any logical support for adopting the former style EXP(m, n)? It doesn’t return church’s numerals when n = 0, so still seems poorly defined for me.

Question is

  1. “Why the definition EXP(m, n) := λmn. (n m) is usually accepted for m^n even though its output can be non church’s numeral for church’s numeral inputs?”

  2. “Do you know any slight correction of EXP so the function serves well for all church’s numeral inputs?”

  3. “Any problem or misunderstanding on my criticism to (0 m).”

In addition, are there logical backgrounds for the result of (0 m) to be λx. x, which is an identity element of function composition, instead of 1? Is this just a coincidence or am I thinking this too seriously?

Any ideas are welcomed.

I want to follow wikipedia definitions of algebra related to church’s numerals if necessary.

CHURCH’S ENCODING: https://en.m.wikipedia.org/wiki/Church_encoding

Thanks.


Solution

  • A simple misunderstanding: you say "λx. x, which is not 1", but λx. x is indeed the Church numeral 1. You probably know the Church numeral 1 as λfx. f x, but a simple eta-reduction and alpha-conversion show that this is equivalent to λx. x.