Penguin
Diff: LambdaCalculus
EditPageHistoryDiffInfoLikePages

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 ProgrammingLanguages , [LISP], [Scheme] and [Haskell] best expose this conceptual model. 
+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 calculatable in LambdaCalculus is calculatable on a FiniteStateMachine. 
+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)