The λ (lambda) calculus, invented and published by Alonzo Church in the 1920s and 1930s, is one of the three best-known formulations of computable functions (along with Turing machines and partially recursive functions). The λ calculus is useful to our study of programming languages for several reasons:

  • Purity and functions: We can regard the lambda calculus as “the simplest reasonable pure functional programming language.” Studying it gets at the essence of (anonymous) functions and shows that they are really all we need.
  • Subsitution: The semantics of the lambda calculus is defined by a substitution-based evaluation model that is different from but equivalent to the environment-based evaluation models we have studied so far with Racket and ML. Studying this alternative execution model reinforces our understanding of the environment-based model and (if time) gives us a foundation for studying macro systems.
  • Evaluation order: Unlike the evaluation rules for Racket and ML, the semantics of the lambda calculus allows multiple evaluation orders (i.e., after each step of evaluation, there may be a choice of what to evaluate next).

Syntax

Terms M of the lambda calculus are defined by the following grammar:

M ::= x | (M M) | (λx.M)

There are three forms:

  • Variables x
  • Application (M1 M2), applying M1 to M2.
  • Lambda abstraction (λx.M), defining an abstraction over the variable x. (Think: anonymous function whose single parameter is named x.)

That’s all! The entire language is variables, applications, and abstractions (a.k.a. functions). For convenience or clarity we sometimes drop or add parentheses. When parentheses in applications are omitted, they are assumed to be left-associative. For example, M N O is the same as (M N) O (think currying).

Evaluation Rules

Evaluation (or reduction) of expressions (terms) in the lambda calculus is based on subsitution. Rather than recording bindings of variables to values in environments and later looking up values for variables in these environments, reduction of lambda calculus terms proceeds by rewriting terms to replace occurrences of a variable with its value.

However, substition cannot be used to replace all occurrences of a variable blindly. Substition must respect scope. We first consider two scoping problems which substition must avoid, illustrated by examples in ML. The rest of this section defines the necessary support to perform correct substitution in the lambda calculus.

Example Subsitution Problems in ML

The following incorrect substituions in ML expressions illustrate how blind substitution can go wrong.

  1. Start with the ML expression:

     let val x = 1
 in
     let val x = x + 8
     in
         x + 7
     end
 end

    Now, replace all uses of “x” with 1, yielding:

     let val x = 1 + 8
 in
     1 + 7
 end

    This program clearly yields a different result than the original ML program and also clearly gets scoping wrong. Substituion must not proceed within the scope of a binding that shadows the variable being replaced.

  2. Start with the ML expression:

     let val x = 1
     val f = fn y => y + x
 in
     let val x = 7
     in
         f 8
     end
 end

    Now, replace all uses of “f” by “fn y => y + x”:

     let

Lexical Scope and Free Variables

When defining first-class functions in Racket and ML, we were very careful about preserving lexical scope, especially in the evaluation of function applications. We introduced the idea of a function closure to help ensure that a function’s body is evaluated in the environment in which it is defined (instead of the environment in which it is applied). The job of a closure is to attach the definition-time environment to a function body, so that when evaluating that function body, any variables in the function body are looked up in the proper environment. Variables for which this matters are called free variables in the function. Variables are free in an expression if their use is not within a scope where they are bound. Although we will not use encironments to define the evaluation of lambda calculus expressions, free variables are still important.

Example in ML

In the following ML code, y is a free variable in the function f. Likewise, z is free in the expression z - 2.

val y = 1
fun f x = x + y
val w = let val z = 3 in z - 2 end

Free variables are defined for an expression without regards to its surrounding context. Hence z is free in z - 2 even though it is bound in the containing expression let val z = 3 in z - 2 end.

Free Variables in the Lambda Calculus

Free variables in a lambda calculus term M (written FV(M)) are defined as follows:

  • FV(x) = {x}: x is free in the term x
  • FV(M N) = FV(M) ∪ FV(N): the free varialbes in an application are the union of the free variables of both subexpressions.
  • FV(λx.M) = FV(M) - {x}: the free variables of a lambda abstraction are all of the free variables of its body expression, minus the variable over which the abstraction applies (a.k.a., the parameter).

For example, FV((λz.z) (λx.(λy.x))) = {}, while FV(λy.x) = {x}.

Evaluation Rules

Evaluation (or reduction) of expressions (terms) in the lambda calculus is based on subsitution. Rather than introducing bindings of variables to values and later looking up values for variables in environments, reduction of the lambda calculus proceeds by rewriting terms to replace all occurrences of a variable with its value.

There are three reduction rules for the lambda calculus. Evaluation (a.k.a., reduction) proceeds by rewriting the lambda expression according to these rules. Any of these rules may be applied to reduce a lambda calculus expression or any of its subexpressions in any order. The notation M → M’ indicates that M may be reduced to M’. The notation [N/x] M indicates the term M with all free occurences of the variable x replaced by N.

  • Renaming (α-reduction): λx.M → λy.([y/x]M), if y ∉ FV(M).
  • Substitution (β-reduction): (λx.M) N → [N/x] M
  • η-reduction: (λx.(M x)) → M