Annotated edit history of
LambdaCalculus version 11 showing authors affecting page license.
View with all changes included.
| Rev |
Author |
# |
Line |
| 1 |
StuartYeates |
1 |
A conceptual model of computers based on defining and evaluating functions. Of the current [ProgrammingLanguage]s, [LISP], [Scheme], [Haskell] and other Category:FunctionalProgrammingLanguages best expose this conceptual model. |
| |
|
2 |
|
| |
|
3 |
One of the fundamental proofs in ComputerScience is that any result calculable in LambdaCalculus is calculable on a FiniteStateMachine. |
| 2 |
PerryLorier |
4 |
|
| |
|
5 |
(From memory:) |
| |
|
6 |
|
| |
|
7 |
LambdaCalculus is based on the idea that you have two types of rewrite rules, one where you change the names of variables, and one where you replace a variable with its expansion. And that's it. |
| |
|
8 |
|
| |
|
9 |
For instance, if we define "one" as a function which outputs its argument once, we have: |
| |
|
10 |
|
| |
|
11 |
one = λx(x) |
| |
|
12 |
|
| |
|
13 |
then the successor function might be defined as |
| |
|
14 |
successor = λx.y(x y y) |
| |
|
15 |
|
| |
|
16 |
so "successor one" is |
| |
|
17 |
two = successor one |
| |
|
18 |
two = λx.y(x y y) λx(x) |
| |
|
19 |
now we do an alpha reduction (rename some variables) |
| |
|
20 |
two = λx.y(x y y) λz(z) |
| |
|
21 |
now we do a beta reduction (replace x with its value (λz(z)) |
| |
|
22 |
two = λy(λz(z) y y) |
| |
|
23 |
and a beta reduction on z |
| |
|
24 |
two = λy(y y) |
| |
|
25 |
we now have a function that outputs its argument twice. |
| |
|
26 |
|
| 3 |
PerryLorier |
27 |
Three is obvious |
| |
|
28 |
three = sucessor two |
| |
|
29 |
which eventually expands to |
| |
|
30 |
three = λx(x x x) |
| |
|
31 |
|
| |
|
32 |
Addition is easy |
| |
|
33 |
add = λx.y.z(x z y z) |
| |
|
34 |
|
| |
|
35 |
five = add two three |
| |
|
36 |
five = λx.y.z(x z y z) λa(a a) λa(a a a) |
| |
|
37 |
five = λz(Λa(a a) z λa(a a a) z) |
| |
|
38 |
five = λz(z z z z z) |
