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.

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: ${\displaystyle (\lambda x.\lambda y.(\lambda z.(\lambda x.z\ x)\ (\lambda y.z\ y))(x\ y)).}$

In Extended Backus-Naur Form, this might be summarized as ${\displaystyle e::=v\mid (\lambda v.e)\mid (e\,e)}$, where the variables ${\displaystyle v}$ come from an infinite set ${\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:

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 ${\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.

Following the mathematical concepts of free variables and bound variables, the abstraction operator, ${\displaystyle \lambda }$, 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 ${\displaystyle f(x)=x+y}$ could be represented as the lambda term ${\displaystyle \lambda 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 ${\displaystyle \lambda 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 ${\displaystyle x}$ in the expression is bound by the second lambda: ${\displaystyle \lambda x.y(\lambda x.z\ x)}$ A variable may occur both free and bound in a term; for example ${\displaystyle y}$ in ${\displaystyle y(\lambda y.y)}$.

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