Lambda calculus definition


The lambda calculus is a formal mathematical system consisting of constructing lambda terms and performing [|reduction] operations on them. The definition of a [|lambda term] is simply a variable, a lambda abstraction, or a function application, but a formal presentation can be somewhat lengthy. The focus of this article is to present a full and complete definition of the lambda calculus, specifically the pure untyped lambda calculus without extensions, although a lambda calculus extended with numbers and arithmetic is used for explanatory purposes.

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:
  1. A variable is a character or string representing a parameter, itself a valid lambda term.
  2. A lambda abstraction is a function definition, taking as input the bound variable and returning the body. 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 and returns. The syntax binds the variable in the term. For example, is an abstraction representing the anonymous function. More concretely, we might give this function the name, and then we could write, although this name is superfluous when using the lambda calculus.
  3. An application represents the application of a function to an argument. Both and are lambda terms. The application represents the act of calling function on input to produce.
In Extended Backus-Naur Form, this might be summarized as, where the variables come from an infinite set, and the other symbols consist of lambda , dot '.', and parentheses . A more formal and permissive presentation of the grammar might be as follows:
NameBNFDescription
Expression ::= | | | A lambda term is either an abstraction, an application, a variable, or a bracketed expression.
Abstraction ::= λ . Anonymous function definition.
Variable list ::= , | A comma separated list of variables.
Application ::= +An application is two or more expressions in a row.
Variable ::= *A variable name, e.g. x, y, fact, sum,...
Grouping ::= Expression bracketed with parentheses.

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:
  1. If x is a variable, then
  2. If x is a variable and then
  3. If then
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 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 could be represented as the lambda term, which contains two variables, and. The variable is bound by the lambda abstraction, while is free. The free variable has not been defined and is considered an unknown. The abstraction is a syntactically valid term and represents a function that adds its input to the yet-unknown. Also note that a variable is bound by its "nearest" abstraction. In the following example the single occurrence of in the expression is bound by the second lambda: A variable may occur both free and bound in a term; for example in.
More formally, the sets of free variables and bound variables of a lambda expression,, are denoted as and and can be defined by recursion on the structure of the terms, as follows:
- Free Variable SetComment- Bound Variable SetComment
where x is a variable. In words, the free variables of are just.where x is a variable
Free variables of M, but with removedBound variables of M plus x.
Union of the free variables from the function and the parameterUnion of the bound variables from the function and the parameter

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 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— instead of. However, not all parentheses can be eliminated. For example,
  1. is of form and is therefore an abstraction, while
  2. is of form 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 is a placeholder in both examples.
Here, example 1 defines a function, where is, an anonymous function, with input ; while example 2, , is M applied to N, where is the lambda term being applied to the input which is. Both examples 1 and 2 would evaluate to the identity function.
To allow further concision in these situations, the following conventions are usually applied:
  • Applications are assumed to be left-associative: may be written instead of
  • The body of an abstraction extends as far right as possible: means and not. Said another way, a lambda abstraction has a lower precedence than an application.
  • A sequence of abstractions is contracted: is abbreviated as
  • When all variables are single-letter, the space in applications may be omitted: MNP instead of M ''N P''.

    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 ;
  • β-reduction: applying functions to their arguments, calling functions;
  • η-reduction: which captures a notion of extensionality.
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, is a β-redex in expressing the substitution of for in ; if is not free in, 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 and.

α-conversion

α-conversion, sometimes known as α-renaming, allows bound variable names to be changed. For example, alpha-conversion of might yield. The terms and 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 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 could result in, but it could not result in. 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 with in, we get, 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:
α-conversionλ-expressionde Brujin notationComment
Original expressions.
correctly rename y to k, No change to de Brujin expression.
naively rename y to z, is captured.