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.