Lambda Calculus

In mathematical logic and computer science, lambda calculus, also λ-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 lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. Lambda calculus can be used to define what a computable function is.

In Turing's words:"a function is said to be 'effectively calculable' if its values can be found by some purely mechanical process. Although it is fairly easy to get an intuitive grasp of this idea, it is nevertheless desirable to have some more definite, mathematically expressible definition. Such a definition was first given by Godel at Princeton in 1934... These functions were described as 'general recursive' by Godel ... Another definition of effective calculability has been given by Church... who identifies it with definability. The author [i.e. Turing himself] has recently suggested a definition corresponding more closely to the intuitive idea... It was stated above that 'a function is effectively calculable if its values can be found by some purely mechanical process. ' We may take this statement literally, understanding by a purely mechanical process one which could be carried out by a machine... The development of these ideas leads to the author's definition of a computable function, and to an identification of computability [in Turing's precise technical sense] with effective calculability. It is not difficult, though somewhat laborious, to prove that these three definitions are equivalent."

Turing here gives a view on what is now known and famous as Church's thesis. Although Church's thesis is nowadays given various other interpretations, in 1936 it was the claim that effective calculability could be identified with the operations of Church's very elegant and surprising formalism, that of the lambda-calculus. As such it lay within the world of mathematical formalism. But Turing offers a reason why Church's thesis should be true, drawing on ideas external to mathematics such as that one cannot do see or choose between more than a finite number of things at one time. Church's thesis is now sometimes called the
Church-Turing thesis, but the Turing thesis is different, bringing the physical world into the picture with a claim of what can be done. It should not go without mention that Turing after referring to his machine definition of computability, also cited the work of the Polish-American logician Emil Post, which had also brought an idea of physical action into computation. However Post had not developed his ideas so fully.

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, such as Lisp, ML and Haskell.

Lambda calculus can be called the smallest universal programming language. It consists of a single transformation rule (variable substitution) and a single function definition scheme. Lambda calculus is universal in the sense that any computable function can be expressed and evaluated using this formalism. It is thus equivalent to the Turing machine formalism. However, 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.

History and Evolution

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.

The lambda calculus was originally developed as a foundation for mathematics. This work was done in the 1930s several years before digital computers were invented. A little earlier (in the 1920s) Moses Schonfinkel developed another theory of functions based on what are now called combinators. In the 1930s Haskell Curry rediscovered and extended Schonfinkel's theory and showed that it was equivalent to the lambda calculus. About this time Kleene showed that the lambda calculus was a universal computing system; it was one of the first such systems to be rigorously analysed. In the 1950s John McCarthy was inspired by the lambda calculus to invent the programming language LISP. In the early 1960s Peter Landin showed how the meaning of imperative programming languages could be specified by translating them into the lambda calculus. He also invented an influential prototype programming language called ISWIM. This introduced the main notations of functional programming and influenced the design of both functional and imperative languages. Building on this work, Christopher Strachey laid the foundations for the important area of denotational semantics. Technical questions concerning Strachey's work inspired the mathematical logician Dana Scott to invent the theory of domains which is now one of the most important parts of theoretical computer science. During the 1970s Peter Henderson and Jim Morris took up Landin's work and wrote a number of influential papers arguing that functional programming had important advantages for software engineering. At about the same time David Turner proposed that Schonfinkel and Curry's combinators could be used as the machine code of computers for executing functional programming languages. Such computers could exploit mathematical properties of the lambda calculus for the parallel evaluation of programs. During the 1980s several research groups took up Henderson's and Turner's ideas and started working on making functional programming practical by designing special architectures to support it; some of them with many processors.

Definition

Lambda calculus power to express any computable function derived of a very simple mechanism to define functions. Grammatically it is composed of a set of rules for function conversion (or reduction). From that it is possible to represent algebra, logic, recursion and other formalisms. In that sense it is considered an universal language.

There are three main types of conversions allowed: alfa, beta, and eta. The most important kind of conversion is beta conversion; it is the one that can be
used to simulate arbitrary evaluation mechanisms. alfa conversion is to do with the technical manipulation of bound variables and eta conversion expresses the fact that two functions that always give the same results on the same arguments are equal.

A lambda expression (necessarily an abstraction) to which alfa reduction can be applied is called an alfa-redex The term 'redex' abbreviates 'reducible expression'. The rule of alfa conversion just says that bound variables can be renamed provided no 'name clashes' occur.

A lambda expression (necessarily an application) to which beta reduction can be applied is called a beta-redex. The rule of beta conversion is like the evaluation of a function call in a programming language: the body expression of a function is evaluated in an environment in which the 'formal parameter' is bound to the 'actual parameter'.

A lambda expression (necessarily an abstraction) to which eta reduction can be applied is called an eta-redex. The rule of eta conversion expresses the property that two functions are equal if they give the same results when applied to the same arguments. This property is called extensionality.

The central concept in lambda calculus is the "expression". A "name", also called a "variable", is an identifier. An expression is defined recursively as follows:

expression := name | function | application
function := λname.expression
application := expression expression

Computable functions and lambda calculus

A function F: N -> N of natural numbers is a computable function if and only if there exists a lambda expression f such that for every pair of x, y in N, F(x) = y if and only if f x == y, where x and y are the Church numerals corresponding to x and y, respectively. This is one of the many ways to define computability; see the Church-Turing thesis for a discussion of other approaches and their equivalence.

Undecidability of equivalence

There is no algorithm which takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which the unsolvability could be proven. Of course, in order to do so, the notion of algorithm has to be cleanly defined; Church used a definition via recursive functions, which is now known to be equivalent to all other reasonable definitions of the notion.

Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression which cannot be reduced any further. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, he constructs a lambda expression e which closely follows the proof of Gödel's first incompleteness theorem. If e is applied to its own Gödel number, a contradiction results.

Lambda calculus and programming languages

As pointed out by Peter Landin's 1965 classic A Correspondence between ALGOL 60 and Church's Lambda-notation, most programming languages are rooted in the lambda calculus, which provides the basic mechanisms for procedural abstraction and procedure (subprogram) application.

Implementing the lambda calculus on a computer involves treating "functions" as first-class objects, which raises implementation issues for stack-based programming languages. This is known as the Funarg problem.

The most prominent counterparts to lambda calculus in programming are functional programming languages, which essentially implement the calculus augmented with some constants and datatypes. Lisp uses a variant of lambda notation for defining functions, but only its purely functional subset ("Pure Lisp") is really equivalent to lambda calculus.

Functional languages are not the only ones to support functions as first-class objects. Numerous imperative languages, e.g. Pascal, have long supported passing subprograms as arguments to other subprograms. In C and C++ the equivalent result is obtained by passing pointers to the code of functions (subprograms). Such mechanisms are limited to subprograms written explicitly in the code, and do not directly support higher-level functions. Some imperative object-oriented languages have notations that represent functions of any order; such mechanisms are available in Smalltalk and more recently in Eiffel ("agents") and C# ("delegates"). As an example, the Eiffel "inline agent" expression

agent (x: REAL): REAL do Result := x * x end

denotes an object corresponding to the lambda expression ? x . x*x (with call by value). It can be treated like any other expression, e.g. assigned to a variable or passed around to routines. If the value of square is the above agent expression, then the result of applying square to a value a (ß-reduction) is expressed as square.item ([a]), where the argument is passed as a tuple.

Concurrency and parallelism

The Church-Rosser property of the lambda calculus means that evaluation (ß-reduction) can be carried out in any order, even concurrently. (Indeed, the lambda calculus is referentially transparent.) While this means the lambda calculus can model the various nondeterministic evaluation strategies, it does not offer any richer notion of parallelism, nor can it express any concurrency issues. Process calculi such as CSP, the CCS, the p calculus and the ambient calculus have been designed for such purposes.

Conclusion

We thus see that an obscure branch of mathematical logic underlies important developments in programming language theory such as:

The study of fundamental questions of computation
The design of programming languages
The semantics of programming languages
The architecture of computers.

Bibliography:

"Lambda Calculus" in Wikipedia
A Tutorial Introduction to the Lambda Calculus by Raul Rojas
The Great Philosophers - From Socrates to Turing - "Turing" by Andrew Hodges
Introduction to Functional Programming by Mike Gordon