Lambda Calculus

Lambda calculus is minimal programming language that's Turing complete. In lambda calculus, everything is an anonymous function. The language was invented by Alonzo Church.


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.


Allows bound variable names to be changed (effectively renaming a variable): e[b/a] means e but with every occurrence of a replaced with b. α-conversion of λx.x might yield λy.y (λx.x[y/x] = ~λy.y). Terms that differ only by α-conversion are called α-equivalent.


Captures the idea of function application. In operational semantics, (λx.M N) -> M[N/x].


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.


True   =  λt.λf.t
False  =  λt.λf.f
If     =  λl.λm.λn.((l m) n)


Pair   =  λf.λs.λb.((b f) s)
First  =  λp.(p True)
Second =  λp.(p False)

Whole Numbers (Church Numerals)

c0     =  λz.λs.z
c1     =  λz.λs.(s z)
c2     =  λz.λs.(s (s z))
cn     =  λz.λs.(s (s ... (s z)))
IsZero =  λm.((m True) (λx.False))