Lambda calculus
In mathematical logic, the lambda calculus is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic of this article, is a universal machine, [|i].e. a model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. In 1936, Church found a formulation which was [|logically consistent], and documented it in 1940.
Definition
The lambda calculus consists of a language of lambda terms, which are defined by a formal syntax, and a set of transformation rules for manipulating those terms. In BNF, the syntax is where variables range over an infinite set of names. Terms range over all lambda terms. This corresponds to the following inductive definition:- A variable is a valid lambda term.
- An abstraction is a lambda term where is a lambda term, referred to as the abstraction's body, and is the abstraction's parameter variable,
- An application is a lambda term where and are lambda terms.
Within lambda terms, any occurrence of a variable that is not a parameter of some enclosing λ is said to be free. Any free occurrence of in a term is bound in. Any free occurrence of any other variable within remains free in.
For example, in the term, both and occur free. In, is free, but in the body is not free, and is said to be bound. While is free in, it is bound in. There are two occurrences of in – one is bound, and the other is free.
is the set of free variables of, i.e. such variables that occur free in at least once. It can be defined inductively as follows:
- ; if.
- .
- has three cases:
- * If, becomes .
- * If, becomes.
- * If, first α-rename to with fresh to avoid name collisions, then continue as above. It becomes with.
- α-conversion captures the intuition that the particular choice of a bound variable, in an abstraction, does not matter. If, then the terms and are considered alpha-equivalent, written. The equivalence relation is the smallest congruence relation on lambda terms generated by this rule. For instance, and are alpha-equivalent lambda terms.
- The β-reduction rule states that a β-redex, an application of the form, reduces to the term. For example, for every,. This demonstrates that really is the identity. Similarly,, which demonstrates that is a constant function.
- η-conversion expresses extensionality and converts between and whenever does not appear free in. It is often omitted in many treatments of lambda calculus.
Explanation and applications
Lambda calculus is Turing complete, that is, it is a universal model of computation that can be used to simulate any Turing machine. Its namesake, the Greek letter lambda, is used in lambda expressions and lambda terms to denote binding a variable in a function.Lambda calculus may be untyped or typed. In typed lambda calculus, functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are strictly weaker than the untyped lambda calculus, which is the primary subject of this article, in the sense that typed lambda calculi can express less than the untyped calculus can. On the other hand, more things can be proven with typed lambda calculi. For example, in simply typed lambda calculus, it is a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate. One reason there are many different typed lambda calculi has been the desire to do more without giving up on being able to prove strong theorems about the calculus.
Lambda calculus has applications in many different areas in mathematics, philosophy, linguistics, and computer science. Lambda calculus has played an important role in the development of the theory of programming languages. Functional programming languages implement lambda calculus. Lambda calculus is also a current research topic in category theory.
History
Lambda calculus was introduced by mathematician Alonzo Church 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.
Until the 1960s when its relation to programming languages was clarified, the lambda calculus was only a formalism. Thanks to Richard Montague and other linguists' applications in the semantics of natural language, the lambda calculus has begun to enjoy a respectable place in both linguistics and computer science.
Origin of the ''λ'' symbol
There is some uncertainty over the reason for Church's use of the Greek letter lambda as the notation for function-abstraction in the lambda calculus, perhaps in part due to conflicting explanations by Church himself. According to Cardone and Hindley :
By the way, why did Church choose the notation "λ"? In he stated clearly that it came from the notation "" used for class-abstraction by Whitehead and Russell, by first modifying "" to "" to distinguish function-abstraction from class-abstraction, and then changing "" to "λ" for ease of printing.
This origin was also reported in . 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.
Dana Scott has also addressed this question in various public lectures.
Scott recounts that he once posed a question about the origin of the lambda symbol to Church's former student and son-in-law John W. Addison Jr., who then wrote his father-in-law a postcard:
Dear Professor Church,
Russell had the iota operator, Hilbert had the epsilon operator. Why did you choose lambda for your operator?
According to Scott, Church's entire response consisted of returning the postcard with the following annotation: "eeny, meeny, miny, moe".
Motivation
s are a fundamental concept within computer science and mathematics. The lambda calculus provides simple semantics for computation which are useful for formally studying properties of computation. The lambda calculus incorporates two simplifications that make its semantics simple.The first simplification is that the lambda calculus treats functions "anonymously"; it does not give them explicit names. For example, the function
can be rewritten in anonymous form as
. Similarly, the function
can be rewritten in anonymous form as
where the input is simply mapped to itself.
The second simplification is that the lambda calculus only uses functions of a single input. An ordinary function that requires two inputs, for instance the 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 method, known as currying, transforms a function that takes multiple arguments into a chain of functions each with a single argument.
Function application of the function to the arguments, yields at once
whereas evaluation of the curried version requires one more step
to arrive at the same result.
In lambda calculus, functions are taken to be 'first class values', so functions may be used as the inputs, or be returned as outputs from other functions. For example, the lambda term represents the identity function,. Further, represents the constant function, the function that always returns, no matter the input. As an example of a function operating on functions, the function composition can be defined as.
Normal forms and confluence
It can be shown that β-reduction is confluent when working up to α-conversion. If repeated application of the reduction steps eventually terminates, then by the Church–Rosser theorem it will produce a unique β-normal form. However, the untyped lambda calculus as a rewriting rule under β-reduction is neither strongly normalising nor weakly normalising; there are terms with no normal form such as.Considering individual terms, 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.