code/reduction_with_substitution.ml

   1 type primFunction = Succ | Pred | IsZero | Leq | Leq_partially_applied of int
   2
   3 type constant = Num of int | Bool of bool | Funct of primFunction
   4
   5 type identifier = string
   6
   7 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
   8
   9 let rec free_in (ident:identifier) (term:lambdaTerm) : bool =
  10   match term with
  11     | Constant _ -> false
  12     | Var(var_ident) -> var_ident = ident
  13 (*    | Abstract(bound_ident, body) ->  COMPLETE THIS LINE *)
  14 (*    | App(head, arg) -> COMPLETE THIS LINE *)
  15     | IfThenElse(test, yes, no) -> free_in ident test || free_in ident yes || free_in ident no
  16     | Let(bound_ident, arg, body) -> free_in ident arg || (bound_ident <> ident && free_in ident body)
  17
  18 let fresh_var (base : identifier) (term:lambdaTerm) =
  19   let rec all_vars term vs =  match term with
  20     | Constant _ -> vs
  21     | Var(var_ident) -> var_ident :: vs
  22     | Abstract(bound_ident, body) -> all_vars body (bound_ident :: vs)
  23     | App(head, arg) -> let vs' = all_vars head vs
  24                         in all_vars arg vs'
  25     | IfThenElse(test, yes, no) -> let vs' = all_vars test vs
  26                                    in let vs'' = all_vars yes vs'
  27                                    in all_vars no vs''
  28     | Let(bound_ident, arg, body) -> let vs' = all_vars arg vs
  29                                      in all_vars body (bound_ident :: vs')
  30   in let current = all_vars term []
  31   in let rec check ident = if List.mem ident current then check (ident ^ "'") else ident
  32   in check (base ^ "'") (* keep adding primes until we find a variable unused (either free or bound) in term *)
  33
  34 let rec substitute (term:lambdaTerm) (ident:identifier) (replacement:lambdaTerm) : lambdaTerm =
  35   match term with
  36     | Constant _ -> term
  37     | Var(var_ident) when var_ident = ident -> replacement
  38     | Var _ -> term
  39     | App(head, arg) -> let head' = substitute head ident replacement
  40                         in let arg' = substitute arg ident replacement
  41                         in App(head', arg')
  42     | IfThenElse(test, yes, no) -> let test' = substitute test ident replacement
  43                                    in let yes' = substitute yes ident replacement
  44                                    in let no' = substitute no ident replacement
  45                                    in IfThenElse(test', yes', no')
  46     | Abstract(bound_ident, body) when bound_ident = ident || not (free_in ident body) ->
  47         (* vacuous substitution *)
  48         term
  49     | Abstract(bound_ident, body) when not (free_in bound_ident replacement) ->
  50         (* can substitute without renaming bound_ident *)
  51         let body' = substitute body ident replacement
  52         in (* COMPLETE THIS LINE *)
  53     | Abstract(bound_ident, body) ->
  54         (* find a fresh variable unused in either body or replacement (which we hack by specifying their App) *)
  55         let bound_ident' = fresh_var bound_ident (App(body,replacement))
  56         in let body' = substitute body bound_ident (Var bound_ident')
  57         in let body'' = substitute body' ident replacement
  58         in Abstract(bound_ident', body'')
  59     | Let(bound_ident, arg, body) when bound_ident = ident || not (free_in ident body) ->
  60         let arg' = substitute arg ident replacement
  61         in Let(bound_ident, arg', body)
  62     | Let(bound_ident, arg, body) when not (free_in bound_ident replacement) ->
  63         (* can substitute without renaming bound_ident *)
  64         let body' = substitute body ident replacement
  65         in let arg' = substitute arg ident replacement
  66         in Let(bound_ident, arg', body')
  67     | Let(bound_ident, arg, body) ->
  68         (* find a fresh variable unused in either body or replacement (which we hack by specifying their App) *)
  69         let bound_ident' = fresh_var bound_ident (App(body,replacement))
  70         in let body' = substitute body bound_ident (Var bound_ident')
  71         in let body'' = substitute body' ident replacement
  72         in let arg' = substitute arg ident replacement
  73         in Let(bound_ident', arg', body'')
  74
  75 type reduceOutcome = AlreadyResult | ReducedTo of lambdaTerm | StuckAt of lambdaTerm
  76
  77 exception Stuck of lambdaTerm
  78
  79 let rec reduce1 (term:lambdaTerm) : reduceOutcome =
  80   match term with
  81       (* notice we never evaluate a yes/np branch until it is chosen *)
  82     | IfThenElse(Constant(Bool true), yes, _) -> ReducedTo yes
  83     | IfThenElse(Constant(Bool false), _, no) -> ReducedTo no
  84     | IfThenElse(test, yes, no) -> (match reduce1 test with
  85                                      | AlreadyResult -> StuckAt term (* if test was not reducible, neither is IfThenElse *)
  86                                      | ReducedTo test' -> ReducedTo (IfThenElse (test', yes, no))
  87                                      | StuckAt _ as outcome -> outcome)
  88       (* notice we never evaluate the body except after substituting, and that happens only after arg is reduced to a result *)
  89     | Let(bound_var, arg, body) -> (match reduce1 arg with
  90                                      | AlreadyResult -> (* if arg was not reducible, we can substitute *)
  91                                                         ReducedTo (substitute body bound_var arg)
  92                                      | ReducedTo arg' -> ReducedTo (Let(bound_var, arg', body))
  93                                      | StuckAt _ as outcome -> outcome)
  94       (* notice we only substitute after arg is reduced to a result *)
  95     | App(Abstract(bound_var, body) as head, arg) -> (match reduce1 arg with
  96                                      | AlreadyResult -> (* if arg was not reducible, we can substitute *)
  97                                                         ReducedTo (substitute body bound_var arg)
  98                                      | ReducedTo arg' -> ReducedTo (App(head, arg'))
  99                                      | StuckAt _ as outcome -> outcome)
 100       (* applications of primFunctions are reduced only when their arguments have been reduced to THE RIGHT TYPES of result *)
 101     | App(Constant(Funct Succ), Constant(Num n)) -> ReducedTo (Constant(Num (n+1)))
 102     | App(Constant(Funct Pred), Constant(Num n)) -> ReducedTo (Constant(Num (if n = 0 then 0 else n-1)))
 103     | App(Constant(Funct IsZero), Constant(Num n)) -> ReducedTo (Constant(Bool (n=0)))
 104       (* binary primFunctions are curried, have to be reduced in two steps *)
 105     | App(Constant(Funct Leq), Constant(Num n)) -> ReducedTo (Constant(Funct (Leq_partially_applied n)))
 106     | App(Constant(Funct (Leq_partially_applied m)), Constant(Num n)) -> ReducedTo (Constant(Bool (m<=n)))
 107       (* first the head should be reduced, next the arg *)
 108     | App(head, arg) -> (match reduce1 head with
 109                            | ReducedTo head' -> ReducedTo (App(head', arg))
 110                            | StuckAt _ as outcome -> outcome
 111                            | AlreadyResult -> (* head was not reducible, was arg? *)
 112                                      (match reduce1 arg with
 113                                         | ReducedTo arg' -> ReducedTo (App(head, arg'))
 114                                           (* else the reducible cases of App(result, result) were caught above; this must be stuck *)
 115                                         | AlreadyResult -> StuckAt term
 116                                         | StuckAt _ as outcome -> outcome))
 117     | Var _ -> StuckAt term (* free variables are stuck *)
 118     | Constant _ -> AlreadyResult
 119     | Abstract(_, _) -> AlreadyResult
 120
 121 let rec check_numbers (term:lambdaTerm) : unit =
 122   match term with
 123     | Constant(Num n) when n < 0 -> failwith ("Bad Number: " ^ string_of_int n)
 124     | Constant _ -> ()
 125     | Var _ -> ()
 126     | Abstract(_, body) -> check_numbers body
 127     | App(head, arg) -> let () = check_numbers head
 128                         in check_numbers arg
 129     | Let(_, arg, body) -> let () = check_numbers arg
 130                            in check_numbers body
 131     | IfThenElse(test, yes, no) -> let () = check_numbers test
 132                            in let () = check_numbers yes
 133                            in check_numbers no
 134
 135 let reduce (term:lambdaTerm) : lambdaTerm =
 136   (* scan to verify that term doesn't have any Const(Num (negative)) *)
 137   let () = check_numbers term
 138   in let rec aux term = match reduce1 term with
 139       | AlreadyResult -> term
 140       | ReducedTo term' -> aux term' (* keep trying *)
 141       | StuckAt stuck_term -> raise (Stuck stuck_term) (* fail by raising exception *)
 142   in aux term