User:Wgunther/Lambda Calculus
 | This is not a Wikipedia article: This is a workpage, a collection of material and work in progress that may or may not be incorporated into Lambda calculus. It should not necessarily be considered factual or authoritative. |
The lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation by way of variable binding and substitution. It was first formulated by Alonzo Church as a way to formalize mathematics through the notion of functions, in contrast to the field of set theory which attempts to formalize mathematics through the notion of sets. Although not very successful in that respect, the lambda calculus found early successes in the area of computability theory, such as a negative answer to Hilbert's Entscheidungsproblem.
Because of the importance of the notion of variable binding and substitution, there is not just one system of lambda calculus. Historically, the most important system is the untyped lambda calculus. In the untyped lambda calculus, function application has no restrictions (so the notion of the domain of a function is not built into the system). In the Church-Turing Thesis, the untyped lambda calculus is claimed to be capable of computing all effectively calculatable functions. The typed lambda calculus is a variety of systems that restricts function application, so that functions can only be applied if they are capable of accepting the given input's "type" of data.
Today, the lambda calculus has applications in many different areas in mathematics, philosophy, and computer science. It is still used in the area of computability theory, although Turing machines are arguably the preferred model for computation. Lambda calculus has played an important role in the development of the theory of programming languages. Many languages, especially functional programming languages implement different systems of lambda calculus (augmented with some constants and datatypes); some examples include ML, Haskell, and Lisp. Beyond programming languages, the lambda calculus also has many applications in proof theory. A major example of this is the Curry-Howard correspondence, which gives a correspondence between different systems of typed lambda calculus and systems of formal logic.
History
[edit]The lambda calculus was introduced by mathematician Alonzo Church in a 1932 paper [citation needed] as part of an investigation into the foundations of mathematics. The goal of the system was to give a framework for mathematics based on the idea of the function rather than that of a set. This system was found inconsistent in 1934 by two of Church's students, Kleene and Rosser, by way to the Kleene–Rosser paradox.
Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped I-calculus. This system lacked the aspects of logic in his earlier system, making it immune to the aforementioned paradox. Despite eliminating a lot of the expressiveness, this system was very expressive. Church had already encoded the natural numbers, and it was discovered by him and his students that one could encode many of the basic operations on natural numbers.
Kleene would discover this system was equivalent to the Godel-Herbrand recursive functions. In 1936, Church stated Church's Thesis (which would later be called the Church-Turing Thesis) which said that his calculus expressed exactly the notion of an effective computation. Kurt Godel, however, disagreed with this assessment. It was not until Alan Turing formulated his notion of computability (Turing Machines) when Godel was convinced the correct notion of computation was found[citation needed]. Turing, however, proved that his system was equivalent to Church's -calculus. For more on this, one can read the History of the Church–Turing thesis.
STILL NOT DONE. AND NEED SOME CITATIONS. SOARE, CARDONE/HINDLEY USED AS REFERENCES SO FAR