Lambda calculus
Encyclopedia
In mathematical logic
and computer science
, lambda calculus, also written as λcalculus, is a formal system
for function
definition, function application and recursion
. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus. In both typed lambda calculus
and untyped versions, ideas from lambda calculus have found application in the fields of logic
, recursion theory (computability)
, and linguistics
, and have played an important role in the development of the theory of programming languages
(with untyped lambda calculus being the original inspiration for functional programming
, in particular Lisp, and typed lambda calculi serving as the foundation for modern type system
s). This article deals primarily with the untyped lambda calculus.
in the 1930s as part of an investigation into the foundations of mathematics
. The original system was shown to be logically inconsistent
in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.
Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus
.
are a fundamental concept within computer science
and mathematics. The λcalculus provides simple semantics for computation with functions so that properties of functional computation can be studied.
Consider the following two examples. The identity function
takes a single input, x, and immediately returns x (i.e. the identity does nothing with its input), whereas the function
takes a pair of inputs, x and y and returns the sum of their squares, x*x + y*y. Using these two examples, we can make some useful observations that motivate the major ideas in the lambda calculus.
The first observation is that functions need not be explicitly named. That is, the function
can be rewritten in anonymous form
as
(read as “the pair of x and y is mapped to x*x + y*y”). Similarly,
can be rewritten in anonymous form as x ↦ x, where the input is simply mapped to itself.
The second observation is that the specific choice of name for a function's arguments is largely irrelevant. That is,
express the same function: the identity. Similarly,
also express the same function.
Finally, any function that requires two inputs, for instance the before mentioned sqsum function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts a single input. For example,
can be reworked into
This transformation is called currying
, and can be generalized to functions accepting an arbitrary number of arguments.
Currying may be best grasped intuitively through the use of an example. Compare the function
with its curried form,
Given two arguments, we have:
However, using currying, we have:
and we see the uncurried and curried forms compute the same result. Notice that x*x has become a constant.
Since the names of functions are largely a convenience, the lambda calculus has no means of naming a function. Since all functions expecting more than one input can be transformed into equivalent functions accepting a single input (via Currying
), the lambda calculus has no means for creating a function that accepts more than one argument. Since the names of arguments are largely irrelevant, the native notion of equality on lambda terms is alphaequivalence (see below), which codifies this principle.
Nothing else is a lambda term, though bracketing may be used to disambiguate terms.
Intuitively, a lambda abstraction λx.t represents an anonymous function that takes a single input, and the λ is said to bind x in t, and an application ts represents the application of input s to some function t. In the lambda calculus, functions are taken to be first class values
, so functions may be used as the inputs to other functions, and functions may return functions as their outputs.
For example, λx.x represents the identity function, x ↦ x, and (λx.x)y represents the identity function applied to y. Further, (λx.y) represents the constant function x ↦ y, the function that always returns y, no matter the input. It should be noted that function application is leftassociative, so (λx.x)y z = ((λx.x)y)z.
Lambda terms on their own aren't particularly interesting.
What makes them interesting are the various notions of equivalence and reduction that can be defined over them.
This states that the particular choice of bound variable, in a lambda abstraction, doesn't (usually) matter.
For instance, λx.x and λy.y are alphaequivalent lambda terms, representing the same identity function.
Note that the terms x and y aren't alphaequivalent, because they are not bound in a lambda abstraction.
In many presentations, it is usual to identify alphaequivalent lambda terms.
The following definitions are necessary in order to be able to define beta reduction.
That is, the free variables of x are just x; the free variables of λx.t are the free variables of t, with x removed, and the free variables of ts are the union of the free variables of t and s.
For example, the lambda term representing the identity λx.x has no free variables, but the constant function λx.y has a single free variable, y.
Suppose t, s and r are lambda terms and x and y are variables.
We write t[x := r] for the substitution of r for x in t, in a captureavoiding manner.
That is:
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 r) is crucial in order to ensure that substitution does not change the meaning of functions.
For example, suppose we define another substitution action without the freshness condition.
Then, (λx.y)[y := x] = λx.(y[y := x]) = λx.x, and the constant function λx.y turns into the identity λx.x by substitution.
If our freshness condition is not met, then we may simply alpharename with a suitably fresh variable.
For example, switching back to our correct notion of substitution, in (λx.y)[y := x] the lambda abstraction can be renamed with a fresh variable z, to obtain (λz.y)[y := x] = λz.(y[y := x]) = λz.x, and the meaning of the function is preserved by substitution.
For example, for every s we have (λx.x)s → x[x := s] = s, demonstrating that λx.x really is the identity.
Similarly, (λx.y)s → y[x := s] = y, demonstrating that λx.y really is a constant function.
The lambda calculus may be seen as an idealised functional programming language, like Haskell
or Standard ML
.
Under this view, beta reduction corresponds to a computational step, and in the untyped lambda calculus, as presented here, reduction need not terminate.
For instance, consider the term (λx.xx)(λx.xx).
Here, we have (λx.xx)(λx.xx) → (xx)[x := λx.xx] = (x[x := λx.xx])(x[x := λx.xx]) = (λx.xx)(λx.xx).
That is, the term reduces to itself in a single beta reduction, and therefore reduction will never terminate.
Another problem with the untyped lambda calculus is the inability to distinguish between different kinds of data.
For instance, we may want to write a function that only operates on numbers.
However, in the untyped lambda calculus, there's no way to prevent our function from being applied to truth values, or strings, for instance.
Typed lambda calculi, which will be introduced later in the article, have the property that if a term is welltyped, then it never gets "stuck" (where there is no evaluation rule for the term), and that if a term e has a particular type, and e → e', then e' has the same type.
The set of lambda expressions, Λ, can be defined recursively
:
Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications.
The set of free variables of a lambda expression, M, is denoted as FV(M) and is 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
.
There are three kinds of reduction:
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 betaredex; if x is not free in M, λx.M x is an etaredex. 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.
The precise rules for alphaconversion are not completely trivial. First, when alphaconverting an abstraction, the only variable occurrences that are renamed are those that are bound to the same abstraction. For example, an alphaconversion 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.
Second, alphaconversion 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 programming languages with static scope, alphaconversion can be used to make name resolution
simpler by ensuring that no variable name masks
a name in a containing scope
(see alpha renaming to make name resolution trivial).
Substitution on terms of the λcalculus is defined by recursion on the structure of terms, as follows.
To substitute into a lambda abstraction, it is sometimes necessary to αconvert the expression. For example, it is not correct for (λx.y)[y := x] to result in (λx.x), because the substituted x was supposed to be free but ended up being bound. The correct substitution in this case is (λz.x), up to αequivalence. Notice that substitution is defined uniquely up to αequivalence.
For example, assuming some encoding of 2, 7, *, we have the following βreductions: ((λn.n*2) 7) → 7*2.
, which in this context is that two functions are the same if and only if
they give the same result for all arguments. Etaconversion converts between λx.f x and f whenever x does not appear free in f.
However, it can be shown that βreduction is confluent
. (Of course, we are working up to αconversion, i.e. we consider two normal forms to be equal, if it is possible to αconvert one into the other.)
Therefore, both strongly normalising terms and weakly normalising terms have a unique normal form. For strongly normalising terms, any reduction strategy is guaranteed to yield the normal form, whereas for weakly normalising terms, some reduction strategies may fail to find it.
, data structures and recursion, as illustrated in the following subsections.
s in lambda calculus, but by far the most common are the Church numerals, which can be defined as follows:
and so on. Or using the alternate syntax presented above in Notation:
A Church numeral is a higherorder function
—it takes a singleargument function f, and returns another singleargument function. The Church numeral n is a function that takes a function f as argument and returns the nth composition of f, i.e. the function f composed with itself n times. This is denoted f^{(n)} and is in fact the nth power of f (considered as an operator); f^{(0)} is defined to be the identity function. Such repeated compositions (of a single function f) obey the laws of exponents, which is why these numerals can be used for arithmetic. (In Church's original lambda calculus, the formal parameter of a lambda expression was required to occur at least once in the function body, which made the above definition of 0 impossible.)
We can define a successor function, which takes a number n and returns n + 1 by adding an additional application of f:
Because the mth composition of f composed with the nth composition of f gives the m+nth composition of f, addition can be defined as follows:
PLUS can be thought of as a function taking two natural numbers as arguments and returning a natural number; it can be verified that
and
are equivalent lambda expressions. Since adding m to a number n can be accomplished by adding 1 m times, an equivalent definition is:
Similarly, multiplication can be defined as
Alternatively
since multiplying m and n is the same as repeating the add n function m times and then applying it to zero.
Exponentiation has a rather simple rendering in Church numerals, namely
The predecessor function defined by PRED n = n  1 for a positive integer n and PRED 0 = 0 is considerably more difficult. The formula
can be validated by showing inductively that if T denotes (λgh.h (g f)), then T^{(n)}(λu.x) = (λh.h(f^{(n1)}(x))) for n > 0. Two other definitions of PRED are given below, one using conditionals and the other using pairs. With the predecessor function, subtraction is straightforward. Defining
SUB m n yields m  n when m > n and 0 otherwise.
Then, with these two λterms, we can define some logic operators (these are just possible formulations; other expressions are equally correct):
We are now able to compute some logic functions, for example:
and we see that AND TRUE FALSE is equivalent to FALSE.
A predicate is a function that returns a boolean value. The most fundamental predicate is ISZERO, which returns TRUE if its argument is the Church numeral 0, and FALSE if its argument is any other Church numeral:
The following predicate tests whether the first argument is lessthanorequalto the second:
and since m = n, if LEQ m n and LEQ n m, it is straightforward to build a predicate for numerical equality.
The availability of predicates and the above definition of TRUE and FALSE make it convenient to write "ifthenelse" expressions in lambda calculus. For example, the predecessor function can be defined as:
which can be verified by showing inductively that n (λgk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) is the add n  1 function for n > 0.
A linked list can be defined as either NIL for the empty list, or the PAIR of an element and a smaller list. The predicate NULL tests for the value NIL. (Alternatively, with NIL := FALSE, the construct l (λhtz.deal_with_head_h_and_tail_t) (deal_with_nil) obviates the need for an explicit NULL test).
As an example of the use of pairs, the shiftandincrement function that maps (m, n) to (n, n + 1) can be defined as
which allows us to give perhaps the most transparent version of the predecessor function:
is the definition of a function using the function itself; on the face of it, lambda calculus does not allow this (we can't refer to a value which is yet to be defined, inside the lambda term defining that same value, as all functions are anonymous
in lambda calculus). However, this impression is misleading: in (λx.x x) y both x 's refer to the same lambda term, y, so it is possible for a lambda expression – here y – to be arranged to receive itself as its argument value, through selfapplication.
Consider for instance the factorial
function f(n) recursively defined by
In lambda expression which is to represent this function, a parameter will be assumed to receive the lambda expression itself as its value. This argument is typically the first. Binding it to the function yields a new function that may now recurse (referring to itself through this argument). To achieve recursion, the intendedasselfreferencing argument (called r here) must always be passed to itself within the function body, at a call point:
The selfapplication achieves replication here, passing the function's lambda expression on to the next invocation as an argument value, making it available to be referenced and called there.
This solves the specific problem of the factorial function, but we'd like to have a generic solution, i.e. not forcing a specific rewrite for every recursive function:
Given a lambda term representing the body of a recursive function or loop, with the first argument representing a recursive call, the fixedpoint operator will return the desired recursive function or loop. The function does not need to be explicitly passed to itself at any point, as this is done in advance, when the fixpoint combinator is applied, creating a selfreplicating selfreferencing lambda expression.
In fact, there are many possible definitions for this operator, considered as a type of fixedpoint combinators. The simplest is defined as:
In the lambda calculus, Y g is a fixedpoint of g, as it expands to:
Now, to complete our recursive call to the factorial function, we would simply call (Y g) n, where n is the number we are calculating the factorial of. Given n = 4, for example, this gives:
Every recursively defined function can be seen as a fixed point of some other suitable function, and therefore, using Y, every recursively defined function can be expressed as a lambda expression. In particular, we can now cleanly define the subtraction, multiplication and comparison predicate of natural numbers recursively.
s is a computable function
if and only if
there exists a lambda expression f such that for every pair of x, y in N, F(x)=y if and only if f x =_{β} y, where x and y are the Church numerals corresponding to x and y, respectively and =_{β} meaning equivalence with beta reduction. This is one of the many ways to define computability; see the ChurchTuring thesis for a discussion of other approaches and their equivalence.
can decide the equivalence. Church's thesis is then invoked to show that no algorithm can do so.
Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression that cannot be reduced any further under the rules imposed by the form. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, he constructs a lambda expression e that closely follows the proof of Gödel's first incompleteness theorem
. If e is applied to its own Gödel number, a contradiction results.
can be understood in terms of the lambda calculus, which provides the basic mechanisms for procedural abstraction and procedure (subprogram) application.
Lambda calculus reifies
"functions" and makes them firstclass object
s, which raises implementation complexity when it is implemented. A particular challenge is related to the support of higherorder functions, also known as the Funarg problem
. Lambda calculus is usually implemented using a virtual machine
approach. The first practical implementation of lambda calculus was provided in 1963 by Peter Landin, and is known as the SECD machine
. Since then, several optimized abstract machines for lambda calculus were suggested, such as the Gmachine and the categorical abstract machine
.
The most prominent counterparts to lambda calculus in programming are functional programming languages, which essentially implement the calculus augmented with some constants
and datatypes. Lisp
uses a variant of lambda notation for defining functions, but only its purely functional subset ("Pure Lisp
") is really equivalent to lambda calculus.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
and computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, lambda calculus, also written as λcalculus, is a formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
for function
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
definition, function application and recursion
Recursion
Recursion is the process of repeating items in a selfsimilar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus. In both typed lambda calculus
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambdasymbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
and untyped versions, ideas from lambda calculus have found application in the fields of logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, recursion theory (computability)
Computability theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
, and linguistics
Linguistics
Linguistics is the scientific study of human language. Linguistics can be broadly broken into three categories or subfields of study: language form, language meaning, and language in context....
, and have played an important role in the development of the theory of programming languages
Programming language theory
Programming language theory is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features. It falls within the discipline of computer science, both depending on and affecting...
(with untyped lambda calculus being the original inspiration for functional programming
Functional programming
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
, in particular Lisp, and typed lambda calculi serving as the foundation for modern type system
Type system
A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...
s). This article deals primarily with the untyped lambda calculus.
History
Lambda calculus was introduced by Alonzo ChurchAlonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.Life:Alonzo Church...
in the 1930s as part of an investigation into the foundations of mathematics
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
. The original system was shown to be logically inconsistent
Consistency
Consistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.
Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
.
Motivation
FunctionsFunction (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
are a fundamental concept within computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
and mathematics. The λcalculus provides simple semantics for computation with functions so that properties of functional computation can be studied.
Consider the following two examples. The identity function
Identity function
In mathematics, an identity function, also called identity map or identity transformation, is a function that always returns the same value that was used as its argument...
 I(x) = x
takes a single input, x, and immediately returns x (i.e. the identity does nothing with its input), whereas the function
 sqsum(x, y) = x*x + y*y
takes a pair of inputs, x and y and returns the sum of their squares, x*x + y*y. Using these two examples, we can make some useful observations that motivate the major ideas in the lambda calculus.
The first observation is that functions need not be explicitly named. That is, the function
 sqsum(x, y) = x*x + y*y
can be rewritten in anonymous form
Anonymous function
In programming language theory, an anonymous function is a function defined, and possibly called, without being bound to an identifier. Anonymous functions are convenient to pass as an argument to a higherorder function and are ubiquitous in languages with firstclass functions such as Haskell...
as
 (x, y) ↦ x*x + y*y
(read as “the pair of x and y is mapped to x*x + y*y”). Similarly,
 I(x) = x
can be rewritten in anonymous form as x ↦ x, where the input is simply mapped to itself.
The second observation is that the specific choice of name for a function's arguments is largely irrelevant. That is,
 x ↦ x and
 y ↦ y
express the same function: the identity. Similarly,
 (x, y) ↦ x*x + y*y and
 (u, v) ↦ u*u + v*v
also express the same function.
Finally, any function that requires two inputs, for instance the before mentioned sqsum function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts a single input. For example,
 (x, y) ↦ x*x + y*y
can be reworked into
 x ↦ (y ↦ x*x + y*y)
This transformation is called currying
Currying
In mathematics and computer science, currying is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument...
, and can be generalized to functions accepting an arbitrary number of arguments.
Currying may be best grasped intuitively through the use of an example. Compare the function
 (x, y) ↦ x*x + y*y
with its curried form,
 x ↦ (y ↦ x*x + y*y)
Given two arguments, we have:
 ((x, y) ↦ x*x + y*y)(5, 2)
 = 5*5 + 2*2 = 29
However, using currying, we have:
 ((x ↦ (y ↦ x*x + y*y))(5))(2)
 = (y ↦ 5*5 + y*y)(2)
 = 5*5 + 2*2 = 29
and we see the uncurried and curried forms compute the same result. Notice that x*x has become a constant.
The lambda calculus
The lambda calculus consists of lambda terms and some extra operations.Since the names of functions are largely a convenience, the lambda calculus has no means of naming a function. Since all functions expecting more than one input can be transformed into equivalent functions accepting a single input (via Currying
Currying
In mathematics and computer science, currying is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument...
), the lambda calculus has no means for creating a function that accepts more than one argument. Since the names of arguments are largely irrelevant, the native notion of equality on lambda terms is alphaequivalence (see below), which codifies this principle.
Lambda terms
The syntax of lambda terms is particularly simple. There are three ways in which to obtain them: a lambda term may be a variable, x;
 if t is a lambda term, and x is a variable, then λx.t is a lambda term (called a lambda abstraction);
 if t and s are lambda terms, then ts is a lambda term (called an application).
Nothing else is a lambda term, though bracketing may be used to disambiguate terms.
Intuitively, a lambda abstraction λx.t represents an anonymous function that takes a single input, and the λ is said to bind x in t, and an application ts represents the application of input s to some function t. In the lambda calculus, functions are taken to be first class values
Firstclass object
In programming language design, a firstclass citizen , in the context of a particular programming language, is an entity that can be constructed at runtime, passed as a parameter, returned from a subroutine, or assigned into a variable...
, so functions may be used as the inputs to other functions, and functions may return functions as their outputs.
For example, λx.x represents the identity function, x ↦ x, and (λx.x)y represents the identity function applied to y. Further, (λx.y) represents the constant function x ↦ y, the function that always returns y, no matter the input. It should be noted that function application is leftassociative, so (λx.x)y z = ((λx.x)y)z.
Lambda terms on their own aren't particularly interesting.
What makes them interesting are the various notions of equivalence and reduction that can be defined over them.
Alpha equivalence
A basic form of equivalence, definable on lambda terms, is alpha equivalence.This states that the particular choice of bound variable, in a lambda abstraction, doesn't (usually) matter.
For instance, λx.x and λy.y are alphaequivalent lambda terms, representing the same identity function.
Note that the terms x and y aren't alphaequivalent, because they are not bound in a lambda abstraction.
In many presentations, it is usual to identify alphaequivalent lambda terms.
The following definitions are necessary in order to be able to define beta reduction.
Free variables
The free variables of a term are those variables not bound by a lambda abstraction.That is, the free variables of x are just x; the free variables of λx.t are the free variables of t, with x removed, and the free variables of ts are the union of the free variables of t and s.
For example, the lambda term representing the identity λx.x has no free variables, but the constant function λx.y has a single free variable, y.
Captureavoiding substitutions
Using the definition of free variables, we may now define a captureavoiding substitution.Suppose t, s and r are lambda terms and x and y are variables.
We write t[x := r] for the substitution of r for x in t, in a captureavoiding manner.
That is:
 x[x := r] = r;
 y[x := r] = y if x ≠ y;
 (ts)[x := r] = (t[x := r])(s[x := r]);
 (λx.t)[x := r] = λx.t;
 (λy.t)[x := r] = λy.(t[x := r]) if x ≠ y and y is not in the free variables of r (sometimes said "y is fresh for r").
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 r) is crucial in order to ensure that substitution does not change the meaning of functions.
For example, suppose we define another substitution action without the freshness condition.
Then, (λx.y)[y := x] = λx.(y[y := x]) = λx.x, and the constant function λx.y turns into the identity λx.x by substitution.
If our freshness condition is not met, then we may simply alpharename with a suitably fresh variable.
For example, switching back to our correct notion of substitution, in (λx.y)[y := x] the lambda abstraction can be renamed with a fresh variable z, to obtain (λz.y)[y := x] = λz.(y[y := x]) = λz.x, and the meaning of the function is preserved by substitution.
Beta reduction
Beta reduction states that an application of the form (λx.t)s reduces to the term t[x := s] (we write (λx.t)s → t[x := s] as a convenient shorthand for “(λx.t)s beta reduces to t[x := s]”).For example, for every s we have (λx.x)s → x[x := s] = s, demonstrating that λx.x really is the identity.
Similarly, (λx.y)s → y[x := s] = y, demonstrating that λx.y really is a constant function.
The lambda calculus may be seen as an idealised functional programming language, like Haskell
Haskell (programming language)
Haskell is a standardized, generalpurpose purely functional programming language, with nonstrict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a firstclass citizen" of the programming language. As a functional programming language, the...
or Standard ML
Standard ML
Standard ML is a generalpurpose, modular, functional programming language with compiletime type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...
.
Under this view, beta reduction corresponds to a computational step, and in the untyped lambda calculus, as presented here, reduction need not terminate.
For instance, consider the term (λx.xx)(λx.xx).
Here, we have (λx.xx)(λx.xx) → (xx)[x := λx.xx] = (x[x := λx.xx])(x[x := λx.xx]) = (λx.xx)(λx.xx).
That is, the term reduces to itself in a single beta reduction, and therefore reduction will never terminate.
Another problem with the untyped lambda calculus is the inability to distinguish between different kinds of data.
For instance, we may want to write a function that only operates on numbers.
However, in the untyped lambda calculus, there's no way to prevent our function from being applied to truth values, or strings, for instance.
Typed lambda calculi, which will be introduced later in the article, have the property that if a term is welltyped, then it never gets "stuck" (where there is no evaluation rule for the term), and that if a term e has a particular type, and e → e', then e' has the same type.
Definition
Lambda expressions are composed of variables v_{1}, v_{2}, ..., v_{n}, ...
 the abstraction symbols λ and .
 parentheses
The set of lambda expressions, Λ, can be defined recursively
Recursive definition
In mathematical logic and computer science, a recursive definition is used to define an object in terms of itself ....
:
 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.
Notation
To keep the notation of lambda expressions uncluttered, the following conventions are usually applied. Outermost parentheses are dropped: M N instead of (M N).
 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.
 A sequence of abstractions is contracted: λx.λy.λz.N is abbreviated as λxyz.N.
Free 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 a lambda are said to be bound. All other variables are called free. For example in the following expression y is a bound variable and x is free: λy.x x y. Also note that a variable binds to its "nearest" lambda. In the following expression one single occurrence of x is bound by the second lambda: λx.y (λx.z x)The set of free variables of a lambda expression, M, is denoted as FV(M) and is defined by recursion on the structure of the terms, as follows:
 FV(x) = {x}, where x is a variable
 FV(λx.M) = FV(M) \ {x}
 FV(M N) = FV(M) ∪ FV(N)
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
Combinatory logic
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
.
Reduction
The meaning of lambda expressions is defined by how expressions can be reduced.There are three kinds of reduction:
 αconversion: changing bound variables;
 βreduction: applying functions to their arguments;
 ηconversion: 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, (λx.M) N is a betaredex; if x is not free in M, λx.M x is an etaredex. 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
Alphaconversion, sometimes known as alpharenaming, allows bound variable names to be changed. For example, alphaconversion of λx.x might yield λy.y. Terms that differ only by alphaconversion are called αequivalent. Frequently in uses of lambda calculus, αequivalent terms are considered to be equivalent.The precise rules for alphaconversion are not completely trivial. First, when alphaconverting an abstraction, the only variable occurrences that are renamed are those that are bound to the same abstraction. For example, an alphaconversion 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.
Second, alphaconversion 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 programming languages with static scope, alphaconversion can be used to make name resolution
Name resolution
In computer languages:Expressions in computer languages can contain identifiers. The semantics of such expressions depend on the entities that the identifiers refer to. The algorithm that determines what an identifier in a given context refers to is part of the language definition.The complexity...
simpler by ensuring that no variable name masks
Variable shadowing
In computer programming, variable shadowing occurs when a variable declared within a certain scope has the same name as a variable declared in an outer scope. This outer variable is said to be shadowed...
a name in a containing scope
Scope (programming)
In computer programming, scope is an enclosing context where values and expressions are associated. Various programming languages have various types of scopes. The type of scope determines what kind of entities it can contain and how it affects them—or semantics...
(see alpha renaming to make name resolution trivial).
Substitution
Substitution, written E[V := E′], is the process of replacing all free occurrences of the variable V by expression E′.Substitution on terms of the λcalculus is defined by recursion on the structure of terms, as follows.
 x[x := N] ≡ N
 y[x := N] ≡ y, if x ≠ y
 (M_{1} M_{2})[x := N] ≡ (M_{1}[x := N]) (M_{2}[x := N])
 (λx.M)[x := N] ≡ λx.(M)
 (λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y, provided y ∉ FV(N)
To substitute into a lambda abstraction, it is sometimes necessary to αconvert the expression. For example, it is not correct for (λx.y)[y := x] to result in (λx.x), because the substituted x was supposed to be free but ended up being bound. The correct substitution in this case is (λz.x), up to αequivalence. Notice that substitution is defined uniquely up to αequivalence.
βreduction
Betareduction captures the idea of function application. Betareduction is defined in terms of substitution: the betareduction of ((λV.E) E′) is E[V := E′].For example, assuming some encoding of 2, 7, *, we have the following βreductions: ((λn.n*2) 7) → 7*2.
ηconversion
Etaconversion expresses the idea of extensionalityExtensionality
In logic, extensionality, or extensional equality refers to principles that judge objects to be equal if they have the same external properties...
, which in this context is that two functions are the same if and only if
If and only if
In logic and related fields such as mathematics and philosophy, if and only if is a biconditional logical connective between statements....
they give the same result for all arguments. Etaconversion converts between λx.f x and f whenever x does not appear free in f.
Normal forms and confluence
For the untyped lambda calculus, βreduction as a rewriting rule is neither strongly normalising nor weakly normalising.However, it can be shown that βreduction is confluent
Confluence (abstract rewriting)
In computer science, confluence is a property of rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system. Motivating example :Consider...
. (Of course, we are working up to αconversion, i.e. we consider two normal forms to be equal, if it is possible to αconvert one into the other.)
Therefore, both strongly normalising terms and weakly normalising terms have a unique normal form. For strongly normalising terms, any reduction strategy is guaranteed to yield the normal form, whereas for weakly normalising terms, some reduction strategies may fail to find it.
Encoding datatypes
The basic lambda calculus may be used to model booleans, arithmeticArithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple daytoday counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
, data structures and recursion, as illustrated in the following subsections.
Arithmetic in lambda calculus
There are several possible ways to define the natural numberNatural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s in lambda calculus, but by far the most common are the Church numerals, which can be defined as follows:
 0 := λf.λx.x
 1 := λf.λx.f x
 2 := λf.λx.f (f x)
 3 := λf.λx.f (f (f x))
and so on. Or using the alternate syntax presented above in Notation:
 0 := λfx.x
 1 := λfx.f x
 2 := λfx.f (f x)
 3 := λfx.f (f (f x))
A Church numeral is a higherorder function
Higherorder function
In mathematics and computer science, higherorder functions, functional forms, or functionals are functions which do at least one of the following:*take one or more functions as an input*output a function...
—it takes a singleargument function f, and returns another singleargument function. The Church numeral n is a function that takes a function f as argument and returns the nth composition of f, i.e. the function f composed with itself n times. This is denoted f^{(n)} and is in fact the nth power of f (considered as an operator); f^{(0)} is defined to be the identity function. Such repeated compositions (of a single function f) obey the laws of exponents, which is why these numerals can be used for arithmetic. (In Church's original lambda calculus, the formal parameter of a lambda expression was required to occur at least once in the function body, which made the above definition of 0 impossible.)
We can define a successor function, which takes a number n and returns n + 1 by adding an additional application of f:
 SUCC := λnfx.f (n f x)
Because the mth composition of f composed with the nth composition of f gives the m+nth composition of f, addition can be defined as follows:
 PLUS := λmnfx.m f (n f x)
PLUS can be thought of as a function taking two natural numbers as arguments and returning a natural number; it can be verified that
 PLUS 2 3
and
 5
are equivalent lambda expressions. Since adding m to a number n can be accomplished by adding 1 m times, an equivalent definition is:
 PLUS := λmn.m SUCC n
Similarly, multiplication can be defined as
 MULT := λmnf.m (n f)
Alternatively
 MULT := λmn.m (PLUS n) 0
since multiplying m and n is the same as repeating the add n function m times and then applying it to zero.
Exponentiation has a rather simple rendering in Church numerals, namely
 POW := λbe.e b
The predecessor function defined by PRED n = n  1 for a positive integer n and PRED 0 = 0 is considerably more difficult. The formula
 PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
can be validated by showing inductively that if T denotes (λgh.h (g f)), then T^{(n)}(λu.x) = (λh.h(f^{(n1)}(x))) for n > 0. Two other definitions of PRED are given below, one using conditionals and the other using pairs. With the predecessor function, subtraction is straightforward. Defining
 SUB := λmn.n PRED m,
SUB m n yields m  n when m > n and 0 otherwise.
Logic and predicates
By convention, the following two definitions (known as Church booleans) are used for the boolean values TRUE and FALSE: TRUE := λxy.x
 FALSE := λxy.y
 (Note that FALSE is equivalent to the Church numeral zero defined above)
Then, with these two λterms, we can define some logic operators (these are just possible formulations; other expressions are equally correct):
 AND := λpq.p q p
 OR := λpq.p p q
 NOT := λpab.p b a
 IFTHENELSE := λpab.p a b
We are now able to compute some logic functions, for example:
 AND TRUE FALSE
 ≡ (λpq.p q p) TRUE FALSE →_{β} TRUE FALSE TRUE
 ≡ (λxy.x) FALSE TRUE →_{β} FALSE
and we see that AND TRUE FALSE is equivalent to FALSE.
A predicate is a function that returns a boolean value. The most fundamental predicate is ISZERO, which returns TRUE if its argument is the Church numeral 0, and FALSE if its argument is any other Church numeral:
 ISZERO := λn.n (λx.FALSE) TRUE
The following predicate tests whether the first argument is lessthanorequalto the second:
 LEQ := λmn.ISZERO (SUB m n),
and since m = n, if LEQ m n and LEQ n m, it is straightforward to build a predicate for numerical equality.
The availability of predicates and the above definition of TRUE and FALSE make it convenient to write "ifthenelse" expressions in lambda calculus. For example, the predecessor function can be defined as:
 PRED := λn.n (λgk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0
which can be verified by showing inductively that n (λgk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) is the add n  1 function for n > 0.
Pairs
A pair (2tuple) can be defined in terms of TRUE and FALSE, by using the Church encoding for pairs. For example, PAIR encapsulates the pair (x,y), FIRST returns the first element of the pair, and SECOND returns the second. PAIR := λxyf.f x y
 FIRST := λp.p TRUE
 SECOND := λp.p FALSE
 NIL := λx.TRUE
 NULL := λp.p (λxy.FALSE)
A linked list can be defined as either NIL for the empty list, or the PAIR of an element and a smaller list. The predicate NULL tests for the value NIL. (Alternatively, with NIL := FALSE, the construct l (λhtz.deal_with_head_h_and_tail_t) (deal_with_nil) obviates the need for an explicit NULL test).
As an example of the use of pairs, the shiftandincrement function that maps (m, n) to (n, n + 1) can be defined as
 Φ := λx.PAIR (SECOND x) (SUCC (SECOND x))
which allows us to give perhaps the most transparent version of the predecessor function:
 PRED := λn.FIRST (n Φ (PAIR 0 0)).
Recursion and fixed points
RecursionRecursion
Recursion is the process of repeating items in a selfsimilar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...
is the definition of a function using the function itself; on the face of it, lambda calculus does not allow this (we can't refer to a value which is yet to be defined, inside the lambda term defining that same value, as all functions are anonymous
Anonymous function
In programming language theory, an anonymous function is a function defined, and possibly called, without being bound to an identifier. Anonymous functions are convenient to pass as an argument to a higherorder function and are ubiquitous in languages with firstclass functions such as Haskell...
in lambda calculus). However, this impression is misleading: in (λx.x x) y both x 's refer to the same lambda term, y, so it is possible for a lambda expression – here y – to be arranged to receive itself as its argument value, through selfapplication.
Consider for instance the factorial
Factorial
In mathematics, the factorial of a nonnegative integer n, denoted by n!, is the product of all positive integers less than or equal to n...
function f(n) recursively defined by
 f(n) = 1, if n = 0; else n × f(n  1).
In lambda expression which is to represent this function, a parameter will be assumed to receive the lambda expression itself as its value. This argument is typically the first. Binding it to the function yields a new function that may now recurse (referring to itself through this argument). To achieve recursion, the intendedasselfreferencing argument (called r here) must always be passed to itself within the function body, at a call point:
 g := λr. λn.(1, if n = 0; else n × (r r (n1)))

 with r r x = f x = g r x to hold, so r = g and

 f := g g = (λx.x x) g
The selfapplication achieves replication here, passing the function's lambda expression on to the next invocation as an argument value, making it available to be referenced and called there.
This solves the specific problem of the factorial function, but we'd like to have a generic solution, i.e. not forcing a specific rewrite for every recursive function:
 g := λr. λn.(1, if n = 0; else n × (r (n1)))

 with r x = f x = g r x to hold, so r = g r =: fix g and

 f := fix g where fix g := (r where r = g r) = g (fix g)
Given a lambda term representing the body of a recursive function or loop, with the first argument representing a recursive call, the fixedpoint operator will return the desired recursive function or loop. The function does not need to be explicitly passed to itself at any point, as this is done in advance, when the fixpoint combinator is applied, creating a selfreplicating selfreferencing lambda expression.
In fact, there are many possible definitions for this operator, considered as a type of fixedpoint combinators. The simplest is defined as:
 Y = λg.(λx.g (x x)) (λx.g (x x))
In the lambda calculus, Y g is a fixedpoint of g, as it expands to:
 Y g
 λh.((λx.h (x x)) (λx.h (x x))) g
 (λx.g (x x)) (λx.g (x x))
 g ((λx.g (x x)) (λx.g (x x)))
 g (Y g).
Now, to complete our recursive call to the factorial function, we would simply call (Y g) n, where n is the number we are calculating the factorial of. Given n = 4, for example, this gives:
 (Y g) 4
 g (Y g) 4
 (λrn.(1, if n = 0; else n × (r (n1)))) (Y g) 4
 (λn.(1, if n = 0; else n × ((Y g) (n1)))) 4
 1, if 4 = 0; else 4 × ((Y g) (41))
 4 × (g (Y g) (41))
 4 × ((λn.(1, if n = 0; else n × ((Y g) (n1)))) (41))
 4 × (1, if 3 = 0; else 3 × ((Y g) (31)))
 4 × (3 × (g (Y g) (31)))
 4 × (3 × ((λn.(1, if n = 0; else n × ((Y g) (n1)))) (31)))
 4 × (3 × (1, if 2 = 0; else 2 × ((Y g) (21))))
 4 × (3 × (2 × (g (Y g) (21))))
 4 × (3 × (2 × ((λn.(1, if n = 0; else n × ((Y g) (n1)))) (21))))
 4 × (3 × (2 × (1, if 1 = 0; else 1 × ((Y g) (11)))))
 4 × (3 × (2 × (1 × (g (Y g) (11)))))
 4 × (3 × (2 × (1 × ((λn.(1, if n = 0; else n × ((Y g) (n1)))) (11)))))
 4 × (3 × (2 × (1 × (1, if 0 = 0; else 0 × ((Y g) (01))))))
 4 × (3 × (2 × (1 × (1))))
 24
Every recursively defined function can be seen as a fixed point of some other suitable function, and therefore, using Y, every recursively defined function can be expressed as a lambda expression. In particular, we can now cleanly define the subtraction, multiplication and comparison predicate of natural numbers recursively.
Standard terms
Certain terms have commonly accepted names: I := λx.x
 K := λxy.x
 S := λxyz.x z (y z)
 ω := λx.x x
 Ω := ω ω
 Y := λg.(λx.g (x x)) (λx.g (x x))
Computable functions and lambda calculus
A function F: N → N of natural numberNatural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s is a computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
if and only if
If and only if
In logic and related fields such as mathematics and philosophy, if and only if is a biconditional logical connective between statements....
there exists a lambda expression f such that for every pair of x, y in N, F(x)=y if and only if f x =_{β} y, where x and y are the Church numerals corresponding to x and y, respectively and =_{β} meaning equivalence with beta reduction. This is one of the many ways to define computability; see the ChurchTuring thesis for a discussion of other approaches and their equivalence.
Undecidability of equivalence
There is no algorithm that takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which undecidability could be proven. As is common for a proof of undecidability, the proof shows that no computable functionComputable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...
can decide the equivalence. Church's thesis is then invoked to show that no algorithm can do so.
Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression that cannot be reduced any further under the rules imposed by the form. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, he constructs a lambda expression e that closely follows the proof of Gödel's first incompleteness theorem
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
. If e is applied to its own Gödel number, a contradiction results.
Lambda calculus and programming languages
As pointed out by Peter Landin's 1965 paper A Correspondence between ALGOL 60 and Church's Lambdanotation, sequential procedural programming languagesProcedural programming
Procedural programming can sometimes be used as a synonym for imperative programming , but can also refer to a programming paradigm, derived from structured programming, based upon the concept of the procedure call...
can be understood in terms of the lambda calculus, which provides the basic mechanisms for procedural abstraction and procedure (subprogram) application.
Lambda calculus reifies
Reification (computer science)
Reification is the process by which an abstract idea about a computer program is turned into an explicit data model or other object created in a programming language. A computable/addressable object — a resource — is created in a system as a proxy for a non computable/addressable object...
"functions" and makes them firstclass object
Firstclass object
In programming language design, a firstclass citizen , in the context of a particular programming language, is an entity that can be constructed at runtime, passed as a parameter, returned from a subroutine, or assigned into a variable...
s, which raises implementation complexity when it is implemented. A particular challenge is related to the support of higherorder functions, also known as the Funarg problem
Funarg problem
In computer science, the funarg problem refers to the difficulty in implementing firstclass functions in stackbased programming language implementations....
. Lambda calculus is usually implemented using a virtual machine
Virtual machine
A virtual machine is a "completely isolated guest operating system installation within a normal host operating system". Modern virtual machines are implemented with either software emulation or hardware virtualization or both together.VM Definitions:A virtual machine is a software...
approach. The first practical implementation of lambda calculus was provided in 1963 by Peter Landin, and is known as the SECD machine
SECD machine
The SECD machine is a highly influential virtual machine and abstract machine intended as a target for functional programming language compilers. The letters stand for Stack, Environment, Code, Dump, the internal registers of the machine...
. Since then, several optimized abstract machines for lambda calculus were suggested, such as the Gmachine and the categorical abstract machine
Categorical abstract machine
The categorical abstract machine is a model of computation for programs that preserves the abilities of applicative, functional, or compositional style. It is based on the techniques of applicative computing. Overview :...
.
The most prominent counterparts to lambda calculus in programming are functional programming languages, which essentially implement the calculus augmented with some constants
Constant (programming)
In computer programming, a constant is an identifier whose associated value cannot typically be altered by the program during its execution...
and datatypes. Lisp
Lisp programming language
Lisp is a family of computer programming languages with a long history and a distinctive, fully parenthesized syntax. Originally specified in 1958, Lisp is the secondoldest highlevel programming language in widespread use today; only Fortran is older...
uses a variant of lambda notation for defining functions, but only its purely functional subset ("Pure Lisp
Lispkit Lisp
Lispkit Lisp is a lexically scoped, purely functional subset of Lisp developed as a testbed for functional programming concepts. It was first used for early experimentation with lazy evaluation. An SECD machinebased implementation written in an ALGOL variant was published by the developer Peter...
") is really equivalent to lambda calculus.