Lambda calculus: Difference between revisions
imported>Christopher J. Reiss (fleshing out remaining article content) |
imported>Yuval Langer (→Introduction: a simple function) |
||
| (5 intermediate revisions by 2 users not shown) | |||
| Line 1: | Line 1: | ||
{{subpages}} | {{subpages}} | ||
In mathematical logic and computer science, the '''lambda calculus''' (also '''λ-calculus''') is a formal system designed to investigate functions and recursion. Although it was originally intended as a mathematical formalism and predates the electronic computer, it can be seen as the world's first formalized programming language. The programming language [[Lisp]] was created in large part from the λ-calculus. In mathematics, the λ-calculus was central to the first theorems of ''' | In mathematical logic and computer science, the '''lambda calculus''' (also '''λ-calculus''') is a formal system designed to investigate functions and recursion. Although it was originally intended as a mathematical formalism and predates the electronic computer, it can be seen as the world's first formalized programming language. The programming language [[Lisp]] was created in large part from the λ-calculus. In mathematics, the λ-calculus was central to some of the first theorems of '''computability''' - theorems about the limits of systematic computation which had broad philosophical impact ouside of mathematics. | ||
The λ-calculus was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s as part of a larger effort to base the foundation of mathematics upon functions rather than sets (in the hopes of avoiding set-theoretic obstacles like [[Russell's paradox]]). The λ-calculus was ultimately unable to avoid these pitfalls, but emerged as a powerful and elegant model of computation. In 1936 Church used it in his first investigations of Computability, which studies whether certain mathematical problems yield to ''any'' systematic solution by man or machine. This led to some of the earliest '''undecidability''' results in mathematics which established that certain problems could never be solved by any means. Perhaps most famously, it was used to give a negative answer to the Halting Problem in the [[Alonzo Church|Church]]-[[Alan Turing|Turing]] Thesis. | The λ-calculus was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s as part of a larger effort to base the foundation of mathematics upon functions rather than sets (in the hopes of avoiding set-theoretic obstacles like [[Russell's paradox]]). The λ-calculus was ultimately unable to avoid these pitfalls, but emerged as a powerful and elegant model of computation. In 1936 Church used it in his first investigations of Computability, which studies whether certain mathematical problems yield to ''any'' systematic solution by man or machine. This led to some of the earliest '''undecidability''' results in mathematics which established that certain problems could never be solved by any means. Perhaps most famously, it was used to give a negative answer to the Halting Problem in the [[Alonzo Church|Church]]-[[Alan Turing|Turing]] Thesis. | ||
| Line 7: | Line 7: | ||
The lambda calculus - and the paradigm of functional programming - is still influential, especially within the artificial intelligence community. | The lambda calculus - and the paradigm of functional programming - is still influential, especially within the artificial intelligence community. | ||
==Introduction== | ==Introduction== | ||
The Lambda Calculus is composed of only three basic constructs : '''definition''', '''assignment''' and '''application'''. | The Lambda Calculus is composed of only three basic constructs : '''definition''', '''assignment''' and '''application''', using two special operators, the 'λ' sign and the dot '.' | ||
The λ operator is used to '''define''' a function thus:<br /> | |||
::λ x . body<br /> | |||
which means, "a function which takes a single argument ''x'', evaluates the ''body'' - usually an expression using ''x'' - and returns the result.<br /> | |||
The following function defined doubles the value of the argument x and then adds 3: | |||
::λ x . 2*x+3<br /> | |||
Revision as of 15:23, 12 August 2008
In mathematical logic and computer science, the lambda calculus (also λ-calculus) is a formal system designed to investigate functions and recursion. Although it was originally intended as a mathematical formalism and predates the electronic computer, it can be seen as the world's first formalized programming language. The programming language Lisp was created in large part from the λ-calculus. In mathematics, the λ-calculus was central to some of the first theorems of computability - theorems about the limits of systematic computation which had broad philosophical impact ouside of mathematics.
The λ-calculus was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s as part of a larger effort to base the foundation of mathematics upon functions rather than sets (in the hopes of avoiding set-theoretic obstacles like Russell's paradox). The λ-calculus was ultimately unable to avoid these pitfalls, but emerged as a powerful and elegant model of computation. In 1936 Church used it in his first investigations of Computability, which studies whether certain mathematical problems yield to any systematic solution by man or machine. This led to some of the earliest undecidability results in mathematics which established that certain problems could never be solved by any means. Perhaps most famously, it was used to give a negative answer to the Halting Problem in the Church-Turing Thesis.
The lambda calculus can be thought of as an idealized, minimalist programming language. It is a close cousin of the Turing machine, another abstraction for modeling computation. The difference between the two is that the lambda calculus takes a functional view of algorithms, while the original Turing machine takes an imperative view. That is, a Turing machine maintains 'state' - a 'notebook' of symbols that can change from one instruction to the next. By contrast, the lambda calculus is stateless, it deals exclusively with functions which accept and return data (including other functions), but produce no side effects in 'state' and do not make alterations to incoming data (immutability.) The functional paradigm can be seen in modern languages like Lisp, Scheme and Haskell.
The lambda calculus - and the paradigm of functional programming - is still influential, especially within the artificial intelligence community.
Introduction
The Lambda Calculus is composed of only three basic constructs : definition, assignment and application, using two special operators, the 'λ' sign and the dot '.'
The λ operator is used to define a function thus:
- λ x . body
- λ x . body
which means, "a function which takes a single argument x, evaluates the body - usually an expression using x - and returns the result.
The following function defined doubles the value of the argument x and then adds 3:
- λ x . 2*x+3
- λ x . 2*x+3