Week 14: Notes

This week's lecture was an introduction to the λ-calculus. Here are a few notes reviewing the material from the lecture. For more information, I recommend these books:

introduction

The lambda calculus is a formal system for expressing computation. It was invented by Alonzo Church in the 1930s. It is an important and very widely used formalism in the theory of programming languages.

Other general models of computation include general recursive functions (Godel, 1933) and Turing machines (Turing, 1936). In the 1930s it was proved that all of these models have the same computational power. We say that a function that can be encoded in any of these models is computable.

In this course we are studying the pure untyped lambda-calculus.

syntax

The syntax of the λ-calculus is defined by this context-free grammar:

expr = var | (expr expr) | (λ var . expr)

In other words, every term is one of the following:

Here are some sample terms:

We use lowercase letters to denote variables. In the following, uppercase letters denote λ terms, e.g. T = (λx.(xx)).

We adopt a couple of precedence rules so we don't need to write so many parentheses:

Furthermore, λxyz.M means λx.λy.λz.M.

The notation M ≡ N means that M and N are syntactically equal, i.e. the same term.

scope

In a subterm λx.M, M is the scope of λx.

An occurrence of a variable x is bound if it is in the scope of some λx, otherwise free.

If x has at least one free occurrence in M, x is a free variable of M. We write FV(M) to denote the set of all free variables of M. For example, FV(xv(λyz.yv)w) = {x, v, w}.

A closed term or combinator has no free variables.

substitution

The notation M[x := N] denotes substituting N for x in M. This means replacing all free occurrences of x with N, renaming bound variables to avoid clashes. For example:

Here is a formal recursive definition of substitution:

α-conversion

Notice that in the last substitution rule above we renamed the variable y to z by replacing (λy.P) with λz.P[y := z].

More generally, if we can replace any subterm (λy.P) in M with λz.P[y := z] (z ∉ FV(P)), yielding N, we write

M →α N ("M α-converts to N")

If we can convert M to N by a series of 0 or more α-conversions, then we write

M ≡α N ("M and N are α-equivalent")

Some basic facts about α-equivalence:

Most authors identify all α-equivalent terms, and I will too. Accordingly, from now on ≡ will actually mean ≡α .

β-reduction

(λx.M)N is called a β-redex and contracts to M[x := N], which is called its contractum.

If P contains a β-redex and we replace it with its contractum, yielding Q, we write

P →β Q ("P β-reduces in one step to Q")

If we can transform P to Q by a series of 0 or more β-reductions, we write

P →*β Q ("P β-reduces to Q")

A β-normal form is a term that contains no β-redexes.

If P →*β Q and Q is in normal form, then we say that Q is a normal form of P.

Does every term have a normal form? No – consider Ω ≡ (λx.x x)(λx.x x), or Ω1 ≡ (λx.xxy)(λx.xxy).

confluence

The Church-Rosser theorem (1935) states: If P →*β M and P →*β N, then there exists T such that M →*β T and N →*β T. In other words, β-reduction is confluent.

evaluation strategies

When we β-reduce a term, at each step we must choose which β-redex to reduce next. There are various evaluation strategies for doing so.

Normal-order reduction always reduces the leftmost outermost redex. An outermost redex is one that is not contained inside any other.

Call by name is like normal order, but performs no reductions inside abstractions. For example, it will stop at λx.((λy.y)z) rather than reducing it to λx.z. This is similar to expression evaluation in Haskell and other non-strict programming languages.

Call by value also performs no reductions inside abstractions, and applies all possible reductions to a redux's right-hand side before reducing the redex. This is similar to expression evaluation in strict programming languages, which include most mainstream languages such as C and Java.

The leftmost reduction theorem (Curry, 1958) states: If P has a normal form Q, then every normal-order reduction of P is finite and ends at Q.

Church booleans

We can encode a variety of data types in the λ-calculus.

To begin with, the Church booleans are defined as follows:

Now we can define

pairs

Church numerals

recursion

It is possible to go further: by using a fixed-point combinator we can define recursive functions and, ultimately, any recursive function. This is, however, a subject for a more advanced class.