2008-10-05

Motivation of Lambda calculus

Japanese version

According to the Wikipedia's page, Lambda calculus was introduced by Church and Kleene in the 1930s as part of an investigation into the foundations of mathematics.

By the way, I am an amateur Sunday mathematician, therefore, please do not believe this blog without check by yourself. This is just I think I understand these stuffs. So I think there must be many errors. I try to avoid errors, but, this is not my profession. I am also not confident about my English. Welcome the comments.

The origin of this blog is Wikipedia. I could say in cool way, I was inspired by the Wikipedia's page. If you understand the Wikipedia's entry, I don't recommend to waste of time by reading this blog. There are bunch of interesting text around the world. When you read ``Lambda calculus was introduced by Church and Kleene in the 1930s as part of an investigation into the foundations of mathematics.'', and if you think ``I see, that's the reason of why lambda calculus was introduced. That's easy.'' then, you don't need to read this blog. But, if you think ``In 1930? It seems very recently as the history of mathematics. Why is the foundations of mathematics considered in this time? Wait, what is the foundations of mathematics? Didn't Pythagoras, Apollonius, or Euclid study the foundations of mathematics in B.C.?'' Then, you may continue to read this text.

The foundations of mathematics means that where the mathematics can start, or what kind of starting point is all right for mathematics system. Mathematics starts with a set of definition. A person should define them. One of the most fundamental mathematical object would be numbers. Also propositions and logic, how to calculate numbers would be fundamental stuffs in mathematics. These seems too obvious and many mathematicians did not care them until 20th century. Or Euclid did too good job about formulation and we needed not re-consider until 20th century.

But, why such obvious things are important at that time? Mathematicians started to think about formalization at that time. It may differ the mathematics between languages, how can we sure they are exactly the same. For example, number `1' is exactly the same in English and Japanese? Then, they wanted to define numbers. If someone want to define numbers, it should be done without using numbers. Otherwise, we can define the numbers as ``numbers are numbers.'' For example, ``Love is love,'' ``Consciousness is conscious of consciousness.'' These may be true, but, we can not use it to think about the foundations of mathematics. Then a question is how can we define numbers without using numbers. This seems paranoia, but, mathematicians are perfectionist.

I found this is an interesting idea. Because these are enough to formalized, abstracted, and simplified. We could make a machine to implement that system. If you want to create a machine to compute something, we need to make it by some kind of materials (water, stone, iron, ...). Zaphod may say with his two heads, ``You know, 1 or 2 or 3, something like that. Just make up a machine which can understand them.'' But I think this is not so easy. Numbers are such an abstracted idea. Abstracted means that there are a lot of applications. ``What is the common idea between the earth, humans, a bread, signals, Zaphod's heads, and a church?'' I can answer that ``they are countable.'' I've already said, but I have no idea how to teach the numbers to children. That's a highly abstracted idea.

The motivation of lambda calculus is to think about the foundations of mathematics. This means that re-thinking all the mathematical system from the numbers and calculus even though they seems so obvious by some kind of formulation. At that time, mathematicians are interested in more in the sanity of the mathematical system by formalization. However, this formalization is based on enough simple system and we could build a machine which can partially process the system. The reason I am interested in lambda calculus is this part ``we can build a machine of that.'' Also this is the reason that lambda calculus is the basic theory of the computer and computer languages.

Next time, let's define the natural numbers without using 1, 2, 3, ...

No comments: