diff --git a/Lambda/README.md b/Lambda/README.md index fead8c4..b041bad 100644 --- 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 index cece54e..dee72fb 100644 --- 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 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 index c30a033..d504017 100644 --- 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 }