Lambda calculus
lastmod 2015-05-05created 2015-05-051 edits
Lambda calculus (λ-calculus) is a formal system in theoretical computer science and mathematical logic that abstracts function definition, function application, and recursive functions. In the 1930s, Alonzo Church proposed the formalism of lambda calculus while researching the foundations of mathematics. The original lambda calculus system was proven to contain a logical inconsistency, but in 1936 Church extracted only the part related to computation and published it as a system that later came to be called the untyped lambda calculus. In 1940 he also introduced the simply typed lambda calculus, a weaker form that is free of logical contradiction.
Lambda calculus plays an important role in the theory of computation, linguistics, and other fields, and has contributed greatly to the development of programming language theory in particular. Functional programming languages such as Lisp were born under the direct influence of lambda calculus, and the simply typed lambda calculus became the foundation of type theory in modern programming languages.