lambda calculus library

lab5-library.ml

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";;