2008-10-18

Church numerals continued

Japanese version

Last time, a circle was a symbol to represent a number. But, there is no such thing (a symbol to represent a number) in the Peano's axiom. Peano's axiom only define a Zero and a successor. we employed a square to represent Zero. But when we tell two numbers to a machine, we can not distinguish two numbers if we have only Zeros. See Figure 2. Therefore, we use a circle as a delimiter. One could say, we can use a space, but we also need to tell a space to a machine, otherwise any machine can not know a space exist. We need something like a number 0. 0 means ``there is nothing.'' If we write down nothing, how we could know something is missing. If we put 0, then we know nothing actively exists. 0 can represent ``existence of nothing.'' This is an excellent invention of human being.

By the way, speaking about space, there is no space character in Japanese. I think also Korean and Chinese do not have space character. Therefore, a processing of Asian text starts with finding words. A space character represents no character, but existence of no character makes so easy to find words. Space character is also a brilliant invention. I remind myself that Lao-tsu's ``usefulness of
uselessness.''

The Church numerals, one of the representations of numbers of lambda calculus, are defined as follows:

0 := λ f x. x
1 := λ f x. f x
2 := λ f x. f (f x)
3 := λ f x. f (f (f x))

It seems these are not numbers, but these satisfies Peno's axiom, therefore, these are numbers. Because no matter what it looks like, Peano's axiom defines what the number should be. If the condition is satisfied, they are numbers. That's the rule. If you closely look this numbers, the number of 'f' is represents the number. Zero has no `f,' 1 has one `f'. Two has two `f's . Three are also the same. This is the definition of Church numerals. As you see in Figure 3, this is almost the same as Figure 1's number. (Almost means both f and x are square. Different things should have different symbols. This is not good, but this is for computation.)

Marvin: What a long story to define just NUMBERS! You spent nine articles to define it. In the Wikipedia's lambda calculus page, when the Church numerals are defined, it has already defined all formal lambda expressions. You said just one is one square, two is two squares, ... this simple thing took so long. It is ok to explain something simple, but it is so pedantic. You have not even defined how to compute numbers. I have experienced five universes time. But this is too slow for me. So depressed.

But Marvin, this is the way I understand the Church number. I am a armature mathematician, so I could not understand if only the definitions of Peano's axiom is presented. It is so abstracted and dry for me.

Marvin: Doesn't matter. I am tired. You defined numbers. Now what? Roman number is better than this for computing. How can you write 2008? My co-processor will be depressed.

OK. We have now numbers, let's compute it... so functions.