Difference between revisions of "History of Computers - The Lambda Calculus"
m (History of Computers - Lambda Calculus moved to History of Computers - The Lambda Calculus: It is normally referred to as "the lambda calculus") |
m (re-sectioned) |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
| + | The lambda calculus is a description of all computable functions. Essentially, it consists of three types of data: the '''expression''', the '''function''', and the '''application'''. An expression consists of a '''name''', a function, or an application; a function consists of a name and a function, and an application consists of two functions<ref name="pdf">http://www.utdallas.edu/~gupta/courses/apl/lambda.pdf</ref>. | ||
__TOC__ | __TOC__ | ||
| − | |||
| − | |||
==Overview== | ==Overview== | ||
| − | Alonzo Church (whose students include Alan Turing, known as the "father of computing") was attempting to find the foundations of mathematics when he created the lambda calculus. In essence, the lambda calculus is a system for defining functions. The name "lambda calculus" is consistent with the fact that, as arithmetic deals with changes in numbers and algebra deals with changes in variables, calculus deals with changes in functions. | + | Alonzo Church (whose students include Alan Turing, known as the "father of computing") was attempting to find the foundations of mathematics when he created the lambda calculus<ref name="wiki">http://en.wikipedia.org/wiki/Lambda</ref>. In essence, the lambda calculus is a system for defining functions. The name "lambda calculus" is consistent with the fact that, as arithmetic deals with changes in numbers and algebra deals with changes in variables, calculus deals with changes in functions. |
===Definition=== | ===Definition=== | ||
| − | The lambda calculus can be defined formally (in Backus-Naur Form) thusly: | + | The lambda calculus can be defined formally (in Backus-Naur Form) thusly<ref name="pdf" />: |
<code> | <code> | ||
<expression> := <name> | <function> | <application> | <expression> := <name> | <function> | <application> | ||
| Line 17: | Line 16: | ||
In Scheme, the function <code>(defun (<function-name> <arg-1> ... <arg-n>) <function-body>)</code> is used to define a named function, and <code>(lambda (<arg-1> ... <arg-n>) <function-body>)</code> is used to create an anonymous function. | In Scheme, the function <code>(defun (<function-name> <arg-1> ... <arg-n>) <function-body>)</code> is used to define a named function, and <code>(lambda (<arg-1> ... <arg-n>) <function-body>)</code> is used to create an anonymous function. | ||
===Numbers in the Lambda Calculus=== | ===Numbers in the Lambda Calculus=== | ||
| − | The most common implementation of natural numbers in the lambda calculus is known as the '''Church numeral'''. These are defined as such: | + | The most common implementation of natural numbers in the lambda calculus is known as the '''Church numeral'''<ref name="pdf" />. These are defined as such: |
<code> | <code> | ||
(defun (0 f x) x) | (defun (0 f x) x) | ||
| Line 25: | Line 24: | ||
</code> | </code> | ||
===Currying=== | ===Currying=== | ||
| − | The definition of the lambda calculus only allows for one argument to a function. A technique to use more than one argument (known as currying, after Haskell Curry) can be defined as such: | + | The definition of the lambda calculus only allows for one argument to a function. A technique to use more than one argument (known as currying, after Haskell Curry) can be defined as such<ref name="wiki" />: |
<code> | <code> | ||
λx.λy.<function-body> | λx.λy.<function-body> | ||
</code> | </code> | ||
==Significance== | ==Significance== | ||
| − | The lambda calculus was the first definition of computability, and has led to many other theories of computation. In addition, the lambda calculus greatly influenced the '''functional programming paradigm''', which states that a program should be an application of mathematical functions. However, functional programming is largely limited to academics. The lambda calculus has also influenced more practical languages such as C++ (which has a lambda construct in its new C++0x standard) and JavaScript (which has permits anonymous functions through syntax similar to the definition of a regular function). It has also influenced the popular textbook [http://mitpress.mit.edu/sicp/ Structure and Interpretation of Computer Programs], whose cover features a lambda in a prominent position. | + | The lambda calculus was the first definition of computability, and has led to many other theories of computation<ref name="wiki" />. In addition, the lambda calculus greatly influenced the '''functional programming paradigm''', which states that a program should be an application of mathematical functions. However, functional programming is largely limited to academics. The lambda calculus has also influenced more practical languages such as C++ (which has a lambda construct in its new C++0x standard) and JavaScript (which has permits anonymous functions through syntax similar to the definition of a regular function). It has also influenced the popular textbook [http://mitpress.mit.edu/sicp/ Structure and Interpretation of Computer Programs], whose cover features a lambda in a prominent position. |
http://mitpress.mit.edu/sicp/graphics/main-banner.gif | http://mitpress.mit.edu/sicp/graphics/main-banner.gif | ||
| + | ==References== | ||
| + | <references /> | ||
Latest revision as of 16:53, 28 August 2011
The lambda calculus is a description of all computable functions. Essentially, it consists of three types of data: the expression, the function, and the application. An expression consists of a name, a function, or an application; a function consists of a name and a function, and an application consists of two functions[1].
Contents
Overview
Alonzo Church (whose students include Alan Turing, known as the "father of computing") was attempting to find the foundations of mathematics when he created the lambda calculus[2]. In essence, the lambda calculus is a system for defining functions. The name "lambda calculus" is consistent with the fact that, as arithmetic deals with changes in numbers and algebra deals with changes in variables, calculus deals with changes in functions.
Definition
The lambda calculus can be defined formally (in Backus-Naur Form) thusly[1]:
<expression> := <name> | <function> | <application> <function> := λ<name>.<expression> <application> := <function><function>
However, for the purposes of this article, most code will be written in Scheme, a dialect of Lisp centered around the lambda calculus. The syntax of Scheme is fairly simple:
(<function-name> <arg-1> ... <arg-n>)
In Scheme, the function (defun (<function-name> <arg-1> ... <arg-n>) <function-body>) is used to define a named function, and (lambda (<arg-1> ... <arg-n>) <function-body>) is used to create an anonymous function.
Numbers in the Lambda Calculus
The most common implementation of natural numbers in the lambda calculus is known as the Church numeral[1]. These are defined as such:
(defun (0 f x) x) (defun (1 f x) (f x)) (defun (2 f x) (f (f x))) ...
Currying
The definition of the lambda calculus only allows for one argument to a function. A technique to use more than one argument (known as currying, after Haskell Curry) can be defined as such[2]:
λx.λy.<function-body>
Significance
The lambda calculus was the first definition of computability, and has led to many other theories of computation[2]. In addition, the lambda calculus greatly influenced the functional programming paradigm, which states that a program should be an application of mathematical functions. However, functional programming is largely limited to academics. The lambda calculus has also influenced more practical languages such as C++ (which has a lambda construct in its new C++0x standard) and JavaScript (which has permits anonymous functions through syntax similar to the definition of a regular function). It has also influenced the popular textbook Structure and Interpretation of Computer Programs, whose cover features a lambda in a prominent position.
