Wednesday, 24 December 2014

Lambda calculus, a formal system

Forget about the name "Lambda calculus" which is strange, grand and somehow serious of course,  it is nothing but a well-defined abstraction method in mathematics like what we already learned in school as Euclid's Elements in geometry, Algebra or Calculus and ... These abstraction methods are also called formal systems. A formal system should have a language (symbols and grammar) to be able to express systems with some rules and axioms. In fact, you can assume any programming languages as a formal system which is capable of expressing systems in terms of language statements. As I mentioned a formal system also should have some axioms and rules like what we have in Euclidean geometry, Algebra or Calculus.



Alonzo Church
So whatever Lambda calculus is, it is nothing but a convenient method with its own language, axioms, rules and ... to express systems. Systems which can have many inputs, processes and outputs. It is a logical method of describing things and the only problem with it is that its logic is not what we get used to it before.

Problem with Lambda calculus
There is no serious problem with Lambda calculus at all, the problem is with us! Remember the first time you wanted to write a recursive procedure, for example solving the "Hanoi Towers" it was difficult for us to understand how a recursive procedure works, and I think many programmers still have some problems to think or write recursive procedures to solve their problems. The reason is not that recursive procedures are difficult, the reason is our mind has not been trained to think this way.

Like what we have in classical mechanics vs quantum mechanics or relativity. Same things can be so different in these different areas of physics and while you don't get used to quantum mechanics or relativity you will always get confused to describe the result of a simple experiment in these areas.

Calculus and Lambda Calculus
History says that calculus developed in the 17th century by both Isaac Newton and Gottfried Leibniz. As we told before, calculus is a formal system to describe or model systems. Just look how easy you can model volume of a cone, area under a curve, wave behavior, motion of a planet around the sun and ... with calculus. In fact, if these two mathematicians didn't develop calculus and analytical geometry at that time, we would have no achievement in any other sciences even social sciences today. (Although I always think if for example Pythagoras didn't define his famous theorem, someone else would discover it sooner or later)

Like calculus, Lambda calculus has a developer too, an American mathematician named "Alonzo Church" was the one who introduced this formal system named "Lambda Calculus" in 1936. It was based on his previous papers in Computability Theory he published in 1930. In 1965 Peter Landin a British computer scientists found that the Lambda calculus can be a good used as a model of programming languages too. He mentioned in his paper at that time that a sequential/procedural program can be also interpreted in Lambda calculus too which introduced the functional programming to the world of software.

No comments:

Post a comment