View Source: LambdaCalculus - Waikato Linux Users Group

Edit PageHistory Diff Info LikePages

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

2 pages link to LambdaCalculus:

Last edited on Friday, January 13, 2006 11:02:16 pm by "ToniMarsh"

Edit PageHistory Diff Info LikePages