Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.
In the simplest form of lambda calculus, terms are built using only the following rules:[a] The reduction operations include: If De Bruijn indexing is used, then α-conversion is no longer required as there will be no name collisions.
Lambda calculus has applications in many different areas in mathematics, philosophy,[4] linguistics,[5][6] and computer science.
[9] Lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.
[11][12] Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus.
[13] In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus.
On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and λ just happened to be chosen.
According to Scott, Church's entire response consisted of returning the postcard with the following annotation: "eeny, meeny, miny, moe".
The set of free variables of an expression is defined inductively: For example, the lambda term representing the identity
The lambda calculus may be seen as an idealized version of a functional programming language, like Haskell or Standard ML.
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.
[b] If x is not free in M, λx.M x is also an η-redex, with a reduct of M. α-conversion (alpha-conversion), sometimes known as α-renaming,[23] allows bound variable names to be changed.
η-reduction (eta reduction) expresses the idea of extensionality,[24] which in this context is that two functions are the same if and only if they give the same result for all arguments.
However, it can be shown that β-reduction is confluent when working up to α-conversion (i.e. we consider two normal forms to be equal if it is possible to α-convert one into the other).
The basic lambda calculus may be used to model arithmetic, Booleans, data structures, and recursion, as illustrated in the following sub-sections i, ii, iii, and § iv.
The availability of predicates and the above definition of TRUE and FALSE make it convenient to write "if-then-else" expressions in lambda calculus.
In lambda calculus, a library would take the form of a collection of previously defined functions, which as lambda-terms are merely particular constants.
A notable restriction of this let is that the name f may not be referenced in N, for N is outside the scope of the abstraction binding f, which is M; this means a recursive function definition cannot be written with let.
The letrec[l] construction would allow writing recursive function definitions, where the scope of the abstraction binding f includes N as well as M. Or self-application a-la that which leads to Y combinator could be used.
The function does not need to be explicitly passed to itself at any point, for the self-replication is arranged in advance, when it is created, to be done each time it is called.
SK and BCKW form complete combinator calculus systems that can express any lambda term - see the next section.
The conversion function T can be defined by: In either case, a term of the form T(x,N) P can reduce by having the initial combinator I, K, or S grab the argument P, just like β-reduction of (λx.N) P would do.
Typed lambda calculi are closely related to mathematical logic and proof theory via the Curry–Howard isomorphism and they can be considered as the internal language of classes of categories, e.g., the simply typed lambda calculus is the language of a Cartesian closed category (CCC).
Church's proof of uncomputability first reduces the problem to determining whether a given lambda expression has a normal form.
The notion of computational complexity for the lambda calculus is a bit tricky, because the cost of a β-reduction may vary depending on how it is implemented.
A naïve search for the locations of V in E is O(n) in the length n of E. Director strings were an early approach that traded this time cost for a quadratic space usage.
[38] It is not known if optimal reduction implementations are reasonable when measured with respect to a reasonable cost model such as the number of leftmost-outermost steps to normal form, but it has been shown for fragments of the lambda calculus that the optimal reduction algorithm is efficient and has at most a quadratic overhead compared to leftmost-outermost.
[37] In addition the BOHM prototype implementation of optimal reduction outperformed both Caml Light and Haskell on pure lambda terms.
Such runtime creation of functions is supported in Smalltalk, JavaScript, Wolfram Language, and more recently in Scala, Eiffel (as agents), C# (as delegates) and C++11, among others.
In the 1970s, Dana Scott showed that if only continuous functions were considered, a set or domain D with the required property could be found, thus providing a model for the lambda calculus.