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.



1 Answer 1

  1. Uniqueness of normal forms definitely applies. This is still a theorem you have to prove, but if it doesn't hold, what you have isn't really a normal form. The whole point of normal forms is that there's a unique form for each value, that's what makes it "normal".

  2. For determinancy, I think it holds for most languages in the book. Usually when you're defining a small step semantics, you try to do it in such a way that it's deterministic. However, there are notable exceptions to this. First, if you have a general rewrite system, like the untyped lambda calculus, then it's totally valid to have non deterministic reductions. This is what lets us talk about Church Rosser and the diamond property. Secondly, if you have a language with any sort of concurrency, then you probably want to have non deterministic rules, to model the different possible orders of evaluation, so that you can show your language is well behaved regardless of which interleaving is taken.

That said, I want to be clear that these things do not come for free. They hold for the Languages in the book because Pierce has been very careful to ensure they hold. It is easy to accidentally definite a language where these do not hold.

  • $\begingroup$ Thanks. The proof of Uniqueness theorem is "Proof: Corollary of the determinacy of single-step evaluation (3.5.4)." 3.5.4 is determinancy theorem. So is it possible for a language to have uniqueness without one step determinancy? $\endgroup$
    – Tim
    Sep 2, 2019 at 23:57
  • $\begingroup$ @Tim Yep, for example, in a strongly normalizing calculus. You can perform the reductions in any order, but you'll always get the same result. $\endgroup$ Sep 3, 2019 at 0:02
  • $\begingroup$ Do you mean the proof of uniqueness relies on a unnecessarily strong assumption? $\endgroup$
    – Tim
    Sep 3, 2019 at 0:04
  • $\begingroup$ @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. $\endgroup$ Sep 3, 2019 at 0:06
  • $\begingroup$ Thanks. As to concurrency (and maybe parallelism), Pierce's book doesn't seem to cover it. Do you have some recommendations for books that have chapters/sections or entire book for the topics (e.g. Actor model, CSP, STM, ...)? (Pierce's book is about theory, but actually relatable to real world programming languages, and accessible when I just try to read the concepts and conclusions.) $\endgroup$
    – Tim
    Sep 3, 2019 at 0:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.