X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=code%2Fcaml-lambda%2Flambda.ml;fp=code%2Fcaml-lambda%2Flambda.ml;h=1eaca652e1aa95bb321818a506a8a54daf101956;hp=0000000000000000000000000000000000000000;hb=2ee0d2918d40efc78e75ce8fbc6ae90f8edf6541;hpb=492cb946fbc21f0d3db9de9bd57bd755bf4ca620

diff --git a/code/caml-lambda/lambda.ml b/code/caml-lambda/lambda.ml
new file mode 100644
index 00000000..1eaca652
--- /dev/null
+++ b/code/caml-lambda/lambda.ml
@@ -0,0 +1,389 @@
+(* *)
+
+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)
+