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: ( λ x . λ y . ( λ z . ( λ x . z x ) ( λ y . z y ) ) ( x y ) ) . {\displaystyle (\lambda x.\lambda y.(\lambda z.(\lambda x.z\ x)\ (\lambda y.z\ y))(x\ y)).}
A variable x {\textstyle x} is a character or string representing a parameter, itself a valid lambda term. A lambda abstraction ( λ x . M ) {\textstyle (\lambda x.M)} is a function definition, taking as input the bound variable x {\displaystyle x} (between the λ and the punctum/dot .) and returning the body M {\textstyle 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 ) {\displaystyle (\lambda x.M)} binds the variable x in the term M. For example, λ x . ( x 2 + 2 ) {\displaystyle \lambda x.(x^{2}+2)} is an abstraction representing the anonymous function x ↦ x 2 + 2 {\displaystyle x\mapsto x^{2}+2} . More concretely, we might give this function the name f {\displaystyle f} , and then we could write f ( x ) = x 2 + 2 , {\displaystyle f(x)=x^{2}+2,} , although this name f {\displaystyle f} is superfluous when using the lambda calculus. An application ( M N ) {\textstyle (M\ N)} represents the application of a function M {\textstyle M} to an argument N {\textstyle N} . Both M {\textstyle M} and N {\textstyle N} are lambda terms. The application represents the act of calling function M on input N to produce M ( N ) {\displaystyle M(N)} . In Extended Backus-Naur Form, this might be summarized as e ::= v ∣ ( λ v . e ) ∣ ( e e ) {\displaystyle e::=v\mid (\lambda v.e)\mid (e\,e)} , where the variables v {\displaystyle v} come from an infinite set v 1 , v 2 , v 3 , … {\displaystyle v_{1},v_{2},v_{3},\ldots } , and the other symbols consist of lambda ' λ {\displaystyle \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 . {\displaystyle \lambda 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.
… excerpt ends here. Continue reading the full article.
