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 — also known as typed lambda calculus. Later that same year, this 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).
Contents |
|
