$img lambda.png

* Lambda calculus

The lambda calculus is a formal system for expressing computation using function
application and abstraction invented by Alonzo Church in the 1930s. It is a
universal model of computation.

** Constructing lambda terms

Lambda calculus is based on constructing lambda terms and reducing them. It only
has three methods of creating such terms.

1. Variables

2. Function construction

3. Function application

For instance, the identity function is expressed as λx.x. Here, λx constructs a
new function which takes an argument x. When applied it evaluates to the
expression following the period. λx.x is therefore the function that takes one
argument and evaluates to that argument. An example of applying this function is
(λx.x) y → y.

Using De Brujin indexing, variable names are no longer necessary. With this
indexing system, each variable name instance is replaced by an index. The
K-combinator (λx.λy.x) is expressed with De Brujin indexing as λ λ 2. The '2' is
the index, which refers to the variable bound by the lambda form 2 levels up.

** Reduction

There are two ways of reducing an expression, α-conversion and
β-reduction. α-conversion is simply renaming the bound variables in an
expression. This doesn't change the expression, but can be used to avoid naming
collisions. Because of α-conversion, two functions such as λx.x and λy.y are
said to be α-equivalent. β-reduction is replacing the arguments of a function
with the values they are bound to in an expression. For instance ((λx.λy.xy) f
g) will be β-reduced to f applied to g.

** The Y combinator

The Y combinator is an implementation of a fixed point combinator for the
untyped lambda calculus. It is a higher order function which allows functions to
call themselves. This means it can be used to formally define recursive
functions.

Y = λf.(λx.f (x x)) (λx.f (x x))
