Notes on the Pure Untyped Lambda Calculus
-----------------------------------------
Bernie Pope.
For the sake of simplicity I will hereafter refer to the Pure Untyped Lambda
Calculus as LC.
1. Syntax
---------
The syntax of LC is as follows:
e ::= x | e_1 e_2 | \x.e
Note: x is a "meta variable", and it ranges over the set of possible
identifier names. The notation "e_1" means an expression "e" subscripted by
1, allowing it to possibly be different to e_2 etcetera.
The form "\x.e" is called a "lambda abstraction", where "\x" is its head
and "e" is its body.
The form "e_1 e_2" is an application, where e_1 is the function, and e_2
is its argument. Sometimes e_1 is called a "rator" and e_2 a "rand"
(also operator and operand).
Parentheses can be added to indicate grouping, and application is left
associative, so:
e_1 e_2 e_3
can also be written (redundantly):
(e_1 e_2) e_3
which is _different_ to:
e_1 (e_2 e_3)
2. Bound and free variables
---------------------------
In the expression \x.e, the variable denoted by x is said to be bound in
the (whole) expression. An occurrence of a variable which is not bound by
an outer lambda abstraction is said to be free.
A variable can be both bound and free in an expression, for example:
x (\x.x)
The outer occurrence of x is free, and the inner occurrence is bound.
The set of free variables in an expression can be computed like so:
FV(x) = {x}
FV(e_1 e_2) = FV(e_1) union FV(e_2)
FV(\x.e) = FV(e) minus {x}
An expression which contains no free variables is said to be "closed".
3. Redexes and normal forms
---------------------------
A "redex" is a reducible expression.
Normally we have two kinds of redex:
1) Beta redexes, of the form: (\x.e_1) e_2
2) Eta redexes, of the form: (\x. e x), where x is not free in e.
Some versions of LC recognise only the beta redexes.
An expression is a normal form if it contains no redexes. More specifically, an
expression is a "beta normal form" if it contains no beta redexes, similarly for
"eta normal forms", and "beta-eta normal forms".
4. Conversion and reduction
---------------------------
A redex can be "reduced" by the application of an associated reduction rule.
We introduce a relation called "->" which denotes the reduction of one expression
to another by the single application of a reduction rule:
e_1 -> e_2
Eta: (\x. e x) -> e , if x is not free in e.
Beta: (\x.e_1) e_2 -> e_1[e_2/x] , may require alpha renaming to avoid
variable capture.
The notation e_1[e_2/x] means "replace all free occurrences of the variable x
in e_1 with the expression e_2". The rules for substitution are subtle due to
the need to protect against variable capture.
We also have the concept of "alpha conversion" which is the systematic
renaming of the variable bound in the head of a lambda abstraction, and all free
occurrences of that variable in the body of the lambda abstraction.
Expressions are usually considered equivalent if they are alpha convertible.
Sometimes the -> relation is annotated with eta or beta to indicate which
reduction rule was applied, though it can be inferred from the context.
The -> relation represents exactly one reduction step.
We also introduce the reflexive transitive closure of ->, called ->*, like so:
e ->* e
if e_1 -> e_2 then e_1 ->* e_2
if e_1 -> e_2 and e_2 -> e_3 then e_1 ->* e3
Thus, ->* represents zero or more reduction steps.
Two expressions e_1 and e_2 are "convertible" if they can be rewritten to
each other using zero or more forward or backward applications of the
reduction rules and alpha conversion.
5. Normalisation
----------------
Not all expressions have normal forms, e.g.
(\x. x x) (\x. x x)
6. Reduction order
------------------
The order of reduction _can_ influence whether or not a normal form is found.
For example,
let CONST = \x.(\y.x)
LOOP = (\x.x x) (\x.x x)
Consider this expression:
CONST z LOOP
Reduction of this expression loops forever if the rightmost redex is
always reduced first. But reduction terminates with "z" as a normal
form if the leftmost redex is always reduced first.
A redex is "innermost" if it does not contain any sub-expressions which are
redexes. A redex is "outermost" if it is not contained within another redex.
There may be multiple innermost redexes, and multiple outermost redexes.
The outermost redexes and the innermost redexes can be ordered according to
their position in a left-to-right rendering of an expression.
The "normal order" reduction strategy always chooses the leftmost outermost
redex. The "applicative order" reduction strategy always chooses one of
the innermost redexes (conventionally the leftmost one).
Normal order is guaranteed to reduce to a normal form if one exists for
the initial expression, whereas the applicative order does not give
the same guarantee.
Unsurprisingly, reduction order in LC is closely related to parameter
passing strategies which are used in programming languages. The normal
order has connections to "lazy" parameter passing, and the applicative
order has connections to "eager" parameter passing. But we must be
careful with loose terminology. "Lazy" and "eager" have specific
procedural definitions which are not completely captured by
the normal and applicative strategies. For instance, "lazy" implies
some kind of sharing of argument expressions, to avoid duplicated
work.
Of course other strategies are also possible, such as parallel reduction,
where multiple redexes are reduced at the same time.
7. Church Rosser theorem (confluence of reduction in LC)
--------------------------------------------------------
This is the simplest form of the theorem, and the one most commonly cited:
If e_1 ->* e_2, and e_1 ->* e_3, then there exists an expression e_4,
such that e_2 ->* e_4, and e_3 ->* e_4.
Corollary: if an expression has a normal form, then it is unique.
Confluence is usually considered an important property of computing
systems, but it is not universally required. For instance, there are
other term rewriting systems which are not confluent, but still of
interest (to some people).
8. Fixed point theorem
----------------------
All expressions in LC can be regarded as functions, and all expressions
have at least one fixed point. See my notes on fixed points.