4.2 Evaluation

---

4.2 Evaluation

The implementation of the evaluation relation closely follows the single-step evaluation rules in Figures 3-1 and 3-2. As we have seen, these rules define a partial function that, when applied to a term that is not yet a value, yields the next step of evaluation for that term. When applied to a value, the result of the evaluation function yields no result. To translate the evaluation rules into OCaml, we need to make a decision about how to handle this case. One straightforward approach is to write the single-step evaluation function eval1 so that it raises an exception when none of the evaluation rules apply to the term that it is given. (Another possibility would be to make the single-step evaluator return a term option indicating whether it was successful and, if so, giving the resulting term; this would also work fine, but would require a little more bookkeeping.) We begin by defining the exception to be raised when no evaluation rule applies:

   exception NoRuleApplies 

Now we can write the single-step evaluator itself.

   let rec eval1 t = match t with       TmIf(_,TmTrue(_),t2,t3) →         t2     | TmIf(_,TmFalse(_),t2,t3) →         t3     | TmIf(fi,t1,t2,t3) →         let t1' = eval1 t1 in         TmIf(fi, t1', t2, t3)     | TmSucc(fi,t1) →         let t1' = eval1 t1 in         TmSucc(fi, t1')     | TmPred(_,TmZero(_)) →         TmZero(dummyinfo)     | TmPred(_,TmSucc(_,nv1)) when (isnumericval nv1) →         nv1     | TmPred(fi,t1) →         let t1' = eval1 t1 in         TmPred(fi, t1')     | TmIsZero(_,TmZero(_)) →         TmTrue(dummyinfo)     | TmIsZero(_,TmSucc(_,nv1)) when (isnumericval nv1) →         TmFalse(dummyinfo)     | TmIsZero(fi,t1) →         let t1' = eval1 t1 in         TmIsZero(fi, t1')     | _ →         raise NoRuleApplies 

Note that there are several places where we are constructing terms from scratch rather than reorganizing existing terms. Since these new terms do not exist in the user's original source file, their info annotations are not useful. The constant dummyinfo is used as the info annotation in such terms. The variable name fi (for "file information") is consistently used to match info annotations in patterns.

Another point to notice in the definition of eval1 is the use of explicit when clauses in patterns to capture the eMect of metavariable names like v and nv in the presentation of the evaluation relation in Figures 3-1 and 3-2. In the clause for evaluating TmPred(_,TmSucc(_,nv1)), for example, the semantics of OCaml patterns will allow nv1 to match any term whatsoever, which is not what we want; adding when (isnumericval nv1) restricts the rule so that it can fire only when the term matched by nv1 is actually a numeric value. (We could, if we wanted, rewrite the original inference rules in the same style as the ML patterns, turning the implicit constraints arising from metavariable names into explicit side conditions on the rules

at some cost in compactness and readability.)

Finally, the eval function takes a term and finds its normal form by repeatedly calling eval1. Whenever eval1 returns a new term t′, we make a recursive call to eval to continue evaluating from t′. When eval1 finally reaches a point where no rule applies, it raises the exception NoRuleApplies, causing eval to break out of the loop and return the final term in the sequence.^[3]

   let rec eval t =     try let t' = eval1 t         in eval t'     with NoRuleApplies → t 

Obviously, this simple evaluator is tuned for easy comparison with the mathematical definition of evaluation, not for finding normal forms as quickly as possible. A somewhat more eHcient algorithm can be obtained by starting instead from the "big-step" evaluation rules in Exercise 4.2.2.

4.2.1 Exercise [⋆⋆]

Why not? What is a better way to write eval?

4.2.2 Exercise [Recommended, ⋆⋆⋆ ↛]

Change the definition of the eval function in the arith implementation to the big-step style introduced in Exercise 3.5.17.

^[3]We write eval this way for the sake of simplicity, but putting a try handler in a recursive loop is not actually very good style in ML.

---