33 lines
1.2 KiB
Plaintext
33 lines
1.2 KiB
Plaintext
* 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.
|
||
|
||
** 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.
|