home | alphabetical index | |||||

## Lambda calculus
The This article deals with the "untyped lambda calculus" as originally conceived by Church. Since then, some typed lambda calculi have been developed.
## HistoryOriginally, Church had tried to construct a complete formal system for the foundations of mathematics; when the system turned out to be susceptible to the analog of Russell's paradox, he separated out the lambda calculus and used it to study computability, culminating in his negative answer to the Entscheidungsproblem. ## Informal descriptionare equivalent. A function of two variables is expressed in lambda calculus as a function of one argument which returns a function of one argument (see Currying). For instance, the functionf(x, y) = x - y would be written as λ x. λ y. x - y. The three expressions
- (λ
*x*. λ*y*.*x*-*y*) 7 2 and (λ*y*. 7 -*y*) 2 and 7 - 2
Not every lambda expression can be reduced to a definite value like the ones above; consider for instance - (λ
*x*.*x**x*) (λ*x*.*x**x*)
- (λ
*x*.*x**x**x*) (λ*x*.*x**x**x*)
x. x x) is also known as the ω combinator;
((λ x. x x) (λ x. x x))
is known as Ω,
(λ x. x x x) (λ x. x x x)
as Ω_{2}, etc.)While the lambda calculus itself does not contain symbols for integers or addition, these can be defined as abbreviations within the calculus and arithmetic can be expressed as we will see below.
Lambda calculus expressions may contain - (λ
*x*. λ*y*.*y**x*) (λ*x*.*y*) to λ*z*.*z*(λ*x*.*y*)
## Formal definition
Formally, we start with a countably infinite set of identifiers, say {a, b, c, ..., x, y, z, x - <expr> → <identifier>
- <expr> → (λ <identifier> . <expr>)
- <expr> → (<expr> <expr>)
x. (x x)) (λ y. y)) can be simply written as (λ x. x x) λ y.y.
Lambda expressions such as λ - In an expression of the form
*V*where*V*is a variable this*V*is the single free occurrence. - In an expression of the form λ
*V*.*E*the free occurrences are the free occurrences in*E*except those of*V*. In this case the occurrences of*V*in*E*are said to be bound by the λ before*V*. - In an expresssion of the form (
*E**E'*) the free occurrences are the free occurrences in*E*and*E'*.
alpha-conversion rule and the beta-reduction rule. ## α-conversionifW does not appear freely in E and W is not bound by a λ in E whenever it replaces a V. This rule tells us for example that λ x. (λ x. x) x is the same as λ y. (λ x. x) y.## β-reductionThe beta-reduction rule expresses the idea of function application. It states that if all free occurrences inE' remain free in E[V/E'].The relation == is then defined as the smallest equivalence relation that satisfies these two rules.
A more operational definition of the equivalence relation can be given by applying the rules only from left to right. A lambda expression which does not allow any beta reduction, i.e., has no subexpression of the form ((λ ## η-conversion
There is third rule, eta-conversion, which may be added to these two to form a new equivalence relation. Eta-conversion expresses the idea of extensionality, which in this context is that two functions are the same iff they give the same result for all arguments. Eta-conversion converts between λ
If | |||||

copyright © 2004 FactsAbout.com |