structural:reformatting, linguistic:translation, information:highlighting
Lambda terms

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 C programs and some are not. A valid lambda calculus expression is called a " lambda term ".

The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms:

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. For convenience, some parentheses can be omitted when writing a lambda term. For example, the outermost parentheses are usually not written. See § Notation, below, for an explicit description of which parentheses are optional. It is also common to extend the syntax presented here with additional operations, which allows making sense of terms such as λ x. x 2. {\displaystyle \lambda x.x^{2}.} The focus of this article is the pure lambda calculus without extensions, but lambda terms extended with arithmetic operations are used for explanatory purposes.

An abstraction λ x. t {\displaystyle \lambda x.t} denotes an § anonymous function that takes a single input x and returns t. For example, λ x. (x 2 + 2) {\displaystyle \lambda x.(x^{2}+2)} is an abstraction representing the function f {\displaystyle f} defined by f (x) = x 2 + 2, {\displaystyle f(x)=x^{2}+2,} using the term x 2 + 2 {\displaystyle x^{2}+2} for t. The name f {\displaystyle f} is superfluous when using abstraction. The syntax (λ x. t) {\displaystyle (\lambda x.t)} binds the variable x in the term t. The definition of a function with an abstraction merely "sets up" the function but does not invoke it.

An application t {\displaystyle t} s {\displaystyle s} represents the application of a function t to an input s, that is, it represents the act of calling function t on input s to produce t (s) {\displaystyle t(s)}.

A lambda term may refer to a variable that has not been bound, such as the term λ x. (x + y) {\displaystyle \lambda x.(x+y)} (which represents the function definition f (x) = x + y {\displaystyle f(x)=x+y}). In this term, the variable y has not been defined and is considered an unknown. The abstraction λ x. (x + y) {\displaystyle \lambda x.(x+y)} is a syntactically valid term and represents a function that adds its input to the yet-unknown y.

Parentheses may be used and might be needed to disambiguate terms. For example,

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 {\displaystyle \lambda x.B}, where B {\displaystyle B} is (λ x. x) x {\displaystyle (\lambda x.x)x}, an anonymous function (λ x. x) {\displaystyle (\lambda x.x)}, with input x {\displaystyle x}; while example 2, M {\displaystyle M} N {\displaystyle N}, is M applied to N, where M {\displaystyle M} is the lambda term (λ x. (λ x. x)) {\displaystyle (\lambda x.(\lambda x.x))} being applied to the input N {\displaystyle N} which is x {\displaystyle x}. Both examples 1 and 2 would evaluate to the identity function λ x. x {\displaystyle \lambda x.x}.