# Do determinacy of one-step evaluation and uniqueness of normal forms apply to all (or most) languages in TAPL?

In Types and Programming Languages by Pierce, when talking about untyped arithmetic expressions in Chapter 3, there are two theorems:

$$-→$$ is single-step evaluation relation:

3.5.4 Theorem [Determinacy of one-step evaluation]: If $$t -→ t'$$ and $$t -→ t''$$ , then $$t' = t''$$ .

$$-→ ∗$$ is multi-step evaluation relation:

3.5.11 Theorem [Uniqueness of normal forms]: If $$t -→ ∗ u$$ and $$t -→ ∗ u'$$ , where $$u$$ and $$u'$$ are both normal forms, then $$u = u'$$.

Do the two theorems also apply to all (or most) the other languages/systems in the book, or only to the untyped arithmetic expressions?

From my limited experiences in a few programming languages, it seems that an expression is always evaluated in exactly one deterministic process, so I wonder if both theorems apply to all the languages.

Thanks.

• @Tim no, I mean that Pierce uses Determiniancy to prove normal forms, but they're not inherently tied together. There are languages with unique normal forms, but without a deterministic semantics. Strongly normalizing languages, like System F, are examples of such languages, if you define your semantics as allowing arbitrary $\beta$-reductions. – jmite Sep 3 '19 at 0:06