(* *) module Private = struct type var_t = int*string let var v = (0, v) let string_of_var (i, v) = v ^ String.make i '\'' let equal_var (i1, v1) (i2, v2) = i1 == i2 && (String.compare v1 v2 == 0) type lambda_t = [ `Var of var_t | `Lam of var_t * lambda_t | `App of lambda_t * lambda_t ] (* DeBruijn terms * substitution and translation algorithms from Chris Hankin, An Introduction to Lambda Calculi for Comptuer Scientists *) type debruijn_t = [ `Db_free of var_t | `Db_index of int | `Db_lam of debruijn_t | `Db_app of debruijn_t*debruijn_t ] let debruijn_subst (expr : debruijn_t) (m : int) (new_term : debruijn_t) = let rec renumber m i = function | `Db_free _ as term -> term | `Db_index j as term when j < i -> term | `Db_index j -> `Db_index (j + m - 1) | `Db_app(left, right) -> `Db_app(renumber m i left, renumber m i right) | `Db_lam body -> `Db_lam(renumber m (i+1) body) in let rec loop m = function | `Db_free _ as term -> term | `Db_index j as term when j < m -> term | `Db_index j when j > m -> `Db_index (j-1) | `Db_index j -> renumber j 1 new_term | `Db_app(left, right) -> `Db_app(loop m left, loop m right) | `Db_lam body -> `Db_lam(loop (m+1) body) in loop m expr let debruijn (expr : lambda_t) : debruijn_t = let pos seq (target : var_t) = let rec loop (i : int) = function | [] -> `Db_free target | x::xs when equal_var x target -> `Db_index i | _::xs -> loop (i+1) xs in loop 1 seq in let rec loop seq = function | `Var v -> pos seq v | `Lam (v, body) -> `Db_lam(loop (v::seq) body) | `App (left, right) -> `Db_app(loop seq left, loop seq right) in loop [] expr let rec dbruijn_equal (t1 : debruijn_t) (t2 : debruijn_t) = match (t1, t2) with | (`Db_free v1, `Db_free v2) -> equal_var v1 v2 | (`Db_index j1, `Db_index j2) -> j1 == j2 | (`Db_app(left1, right1), `Db_app(left2, right2)) -> dbruijn_equal left1 left2 && dbruijn_equal right1 right2 | (`Db_lam(body1), `Db_lam(body2)) -> dbruijn_equal body1 body2 | _ -> false let rec debruijn_contains (t1 : debruijn_t) (t2 : debruijn_t) = match (t1, t2) with | (`Db_free v1, `Db_free v2) -> equal_var v1 v2 | (`Db_index j1, `Db_index j2) -> j1 == j2 | (`Db_app(left1, right1), `Db_app(left2, right2)) when dbruijn_equal left1 left2 && dbruijn_equal right1 right2 -> true | (`Db_app(left, right), term2) -> debruijn_contains left term2 || debruijn_contains right term2 | (`Db_lam(body1), `Db_lam(body2)) when dbruijn_equal body1 body2 -> true | (`Db_lam(body1), term2) -> debruijn_contains body1 term2 | _ -> false (* non-normalizing string_of_lambda *) let string_of_lambda (expr : lambda_t) = let rec top = function | `Var v -> string_of_var v | `Lam _ as term -> "fun " ^ dotted term | `App ((`App _ as left), right) -> top left ^ " " ^ atom right | `App (left, right) -> atom left ^ " " ^ atom right and atom = function | `Var v -> string_of_var v | `Lam _ as term -> "(fun " ^ dotted term ^ ")" | `App _ as term -> "(" ^ top term ^ ")" and dotted = function | `Lam (v, (`Lam _ as body)) -> (string_of_var v) ^ " " ^ dotted body | `Lam (v, body) -> (string_of_var v) ^ " -> " ^ top body in top expr (* * substitution and normal-order evaluator based on Haskell version by Oleg Kisleyov * http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell *) (* if v occurs free_in term, returns Some v' where v' is the highest-tagged * variable with the same name as v occurring (free or bound) in term *) let free_in ((tag, name) as v) term = let rec loop = function | `Var((tag', name') as v') -> if name <> name' then false, v else if tag = tag' then true, v else false, v' | `App(left, right) -> let left_bool, ((left_tag, _) as left_v) = loop left in let right_bool, ((right_tag, _) as right_v) = loop right in left_bool || right_bool, if left_tag > right_tag then left_v else right_v | `Lam(v', _) when equal_var v v' -> (false, v) | `Lam(_, body) -> loop body in match loop term with | false, _ -> None | true, v -> Some v let rec subst v new_term term = match new_term with | `Var v' when equal_var v v' -> term | _ -> (match term with | `Var v' when equal_var v v' -> new_term | `Var _ -> term | `App(left, right) -> `App(subst v new_term left, subst v new_term right) | `Lam(v', _) when equal_var v v' -> term (* if x is free in the inserted term new_term, a capture is possible *) | `Lam(v', body) -> (match free_in v' new_term with (* v' not free in new_term, can substitute new_term for v without any captures *) | None -> `Lam(v', subst v new_term body) (* v' free in new_term, need to alpha-convert *) | Some max_x -> let bump_tag (tag, name) (tag', _) = (max tag tag') + 1, name in let bump_tag' ((_, name) as v1) ((_, name') as v2) = if (String.compare name name' == 0) then bump_tag v1 v2 else v1 in (* bump v' > max_x from new_term, then check whether * it also needs to be bumped > v *) let uniq_x = bump_tag' (bump_tag v' max_x) v in let uniq_x' = (match free_in uniq_x body with | None -> uniq_x (* bump uniq_x > max_x' from body *) | Some max_x' -> bump_tag uniq_x max_x' ) in (* alpha-convert body *) let body' = subst v' (`Var uniq_x') body in (* now substitute new_term for v *) `Lam(uniq_x', subst v new_term body') ) ) let check_eta = function | `Lam(v, `App(body, `Var u)) when equal_var v u && free_in v body = None -> body | (_ : lambda_t) as term -> term exception Lambda_looping;; let eval ?(eta=false) (expr : lambda_t) : lambda_t = let rec looping (body : debruijn_t) = function | [] -> false | x::xs when dbruijn_equal body x -> true | _::xs -> looping body xs in let rec loop (stack : lambda_t list) (body : lambda_t) = match body with | `Var v as term -> unwind term stack | `App(left, right) -> loop (right::stack) left | `Lam(v, body) -> (match stack with | [] -> let term = (`Lam(v, loop [] body)) in if eta then check_eta term else term | x::xs -> loop xs (subst v x body) ) and unwind left = function | [] -> left | x::xs -> unwind (`App(left, loop [] x)) xs in loop [] expr let cbv ?(aggressive=true) (expr : lambda_t) : lambda_t = let rec loop = function | `Var v as term -> term | `App(left, right) -> let right' = loop right in (match loop left with | `Lam(v, body) -> loop (subst v right' body) | _ as left' -> `App(left', right') ) | `Lam(v, body) as term -> if aggressive then `Lam(v, loop body) else term in loop expr (* (* (Oleg's version of) Ken's evaluator; doesn't seem to work -- requires laziness? *) let eval' ?(eta=false) (expr : lambda_t) : lambda_t = let rec loop = function | `Var v as term -> term | `Lam(v, body) -> let term = (`Lam(v, loop body)) in if eta then check_eta term else term | `App(`App _ as left, right) -> (match loop left with | `Lam _ as redux -> loop (`App(redux, right)) | nonred_head -> `App(nonred_head, loop right) ) | `App(left, right) -> `App(left, loop right) in loop expr module Sorted = struct let rec cons y = function | x :: _ as xs when x = y -> xs | x :: xs when x < y -> x :: cons y xs | xs [* [] or x > y *] -> y :: xs let rec mem y = function | x :: _ when x = y -> true | x :: xs when x < y -> mem y xs | _ [* [] or x > y *] -> false let rec remove y = function | x :: xs when x = y -> xs | x :: xs when x < y -> x :: remove y xs | xs [* [] or x > y *] -> xs let rec merge x' y' = match x', y' with | [], ys -> ys | xs, [] -> xs | x::xs, y::ys -> if x < y then x :: merge xs y' else if x = y then x :: merge xs ys else [* x > y *] y :: merge x' ys end let free_vars (expr : lambda_t) : string list = let rec loop = function | `Var x -> [x] | `Lam(x, t) -> Sorted.remove x (loop t) | `App(t1, t2) -> Sorted.merge (loop t1) (loop t2) in loop expr let free_in v (expr : lambda_t) = Sorted.mem v (free_vars t) let new_var = let counter = ref 0 in fun () -> (let z = !counter in incr counter; "_v"^(string_of_int z)) ... | `Lam(x, body) as term when not (free_in v body) -> term | `Lam(y, body) when not (free_in y new_term) -> `Lam(y, subst v new_term body) | `Lam(y, body) -> let z = new_var () in subst v new_term (`Lam(z, subst y (`Var z) body)) *) (* let bound_vars (expr : lambda_t) : string list = let rec loop = function | `Var x -> [] | `Lam(x, t) -> Sorted.cons x (loop t) | `App(t1, t2) -> Sorted.merge (loop t1) (loop t2) in loop expr let reduce_cbv ?(aggressive=true) (expr : lambda_t) : lambda_t = let rec loop = function | `Var x as term -> term | `App(t1, t2) -> let t2' = loop t2 in (match loop t1 with | `Lam(x, t) -> loop (subst x t2' t) | _ as term -> `App(term, t2') ) | `Lam(x, t) as term -> if aggressive then `Lam(x, loop t) else term in loop expr let reduce_cbn (expr : lambda_t) : lambda_t = let rec loop = function | `Var x as term -> term | `Lam(v, body) -> check_eta (`Lam(v, loop body)) | `App(t1, t2) -> (match loop t1 with | `Lam(x, t) -> loop (subst x t2 t) | _ as term -> `App(term, loop t2) ) in loop expr *) (* type env_t = (string * lambda_t) list let subst body x value = ((fun env -> let new_env = (x, value) :: env in body new_env) : env_t -> lambda_t) type strategy_t = By_value | By_name let eval (strategy : strategy_t) (expr : lambda_t) : lambda_t = in let rec inner = function | `Var x as t -> (fun env -> try List.assoc x env with | Not_found -> t) | `App(t1, value) -> (fun env -> let value' = if strategy = By_value then inner value env else value in (match inner t1 env with | `Lam(x, body) -> let body' = (subst (inner body) x value' env) in if strategy = By_value then body' else inner body' env | (t1' : lambda_t) -> `App(t1', inner value env) ) ) | `Lam(x, body) -> (fun env -> let v = new_var () in `Lam(v, inner body ((x, `Var v) :: env))) in inner expr ([] : env_t) let pp_env env = let rec loop acc = function | [] -> acc | (x, term)::es -> loop ((x ^ "=" ^ string_of_lambda term) :: acc) es in "[" ^ (String.concat ", " (loop [] (List.rev env))) ^ "]" let eval (strategy : strategy_t) (expr : lambda_t) : lambda_t = let new_var = let counter = ref 0 in fun () -> (let z = !counter in incr counter; "_v"^(string_of_int z)) in let rec inner term = begin Printf.printf "starting [ %s ]\n" (string_of_lambda term); let res = match term with | `Var x as t -> (fun env -> try List.assoc x env with | Not_found -> t) | `App(t1, value) -> (fun env -> let value' = if strategy = By_value then inner value env else value in (match inner t1 env with | `Lam(x, body) -> let body' = (subst (inner body) x value' env) in if strategy = By_value then body' else inner body' env | (t1' : lambda_t) -> `App(t1', inner value env) ) ) | `Lam(x, body) -> (fun env -> let v = new_var () in `Lam(v, inner body ((x, `Var v) :: env))) in (fun env -> (Printf.printf "%s with %s => %s\n" (string_of_lambda term) (pp_env env) (string_of_lambda (res env)); res env)) end in inner expr ([] : env_t) *) let normal ?(eta=false) expr = eval ~eta expr let normal_string_of_lambda ?(eta=false) (expr : lambda_t) = string_of_lambda (normal ~eta expr) let rec to_int expr = match expr with | `Lam(s, `Lam(z, `Var z')) when z' = z -> 0 | `Lam(s, `Var s') when equal_var s s' -> 1 | `Lam(s, `Lam(z, `App (`Var s', t))) when s' = s -> 1 + to_int (`Lam(s, `Lam(z, t))) | _ -> failwith (normal_string_of_lambda expr ^ " is not a church numeral") let int_of_lambda ?(eta=false) (expr : lambda_t) = to_int (normal ~eta expr) end type lambda_t = Private.lambda_t open Private let var = var let pp, pn, pi = string_of_lambda, normal_string_of_lambda, int_of_lambda let pnv, piv= (fun expr -> string_of_lambda (cbv expr)), (fun expr -> to_int (cbv expr)) let debruijn, dbruijn_equal, debruijn_contains = debruijn, dbruijn_equal, debruijn_contains let alpha_eq x y = dbruijn_equal (debruijn x) (debruijn y)