λ calculus

Rules of the universe

0. Permitted keywords: Everything in lambda calculus is function. All the algorithms are represents with functions. There are only 2 keywords, λ and . needed to write a function. And that's it. Everything between λ and . are function arguments, everything after "." is the function body.
Example: λx.x+1 represents a function, that takes an argument x and returns x+1. Note that, x can be replaced by any other names.
A few notes
    a. A function can be written in such a way so that it always takes only 1 argument.
    Example: λxy.(x+y) can be written as, λx.(λy.(x+y)). If this function is applied to argument 3 4 then, the following happens
    (λx.(λy.(x+y))) 3 4 => (λy.(3 + y)) 4 => (3 + 4) => 7
    Writing a function such that it always takes only 1 argument is called function Currying (named after Haskell Curry).
 
    b. functions do not have names. We can say, a function A = λx.x+1, when we say the function does not have a name, we say from inside the function body, we do not know the name of function. So we cannot write a function, A = λx.A(x) because, from the function body we don't have access to names of the caller A.
 
    c. When we say fx we mean f is applied on x, f(x). ABCDE means A, B, C, D and E are functions and is applied the following way
    ((((AB)C)D)E)
    which means A is applied to B, the resulting function is applied to C so on and so forth.

1. Application and value substitution:
Example: A = λx.x+1; A3 means the function A is applied on the value 3. All the x s in the expression x+1 will be replaced by 3. This is expressed as [3/x](x+1) = 3 + 1 = 4

2. Reduction:
By application and substitution, a complex function might be reduced to small one.
Example: (λx.(λy.y))ts = s

Building Blocks of the Universe

Boolean value construction
0. True:
As stated earlier everything in the universe will be functions. The value True is represented as the following function
T : λ xy.x . Basically the true function takes 2 arguments and return the first argument.
1. False:
False, F is represented by the following function.
F : λ xy.y . This function takes 2 arguments and returns the second argument.

Boolean Operations
And, ^:
^ : λxy.xyF
Or, v:
v : λxy.xTy
Not, ¬:
¬ : λx.xFT

Arithmatic value construction
Integers:
0, 1, 2, .. n are all represented by functions that takes two arguments.
0: λfx.x This means the function 0 takes two arguments f and x and applies f on x zero times.
1: λfx.f(x) , 1 takes two arguments, f, x and applies f once to x
2: λfx.f(fx) , 2 takes two argument f, x and applies f twice on x
3: λfx.f(f(fx)) 3 takes two argumetns f,x and applies f three times on x.
so on and so forth
Pairs:
A pair holding two integers a and b is represented by the following function
p : λx.xab
Retrieve the first element from p, pT => (λx.xab)T => Tab => a
Retreive the second element p, pF => (λx.xab)F => Fab => b

Arithmetic Operations:
Successor:
S: λxyz.y(xyz)
Example: S0 => (λxyz.y(xyz))0 => λyz.y(0yz)
            => λyz.y((λfx.x)yz) => λyz.y(z)
            => λfx.f(x) [renaming variable y with f and z with x]
            => 1 [from definition of 1 function]

(+ a b):
+ : (λab.aSb)
Example: (+ 2 3) => 2S3 => (λfx.f(f(x)))S3 => S(S(3)) => S(4) => 5

Predecessor, P:
We want to know the predecessor of 3. Basic idea,
start with the pair holding (0,0) then convert it the following order
(0,0) -> (1, 0) -> (2, 1) -> (3, 2) -> take second element of the pair, which yields 2.
we need a function Φ, that would take a pair (n, n-1) and would generate (n+1, n)
Φ: λpz.z(S(pT)(pT)) => lets say pair , p holds (3, 2). new pair will hold (S(pT), (pT)) => (S(3), 3) => (4, 3)
We can define P: (λn.nΦ(λz.z00))F which means Φ is applied to the pair (0,0) for 3 times and the second element of the pair is taken in the end.

(- a b) :
- = (λab.bPa)
Example: (- 3 2) => 2 P 3 => P(P(3)) => P(2) => 1

Conditionals:
Conditional such as a == b, a >= b or a <= b etc can be expressed by function.
(>= a b):
a >= b check can be done with the following function 
>= : (λab.Z(- b a))

(== a b):
a == b check can be done with the following function 
== : (λab.( >= b a) ^ (>= a b))

Recursion:

The λ functions don't have name, so from inside the body it is not possible to call the * function. Recursive calls are made using Y combinator.

Y : (λ f  . (λ x .  (f (x x)) (λ x . f (x x))))

R is a function that needs to be called recursively. Then, Y is applied to R

YR = Y(R) = (λ x. (R (x x)) (λx. R (x x)))

= R ((λ x. (R (x x)) (λx. R (x x)))) [value substitution]

= R (YR) ...... 

= R(R(R(R....(YR))))

We can see that YR is being computed with computing R first, one return value of R is used to compute caller's value.

Example:

we want to compute (1+2+3+...+n)

R : (λrn.Zn0(+ n r((- n 1))))

R is a function that takes 2 arguments, n and r. 

In base case, n become 0. Zn returns T then T gets two arguments 0 and (+ n r((- n 1))). We know T always returns the first argument so in this case R will return 0.

if n > 0 then Zn returns F. F would return the second argument (+ n r((- n 1))), which means it would return n + r(n-1)

Example evaluation:

YR3 = R(YR)3

= (λnr.Zn0(+ n r((- n 1)))) (YR) 3

= Z 3 0 (+ 3 YR(- 3 1))

= Z 3 0 (+ 3 YR2)

= F 0  (+ 3 R(YR)2)

= (+ 3 (λnr.Zn0(+ n r((- n 1)))) (YR) 2)

..........

= (+ 3 (+ 2 (+ 1 0) ))

= 6

References
[0] computerphile video on lamda calc: https://www.youtube.com/watch?v=eis11j_iGMs
[1] Dason's slide: https://www.slideshare.net/g33ktalk/lambda-calculus-by-dustin
[2] friendly explanation: http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf
[3] Dustin's presentation: https://www.youtube.com/watch?v=E5DwIxGOu1E