Index: > A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
Business Industries Finance Tax

Home > Lambda calculus


First Prev [ 1 2 3 4 ] Next Last

The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. The calculus can be used to cleanly define what a computable function is. The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, especially Lisp.

The lambda calculus can be called the smallest universal programming language. The lambda calculus consists of a single transformation rule (variable substitution) and a single function definition scheme. The lambda calculus is universal in the sense that any computable function can be expressed and evaluated using this formalism. It is thus equivalent to Turing machines. However, the lambda calculus emphasizes the use of transformation rules, and does not care about the actual machine implementing them. It is an approach more related to software than to hardware.

This article deals with the "untyped lambda calculus" as originally conceived by Church. Since then, some typed lambda calculi have been developed.

1 History

Originally, 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.

2 Informal description

In lambda calculus, every expression stands for a function with a single argument; the argument of the function is in turn a function with a single argument, and the value of the function is another function with a single argument. Functions are anonymously defined by a lambda expression which expresses the function's action on its argument. For instance, the "add-two" function f(x) = x + 2 would be expressed in lambda calculus as λ x. x + 2 (or equivalently as λ y. y + 2; the name of the formal argument is immaterial) and the number f(3) would be written as (λ x. x + 2) 3. Function application is left associative: f x y = (f x) y. Consider the function which takes a function as argument and applies it to the argument 3: λ x. x 3. This latter function could be applied to our earlier "add-2" function as follows: (λ x. x 3) (λ x. x+2). It is clear that the three expressions

x. x 3) (λ x. x+2)   and    (λ x. x + 2) 3    and    3 + 2

are 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 CurryingIn computer science, currying is the technique of transforming a function taking multiple arguments into a function that takes a single argument (the first of the arguments to the original function) and returns a new function which takes the remainder of). For instance, the function f(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

are equivalent. It is this equivalence of lambda expressions which in general can not be decided by an algorithm.

Not every lambda expression can be reduced to a definite value like the ones above; consider for instance

x. x x) (λ x. x x)

or

x. x x x) (λ x. x x x)

and try to visualize what happens as you start to apply the first function to its argument. (λ 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 free variables, i.e. variables not bound by any λ. For example, the variable y is free in the expression (λ x. y), representing a function which always produces the result y. Occasionally, this necessitates the renaming of formal arguments, for instance in order to reduce

x. λ y. y x) (λ x. y)     to     λ z. zx. y)

If one only formalizes the notion of function application and does not allow lambda expressions, one obtains combinatory logicThis article is about a topic in theoretical computer science, and is not to be confused with combinatorial logic, a topic in electronics. Combinatory logic is a simplified model of computation, used in computability theory (the study of what can be compu.





Non User