Definition 5.6 We say that t is a fair level 1 unfolding step if t is of form Is(r1&. . .&rk), k≥1, where r1. . . rk are level 0 rules.
For a fair level 1 unfolding step t, we clearly have 1u t.
Definition 5.7 We say that B loops at level 1 by a fair strategy if for all n ≥1 there exists a fair level 1 unfolding step tn and a Bn not failure such 1u tn :Bn−1 →Bn (here B0 =B).
Similar to lemma 5.5, we may prove
Lemma 5.8 The following are sufficient conditions for B to loop at level 1 by a fair strategy:
1. For all N ≥ 0, there for all n with 1 ≤ n ≤ N exists a fair level 1 unfolding step tn and Bn not failure such that 1 u tn : Bn−1 → Bn
(again, B0 =B).
2. For all n ≥ 0, there exists Bn not failure and tn such that 1 u tn : B → Bn, where each working path in tn (viewed as a U-forest) has length ≥n and there exists a working path.
3. For all n ≥ 0, there exists Bn not failure and tn such that 1 u tn : B →Bn, where tn satisfies F(n).
LR strategy
Definition 5.9 We say that t is a LR level 1 unfolding step if t is of form Is(r&Id ) with r a level 0 rule.
We say thatt is aLRlevel 1 unfolding ift is of form t1' . . . ' tn with each ti being aLR level 1 unfolding step.
The U-forest corresponding to a LR level 1 unfolding is termed a LR U-forest.
Definition 5.10 We say that B loops at level 1 by a LR strategy if for all n ≥ 1 there exists a LR level 1 unfolding step tn and a Bn not failure such that 1 u tn :Bn−1 →Bn (here B0 =B).
Recall the functions E(m) and L(m) introduced in section 4.3.
Lemma 5.11 The following are sufficient conditions for B to loop at level 1 by a LR strategy:
1. For all N ≥ 0, there for all n with 1 ≤ n ≤ N exists a LR level 1 unfolding step tn and Bn not failure such that 1 Su tn : Bn−1 → Bn
(again, B0 =B).
2. For all n ≥ 0, there exists a transition tn and Bn not failure, with 1u tn :B →Bn, such thatE(tn)≥n.
3. For all n ≥ 0, there exists a transition tn and Bn not failure, with 1 u tn : B → Bn, such that the length of the leftmost working path
≥n.
4. For all n ≥ 0, there exists a transition tn and Bn not failure, with 1u tn :B →Bn, such thatL(tn)≥n.
Proof: First consider (1); then (2) ⇒ (1); then (3) ⇒ (1) and finally (4)
⇒ (3). ✷
5.4 Folding at level 1
We now define what it means for a transition t fromB to B to be a level 1 folding step, to be written 1Sf t:B →B.
We will assume the existence of a partial functions(G, i) such that Is(G,i)
(t(G, i)) is reversible, and such that Is(G,i)(c(G, i)) is failure for all i =i.
t(G, i)∈ RU0, s(G, i) defined
1Sf Is(Id CaH1&R(Is(G,i)(t(G, i)))&Id CaH2) (8) Next we define what it means for a transition t fromB toB to be a level 1 folding, to be written 1f t:B →B:
1Sf t:B →B
1f t:B →B (9)
1f IdB :B →B (10)
1f t:B →B,1f t :B →B
1f t ' t :B →B (11)
Fact 5.12
1. If 1Sf t, then 1Sf t&IdB and 1Sf IdB&t for basic configuration B. 2. If 1f t1 and 1f t2, then 1f t1&t2.
3. If 1Sf t (1f t), then 1Sf Is(t) (1f Is(t)) for specialization s.
4. If 1Sf t:B →B (or 1f t :B →B), then t is reversible.
5 . If 1Sf t: B →B then 1Su R(t) : B → B. If 1f t: B → B) then 1u R(t) :B →B.
Proof: Mostly as in the proof of fact 5.1. The last point follows from R(Is(Id CaH1&R(Is(G,i)(t(G, i)))&Id CaH2))
= Is(Id CaH1&Is(G,i)(t(G, i))&Id CaH2)
= Is(IId (Id CaH1)&Is(G,i)(t(G, i)&IId (IdCaH2))
= Is(IId &s(G,i)&Id (Id CaH1&t(G, i)&Id CaH2))
= Is(Id &s(G,i)&Id )(Id CaH1&t(G, i)&Id CaH2)
✷
5.5 Unfold/fold at level 1
We now define what it means for a transition t fromB to B to be a level 1 transition, to be written 1t:B →B.
1Su B →B
1t :B →B (12)
1Sf t:B →B
1t :B →B (13)
1IdB :B →B (14) 1t :B →B,1t :B →B
1t ' t :B →B (15)
Fact 5.13
1. If 1t1 and 1t2, then 1t1&t2.
2. If 1t, then 1 Is(t) for specializations.
5.6 Fundamental properties of level 1 transitions
The switching lemma
Lemma 5.14 Suppose 1 Sf t1 : B1 → B, 1 Su t2 : B → B2, with B2
not failure. Then one of two holds:
• B1 =B2, t1' t2 =IdB1
• There exists B, t1, t2 with 1 Su t1 :B1 → B, 1 Sf t2 : B → B2 such that
t1' t2 =t1' t2
Proof: This lemma, as well as its proof, is very similar to lemma 5.2.
We can assume that the transitions involved are of the following form:
t1 = Is1(Id CaH11&R(Is(G1,i1)(t(G1, i1)))&Id CaH12) t2 = Is2(Id CaH21&t(G2, i2)&Id CaH22)
With s = s1 ' (Id &s(G1, i1)&Id ), we from the fact that t1 is a transi-tion to B and t2 is a transition from B get
Is(CaH
11&G1&H12) =B =Is2(CaH
21&G2&H22)
From this we infer H11&G1&H12 = H21&G2&H22 and that s = s2. Now two posse bilities:
• H11=H21. ThenG1 =G2, and H12 =H22. Again two possibilities:
– i1 =i2. Then we have
B2 =Is1(CaH21&Is(G1,i1)(c(G1, i2))&CaH22) butIs(G1,i1)(c(G1, i2)) is failure by the definition of s(G, i), hence B2 is failure contra-dicting our assumption.
– i1 =i2. Then it is obvious that B1 =B2. And
t1' t2 = Is(Id CaH11&(R(t(G1, i1))' t(G1, i1))&Id CaH12)
= Is(Id CaH11&Idc(G1,i1)&Id CaH12)
= IdIs(CaH11&c(G1, i1)&CaH12) =IdB1
where we have used fact 4.30,(4).
• H11 =H21. We can wlog. assume that H11 is shorter than H21. Then there exists H such that H12=H&G2&H22, H21=H11&G1&H. Now define
t1 = Is(Id CaH11&Idc(G1,i1&Id CaH&t(G2, i2)&Id CaH22)
t2 = Is1(Id CaH11&R(Is(G1,i1)(t(G1, i1)))&Id CaH&Idc(G2,i2)&Id CaH22) We can easily calculate
t1' t2
= Is1(Id CaH11&R(Is(G1,i1)(t(G1, i1)))&Id CaH&t(G1, i1)&Id CaH22)
= t1' t2
To show that 1 Su t1, notice that we can write c(G1, i1) on the form Is(CaH) for some s, H. To show that 1Sf t2, apply the same obser-vation to c(G2, i2).
✷
The normalization lemma
Lemma 5.15Suppose 1t :B →B, withB not failure. Then there exists B, t1 and t2 such that 1u t1 :B →B, 1f t2 :B →B, t1' t2 =t.
From transitions being non-increasing we conclude thatB is not failure, and from t1, t2 and t1' t2 trivially being =⊥ we conclude t =⊥.
Proof: There exists t1, . . . , tn such that t = t1 '· · · ' tn and such that for each i ∈ {1. . . n} either 1 Su ti or 1 Sf ti. We will use induction in
the number of times an application of the fold-rule precedes (not necessarily immediately) an application of the unfold-rule. If this number is zero, we are through. Otherwise there exists i, 1 ≤ i ≤ n, such that 1 Sf ti, 1 Su ti+1. Now apply lemma 5.14. Two possibilities:
• ti' ti+1 =Id . Then
t=t1 '· · ·' ti−1' ti+2'· · ·' tn
with a strictly smaller number of “inversions”.
• There exists ti, ti+1 such that ti' ti+1 =ti' ti+1, and such that 1Su ti, 1Su ti+1. Now
t =t1 '· · ·' ti−1' ti' ti+1' ti+2'· · ·' tn
and again the number of inversions has decreased.
✷
5.7 Unfolding at level 2
Now assume that we have defined RU1, a finite set of rules at level 1, such that t ∈ RU1 implies that 1t.
We now define what it means for a transition t fromB toB to be a level 2 unfolding step, to be written 2S t:B →B:
t ∈ RU1
2S Is(Id CaH1&t&Id CaH2) (16) Next we define what it means for a transition t fromB toB to be a level 2 unfolding, to be written 2t: B →B:
2S t:B →B
2t :B →B (17)
2IdB :B →B (18)
2t :B →B,2t :B →B
2t ' t :B →B (19)
Fact 5.16 Suppose 2S t or 2t. Then 1t.
Proof: For 2 S t, exploit e.g. fact 5.13. For 2 t, a straight forward
induction in the derivation tree. ✷
Definition 5.17 We say that B loops at level 2 by some strategy if for all n ≥ 1 there exists a tn and a Bn not failure such that 2S tn :Bn−1 →Bn
(here B0 =B).
Definition 5.18We say thattis afair level 2 stepiftis of formIs(r1&· · ·&rk), k ≥1, where r1. . . rk are level 1 rules.
For a fair level 2 stept, we clearly have 2t.
Definition 5.19 We say that B loops at level 2 by a fair strategy if for all n ≥ 1 there exists a fair level 2 step tn and a Bn not failure such that 2tn :Bn−1 →Bn (here B0 =B).
Definition 5.20 We say thatt is a LRlevel 2 step if t is of formIs(r&Id ) with r a level 1 rule.
Definition 5.21 We say that B loops at level 2 by a LR strategy if for all n ≥ 1 there exists a LR level 2 step tn and a Bn not failure such that 2S tn :Bn−1 →Bn (here B0 =B).