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.
Name
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.
Computer science
Lambda calculus is taught and used in computer science because of its usefulness in showcasing functional thinking and iterative reduction.
Typed and untyped variants
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.
Untyped lambda calculus
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
- Abstraction (computer science)
- Applicative computing systems – Treatment of objects in the style of the lambda calculus
- Binary lambda calculus – A version of lambda calculus with binary I/O, a binary encoding of terms, and a designated universal machine.
- Calculus of constructions – A typed lambda calculus with types as first-class values
- Cartesian closed category – A setting for lambda calculus in category theory
- Alonzo Church
- Church–Rosser theorem
- Church–Turing Thesis
- Categorical abstract machine – A model of computation applicable to lambda calculus
- Combinatory logic – A notation for mathematical logic without variables
- Computability theory
- Computation
- Computer science
- Curry-Howard isomorphism – The formal correspondence between programs and proofs
- Deductive lambda calculus – The consideration of the problems associated with considering lambda calculus as a Deductive system.
- Domain theory – Study of certain posets giving denotational semantics for lambda calculus
- Entscheidungsproblem
- Evaluation strategy – Rules for the evaluation of expressions in programming languages
- Explicit substitution – The theory of substitution, as used in β-reduction
- Functional programming
- Harrop formula – A kind of constructive logical formula such that proofs are lambda terms
- Kappa calculus – A first-order analogue of lambda calculus
- Kleene-Rosser paradox – A demonstration that some form of lambda calculus is inconsistent
- Knights of the Lambda Calculus – A semi-fictional organization of * LISP and Scheme hackers
- Lambda calculus definition - Formal definition of the lambda calculus.
- Lambda cube – A framework for some extensions of typed lambda calculus
- Lambda-mu calculus – An extension of the lambda calculus for treating classical logic
- Let expression – An expression close related to a lambda abstraction.
- Mathematical logic
- Mathematics
- Minimalism (computing)
- Rewriting – Transformation of formulæ in formal systems
- SECD machine – A virtual machine designed for the lambda calculus
- Simply typed lambda calculus - Version(s) with a single type constructor
- SKI combinator calculus – A computational system based on the S, K and I combinators
- Supercombinator - a mathematical expression which is fully bound and self-contained.
- System F – A typed lambda calculus with type-variables
- Turing completeness
- Turing machine
- Typed lambda calculus – Lambda calculus with typed variables (and functions)
- Universal Turing machine – A formal computing machine that is equivalent to lambda calculus
- Unlambda – An esoteric functional programming language based on combinatory logic
External links
- Lambda calculus @ Wikipedia
