Y-combinator.

aktemur · Dec 3, 2016 · 063d9fc · 063d9fc
1 parent 5ef5b3c
commit 063d9fc
Show file tree

Hide file tree

Showing 3 changed files with 40 additions and 0 deletions.
diff --git a/Lambda/README.md b/Lambda/README.md
@@ -111,3 +111,38 @@ Booleans, "if", and "isZero" predicate:
 - : string = "(\\f.(\\x.(f (f (f (f x))))))"
 ```
 
+Recursion, using fix-point calculation via a Y-combinator.
+Below, we are calculation 3! and 4!.
+
+```ocaml
+# str(run "(Y (\fact.\m.if (isZero m)
+                        one
+                        (mult m (fact (pred m))))
+           ) three");;
+- : string = "(\\f.(\\x.(f (f (f (f (f (f x))))))))"
+# str(run "(Y (\fact.\m.if (isZero m)            
+                        one                      
+                        (mult m (fact (pred m))))
+           ) four");;                            
+- : string =
+"(\\f.(\\x.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))"
+```
+
+Note that the programs below are pure lambda terms;
+"if", "pred", "mult" and other names with special meanings are
+just syntactic convenience. They are converted to plain lambda terms by the parser.
+E.g:
+
+```ocaml
+# str(parse "(Y (\fact.\m.if (isZero m)        
+                          one                  
+                          (mult m (fact (pred m))))
+             ) four");;                            
+- : string =
+"(((\\h.((\\x.(\\a.((h (x x)) a))) (\\x.(\\a.((h (x x)) a)))))
+(\\fact.(\\m.((((\\cond.(\\then.(\\else.((cond then) else))))
+((\\n.((n (\\x.(\\a.(\\b.b)))) (\\a.(\\b.a)))) m)) (\\f.(\\x.(f x))))
+(((\\m.(\\n.(\\f.(\\x.((m (n f)) x))))) m)
+(fact ((\\n.(\\f.(\\x.(((n (\\g.(\\h.(h (g f))))) (\\u.x)) (\\u.u))))) m)))))))
+(\\f.(\\x.(f (f (f (f x)))))))"
+```
diff --git a/Lambda/grammar.mly b/Lambda/grammar.mly
@@ -12,6 +12,7 @@
 %token SUCC ADD
 %token MULT PRED
 %token IF TRUE FALSE ISZERO
+%token YCOMB
 
 %start main
 %type <expr> main
@@ -50,6 +51,9 @@ atomExpr:
   | IF        { Lambda("cond", Lambda("then", Lambda("else", App(App(Var "cond", Var "then"), Var "else")))) }
   | ISZERO    { Lambda("n", App(App(Var "n", Lambda("x", Lambda("a", Lambda("b", Var "b")))),
                                 Lambda("a", Lambda("b", Var "a")))) }
+  /* Definition of Y-combinator taken from PLC, page 85. */
+  | YCOMB     { Lambda("h", App(Lambda("x", Lambda("a", App(App(Var "h", App(Var "x", Var "x")), Var "a"))),
+                                Lambda("x", Lambda("a", App(App(Var "h", App(Var "x", Var "x")), Var "a"))))) } 
   | LPAR expression RPAR               { $2 }
 ;
 

diff --git a/Lambda/lexer.mll b/Lambda/lexer.mll
@@ -32,6 +32,7 @@ let keyword s =
     | "true"  -> TRUE
     | "false" -> FALSE
     | "isZero" -> ISZERO
+    | "Y"     -> YCOMB
     | _       -> NAME s
 }