Why the definition of Church's Numerals

Question

I want to understand, why Church define the numerals like:

0 = λ f . λ x . x
1 = λ f . λ x . f x
2 = λ f . λ x . f f x
3 = λ f . λ x . f f f x
4 = λ f . λ x . f f f f x

What is the logic behind?

Why 0 is represent like:

0 = λ f . λ x . x

Answer 1

Church wasn't trying to be practical. He was trying to prove results about the expressive power of lambda calculus — that in principle any possible computation can be done in lambda calculus, hence lambda calculus can serve as a theoretical foundation for the study of computability. In order to do so, it was necessary to encode numbers as lambda expressions, in such a way that things like the successor function are easily definable. This was a key step in showing the equivalence of lambda calculus and Gödel's recursive function theory (which was about computable functions on the natural numbers). Church numerals are basically a convenient albeit not very readable encoding of numbers. In some sense, there isn't any very deep logic to it. The claim isn't that 1 in its essence is λ f . λ x . f x, but that the latter is a serviceable encoding of the former.

This doesn't mean that it is an arbitrary encoding. There is a definite logic to it. The most natural way to encode a number n is by something which involves n. Church numerals use n function applications. The natural number n is represented by the higher order function which applies a function n times to an input. 1 is encoded by a function applied once, 2 by a function applied twice and so on. It is a very natural encoding, especially in the context of lambda calculus. Furthermore, the fact that it is easy to define arithmetic on them streamlines the proof that lambda calculus is equivalent to recursive functions.

To see this in practice, you can run the following Python3 script:

#some Church numerals:

ZERO = lambda f: lambda x: x
ONE = lambda f: lambda x: f(x)
TWO = lambda f: lambda x: f(f(x))
THREE = lambda f: lambda x: f(f(f(x)))

#function to apply these numerals to:

def square(x): return x**2

#so ZERO(square), ONE(square), etc. are functions
#apply these to 2 and print the results:

print(ZERO(square)(2), ONE(square)(2), TWO(square)(2),THREE(square)(2))

Output:

2 4 16 256

Note that these numbers have been obtained by squaring the number two 0 times, 1 times, 2 times, and 3 times respectively.

Answer 2

According to the Peano axioms, a natural number is either 0 or S(n) for another natural number n:

0 = 0
1 = S(0)
2 = S(S(0))
...

You can see Church numerals as a generalization of Peano numbers, where you provide your own 0 and S:

0 = λs.λz. z
1 = λs.λz. s(z)
2 = λs.λz. s(s(z))
...

Since this is a programming forum, let's create some Church numerals in EcmaScript 6:

const ZERO = s => z => z;
const ONE  = s => z => s(z);
const TWO  = s => z => s(s(z));
...

You can convert these Church numerals to JavaScript numbers by providing the appropriate zero and successor:

function toInt(n) {
    return n(i => i + 1)(0);
}

And then:

> toInt(TWO)
2

You could use Church numerals to do some practical things:

function shout(text) {
    return text + "!";
}

> shout("hi")
"hi!"
> NINE(shout)("hi")
"hi!!!!!!!!!"

​

You can try it here: https://es6console.com/iyoim5y8/