--- /dev/null
+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
+
--- /dev/null
+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
+