Differences between current version and predecessor to the previous major change of LambdaCalculus.

Other diffs: Previous Revision, Previous Author, or view the Annotated Edit History

Newer page: | version 11 | Last edited on Friday, January 13, 2006 11:02:16 pm | by ToniMarsh | |

Older page: | version 1 | Last edited on Friday, October 24, 2003 11:49:11 am | by StuartYeates | Revert |

`@@ -1,3 +1,38 @@`

`-`A conceptual model of computers based on defining and evaluating functions. Of current

`+`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.

`-`One of the fundamental proofs in ComputerScience is that any result

`+`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 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)

`+`

`+`then the successor function might be defined as

`+`successor = λx.y(x y y)

`+`

`+`so "successor one" is

`+`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 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.

`+`

`+`Three is obvious

`+`three = sucessor two

`+`which eventually expands to

`+`three = λx(x x x)

`+`

`+`Addition is easy

`+`add = λ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)