Lambda calculus
Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.
Contents
Description
First formulated by Alonzo Church to formalize the concept of effective computability, lambda calculus found early successes in the area of computability theory, such as a negative answer to David Hilbert's Entscheidungsproblem.
Lambda calculus is a conceptually simple universal model of computation.
Alan Turing showed in 1937 that Turing machines equated the lambda calculus in expressiveness.
The name derives from the Greek letter lambda (λ) used to denote binding a variable in a function. The letter itself is arbitrary and has no special meaning.
Lambda calculus is taught and used in computer science because of its usefulness in showcasing functional thinking and iterative reduction.
Because of the importance of the notion of variable binding and substitution, there is not just one system of lambda calculus, and in particular there are typed and untyped variants.
Historically, the most important system was the untyped lambda calculus, in which function application has no restrictions (so the notion of the domain of a function is not built into the system).
Church–Turing Thesis
In the Church–Turing Thesis, the untyped lambda calculus is claimed to be capable of computing all effectively calculable functions.
Typed lambda calculus
The typed lambda calculus is a variety that restricts function application, so that functions can only be applied if they are capable of accepting the given input's "type" of data.
Modern applications
Today, the lambda calculus has applications in many different areas in:
Computability theory
It is still used in the area of computability theory, although Turing machines are also an important computational model.
Programming language theory
Lambda calculus has played an important role in the development of the [[Programming language theory|theory of Programming language|programming languages.
Functional programming languages
Counterparts to lambda calculus in computer science are functional programming languages, which essentially implement the lambda calculus (augmented with some constants and data types).
Proof theory
Beyond programming languages, the lambda calculus also has many applications in proof theory.
See also
- Alonzo Church
- Church–Rosser theorem
- Church–Turing Thesis
- Computability theory
- Computation
- Computer science
- Entscheidungsproblem
- Functional programming language
- Mathematical logic
- Mathematics
- Turing machine
External links
- Lambda calculus @ Wikipedia
