Types and Programming Languages

A.5 Lemma

If in the augmented semantics and t contains wrong as a subterm, then g is stuck in the original semantics.

Proof: Straightforward induction on (augmented) evaluation derivations.

Combining this with Lemma A.3 yields the "if" (Þ) half of Proposition A.2, and we are finished.

3.5.17 Solution

We prove the two directions of the "iff" separately, in Propositions A.7 and A.9. In each case, we begin with a technical lemma establishing some useful properties of multi-(small-)step evaluation.