Lambda Calculus

Expression  -> Variable | Application | Abstraction
Variable    -> ID
Application -> (Expression Expression)
Abstraction -> λID.Expression

Or condensed as:

e -> x | (e1 e2) | λx.e

• A lambda abstraction λx.e is a definition of an anonymous function capable of taking a single input x and substituting it into (and thus evaluating) the expression e.
• An application (e1 e2) applies the e1 function to the e2 value, that is, it represents the act of calling function e1 on input e2 to product e1(e2).
• In λx.e, e is bound in e (i.e. x would have a value associated with it).
• A free variable is a variable that is not bound. Formally:

  FV(x)       = {x}
  FV((e1 e2)) = FV(e1) U FV(e2)
  FV(λx.e)    = FV(e) - {x}
  

• A combinator is an expression with no free variables.
• A value is an expression in final form (can't be reduced any more), i.e. an abstraction.
• An expression in the form (x e) is stuck.

The meaning of lambda expressions is defined by how expressions can be reduced. Evaluation consists of reducing until either one can't anymore or there is a problem. There are three kinds of reduction: α-conversion, β-reduction, and η-conversion.

Since recursion consists of calling the function within itself, the technique can be tricky because every function is anonymous (that is, it doesn't have a name). To simulate recursion, make a function that you want to be recursive take an extra argument that will be that function itself, the write a wrapper that passes that function as the second argument. For example:

Fact      = λn.λf.If (IsZero n) c1 (Times n (f (Pred n) f))
Factorial = λn.Fact n Fact

The simplest function is the identity function λx.x, it takes something and returns that same thing.