Penguin
Recent Changes
Blame: LambdaCalculus
EditPageHistoryDiffInfoLikePages
Annotated edit history of LambdaCalculus version 11, including all changes. View license author blame.
Rev Author # Line
10 AristotlePagaltzis 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.
1 StuartYeates 2
8 CarstenKlapp 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
9 CarstenKlapp 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.
2 PerryLorier 8
8 CarstenKlapp 9 For instance, if we define "one" as a function which outputs its argument once, we have:
2 PerryLorier 10
5 PerryLorier 11 one = λx(x)
2 PerryLorier 12
13 then the successor function might be defined as
5 PerryLorier 14 successor = λx.y(x y y)
2 PerryLorier 15
16 so "successor one" is
17 two = successor one
5 PerryLorier 18 two = λx.y(x y y) λx(x)
2 PerryLorier 19 now we do an alpha reduction (rename some variables)
5 PerryLorier 20 two = λx.y(x y y) λz(z)
9 CarstenKlapp 21 now we do a beta reduction (replace x with its value (λz(z))
5 PerryLorier 22 two = λy(λz(z) y y)
2 PerryLorier 23 and a beta reduction on z
5 PerryLorier 24 two = λy(y y)
8 CarstenKlapp 25 we now have a function that outputs its argument twice.
2 PerryLorier 26
3 PerryLorier 27 Three is obvious
28 three = sucessor two
29 which eventually expands to
5 PerryLorier 30 three = λx(x x x)
3 PerryLorier 31
7 CarstenKlapp 32 Addition is easy
11 ToniMarsh 33 add = λx.y.z(x z y z)
3 PerryLorier 34
35 five = add two three
5 PerryLorier 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)