Lambda calculus definition

Lambda terms

The lambda calculus consists of a language of lambda terms, that are defined by a certain formal syntax. The syntax of the lambda calculus defines some expressions as valid lambda calculus expressions and some as invalid, just as some strings of characters are valid computer programs and some are not. A valid lambda calculus expression is called a "lambda term". In the simplest form of lambda calculus, terms are built using only the following three rules. These rules give an inductive definition that can be applied to build all syntactically valid lambda terms, and produce expressions such as: $(λ x . λ y . (λ z . (λ x . z x) (λ y . z y)) (x y)) .$

A variable $x$ is a character or string representing a parameter, itself a valid lambda term.
A lambda abstraction $(λ x . M)$ is a function definition, taking as input the bound variable $x$ (between the λ and the punctum/dot .) and returning the body $M$ . The definition of a function with an abstraction merely "sets up" the function but does not invoke it. An abstraction denotes an anonymous function that takes a single input x and returns M. The syntax $(λ x . M)$ binds the variable x in the term M. For example, $λ x . (x^{2} + 2)$ is an abstraction representing the anonymous function $x \mapsto x^{2} + 2$ . More concretely, we might give this function the name $f$ , and then we could write $f (x) = x^{2} + 2,$ , although this name $f$ is superfluous when using the lambda calculus.
An application $(M N)$ represents the application of a function $M$ to an argument $N$ . Both $M$ and $N$ are lambda terms. The application represents the act of calling function M on input N to produce $M (N)$ .

In Extended Backus-Naur Form, this might be summarized as $e ::= v ∣ (λ v . e) ∣ (e e)$ , where the variables $v$ come from an infinite set $v_{1}, v_{2}, v_{3}, \dots$ , and the other symbols consist of lambda ' $λ$ ', dot '.', and parentheses '(' and ')'. A more formal and permissive presentation of the grammar might be as follows:

The set of lambda expressions is defined inductively, for example as a set Λ, where the results of applying rules 1-3 are all and only the elements of Λ. In the strictest sense, nothing else is a lambda term. That is, a lambda term is valid if and only if it can be obtained by repeated application of these three rules. Formally:

If x is a variable, then x ∈ Λ.
If x is a variable and M ∈ Λ, then (λx.M) ∈ Λ.
If M, N ∈ Λ, then (M N) ∈ Λ.

Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications.

It is also common to extend the syntax presented here with additional operations, for example introducing terms for mathematical constants and operations, which allows making sense of terms such as $λ x . x^{2} .$ The untyped lambda calculus is flexible in that it does not distinguish between different kinds of data. For instance, there may be a function intended to operate on numbers. However, in the untyped lambda calculus, there is no way to prevent a function from being applied to truth values, strings, or other non-number objects. Depending on the encoding of the data, this may lead to nonsensical results, or work as intended.

Free and bound variables

Following the mathematical concepts of free variables and bound variables, the abstraction operator, $λ$ , is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of an abstraction are said to be bound, and the part λx is often called the binder of x. Variables that are not bound are called free. For example, the function definition $f (x) = x + y$ could be represented as the lambda term $λ x . (x + y)$ , which contains two variables, x and y. The variable x is bound by the lambda abstraction, while y is free. The free variable y has not been defined and is considered an unknown. The abstraction $λ x . (x + y)$ is a syntactically valid term and represents a function that adds its input to the yet-unknown y. Also note that a variable is bound by its "nearest" abstraction. In the following example the single occurrence of $x$ in the expression is bound by the second lambda: $λ x . y (λ x . z x)$ A variable may occur both free and bound in a term; for example $y$ in $y (λ y . y)$ .

More formally, the sets of free variables and bound variables of a lambda expression, $M$ , are denoted as $FV (M)$ and $BV (M)$ and can be defined by recursion on the structure of the terms, as follows:

An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic. It is common to restrict discussion to only closed terms, and some presentations of the lambda calculus only consider closed terms. For example, the lambda term representing the identity $λ x . x$ has no free variables and is closed.

Notation

For convenience, parentheses can be dropped if the expression is unambiguous. For example, the outermost parentheses can always be dropped— $M N$ instead of $(M N)$ . However, not all parentheses can be eliminated. For example,

$λ x . ((λ x . x) x)$ is of form $λ x . B$ and is therefore an abstraction, while
$(λ x . (λ x . x)) x$ is of form $M N$ and is therefore an application.

The examples 1 and 2 denote different terms, differing only in where the parentheses are placed. They have different meanings: example 1 is a function definition, while example 2 is a function application. The lambda variable x is a placeholder in both examples.

Here, example 1 defines a function $λ x . B$ , where $B$ is $(λ x . x) x$ , an anonymous function $(λ x . x)$ , with input $x$ ; while example 2, $M$ $N$ , is M applied to N, where $M$ is the lambda term $(λ x . (λ x . x))$ being applied to the input $N$ which is $x$ . Both examples 1 and 2 would evaluate to the identity function $λ x . x$ .

To allow further concision in these situations, the following conventions are usually applied:

Applications are assumed to be left-associative: $M N P$ may be written instead of $((M N) P)$
The body of an abstraction extends as far right as possible: $λ x . M N$ means $λ x . (M N)$ and not $(λ x . M) N$ . Said another way, a lambda abstraction has a lower precedence than an application.
A sequence of abstractions is contracted: $λ x . λ y . λ z . N$ is abbreviated as $λ x y z . N$
When all variables are single-letter, the space in applications may be omitted: MNP instead of M N P.

2 more chapters are free with a Lably account.

Transformation and reduction

The meaning of lambda expressions is defined by how expressions can be transformed and reduced.

There are three kinds of transformation:

α-conversion: changing bound variables (alpha);
β-reduction: applying functions to their arguments (beta), calling functions;
η-reduction: which captures a notion of extensionality (eta).

We also speak of the resulting equivalences: two expressions are β-equivalent, if they can be β-converted into the same expression, and α/η-equivalence are defined similarly.

The term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, $(λ x . M) N$ is a β-redex in expressing the substitution of $N$ for $x$ in $M$ ; if $x$ is not free in $M$ , $λ x . M x$ is an η-redex. The expression to which a redex reduces is called its reduct; using the previous example, the reducts of these expressions are respectively $M [x := N]$ and $M$ .

α-conversion

α-conversion (alpha-conversion), sometimes known as α-renaming, allows bound variable names to be changed. For example, alpha-conversion of $λ x . x$ might yield $λ y . y$ . The terms $x$ and $y$ by themselves are not alpha-equivalent, because they are not bound in an abstraction. Terms that differ only by alpha-conversion are called α-equivalent, capturing the intuition that the particular choice of a bound variable, in an abstraction, does not (usually) matter. Frequently in uses of lambda calculus, α-equivalent terms are considered to be equivalent.

The precise rules for alpha-conversion are not completely trivial. First, when alpha-converting an abstraction, the only variable occurrences that are renamed are those that are bound by the same abstraction. For example, an alpha-conversion of $λ x . λ x . x$ could result in $λ y . λ x . x$ , but it could not result in $λ y . λ x . y$ . The latter has a different meaning from the original. This is analogous to the programming notion of variable shadowing.

Second, alpha-conversion is not possible if it would result in a variable getting captured by a different abstraction. For example, if we replace $x$ with $y$ in $λ x . λ y . x$ , we get $λ y . λ y . y$ , which is not at all the same. In the De Bruijn index notation, any two α-equivalent terms are syntactically identical, and confusion in this way cannot occur.

See example:

Substitution

Substitution, written $E [V := R]$ , is the process of replacing all free occurrences of the variable $V$ in the expression $E$ with expression $R$ . Substitution on terms of the lambda calculus is defined by recursion on the structure of terms, as follows (note: x and y are variables while M and N are any λ expression).

$x [x := N] = N$ ; with $N$ substituted for $x$ , $x$ becomes $N$
$y [x := N] = y$ if $x \neq y$ ; with $N$ substituted for $x$ , $y$ (which is not $x$ ) remains $y$
$(M_{1} M_{2}) [x := N] = (M_{1} [x := N]) (M_{2} [x := N])$ ; substitution distributes to both sides of an application
$(λ x . M) [x := N] = λ x . M$ ; a variable bound by an abstraction is not subject to substitution; substituting such a variable leaves the abstraction unchanged
$(λ y . M) [x := N] = λ y . (M [x := N])$ if $x \neq y$ and $y \notin F V (N)$ ; substituting a variable which is not bound by an abstraction proceeds in the abstraction's body, provided that the abstracted variable $y$ is "fresh" for the substitution term $N$ , meaning it does not appear among the free variables of $N .$

For example, $(λ x . x) [y := y] = λ x . (x [y := y]) = λ x . x$ , and $((λ x . y) x) [x := y] = ((λ x . y) [x := y]) (x [x := y]) = (λ x . y) y$ .

The freshness condition (requiring that $y$ is not in the free variables of $N$ ) is crucial in order to ensure that substitution does not change the meaning of functions. The situation where the substituted $x$ was supposed to be free but ended up being bound is a situation known as capturing $x$ . To substitute into a lambda abstraction, it is sometimes necessary to α-convert the expression. For example, this substitution $(λ x . y) [y := x] \neq λ x . (y [y := x]) = λ x . x$ is erroneous because it would turn the constant function $λ x . y$ into the identity $λ x . x$ . The correct substitution is to rename the bound variable using α-equivalence, in this case $(λ x . y) [y := x] = (λ z . y) [y := x] = λ z . (y [y := x]) = λ z . x$ .

In general, failure to meet the freshness condition can be remedied by alpha-renaming first, with a suitable fresh variable. Substitution is defined uniquely up to α-equivalence. Most implementations of substitution use alpha-conversion automatically to avoid capture during substitution, an operation called capture-avoiding substitution. In programming languages with static scope, capture-avoiding substitution can be used to implement name resolution by carefully handling variable shadowing in containing scopes. Another strategy is to require alpha renaming in the source program to make name resolution trivial. If De Bruijn indexing is used, then α-conversion is no longer required, as there will be no name collisions. Variable names are also not needed if a universal function is used, such as in Iota and Jot.

β-reduction

β-reduction (beta reduction) captures the idea of function application. β-reduction is defined in terms of substitution: the β-reduction of $((λ V . E) E^{'})$ is $E [V := E^{'}]$ . The β-reduction rule states that an application of the form $(λ x . t) s$ reduces to the term $t [x := s]$ . The notation $(λ x . t) s \to t [x := s]$ is used to indicate that $(λ x . t) s$ β-reduces to $t [x := s]$ . β-reduction captures the idea of function application (also called a function call), and implements the substitution of the actual parameter expression for the formal parameter variable. β-reduction can be seen to be the same as the concept of local reducibility in natural deduction, via the Curry–Howard isomorphism.

For example, for every $s$ , $(λ x . x) s \to x [x := s] = s$ . This demonstrates that $λ x . x$ really is the identity. Similarly, $(λ x . y) s \to y [x := s] = y$ , which demonstrates that $λ x . y$ is a constant function. Assuming some encoding of $2, 7, \times$ , we have the following β-reduction: $((λ n . n \times 2) 7) \to 7 \times 2$ .

More formally, β-reduction may be performed on the lambda abstraction without alpha renaming only if no variable names are free in the actual parameter and bound in the body:

F V (y) \cap B V (b) = {} \to (λ x . b) y = b [x := y]

Alpha renaming may be used on $b$ to rename names that are free in $y$ but bound in $b$ , to meet the pre-condition for this transformation. See example:

Looking closer, the key substitutions are

\begin{array}{r} ((λ x . z x) (λ y . z y)) [z := (x y)] (blocked - will capture) \\ ((λ a . z a) (λ b . z b)) [z := (x y)] (allowed - no capture) \end{array}

In this example,

In the β-redex,
1. The free variables are, $FV (x y) = {x, y}$
2. The bound variables are, $BV ((λ x . z x) (λ y . z y)) = {x, y}$
The naive β-reduction changed the meaning of the expression because x and y from the actual parameter became captured when the expressions were substituted in the inner abstractions.
The alpha renaming removed the problem by changing the names of x and y in the inner abstraction so that they are distinct from the names of x and y in the actual parameter.
1. The free variables are, $FV (x y) = {x, y}$
2. The bound variables are, $BV ((λ a . z a) (λ b . z b)) = {a, b}$
The β-reduction then proceeded with the intended meaning.

η-reduction

η-reduction (eta reduction) converts from $λ x . (f x)$ to $f$ , given that $x$ does not appear free in $f$ . The problem with using an η-reduction when f has free variables is shown in this example:

This improper use of η-reduction changes the meaning by leaving x in $λ y . y x$ unsubstituted.

η-reduction is often paired with its inverse, η-expansion, which converts from $f$ to $λ x . (f x)$ , again given that $x$ does not appear free in $f$ . The two processes together are called η-conversion. η-conversion expresses the idea of extensionality, which in this context is that two functions are the same if and only if they give the same result for all arguments. η-conversion can be seen to be the same as the concept of local completeness in natural deduction, via the Curry–Howard isomorphism.

Evaluation and normalization

The lambda calculus may be seen as an idealized version of a functional programming language, like Haskell or Standard ML. Under this view, β-reduction corresponds to a computational step. This step can be repeated by additional β-reductions until there are no more applications left to reduce. If evaluation does terminate, the result is a lambda expression that cannot be reduced further by β-reduction. This is called the normal form of the expression. A lambda expression that cannot be reduced further by β-reductions is in beta normal form, and similarly if it also cannot be reduced by η-reductions it is in beta-eta normal form. All normal forms that can be converted into each other by α-conversion are defined to be equal. By the Church–Rosser theorem, the normal form is unique if it exists, regardless of the order in which the reductions are performed (the reduction strategy).

However, not all lambda expressions have a normal form. For example, consider the term $Ω = (λ x . x x) (λ x . x x)$ . Here $(λ x . x x) (λ x . x x) \to (x x) [x := λ x . x x] = (x [x := λ x . x x]) (x [x := λ x . x x]) = (λ x . x x) (λ x . x x)$ . That is, the term reduces to itself in a single β-reduction, and therefore the reduction process will never terminate. Typed lambda calculi, such as the simply typed lambda calculus, do not allow the construction of terms like $Ω$ , and therefore all well-typed terms in these systems have a normal form.