||The English used in this article or section may not be easy for everybody to understand. (November 2011)|
In mathematical logic and computer science, lambda calculus, also λ-calculus, is a formal system. It was designed to investigate the definition of functions, and how to apply them. It is also a tool for analysing 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. No general algorithm can answer the question of whether two lambda calculus expressions are equivalent. 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 the same as the Turing machine formalism. However, lambda calculus emphasizes the use of transformation rules. It does not care about the actual machine that implements them. It is an approach more related to software than to hardware.