In
mathematical logic and
computer science,
lambda calculus, also written as
?-calculus, is a
formal system for
function definition, function application and
recursion. It was introduced by
Alonzo Church in 1932 as part of an investigation into the
foundations of mathematics[1]. When that originally conceived
untyped lambda calculus system turned out to be
inconsistent, Church isolated and published in 1936
[2] just the portion relevant to computation, what is now called the lambda calculus. Later that same year, this version of the lambda calculus was proved
[3] to be consistent. This version is the one used in most modern applications. It has emerged as a useful tool in the investigation of problems in
computability or recursion theory, and forms the basis of a paradigm of computer programming called
functional programming.
[4] This article deals with the
untyped lambda calculus.
In the lambda calculus, functions are first-class entities they are passed as arguments, and returned as results. Thus lambda expressions are a reification of the concept of an unnamed procedure without side effects. The lambda calculus can be thought of as an idealized, minimalistic programming language. It is capable of expressing any algorithm, and it is this fact that makes the model of functional programming an important one. Functional programs are stateless and deal exclusively with functions that accept and return data (including other functions), but they produce no side effects in 'state' and thus make no alterations to incoming data. Modern functional languages, building on the lambda calculus, include Erlang, Haskell, Lisp, ML, and Scheme, as well as nascent languages like Clojure, F_, Nemerle, and Scala.
The lambda calculus continues to play an important role in mathematical foundations, through the Curry-Howard correspondence. However, as a naïve foundation for mathematics, the untyped lambda calculus is unable to avoid set-theoretic paradoxes (see the Kleene–Rosser paradox).
The key concept of lambda calculus is a lambda expression. A lambda expression represents an anonymous function[clarification needed] and defines the transformation that the function performs to its argument. For some simple examples, it is helpful to suppose we have a + operation and some constants 1, 2 etc.. A numeric add-two function, which adds 2 to its argument, can be expressed in lambda calculus as ?x.x + 2. The variable x is incidental to this lambda expression, which can be equivalently expressed as ?y.y + 2; the name of the argument is immaterial (see a-conversion). In a more conventional mathematical notation this function can be expressed as f such that f(x) = x + 2, or sometimes (using anonymous function notation) as x ? x + 2.
