On lambda calculus

Variable: x

Abstraction: λx.M

Application: (M N)

1. Correspondence:

    λx.x -> f(x) = x
    λx.λy.x -> f(x,y) = x

   This notation make use of currying, a function return a function.

   Used in some languages like Haskell:

    f :: x -> y
   
    f :: a -> (b -> c)     -- which can also be written as    f :: a -> b -> c

   is the curried form of

    g :: (a, b) -> c

2. Nested abstraction:

    λx.(λy.x) -> f(f(y)) = x ???

3. Application:

    λx.λy.xy -> x(y(xy)) = xy
   
    (xy)z -> x(y,z)

Example

Remember that λx.x is the identity function, any value passed to this function is returned without changes.

(λx.x)y means: y applied to the function λx.x, so we can wrote x(y) = y

(λx.x)y = y -> x(y) = y

(λx.λy.x)z -> (λx.(λy.x))z -> λy.z
f(z) = f(y(z))

(λx.λy.x y) (λx.x) (z) -> (λx.(λy.x y)) (λx.x) (z) -> (λy.(λx.x) y) (z)
-> (λx.x) z -> z

Increment by one:

λn.λf.x.f (n f x)

Church encoding:

- λf.λx.x   : zero
- λf.λx.f x : one

Example: incrementing zero by one:

(λn.λf.x.f (n f x)) (λf.λx.x)
(λf.λx.f ((λf.λx.x) f x))
(λf.λx.f ((λx.x) x)) <!-- f and x cannot be passed to the outer closure -->
(λf.λx.f ((x)))
λf.λx.f x

Hey look at the result and the value of one !

Example: incrementing one by one:

(λn.λf.λx.f (n f x)) (λf.λx.f x)
(λf.λx.f ((λf.λx.f x) f x))
(λf.λx.f ((λx.f x) x))
λf.λx.f (f x)