Monday 12 January 2015

Lambda Calculus, Boolean and Comparison

True & False
In lambda calculus, True and False are both functions and at first, they may look like a bit strange, look at them:

True  :  λxy.x
False :  λxy.y

Let us see what they mean. A typical inline conditional statement in programming languages usually is something like the following:

Condition ? TrueStatement : FalseStatement

If we use True and False to simply rewrite it, we can have the definition of True and False:

True ? True : False  or in lambda calculus  λxy.x
False ? True : False or in lambda calculus  λxy.y

What this means, is that the true and false are in fact the result of 2 option choosing process, if it chooses the first we call it true and if it chooses the second we call it false, as simple as this. Look at the below examples:

if (true) then {Exp1} else {Exp2}  or in lambda calculus  (λxy.x) T1 T2 or T1
if (false) then {Exp1} else {Exp2}  or in lambda calculus  (λxy.y) T1 T2 or T2

Predicator function and if-then-else
If we have an operator or function which evaluates a condition then we can use it with the previous results to build an if-then-else statement. This function in λ calculus is called predicator which returns True or False. Like many programming languages, most of the time the predicator is nothing but a compare with number zero. So the familiar if-then-else expression:

Condition ? TrueStatement : FalseStatement

can be shown as below:

λpxy.p x y 

in which λp is the predicator function and you need to pass the condition to it. Now let us see what happens if we pass True & False to this term:

(λpxy.p x y) True → (λp.(λxy).p x y) True →  λxy x   // since the passed parameter is true the first  parameter has been chosen
(λpxy.p x y) False  → (λp.(λxy).p x y) False →  λxy y  // since the passed parameter is false the first parameter has been chosen

Note that you can pass any lambda term instead of True or False, I just wanted to give a simple example. It is the duty of λp to evaluate and choose one of the passed terms.