Differences between version 9 and previous revision of LambdaCalculus.
Other diffs: Previous Major Revision, Previous Author, or view the Annotated Edit History
| Newer page: | version 9 | Last edited on Friday, October 24, 2003 7:02:11 pm | by CarstenKlapp | Revert |
| Older page: | version 8 | Last edited on Friday, October 24, 2003 7:00:46 pm | by CarstenKlapp | Revert |
@@ -3,9 +3,9 @@
One of the fundamental proofs in ComputerScience is that any result calculable in LambdaCalculus is calculable on a FiniteStateMachine.
(From memory:)
-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 that's it.
+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.
For instance, if we define "one" as a function which outputs its argument once, we have:
one = λx(x)
@@ -17,9 +17,9 @@
two = successor one
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))
+now we do a beta reduction (replace x with its
value (λz(z))
two = λy(λz(z) y y)
and a beta reduction on z
two = λy(y y)
we now have a function that outputs its argument twice.
