49 lines
1.9 KiB
Plaintext
49 lines
1.9 KiB
Plaintext
$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))
|