Types and Programming Languages
|
| < Free Open Study > |
|
A.3 Lemma
The augmented evaluation relation is deterministic.
This means that whenever g can take a single step to g′ in the original semantics, it can also step to g′ in the augmented semantics, and furthermore that g′ is the only term g can step to in the new semantics.
Next, we show that a term that is (already) stuck in the original semantics will always evaluate to wrong in the augmented semantics.
|
| < Free Open Study > |
|