Appendix A: Solutions to Selected Exercises

---

3.2.4 Solution

|S_i+1| = |S_i|³ + |S_i| × 3 + 3, and |S₀| = 0. So |S₃| = 59439.

3.2.5 Solution

A straightforward inductive proof does the trick. When i = 0, there is nothing to prove. Next, supposing that i = j + 1, for some j ≥ 0, and that S_j ⊆ S_i, we must show that S_i ⊆ S_i+1-that is, for any term t Î S_i, we must show t Î S_i+1. So suppose we have t Î S_i. By the definition of S_i as the union of three sets, we know that t must have one of three forms:

1. t Î {true, false, 0}. In this case, we obviously have t Î S_i+1, by the definition of S_i+1.

2. t = succ t₁, pred t₁, or iszero t₁, where t₁ Î S_j. Since S_j ⊆ S_i by the induction hypothesis, we have t₁ Î S_i, so t Î S_i+1 by definition of S_i+1.

3. t = if t₁ then t₂ else t₃, where t₁, t₂, t₃ Î S_j. Again, since S_j ⊆ S_i by the induction hypothesis, we have t Î S_i+1, by the definition of S_i+1.

3.3.4 Solution

(We give the argument just for the depth-induction principle; the others are similar.) We are told that, for each term s, if P(r) for all r with smaller depth than s, then P(s); we must now prove that P(s) holds for all s. Define a new predicate Q on natural numbers as follows:

•  

  Q(n)

  =

  "s with depth(s) = n.P(s)

Now use natural number induction (2.4.2) to prove that Q(n) holds for all n.

3.5.5 Solution

Suppose P is a predicate on derivations of evaluation statements.

• If, for each derivation D,

  • given P(C) for all immediate subderivations C

  • we can show P(D),

• then P(D) holds for all D.

3.5.10 Solution

3.5.13 Solution

(1) 3.5.4 and 3.5.11 fail. 3.5.7, 3.5.8, and 3.5.12 remain valid. (2) Now just 3.5.4 fails; the rest remain valid. The interesting fact in the second part is that, even though single-step evaluation becomes nondeterministic in the presence of this rule, the final results of multi-step evaluation are still deterministic: all roads lead to Rome. Indeed, a rigorous proof of this fact is not very hard, though it is not as trivial as before. The main observation is that the single-step evaluation relation has the so-called diamond property:

---