Differences between version 4 and previous revision of LambdaCalculus.
Other diffs: Previous Major Revision, Previous Author, or view the Annotated Edit History
| Newer page: | version 4 | Last edited on Friday, October 24, 2003 12:56:22 pm | by PerryLorier | Revert |
| Older page: | version 3 | Last edited on Friday, October 24, 2003 12:47:40 pm | by PerryLorier | Revert |
@@ -7,32 +7,32 @@
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 it's expansion. And thats it.
For instance, if we define "one" as a function which outputs it's argument once, we have:
- one = \
x(x)
+ one = Λ
x(x)
then the successor function might be defined as
- successor = \
x.y(x y y)
+ successor = Λ
x.y(x y y)
so "successor one" is
two = successor one
- two = \
x.y(x y y) \
x(x)
+ two = Λ
x.y(x y y) Λ
x(x)
now we do an alpha reduction (rename some variables)
- two = \
x.y(x y y) \
z(z)
-now we do a beta reduction (replace x with it's value (\
z(z))
- two = \
y(\
z(z) y y)
+ two = Λ
x.y(x y y) Λ
z(z)
+now we do a beta reduction (replace x with it's value (Λ
z(z))
+ two = Λ
y(Λ
z(z) y y)
and a beta reduction on z
- two = \
y(y y)
+ two = Λ
y(y y)
we now have a function that outputs it's argument twice.
Three is obvious
three = sucessor two
which eventually expands to
- three = \
x(x x x)
+ three = Λ
x(x x x)
Addiction is easy
- addition = \
x.y.z(x z y z)
+ addition = Λ
x.y.z(x z y z)
five = add two three
- five = \
x.y.z(x z y z) \
a(a a) \
a(a a a)
- five = \
z(\
a(a a) z \
a(a a a) z)
- five = \
z(z z z z z)
+ five = Λ
x.y.z(x z y z) Λ
a(a a) Λ
a(a a a)
+ five = Λ
z(Λ
a(a a) z Λ
a(a a a) z)
+ five = Λ
z(z z z z z)
