A.1 Lemma Diamond Property

---

A.1 Lemma [Diamond Property]

If r → s and r → t, with s ≠ t, then there is some term u such that s → u and t → u.

Proof: From the evaluation rules, it is clear that this situation can arise only when r has the form if r₁ then r₂ else r₃. We proceed by induction on the pair of derivations used to derive r → s and r → t, with a case analysis on the final rules in both derivations.

Case i:

Suppose r → s by E-IF TRUE and r → t by E-FUNNY2. Then, from the forms of these rules, we know that s = r₂ and that , where . But then choosing gives us what we need, since we know that and we can see that by E-IFTRUE.

Case ii:

Suppose the final rule in the derivations of both r → s and r → t is E-IF. By the form of E-IF, we know s must have the form and t must have the form , where and . But then, by the induction hypothesis, there is some term with and . We can complete the argument for this case by taking and observing that s → u and t → u by E-IF.

The arguments for the other cases are similar.

The proof of uniqueness of results now follows by a straightforward "diagram chase." Suppose that r →* s and r →* t.

Then we can use Lemma A.1 to "pull together" s₁ and t₁

then use it to pull together s₂ and u₂ and again to pull together u₂ and t₂

and so on until we have pulled together s and t, building a complete large diamond out of individual single-step diamonds.

It follows that, if r can be evaluated to v and to w, then they must be the same (they are both normal forms, so the only way they can evaluate to the same thing is to start out the same).

3.5.14 Solution

By induction on the structure of t.

Case: t is a value

Since every value is in normal form, this case cannot occur.

Case:

t = succ t₁

Looking at the evaluation rules, we find that only the rule E-SUCC could possibly be used to derive t → t′ and t → t″ (all the other rules have left-hand sides whose outermost constructor is something other than succ). So there must be two subderivations with conclusions of the form and . By the induction hypothesis (which applies because t₁ is a subterm of t), we obtain . But then , as required.

Case:

t = pred t₁

Here there are three evaluation rules (E-PRED, E-PREDZERO, and E-PREDSUCC) that might have been used to reduce t to t′ and t″. Notice, however, that these rules do not overlap: if t matches the left-hand side of one rule, then it definitely does not match the left-hand side of the others. (For example, if t matches E-PRED, then t₁ is definitely not a value, in particular not 0 or succ v.) This tells us that the same rule must have been used to derive t → t′ and t → t″. If that rule was E-PRED, then we use the induction hypothesis as in the previous case. If it was E-PREDZERO or E-PREDSUCC, then the result is immediate.

Case: Other cases

Similar.

3.5.16 Solution

Let us use the metavariable t to range over the new set of terms extended with wrong (including all terms with wrong as a subphrase), and g to range over the original set of "good" terms that do not involve wrong. Write for the new evaluation relation augmented with wrong transitions, and for the original form of evaluation. Now, the claim that the two treatments agree can be formulated precisely as follows: any (original) term whose evaluation gets stuck in the original semantics will evaluate to wrong in the new semantics, and vice versa. Formally:

---