| < Free Open Study > |
|
|Si+1| = |Si|3 + |Si| × 3 + 3, and |S0| = 0. So |S3| = 59439.
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 Sj ⊆ Si, we must show that Si ⊆ Si+1-that is, for any term t Î Si, we must show t Î Si+1. So suppose we have t Î Si. By the definition of Si as the union of three sets, we know that t must have one of three forms:
t Î {true, false, 0}. In this case, we obviously have t Î Si+1, by the definition of Si+1.
t = succ t1, pred t1, or iszero t1, where t1 Î Sj. Since Sj ⊆ Si by the induction hypothesis, we have t1 Î Si, so t Î Si+1 by definition of Si+1.
t = if t1 then t2 else t3, where t1, t2, t3 Î Sj. Again, since Sj ⊆ Si by the induction hypothesis, we have t Î Si+1, by the definition of Si+1.
(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.
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.
(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:
| < Free Open Study > |
|