Skip to content

Instantly share code, notes, and snippets.

@rctay
Last active December 26, 2015 03:09
Show Gist options
  • Save rctay/7083700 to your computer and use it in GitHub Desktop.
Save rctay/7083700 to your computer and use it in GitHub Desktop.
lambda calculus library
module EvalLibrary = struct
(* Our familiar friend, the pipe operator *)
let ( |> ) (x:'a) (f:'a->'b) : 'b = f x
(* Takes/returns functions that take a expression to be wrapped *)
let bind name expr (fn:string -> string) =
(* (head^"let "^name^" = "^expr^" in ", " end"^tail) *)
fun body ->
fn ((Printf.sprintf "let %s = %s in %s end") name expr body)
(*** begin our library... ***)
let bools x =
x
|> bind "true" "\\t.\\f.t"
|> bind "false" "\\t.\\f.f"
|> bind "if" "\\l.\\m.\\n.l m n"
and num x =
x
|> bind "c0" "\\s.\\z.z"
|> bind "c1" "\\s.\\z.s z"
(* Notice how the s, z are reversed; hopefully catch beta reduction + alpha renaming bugs *)
|> bind "c2" "\\z.\\s.z (z s)"
(* ...2 in the usual s, z style *)
|> bind "c2N" "\\s.\\z.s (s z)"
|> bind "succ" "\\z.\\n.\\s.n (z n s)"
|> bind "succN" "\\n.\\s.\\z.s (n s z)"
(* Taken from wikipedia [1]; renamed to the familiar s, z
[1] http://en.wikipedia.org/wiki/Lambda_calculus#Arithmetic_in_lambda_calculus
*)
|> bind "pred" "\\n. \\s. \\z. n (\\g. \\h. h (g s)) (\\u. z) (\\u. u)"
and arith x =
x
|> bind "plus" "\\m.\\n.\\s.\\z.m s (n s z)"
|> bind "times" "\\m.\\n.m (plus n) c0"
and cond =
bind "iszero" "\\m.m (\\x.false) true"
and fix x =
x
|> bind "Y" "\\f.(\\x.f (\\y.x x y)) (\\x.f (\\y.x x y))"
|> bind "YY" "\\f.(\\x.f (x x))(\\x. f (x x))"
and fact =
(* lazy to implement less than, hence iszero *)
bind "fact" "Y (\\h.\\n.if (iszero n) c1 (times n (h (pred n))))";;
(*** end ***)
(* wrap an expression s in this library *)
let with_my_library : string -> string =
(fun x -> x)
|> bools
|> num
|> arith
|> cond
|> fix
|> fact
(* eval without printing bindings *)
let test_eval strategy s =
let wrapped_s = with_my_library s in
let (expr,steps) = strategy 10000 (Parser.reader Lambda.lam_expr wrapped_s) in
print_endline (s^" =eval("^(string_of_int steps)^")=> "^(Lambda.string_of_lambda expr));
expr
let count_num (expr:Lambda.lambda) =
match expr with
| Lambda.Lam(s, Lambda.Lam(z, body)) ->
let rec aux body count =
match body with
| Lambda.Var(y) when y=z -> count
| Lambda.App(Lambda.Var(r),body) when r=s -> aux body (count+1)
| _ -> failwith "not a number" in
aux body 0
| _ -> failwith "not a number";;
let test_num strategy s =
let expr = test_eval strategy s in
print_endline ("\t=count=> "^(string_of_int (count_num expr)))
end;;
(* Usage: *)
EvalLibrary.test_eval L.eval_by_name "times c2 c2";;
EvalLibrary.test_eval L.eval_by_value "times c2 c2";;
(* doesn't work *)
EvalLibrary.test_num L.eval_by_name "fact c2";;
EvalLibrary.test_num L.eval_by_value "fact c2";;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment