| 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 |
|
|||||
| First Prev [ 1 2 3 4 ] Next Last |
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.
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.
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
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
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
or
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
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.