less_retarded_wiki/lambda_calculus.md

Lambda Calculus

Lambda calculus is a formal mathematical system for describing computation with functions. It is a theoretical basis for functional languages. It is a model of computation similar to e.g. a Turing machine -- in fact lambda calculus has exactly the same computational power as a Turing machine and so it is an alternative to it. Lambda calculus can also be seen as a simple programming language, however it is so extremely simple that its pure form isn't used for practical programming, it is more of a mathematical tool for constructing proofs etc. Nevertheless, anything that can be programmed in any classic programming language can in theory be also programmed in lambda calculus.

While Turing machines use memory in which computations are performed, lambda calculus performs computations only with pure mathematical functions, i.e. there are no global variables or side effects. It has to be stressed that the functions in questions are mathematical functions, also called pure functions, NOT functions we know from programming. A pure function cannot have any side effects such as changing global state and its result also cannot depend on any global state or randomness, the only thing a pure function can do is return a value, and this value has to always be the same if the arguments to the function are same.

How It Works

(For simplicity we'll use pure ASCII text. Let the letters L, A and B signify the Greek letters lambda, alpha and beta.)

Lambda calculus is extremely simple, though it may not be so simple to learn to understand it.

In lambda calculus function have no names, they are what we'd call anonymous functions or lambdas in programming (now you know why they're called lambdas).

Computations in lambda calculus don't work with numbers but with sequences of symbols, i.e. the computation can be imagined as manipulating text strings with operations like "search/replace".

In lambda calculus an expression, also a lambda term or "program" if you will, consists only of three types of syntactical constructs:

1. x: variables, represent unknown values.
2. (Lx.T): abstraction, where T is a lambda term, signifies a function definition (x is a variable that's the function's parameter, T is its body).
3. (S T): application of T to S, where S and T are lambda terms, signifies a function call/invocation (S is the function, T is the argument).

Brackets can be left out if there's no ambiguity. Furthermore we need to distinguish between two types of variables:

• bound: A variable whose name is the same as some parameter of a function this variable is in. E.g. in (Lx.(Ly.xyz)) variables x and y are bound.
• free: Variable that's not bound.

Every lambda term can be broken down into the above defined three constructs. The actual computation is performed by simplifying the term with special rules until we get the result (similarly to how we simplify expression with special rules in algebra). This simplification is called a reduction, and there are only two rules for performing it:

1. A-conversion: Renames (substitutes) a bound variable inside a function, e.g. we can apply A-conversion to Lx.xa and convert it to Ly.ya. This is done in specific cases when we need to prevent a substitution from making a free variable into a bound one.
2. B-reduction: Replaces a parameter inside a function with provided argument, i.e. this is used to reduce applications. For example (Lx.xy) a is an application, when we apply B-reduction, we take the function body (xy) and replace the bound variable (x) with the argument (a), so we get ay as the result.

A function in lambda calculus can only take one argument. The result of the function, its "return value", is a "string" it leaves behind after it's been processed with the reduction rules. This means a function can also return a function (and a function can be an argument to another function), which allows us to implement functions of multiple variables with so called currying.

For example if we want to make a function of two arguments, we instead create a function of one argument that will return another function of one argument. E.g. a function we'd traditionally write as f(x,y,z) = xyz can in lambda calculus be written as (Lx.(Ly.(Lz.xyz))), or, without brackets, Lx.Ly.Lz.xyz which will sometimes be written as Lxyz.xyz (this is just a syntactic sugar).

This is all we need to implement any possible program. For example we can encode numbers with so called Church numerals: 0 is Lf.Lx.x, 1 is Lf.Lx.fx, 2 is Lf.Lx.f(fx), 3 is Lf.Lx.f(f(fx)) etc. Then we can implement functions such as an increment: Ln.Lf.Lx.f((nf)x), etc.

Let's take a complete example. We'll use the above shown increment function to increment the number 0 so that we get a result 1:

(Ln.Lf.Lx.f((nf)x) (Lf.Lx.x)     application
(Ln.Lf.Lx.f((nf)x) (Lf0.Lx0.x0)  A-conversion (rename variables)
(Lf.Lx.f(((Lf0.Lx0.x0)f)x)       B-reduction (substitution)
(Lf.Lx.f((Lx0.x0)x)              B-reduction
(Lf.Lx.fx)                       B-reduction

We see we've gotten the representation of number 1.

TODO: C code

See Also

• sigma calculus
• interaction calculus