Lecture notes on Lambda Calculus – Part 1: Syntax and Operational Semantics

Abstraction expressions take a single formal parameter and, correspondingly applications involve a single argument applied to an expression denoting a function. To avoid clutter, we rely on the following syntactic extension: an expression \(e_0\ e_1\ e_2\) is shorthand for \(((e_0 e_1) e_2)\). The shorthand \(\lambda\ x\ y.\ e\) abbreviates \(\lambda\ x.\ (\lambda\ y.\ e)\).

The size of an expression \(e\), denoted \(|e|\) is recursively defined as follows:

In earlier classes, we learned how to connect identifier references to their binding occurrences (if they exist). A identifier x in an expression e that has a reference occurrence without a corresponding binding occurrence in e is said to occur free in e. Otherwise, it is said to be bound.

The set of free identifiers contained in an expression may also be inductively defined as follows:

Note that it is possible for a identifier to occur free as well as bound in an expression. \(\id{FV}(e)\) denotes the set of all identifiers occurring in an expression, whether free or bound.

An expression is open if it contains free identifiers; it is closed otherwise.

A combinator is an expression that is closed. Examples of some well-known combinators and closed expressions and their names are given below. We use the lambda: notation for curried form of lambda and the : for curried application.

(lambda (x) x)                  ; I combinator, the identity function
(lambda: (x y) x)               ; K combinator.  Note that this short for  
                                ; (lambda (x) (lambda (y) x))

(lambda: (x y z) (: x z (y z))   ; S combinator.  Note that this short for  
                                 ;  (lambda (x) 
                                   (lambda (y) 
                                     (lambda (z) 
                                       ((x z) (y z))))).

(lambda (x) (x x))             ; omega combinator.  
(omega omega)                  ; Omega.  An example of self application.

(lambda (g)                     ; Y combinator.
  ((lambda (x) (g (x x)))       ; Also called the (normal order)
   (lambda (x) (g (x x)))))     ; fixed point combinator


(lambda (g)                                  ; Z combinator
  ((lambda (x) (g (lambda (y) (: x x y))))   ; Also called the (applicative order)
   (lambda (x) (g (lambda (y) (: x x y)))))) ;  fixed point combinator

A renaming is a syntactic operation on an expression in which an identifier is replaced with another in an expression. \(e\set{x/y}\) is read as ``rename in \(e\) the identifier \(x\) with the identifier \(y\).'' It is defined inductively as follows.

Used without restriction, a renaming applied on an expression could transform not just the expression but also its meaning. (Exercise: give an example.) However, we will employ the renaming application sparingly and in the right context so that it actually serves our purpose of establishing α equivalance of two expressions.

The relation \(\alphaequiv\), read α-equivalence, is defined as the smallest binary relation on \(\lambda\)-expressions that is closed under the following rules:

Observe the judicious use of renaming in the definition of α-equivalence.

By α equivalence, we may ensure that all bound identifiers (i.e., formals) in an expression are distinct from each other and any free identifiers.

Show the steps involved in applying the substitution \([x/(y\ z)]\) to \(\lambda\ y.\ \ x\ y\ (\lambda\ y.\ \ y)\). Also refer to the clause in the definition employed at each step, along with evidence that the side conditions are satisfied.

Here are some cases that would arise if we were less than careful with the definition:

The fundamental rewrite rule in the λ-calculus is the β rewrite rule:

The β rule captures the fundamental operation involved in applying a function to its argument: the formal parameter is substituted with the argument in the body of a function.

η reduction captures an optimization in the way functions operate. If a function \(f\) merely passes its formal parameter \(x\) to another function \(g\) we may simply eliminate \(f\) and use \(g\) instead. This idea translates to the following \(\eta\) rewrite rule:

Recall the the definitions of the following properties of an arbitrary reduction system \(\reducesto\):

(a) Confluent (Church-Rosser)

\(\reducesto\) is confluent or has the Church-Rosser property if \(a\simplifiesto b\) and \(a\simplifiesto c\) implies that there exists \(d\) such that \(b\simplifiesto d\) and \(c\simplifiesto d\).

(c) Diamond property

\(\reducesto\) has the diamond property if \(a\reducesto b\) and \(a\reducesto c\) implies there exists \(d\) such that \(b\reducesto d\) and \(c\reducesto d\).

The Diamond property and confluence are related in the following way:

1. Diamond implies Confluence

the proof is by induction on \(\simplifiesto\) deductions. Geometrically, a grid of diamonds may be arranged to fill the area between the rectangle between \(a\), \(b\), \(c\) and \(d\) (See diagram on page 31 of Selinger's notes.)

2 \(\reducesto\) is confluent iff \(\simplifiesto\) satisfies Diamond

this is evident from the definitions of transitive closure and the definitions of the respective properties.

Note that as a consequence of 1., if βη-reduction satisfied the Diamond property, we would have a proof of the confluence of βη-reduction. Unfortunately, however, βη doesn't satisfy the Diamond property.

If we find a relation, say \(\preducesto\), such that:

• A. \(\psimplifiesto\) coincides with \(\simplifiesto\),
• B. \(\preducesto\) satisfies the Diamond property

then, from A., B., and 2., we have a proof of the confluence of \(\reducesto\).

In the rest of sketch, we

• define a relation \(\preducesto\) on λ expressions, called parallel reduction that has the above two properties,
• show Property A,
• define the notion of a maximally parallel reduct, and
• use this to prove Property B.

Intuitively, parallel reduction allows you to look at all redexes in an expression and then apply a subset of them.

The examples above hint that parallel reduction can be simulated with a sequence of reductions. In fact, something stronger is true:

\[\psimplifiesto = \simplifiesto\]

The proof is in three parts:

(a) \(e\reducesto e' \implies e\preducesto e'\)

Each \(\beta\eta\) reduction is a parallel reduction. The proof of this is by induction on \(\reducesto\). The details are in Lemma 4.6(a) of Selinger.

(b) \(e\preducesto e' \implies e\simplifiesto e'\)

Each parallel reduction \(\preducesto\) may be simulated by a sequence of \(\reducesto\) reductions, i.e., by a single \(\simplifiesto\) relation. The proof is by induction on \(\preducesto\). Details are Lemma 4.6(b) of Selinger's notes.

(c) \(\psimplifiesto\) and \(\simplifiesto\) coincide

This is a consequence of (a) and (b) and the definition of reflexive transitive closure. Details are in Lemma 4.6(c) of Selinger's notes.

When all original redexes are applied exhaustively in parallel on an expression \(e\), we get its maximally parallel reduct \(e^*\). Assume that we have an expression \(e\). We define \(e^*\), the unique maximally parallel one-step reduct of \(e\) as follows:

The proof is in two parts:

(a) \(e\preducesto e' \implies e'\preducesto e^*\)

the intuition that once a subset of redexes are applied on an expression \(e\) to yield a residual expression \(e'\), i.e., \(e\preducesto e'\), the residual \(e'\) still has some of the original redexes of \(e\). By applying these remaining original redexes \(e\) via parallel reduction, we can arrive at \(e^*\). Recall that its possible to steer \(e'\) into a reduction sequence that takes us into an expression quite different from \(e^*\). But all we are saying here is that there is a way to get from \(e'\) to \(e^*\). The formal proof is by induction on \(e\) and given as Lemma 4.8 in Selinger's notes. The second case in the proof of Lemma 4.8 depends on a Substitution Lemma (Lemma 4.7) in Selinger's notes. Please read both proofs.

(b) \(\preducesto\) satisfies the Diamond Property

Pick any two expressions \(e_1\) and \(e_2\) such that \(e\preducesto e_1\) an \(e\preducesto e_2\). From (a), it follows that \(e_1\preducesto e^{*}\) and \(e_2\preducesto e^{*}\). Thus, \(\preducesto\) satisfies the Diamond Property.

In full reduction, any redex in the expression may be picked as the next one for reduction. In the example below, adapted from Pierce's book (TAPL), the following is one possible full reduction sequence:

Note that the disadvantage of complete choice in full reduction is that one may veer off into a non-terminating reduction of an expression sequence even though the expression has a normal form. Just consider the expression \((\lambda\ x.\ \id{Id})\ \Omega\) with the hopeless strategy of always ignoring the top level redex and choosing instead to reduce Ω.

If an expression has a normal form, is there a strategy that guarantees arriving at it, without getting sucked into an infinite reduction sequence? The next strategy answers this in the affirmative.

The normal order strategy is based on the observation that given any two redexes at positions \(i\) and \(j\) in an expression \(e\):

• 1. Seen from the root, \(i\) `above' \(j\) (or vice versa), or
• 2. Either \(i\) is to the left of \(j\) (or vice versa).
• It is not possible for two redexes in a \(\lambda\) expression to overlap.

Normal order strategy involves locating the next redex in the expression \(e\) as follows:

• 1. If \(e\) is a redex, use it
• 2. If \(e\) is not a redex but a λ abstraction \(\lambda\ x.\ e'\), then locate the redex inside the body \(e'\).
• 3. If \(e\) is not a redex but an application, \((e_1\ e_2)\), then locate the redex in the \(e_1\).
• 4. If there's no redex in \(e_1\), then locate a redex in \(e_2\).

This result is called the `Standardization' theorem in λ calculus. A proof of this result using parallel reductions (see above) is given in Takahashi's Parallel Reductions in λ-calculus 1995 paper (Information and Computation No. 118, 120-127). Another approach for the standardization result λ-calculus is in Ryo Kashima's 2000 paper, using a inductively defined notion of β-reducibility with a standard sequence.

The applicative order strategy requires that in any β redex, the argument position is in normal form before the β redex is chosen for reduction.

• Apply normal order strategy but stop when you hit an abstraction: no reductions inside abstractions.

This was the strategy adopted in the Algol programming language. Although now dead, Algol pioneered many concepts in the design of programming. It was amongst the first high level programming languages based directly on λ-calculus. The official report defining the Scheme/Racket language is dedicated to the memory of Algol.

The call by name strategy can cause duplicate evaluations.

The other language that is based on the call by name strategy is the programming language Haskell. Actually Haskell uses a strategy called lazy evaluation. Lazy evaluation may be seen as an optimization over the call by name strategy in which values once computed are stored, to avoid recomputation.

The call by value strategy uses the following rules:

• 1. Choose the outermost redex
• 2. Do not choose any redex inside a λ abstraction.
• 3. When applying a β-redex, ensure that the argument expression is in normal form.

Here is an example of simplification using a call-by-value strategy:

The call-by-value strategy is the one most commonly by programming languages: C, Java, Scheme, Python, included.

We say that in call-by-value, function application is strict on the arguments: the application doesn't trigger unless the arguments are in normal forms.

Here is an example of the expression

\[(\lambda\ x.\ (\lambda\ z.\ \id{Id}\ \ \id{Id})) (\lambda\ y. \Omega)\]

simplified under various reduction strategies

NPTEL course on POPL: Church-Rosser lecture notes

TAPL chapter on The Untyped Lambda Calculus

Photocopy of chapter from Types and Programming Languages by Benjamin Pierce. Available on reserve at the library.

Peter Selinger's notes on the Lambda Calculus

The definitions of renaming, α equivalence, substitution application and the proof sketch for the Church-Rosser property of λ-calculus is based on these notes.

Susan Horwtiz's notes on the lambda calulus

Has lot's of good examples.

A mechanical proof of the Church Rosser Theorem

by N. Shankar. JACM 1988. An account of perhaps the earliest mechanised proof of the Church-Rosser theorem for Lambda Calculus. Uses the main idea of a walk (parallel reduction). Shankar quotes Rosser about the long and somewhat tortuous history of the proof of the theorem. Note that "reduction" in the paper refers to the notion of simplification as done in class.

Kashima's proof of the Standardization theorem

Dave Schmidt's (Kansas State Univ) chapter on Lambda Calculus

Lambda Calculus Types and Models by Jean-Louis Krivine

Univ Chicago Class notes on λ-calculus

by Acar and Ahmed.

OpenDSA Programming Languages

Introduction to Lambda calculus by Barendregt and Barendsen

History of the Lambda-Calculus and Combinatory Logic

by Felice Cardone and J Roger Hindley

Smolka's notes on Confluence and Normalization in Reduction Systems

Logical Verification slides on Confluence

Normal forms

discusses diff between NF, HNF and WHNF.

Harvard CS152 lec on Reductions and λ calculus

Vriej University book on Term Rewriting

Short, neat intro to the Lambda calculus by Paul Hudak

Columbia Univ Fall 2010 slides on the lambda calculus

Head Normal Form

WHNF

Wikipedia page on Beta normal form

gives formal defn of head normal form.

Normark's online book on Programming Languages

Rewrite rules, reduction and normal forms.

Church-Turing Thesis: Story and Recent Progress

Lecture by Yuri Gurevich