From: Jim Date: Thu, 19 Mar 2015 02:11:18 +0000 (-0400) Subject: remove extraneous code file X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=7acee0fbdbcefcac2ebf8e27e8b0312767dc575e remove extraneous code file --- diff --git a/_reduction_with_substitution.ml b/_reduction_with_substitution.ml deleted file mode 100644 index 3882c7fb..00000000 --- a/_reduction_with_substitution.ml +++ /dev/null @@ -1,143 +0,0 @@ -type primFunction = Succ | Pred | IsZero | Leq | Leq_partially_applied of int - -type constant = Num of int | Bool of bool | Funct of primFunction - -type identifier = string - -type lambdaTerm = Constant of constant | Var of identifier | Abstract of identifier * lambdaTerm | App of lambdaTerm * lambdaTerm | IfThenElse of lambdaTerm * lambdaTerm * lambdaTerm | Let of identifier * lambdaTerm * lambdaTerm - -let rec free_in (ident:identifier) (term:lambdaTerm) : bool = - match term with - | Constant _ -> false - | Var(var_ident) -> var_ident = ident - | Abstract(bound_ident, body) -> bound_ident <> ident && free_in ident body - | App(head, arg) -> free_in ident head || free_in ident arg - | IfThenElse(test, yes, no) -> free_in ident test || free_in ident yes || free_in ident no - | Let(bound_ident, arg, body) -> free_in ident arg || (bound_ident <> ident && free_in ident body) - -let fresh_var (base : identifier) (term:lambdaTerm) = - let rec all_vars term vs = match term with - | Constant _ -> vs - | Var(var_ident) -> var_ident :: vs - | Abstract(bound_ident, body) -> all_vars body (bound_ident :: vs) - | App(head, arg) -> let vs' = all_vars head vs - in all_vars arg vs' - | IfThenElse(test, yes, no) -> let vs' = all_vars test vs - in let vs'' = all_vars yes vs' - in all_vars no vs'' - | Let(bound_ident, arg, body) -> let vs' = all_vars arg vs - in all_vars body (bound_ident :: vs') - in let current = all_vars term [] - in let rec check ident = if List.mem ident current then check (ident ^ "'") else ident - in check (base ^ "'") (* keep adding primes until we find a variable unused (either free or bound) in term *) - -let rec substitute (term:lambdaTerm) (ident:identifier) (replacement:lambdaTerm) : lambdaTerm = - match term with - | Constant _ -> term - | Var(var_ident) when var_ident = ident -> replacement - | Var _ -> term - | App(head, arg) -> let head' = substitute head ident replacement - in let arg' = substitute arg ident replacement - in App(head', arg') - | IfThenElse(test, yes, no) -> let test' = substitute test ident replacement - in let yes' = substitute yes ident replacement - in let no' = substitute no ident replacement - in IfThenElse(test', yes', no') - | Abstract(bound_ident, body) when bound_ident = ident || not (free_in ident body) -> - (* vacuous substitution *) - term - | Abstract(bound_ident, body) when not (free_in bound_ident replacement) -> - (* can substitute without renaming bound_ident *) - let body' = substitute body ident replacement - in Abstract(bound_ident, body') - | Abstract(bound_ident, body) -> - (* find a fresh variable unused in either body or replacement (which we hack by specifying their App) *) - let bound_ident' = fresh_var bound_ident (App(body,replacement)) - in let body' = substitute body bound_ident (Var bound_ident') - in let body'' = substitute body' ident replacement - in Abstract(bound_ident', body'') - | Let(bound_ident, arg, body) when bound_ident = ident || not (free_in ident body) -> - let arg' = substitute arg ident replacement - in Let(bound_ident, arg', body) - | Let(bound_ident, arg, body) when not (free_in bound_ident replacement) -> - (* can substitute without renaming bound_ident *) - let body' = substitute body ident replacement - in let arg' = substitute arg ident replacement - in Let(bound_ident, arg', body') - | Let(bound_ident, arg, body) -> - (* find a fresh variable unused in either body or replacement (which we hack by specifying their App) *) - let bound_ident' = fresh_var bound_ident (App(body,replacement)) - in let body' = substitute body bound_ident (Var bound_ident') - in let body'' = substitute body' ident replacement - in let arg' = substitute arg ident replacement - in Let(bound_ident', arg', body'') - -type reduceOutcome = AlreadyResult | ReducedTo of lambdaTerm | StuckAt of lambdaTerm - -exception Stuck of lambdaTerm - -let rec reduce1 (term:lambdaTerm) : reduceOutcome = - match term with - (* notice we never evaluate a yes/np branch until it is chosen *) - | IfThenElse(Constant(Bool true), yes, _) -> ReducedTo yes - | IfThenElse(Constant(Bool false), _, no) -> ReducedTo no - | IfThenElse(test, yes, no) -> (match reduce1 test with - | AlreadyResult -> StuckAt term (* if test was not reducible, neither is IfThenElse *) - | ReducedTo test' -> ReducedTo (IfThenElse (test', yes, no)) - | StuckAt _ as outcome -> outcome) - (* notice we never evaluate the body except after substituting, and that happens only after arg is reduced to a result *) - | Let(bound_var, arg, body) -> (match reduce1 arg with - | AlreadyResult -> (* if arg was not reducible, we can substitute *) - ReducedTo (substitute body bound_var arg) - | ReducedTo arg' -> ReducedTo (Let(bound_var, arg', body)) - | StuckAt _ as outcome -> outcome) - (* notice we only substitute after arg is reduced to a result *) - | App(Abstract(bound_var, body) as head, arg) -> (match reduce1 arg with - | AlreadyResult -> (* if arg was not reducible, we can substitute *) - ReducedTo (substitute body bound_var arg) - | ReducedTo arg' -> ReducedTo (App(head, arg')) - | StuckAt _ as outcome -> outcome) - (* applications of primFunctions are reduced only when their arguments have been reduced to THE RIGHT TYPES of result *) - | App(Constant(Funct Succ), Constant(Num n)) -> ReducedTo (Constant(Num (n+1))) - | App(Constant(Funct Pred), Constant(Num n)) -> ReducedTo (Constant(Num (if n = 0 then 0 else n-1))) - | App(Constant(Funct IsZero), Constant(Num n)) -> ReducedTo (Constant(Bool (n=0))) - (* binary primFunctions are curried, have to be reduced in two steps *) - | App(Constant(Funct Leq), Constant(Num n)) -> ReducedTo (Constant(Funct (Leq_partially_applied n))) - | App(Constant(Funct (Leq_partially_applied m)), Constant(Num n)) -> ReducedTo (Constant(Bool (m<=n))) - (* first the head should be reduced, next the arg *) - | App(head, arg) -> (match reduce1 head with - | ReducedTo head' -> ReducedTo (App(head', arg)) - | StuckAt _ as outcome -> outcome - | AlreadyResult -> (* head was not reducible, was arg? *) - (match reduce1 arg with - | ReducedTo arg' -> ReducedTo (App(head, arg')) - (* else the reducible cases of App(result, result) were caught above; this must be stuck *) - | AlreadyResult -> StuckAt term - | StuckAt _ as outcome -> outcome)) - | Var _ -> StuckAt term (* free variables are stuck *) - | Constant _ -> AlreadyResult - | Abstract(_, _) -> AlreadyResult - -let rec check_numbers (term:lambdaTerm) : unit = - match term with - | Constant(Num n) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n) - | Constant _ -> () - | Var _ -> () - | Abstract(_, body) -> check_numbers body - | App(head, arg) -> let () = check_numbers head - in check_numbers arg - | Let(_, arg, body) -> let () = check_numbers arg - in check_numbers body - | IfThenElse(test, yes, no) -> let () = check_numbers test - in let () = check_numbers yes - in check_numbers no - -let reduce (term:lambdaTerm) : lambdaTerm = - (* scan to verify that term doesn't have any Const(Num (negative)) *) - let () = check_numbers term - in let rec aux term = match reduce1 term with - | AlreadyResult -> term - | ReducedTo term' -> aux term' (* keep trying *) - | StuckAt stuck_term -> raise (Stuck stuck_term) (* fail by raising exception *) - in aux term -