Corollary 4.5.5 Supposei ∗ r1 : G1 ⇒cN n1 1 G1 andi ∗ r2 : G2 ⇒cN n2 2 G2, i ≥ 1.Then
i ∗ r1+r2 :G1+G2 ⇒(cN1(n+c1+n2) 2) G1+G2
✷ Proof: By lemma 4.5.4, we have
i ∗ r1+idG2 : G1+G2 ⇒cN n1 1 G1+G2, i ∗ idG1+r2 : G1+G2 ⇒cN n2 2 G1+G2 By fact 4.1.15, we have (r1+idG2)+(idG1+r2) = r1+r2 – hence the claim. ✷
4.6 Correctness and speedup bounds
In this section we will investigate the relationship between the various levels present in a multilevel system.In particular, we will
1.give bounds for the speedup one can expect to gain when working at level i instead of level 1;
2.give conditions for a multilevel system to be “correct”, in the sense that “working at level i gives the same result as working at level 1”
– the nontrivial point is to ensure that working at level i does not increase the risk of nontermination.
First some notation:
• for i ≥ 1, define Ci as the maximum of the c’s such that there exists a rule ( : ⇒cN ) ∈ Ri – however, if this maximum is 0 we stipulate Ci = 1.Since we required eachRi to be finite, Ci < ∞.As rules represent shortcuts in the computation process, the intuition is that Ci is “the maximal shortcut represented by a level i rule”.
• for i ≥ 1, define Ti as follows: Let {(rj, Gj, Gj, cj, nj)|j ∈ J} be such that (r : G ⇒cN n G) ∈ Ri iff there exists j ∈ J with r = rj, G =Gj, G = Gj, c = cj and n =nj.Then we stipulate
Ti =
j∈J cj + 1
(the “+1” is added for technical reasons and will often be dispensed with in examples.) One should think of Ti as denoting “the total cost of deriving the level i rules”, as intuitively the cost of deriving a rule is proportional to the shortcut it represents.
• for i ≥ 1, we define T Ti =
i j=1
Tj
to be interpreted as the total cost of deriving the rules at level ≤ i.
Next we are – hardly surprising! – able to show that “level i can simulate level i+ 1”:
Lemma 4.6.1 Suppose i + 1 ∗ r : G ⇒cN n G, i ≥ 1.Then there exists c ≤ Ci ·c, n ≥ n such that i ∗ r : G ⇒cN n G. ✷ Proof: We will use induction in the proof tree fori + 1 ∗ r :G ⇒cN n G. Three cases:
• A rule at level i < i+ 1 has been exploited, then c = 1.Two cases:
– i < i.Then we also have i ∗ r : G ⇒cN n G, and as Ci ≥ 1 we have c ≤ Cic.
– i = i (so i = 0).Then there exists (r1 : G1 ⇒cN n1 1 G1) ∈ Ri, G2 and specialization s from G1+G2 to G, such that (G, r, ) is the pushout of (r1+idG2, s).Moreover n1 = n.
By assumption, we have i ∗ r1 : G1 ⇒cN n1 G1. By lemma 4.5.4, we have
i ∗ r1+idG2 : G1+G2 ⇒cN n1 G1+G2
and by lemma 4.5.2 we then find that there exists n ≥n such that
i ∗ r : G ⇒cN n1 G
As c1 ≤ Ci by definition, we finally obtain c1 ≤ Cic as desired.
• We have G = G, r = idG and c = n = 0.But then clearly i ∗ r : G ⇒0N0 G – and 0 ≤ Ci0, 0 ≥ 0.
• We havei + 1 ∗ r1 : G ⇒cN n1 1 G, i + 1 ∗ r2 : G ⇒cN n2 2 G withr = r1+r2, c = c1 + c2 and n = n1 + n2.By induction, there exists c1 ≤ Cic1, c2 ≤ Cic2, n1 ≥ n1 and n2 ≥ n2 such that
i ∗ r1 : G ⇒cN n1 1 G, i ∗ r2 : G ⇒cN n2 2 G
By defining c = c1 +c2, n = n1 + n2 we thus as desired obtain i ∗ r : G ⇒cN n G.And
c ≤ Ci(c1) +Ci(c2) = Cic, n ≥ n1 +n2 = n
✷ By repeated application of lemma 4.6.1, we find
Corollary 4.6.2 Suppose i ∗ r : G ⇒cN ni i G, i > 1.Then there exists c1,n1 such that
1 ∗ r : G⇒cN n1 1 G.
where c1 ≤ C1. . .Ci−1ci, n1 ≥ ni. ✷
The partial correctness/speedup theorem(s)
We are now ready for a main theorem, which can be read as follows:
suppose G at level i by an arbitrary strategy reduces to a normal form.
Then G at level 1 by a normal order strategy will reduce to an equivalent normal form; and the cost of working at level 1 does not exceed the cost of working at level i by more than a factor C1. . .Ci−1.
Theorem 4.6.3 Let G be singlelabeled with result node n0.Suppose for i > 1 we have
i ∗ r : G ⇒cN ni i G, G in well-typed normal form.
Then there exists r, G and c1 such that 1 ∗ r : G ⇒cN c1 1 G where
• G is in well-typed normal form, and ValG(r(n0)) = ValG(r(n0));
• ni ≤c1 ≤ C1. . .Ci−1 ·ci.
✷
Proof: By corollary 4.6.2 we find that 1 ∗ r : G ⇒cN n G where c ≤ C1. . .Ci−1ci, n ≥ni. By theorem 4.4.14, there exists G in well-typed nor-mal form, reductionr andc1 withn ≤ c1 ≤ c such that 1 ∗ r : G ⇒cN c1 1 G. That ValG(r(n0)) = ValG(r(n0)) follows from theorem 4.4.11. ✷ Theorem 4.6.3 is formulated relative to a fixed multilevel system (i.e. a fixed set of rules): working within this multilevel system one can gain a constant factor only.But given a graph G such that 1 ∗ r : G ⇒cN n G with G in normal form it will of course always be possible to construct a multilevel system (even a 2-level system) such that 2 ∗ r : G ⇒1N n G – just store the above level 1 transition as a level 1-rule! However, by doing so we have just transferred the cost from “run time” to “rule generation time”.
This motivates why we now formulate a speedup bound which does not depend on the actual multilevel system (only on the number of levels employed), and which takes “rule generation time” into account:
Theorem 4.6.4 In theorem 4.6.3, we have T T i−1 +ci ≥ i√i
c1
✷ Here the left hand side can be interpreted10 as the total cost associated with working at level i, and c1 can be interpreted as the total cost associ-ated with working at level 1 – thus there is justification for the following Essential Result 4.6.5 By having an upper bound on the number of levels employed in a multilevel system, one at most gains a polynomial speedup.
Proof: (of theorem 4.6.4) We have c1 ≤ C1. . .Ci−1ci, and hence (as Ci ≤ Ti)
i·√i
c1 ≤ i·iC1. . .Ci−1ci ≤ i·iT1. . .Ti−1ci Thus the theorem will follow if we can show
i·iT1. . .Ti−1ci ≤ T T i−1 +ci
which amounts to showing
iiT1. . .Ti−1ci ≤(T1 +. . .+Ti−1 +ci)i
10Wlog.we can assume that a program is run once only, as if it is to be run on several arguments these can be supplied simultaneously.
But this is an instance of the inequality
ii(n1. . . ni) ≤ (n1 +. . .+ni)i, all nj ≥0 (4.14) the validity of which follows from the two observations below:
• if n1 =. . . = ni(= n), then (4.14) reads ii ·ni ≤(i·n)i
which certainly holds (with = instead of ≤).
• for fixed value of n1+. . .+ni, n1. . . ni assumes its maximum value when n1 = . . . = ni.This is an easy consequence of the observation below, which trivially holds:
Given n,n and d, with 0 ≤ d ≤ n≤ n.Then n·n ≥ (n−d)·(n +d).
✷
4.6.1 Total correctness
Theorem 4.6.3 showed that working at higher levels always will be par-tially correct, in the sense that every result could have been achieved at level 1 too.Now we are aiming at conditions for total correctness, the meaning of this term being
1.if reduction of G at level i gets “stuck”, then it also gets stuck at level 1;
2.if reduction of G at level i “loops”, then it also loops at level 1.
Concerning 1, it is easily seen (by combining corollary 4.6.2 and theorem 4.4.14) that the following holds:
Corollary 4.6.6 If i ∗ : G ⇒N G, with G singlelabeled and with G in normal form but not in well-typed normal form, then there exists G in normal form but not in well-typed normal form such that (for some c)
1 ∗ : G ⇒cN c G. ✷
On the other hand, a configuration may be “stuck at level i” even if it does contain a redex a with D(a) ≥1 – this will happen if
• one is not allowed to use (all) level 0 rules, when working at level i and
• the set of rules one is allowed to use is not “complete”.
We do not wish to formulate conditions for a set of rules to be “complete”, as such a treatment will depend heavily on the concrete multilevel system – hence we from now on solely focus upon condition 2, i.e. that “looping at level i implies looping at level 1”.
The discussion back in section 2.1.2 suggests that “all rules should represent some computation step”, so obviously it would be a bad idea if we had (idG : G ⇒0N0 G) ∈ Ri for some i.However, it is not enough that all rules represent some computation step – they should also represent a useful computation step.In our formalism (which has been partly designed for this purpose!) this can be coded up in the theorem below which says “if one, when working at level i, only uses either level i rules (1 ≤ i < i) representing at least one normal order step or a level 0 rule the redex of which is needed; then total correctness is ensured”.
Theorem 4.6.7 Given i > 1.Assume we have the following (restricted) definition of when i r : G ⇒N n G holds: (G, r, ) shall be the pushout of (r1+idG2, s) where s is a specialization from G1+G2 to G, and where either
1.(r1 : G1 ⇒a1 G1) ∈ R0 with D(s(in1(a1))) ≥ 1 or 2.(r1 : G1 ⇒cN n1 1 G1) ∈ Ri for some i < i with n1 ≥1.
Now suppose that G0 (singlelabeled) is such that for all k ≥ 0 there exist Gk and nk such that
i ∗ : G0 ⇒kN nk Gk
i.e. “G0 loops at level i by some strategy”.Then G0 loops at level 1 by a
normal order strategy. ✷
Proof: Let k be given.It is immediate from the assumptions of the theorem that nk ≥ k. By corollary 4.6.2 we find that there exists nk ≥ nk(≥ k) such that
1 ∗ : G0 ⇒N nk Gk
Now apply theorem 4.4.16. ✷
It may not be quite obvious how the above theorem applies to concrete
multilevel systems. In section 4.7.2, examples will be given to clarify this issue.
Not surprisingly, the same assumptions guarantee that “we do not risk a slowdown by working at level i”:
Theorem 4.6.8 Let the assumptions about which transitions are made at level i be as in theorem 4.6.7. Now suppose (with G singlelabeled)
i ∗ : G ⇒cN n G, with G in normal form.
Then there exists G in normal form and c1 ≥ c such that 1 ∗ : G ⇒cN c1 1 G
✷ Proof: From the assumptions we find that n ≥ c.By corollary 4.6.2, we find that there exists n1 ≥ n such that 1 ∗ : G ⇒N n1 G. By theorem 4.4.14, we find G in normal form and c1 ≥ n1 such that
1 ∗ : G ⇒cN c1 1 G; hence the claim. ✷
The above theorem gives a sufficient condition for “the speedup factor being at least 1”.One may ask whether we in general can give condi-tions for “the speedup factor being at least k”.This does not seem quite easy – of course, a natural requirement would be that if one uses a rule ( : ⇒N n ) ∈ Ri, 1 ≤ i < i then n ≥k.However, excessive use of level 0 rules will make the speedup factor closer to 1 than to k – and we do not want to exclude the possibility of using level 0 rules, as target programs should be allowed to use operators like +!