(* This is a simplified version of the code at http://lambda.jimpryor.net/code/untyped_full-1.4.tgz You can use this code as follows: 1. First, use a text editor to fill in the (* COMPLETE THIS *) portions. 2. Then see if OCaml will compile it, by typing `ocamlc -c untyped_evaluator.ml` in a Terminal. 3. If it doesn't work, go back to step 1. 4. If it does work, then you can start up the OCaml toplevel using `ocaml -I DIRECTORY`, where DIRECTORY is the name of the folder that contains your `untyped_evaluator.ml` file. (Alternatively, if OCaml is already started, you can type `#directory "DIRECTORY";;` 5. Then once OCaml is started, you can either: (a) type `#load "untyped_evaluator.cmo";;`, then type `open Untyped_evaluator;;` (this has to be on a separate line from step (a), it seems); or (b) instead you can type `#use "untyped_evaluator.ml";;` 6. Now you can try commands like: `reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y")))` `evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y")))` The two interpreters presented below are (VersionA) a substitute-and-repeat interpreter, and (VersionB) an environment-based interpreter. We discuss the differences between these in the course notes. The implementeations we provide make both of these call-by-value. When given a term `App(head, arg)`, the steps are: first, reduce or evaluate `head`---it might involve further `App`s itself. Second, reduce or evaluate `arg`. Third, only _when_ `arg` reduces or evaluates to a result value, then "perform" the application. What this last step amounts to is different in the two interpreters. Call-by-name interpreters would "perform" the application regardless, and without even trying to reduce or evaluate arg to a result value beforehand. Additionally, these implementations assume that free variables are "stuck" terms rather than result values. That is a bit inconvenient with this simplified program: it means that Lambdas (or Closures, in VB) are the only result values. But in the fuller code from which this is simplified, it makes more sense, because there we also have literal number and boolean values as results, too. The environments play absolutely no role in the simplified VA interpreter presented here. In the fuller code, they have a limited role in the VA interpreter. In the VB interpreter, the environments are essential. *) type identifier = string type term = | Var of identifier | App of term * term | Lambda of identifier * term (* in VB, never used as a result *) | Let of identifier * term * term | If of term * term * term (* the following variant is never used as a term, only as a VB result *) | Closure of identifier * term * env (* in the fuller code, we separate the term and result types *) and result = term (* This simplified code just provides a single implementation of environments; but the fuller code provides more. *) and env = (identifier * term) list (* Operations for environments *) let empty = [] let shift (ident : identifier) binding env = (ident,binding) :: env let rec lookup (sought_ident : ident) (env : env) : term option = match env with | [] -> None | (ident, binding) :: _ when ident = sought_ident -> Some binding | _ :: env' -> lookup sought_ident env' (* eval raises this exception when it fails to reduce/evaluate a term, because it has components for which no reduction/evaluation is defined, such as `x y`. The substitute-and-repeat interpreter just signals this with a normal return value; but the environment-based interpreter uses an exception to abort prematurely. In this simplified version of the code, we also use this exception to report a failed term in VA, since we lack the resources to print the term instead, as the full code does. *) exception Stuck of term module VA = struct (* --------------------------------------------------------------- Interpreter that reduces by substituting, using: val reduce_head_once : term -> env -> reduceOutcome val reduce : term -> env -> result reduce_head_once is similiar to reduce_if_redex in the combinatory logic interpreter, except that the latter only performed a reduction if its argument was exactly a redex. It had to rely on its caller to detect cases where the term was instead a longer sequence of applications that had a redex at its head. In the present code, on the other hand, we have reduce_head_once take care of this itself, by calling itself recursively where appropriate. Still, it will only perform at most one reduction per invocation. *) (* Search term and find a variable that isn't used in it, either free or bound. We do this by appending primes to base until we find an unused or "fresh" variable. *) let fresh_var (base : identifier) (term : term) : identifier = let rec aux term vars = match term with | Var(var_ident) -> var_ident :: vars | App(head, arg) -> let vars' = aux head vars in aux arg vars' | Lambda(bound_ident, body) -> aux body (bound_ident :: vars) | Let(bound_ident, arg, body) -> let vars' = aux arg vars in aux body (bound_ident :: vars') | If(test, yes, no) -> let vars' = aux test vars in let vars'' = aux yes vars' in aux no vars'' | Closure _ -> assert false in let used_vars = aux term [] in let rec check ident = if List.mem ident used_vars then check (ident ^ "'") else ident in check (base ^ "'") let rec free_in (ident : identifier) (term : term) : bool = match term with | Var(var_ident) -> var_ident = ident | App(head, arg) -> free_in ident head || free_in ident arg | Lambda(bound_ident, body) -> bound_ident <> ident && free_in ident body | Let(bound_ident, arg, body) -> free_in ident arg || (bound_ident <> ident && free_in ident body) | If(test, yes, no) -> free_in ident test || free_in ident yes || free_in ident no | Closure _ -> assert false let rec substitute (ident:identifier) (replacement : term) (original : term) = match original with | Var(var_ident) when var_ident = ident -> replacement | Var _ as orig -> orig | App(head, arg) -> let head' = substitute ident replacement head in let arg' = substitute ident replacement arg in App(head', arg') | Lambda(bound_ident, body) as orig when bound_ident = ident || not (free_in ident body) -> (* vacuous substitution *) orig | Lambda(bound_ident, body) when not (free_in bound_ident replacement) -> (* can substitute without renaming bound_ident *) let body' = substitute ident replacement body in Lambda(bound_ident, body') | Lambda(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 bound_ident (Var bound_ident') body in let body'' = substitute ident replacement body' in Lambda(bound_ident', body'') | Let(bound_ident, arg, body) when bound_ident = ident || not (free_in ident body) -> let arg' = substitute ident replacement arg 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 ident replacement body in let arg' = substitute ident replacement arg 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 bound_ident (Var bound_ident') body in let body'' = substitute ident replacement body' in let arg' = substitute ident replacement arg in Let(bound_ident', arg', body'') | If(test, yes, no) -> let test' = substitute ident replacement test in let yes' = substitute ident replacement yes in let no' = substitute ident replacement no in If(test', yes', no') | Closure _ -> assert false type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term let rec reduce_head_once (term : term) (env : env) : reduceOutcome = match term with | Lambda _ -> AlreadyResult term | Var var -> failwith ("Unbound variable `" ^ var ^ "`") | Closure _ -> assert false (* no Closures in VA *) (* In this simplified version there are no Bool Literals, so If terms are always stuck | If(Literal(Bool true),yes,no) -> ReducedTo yes | If(Literal(Bool false),yes,no) -> ReducedTo no *) | If(test,yes,no) -> (match reduce_head_once test env with | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *) | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) | ReducedTo test' -> ReducedTo(If(test',yes,no))) (* 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 reduce_head_once arg env with | AlreadyResult _ -> (* if arg was not reducible, we can substitute *) ReducedTo (substitute bound_var arg body) | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) | ReducedTo arg' -> ReducedTo (Let(bound_var,arg',body))) (* notice we only substitute after arg is reduced to a result *) | App(Lambda(bound_var, body) as head, arg) -> (match reduce_head_once arg env with | AlreadyResult _ -> (* if arg was not reducible, we can substitute *) ReducedTo (substitute bound_var arg body) | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) | ReducedTo arg' -> ReducedTo (App(head, arg'))) (* first the head should be reduced, next the arg *) | App(head, arg) -> (match reduce_head_once head env with | AlreadyResult _ -> (* head was not reducible, was arg? *) (match reduce_head_once arg env with | ReducedTo arg' -> ReducedTo (App(head, arg')) (* reducible cases of App(result, result) were caught above; so here we're stuck *) | AlreadyResult _ -> StuckAt term | StuckAt _ as outcome -> outcome) (* propagate Stuck subterm *) | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *) | ReducedTo head' -> ReducedTo (App(head', arg))) let rec reduce (term : term) (env : env) = match reduce_head_once term env with | AlreadyResult res -> res | StuckAt subterm -> raise (Stuck subterm) | ReducedTo term' -> reduce term' env (* keep trying *) end (* module VA *) module VB = struct (* --------------------------------------------------------------- Interpreter that employs an "environment" or assignment function of results, using: val eval term -> env -> result, or may raise (Stuck term) val evaluate term -> env -> result *) let rec eval (term : term) (env : env) : result = match term with | Closure _ -> term | Lambda(bound_var, body) -> Closure(bound_var, body, env) | Var var -> (match lookup var env with (* In this call-by-value design, only results get saved in the environment, so we can be sure this is a result. *) | Some res -> res | None -> failwith ("Unbound variable `" ^ var ^ "`")) | If(test, yes, no) -> (match eval test env with (* In this simplified version there are no Bool Literals, so If terms are always stuck | Literal(Bool true) -> eval yes env | Literal(Bool false) -> eval no env *) | res -> raise (Stuck(If(res,yes,no)))) | Let(bound_var, arg, body) -> (* evaluate body under a new env where bound_var has been bound to the result of evaluating arg under the current env *) let arg' = eval arg env in let env' = shift bound_var arg' env in eval body env' | App(head, arg) -> (match eval head env with | Closure(bound_var, body, saved_env) -> (* argument gets evaluated in current env *) let arg' = eval arg env in (* evaluate body under saved_env to govern its free variables, except that we add a binding of bound_var to arg' *) let saved_env' = shift bound_var arg' saved_env in eval body saved_env' | head' -> raise (Stuck(App(head',arg)))) let evaluate (term : term) (env : env) : result = eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *) end (* module VB *) let reduce term = VA.reduce term empty let evaluate term = VB.evaluate term empty