Lamda-Calculus session round-up

Lambda Calculus Round-up
The session started with the example of designing a chair. Producers have to face a lot of constraints, some of which are endurance, appropriate height, portability and simplicity. We notice that among these criteria, some are even conflict to each others. Therefore, in the process of making, producers cannot eliminate any features but satisfy each to a specified level.
One similar example can be observed in Physics. We have Newton’s 3 Laws of motion: Any particle without a force exerting will continue moving uniformly or staying still, particle with a force exerting on has F= ma, and what exerts a force will receive the same force from opposite direction. Also, we have Kepler’s laws about motion of planets, which is much more complicated. However, later on, Newton proved that Kepler’s law can be derived from his 3 laws of motion. Therefore, Physics still exist without one of the two laws, and what we have to remember is only one of them. That is the principal of minimalism, as quoted in Occam’s Razor: “Entities must not be multipled beyond necessities”. Actually, people still prefer Newton’s Laws for the following reasons:
- Practicality: easier to remember and document, etc
With concise content, it is easier to reason about or to falsify
- Aesthetic: small theories are more beautiful

In Programming, we have two iterative Loop known as For loop and While loop. The two can be applied to any situation equally. We can switch from one loop to the other without changing the meaning of the program. So, do we need both or can eliminated one of them? There are two different people with two different answers:
The programmer will say definitely we need both for convenience. The theoretician, on the other hand, opposes that we should discard one of them, for they will duplicate out proofs and we need hours and pages to deal with problems they cause.

The appropriately long introduction leads us to the main part: A Theoretician’s Programming Language. We will see how simple it is.
In this special kind of programming language, we will eliminate all what we do not need and take only minimal necessities for granted. As said, we will consider only functions definition and application without paying attention to functions with multiple parameters, numbers, loops and conditionals.

The first example is additional operation. The point you may not have noticed is that the address bar can be used as a debugging tool.
Normally to find the sum of two numbers, the code will be
Function plus(x+y){return (x+y);}
And to call the function: plus(5,7)
The answer is 12.

But the theoretician says “We do not need multiple arguments like that.” And he starts writing function that adds two numbers but, this time, with only one parameter.
Function plusx(y){….}
To call: plusfive(7)

And some functions that totally eliminate loops, conditionals and even numbers!
Another example in conditionals eliminating:
In a normal Java program, we write (20<10)? 5:7
The idea of change is to represent Booleans with functions:
Function true(x)
Return function(y)
Return x;
This function will return x if the condition is true and y oppositely.

The theoretician makes a step further. He does not need the name of the functions, because the function automatically applies itself into the value computation.
::=()()
Function () {return ;}

To conclude, the method that the theoretician applied excludes all the characteristics of the specified programming language. No matter what kind of language you use, any program can be written in  Calculus.

Last but not least, here is a glimpse into  Calculus:
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. It was introduced by Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.[1][2] After the original system was shown to be logically inconsistent (the Kleene–Rosser paradox), Church isolated and published in 1936[3] just the portion relevant to computation, what is now called the untyped lambda calculus.

(from http://en.wikipedia.org/wiki/Lambda_calculus)