Lambda Calculus

   Lambda calculus is an extremely simple and low-level [1]mathematical
   system that can describe computations with [2]functions, and can in fact
   be used to describe and perform any computation. Lambda calculus provides
   a theoretical basis for [3]functional programming languages and is a
   [4]model of computation similar to e.g. a [5]Turing machine or
   [6]interaction nets -- lambda calculus has actually exactly the same
   computational power as a Turing machine, which is the greatest possible
   computational power, and so it is an alternative to it. Lambda calculus
   can also be seen as a simple [7]programming language, however it is so
   extremely simple (there are e.g. no numbers) that its pure form isn't used
   for practical programming, it is more of a mathematical tool for studying
   computers theoretically, 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 cells in which computations are performed
   -- which is similar to how real life computers work -- lambda calculus
   performs computations only by simplifying an expression made of pure
   mathematical functions, i.e. there are no [8]global variables or [9]side
   effects (the concept of memory is basically present in the expression
   itself, the lambda expression is both a program and memory at the same
   time). It has to be stressed that the functions in question are
   mathematical functions, also called pure functions, NOT functions we know
   from programming (which can do all kinds of nasty stuff). 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 in its definition, but it may not be
   so simple to learn to understand it. Most students don't get it the first
   time, so don't worry :)

   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 that can intuitively just be seen as
   "search/replace". If you know some programming language already, the
   notation of lambda calculus will seem familiar to functions you already
   know from programming (there are functions, their bodies, arguments,
   variables, ...), but BEWARE, this will also confuse you; functions in
   lambda calculus work a little different (much simpler) than those in
   traditional programming languages; e.g. you shouldn't imagine that
   variables and function arguments represent numbers -- they are really just
   "text symbols", all we're doing with lambda calculus is really
   manipulating text with very simple rules. Things like numbers, their
   addition etc. don't exist at the basic level of lambda calculus, they have
   to be implemented (see later). This is on purpose (feature, not a bug),
   lambda calculus is really trying to explore how simple we can make a
   system to still keep it as powerful as a Turing machine.

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

    1. x: variables, represent unknown values (of course we can use also
       other letters than just x).
    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 S to T, where S and T are lambda terms,
       signifies a function call/invocation (S is the function, T is the
       argument).

   For example (La.(Lb.x)) x is a lambda term while xLx..y is not.

   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 [11]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: Takes a body of a function and replaces a parameter
       inside this body with provided argument, i.e. this is used to reduce
       applications. For example (Lx.xy) a is an application (we apply
       (Lx.xy) to a ). 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 of the whole B-reduction here.

   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 [12]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
   [13]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

     * [14]sigma calculus (for [15]OOP)
     * [16]interaction calculus

Links:
1. math.md
2. function.md
3. functional.md
4. model_of_computation.md
5. turing_machine.md
6. interaction_net.md
7. programming_language.md
8. variable.md
9. side_effect.md
10. syntax.md
11. algebra.md
12. currying.md
13. syntactic_sugar.md
14. sigma_calculus.md
15. oop.md
16. interaction_calculus.md