In this section we consider a syntactic endofunctor Σ with a freely gen-erated monad T, the behaviour functor BX = Pf(A×X), and a set R of GSOS rules with the corresponding natural transformation
λ: Σ(id×B)→BT
The purpose is to describe syntactic conditions on R that would ensure that λ lifts to a natural transformation
λ: Σ∗(id×BW)→BWT∗
where W ∈ {Tr,CTr,Fl}. As a consequence of Theorem 23, such syn-tactic conditions ensure that the respective operational preorders are precongruences.
Theorem 24. If R is in Tr-format (Format 2), then λ: Σ∗(Id×BTr)→BTrT∗ is a natural transformation inSet∗.
Proof. It is enough to ensure that given an object hX, τi inSet∗, λ: Σ∗(hX, τi ×BTrhX, τi)→BTrT∗hX, τi
is a morphism inSet∗; in other words, that for every test V ∈BT XTr TXτ, λ−1V is a test in ΣX×BX(τ 1BXTrτ).
To do this, it will be useful to understand the nature of tests in ΣXτ, TXτ and BT XTr TXτ, for a given hX, τi.
Definition 25. For a syntactic Σ, a set X and a test suite τ on X, a basic flat τ-check on ΣX is a term
γ ∈Στ
A termt∈ΣX passesa basic flat τ-check γ, ift can be obtained fromγ by replacing everyV ∈τ by somex∈V.
The set of terms passing a given basic flat τ-check γ is denoted υ(γ).
Sets of this kind will be calledbasic flat τ-tests on ΣX.
Lemma 26. For any Σ, hX, τi, tests from ΣXτ are exactly all unions of basic flat τ-tests on ΣX.
Proof. Take any test
V ∈ Mk
i=1
τ⊗ni
By definition, V = V1 +· · · +Vk, where Vi ∈ τ⊗ni. Then for every 1≤i≤k,
Vi =U1× · · · ×Uni where Uj ∈τ
(in the above, + and × denote disjoint union and cartesian product on sets). Note thatγ =ιihU1, . . . , Unii is a basic flat τ-check, and
ιi(Vi) =υ(γ)
whereιi :Xni → ΣX is the i-th coproduct injection into ΣX. Finally V =V1+V2· · ·+Vk=ι1(V1)∪ι2(V2)∪ · · · ∪ιk(Vk)
which completes the presentation ofV as a union of basic flatτ-tests.
Definition 27. For a setX and a test suiteτ onX, abasic termτ-check is a term
c∈T τ
A term t∈ T X passes a basic term τ-check c, if t can be obtained from cby replacing every V ∈τ by some x∈V.
The set of terms passing a given basic term τ-check c is denoted υ(c).
Sets of this kind will be calledbasic term τ-tests onT X.
Lemma 28. For any Σ, hX, τi, every test in TXτ is a union of basic term τ-tests on T X.
Proof. Recall from Corollary ?? that TXτ is the greatest fix point of the operator Ψ:
Ψτ0 = (ψ−1)∗(τ⊕ΣT Xτ0)
The proof proceeds by constructing for all n and for any test V ∈ Ψn(PT X), a family Γn(V) of basic term τ-checks fromTnτ such that
V ∩TnX = [
γ∈Γn(V)
υ(γ)
whereTnX denotes the set of Σ-terms of depth at most n.
Given this construction, for any testV ∈TXτ we have V = [
n∈N
[
γ∈Γn(V)
υ(γ) which will complete the proof.
The families Γn(V) are constructed by induction onn. For the base case, take Γ0(V) =∅ for any V. Indeed,
V ∩T0X =V ∩ ∅=[
γ∈∅
υ(γ)
For the induction step, take a test V ∈ Ψn(PT X). By definition, V = V0 +V00 (+ denotes disjoint union of sets), where V0 ∈ τ, and V00 ∈ ΣT XΨn−1(PT X). By Lemma 26, for some indexing set I
V00=[
i∈I
υ(δi)
where each δi is a basic flat Ψn−1(PT X)-check on ΣT X, i.e.
δi ∈Σ(Ψn−1(PT X))
By the inductive assumption, for every testU ∈Ψn−1(PT X) there exist a family Γn−1(U) of basic term τ-checks such that
U ∩Tn−1X= [
u∈Γn−1(U)
υ(u)
Now for anyδi as above, take δi0 =δi[σ], where σ(U) = [
u∈Γn−1(U)
υ(u)
is a substitution from Ψn−1(PT X) toPT X. Obviously, eachδ0i is a basic flat (PT X)-check and
υ(δi0) =υ(δi)∩ΣTn−1X ι2(υ(δi0)) =ι2(υ(δi))∩TnX whereι2 : ΣT X →T X is the coproduct inclusion.
Moreover, for anyδi as above, consider the family of basic termτ-checks:
Θ(δi) ={ι2(δi[σ0]) : σ0(U)∈Γn−1(U)} ⊆Tnτ
where ι2 : ΣTn−1τ → Tnτ is the coproduct inclusion, and σ0 ranges on substitutions from Ψn−1(PT X) to Tn−1τ.
From definition of υ, it is easy to see that [
γ∈Θ(δi)
υ(γ) =ι2(υ(δi0))
Now take
Γn(V) = {ι1(V0)} ∪[
i∈I
Θ(γi) and check that
V ∩TnX = (V0+V00)∩TnX
= (ι1(V0)∪ι2(V00))∩TnX
= (ι1(V0)∩TnX)∪(ι2(V00)∩TnX)
=ι1(V0)∪ [
i∈I
ι2(υ(δi))∩TnX
=υ(ι1(V0))∪ [
i∈I
ι2(υ(γi0))
=υ(ι1(V0))∪ [
i∈I
[
γ∈Θ(δi)
υ(γ)
This completes the induction step, and the proof of Lemma 28.
Definition 29. For a given hX, τi, a basic positive τ-checkon BX is an expression of the form a IV, where a∈ A and V ∈τ. A set β ∈BX passes such a check, if there is some ha, xi ∈ β such that x ∈ V. As usual, the test onBX associated to a basic positiveτ-check cis denoted υ(c) and is called a basic positive τ-test.
Similarly, for a given hX, τi, a basic positive term τ-checkonBT X is an expression of the form a Iγ, where a∈A and γ is a basic termτ-test on T X. The definition of passing and of the basic positive term τ-test υ( a Iγ) is as usual.
Lemma 30. A test in BT XTr TXτ is either the always true test BT X, or a union of basic positive term τ-tests.
Proof. If a test V ∈BT XTr TXτ is not equal to BT X, then V =whai◦BV0 ={β ∈BT X : ha, ti ∈β, t∈V0}
for some V0 ∈TXτ. But then, by Lemma 28, V0 is a union of basic term τ-tests:
V0 =[
i∈I
υ(γi) hence
V =[
i∈I
{β ∈BT X : ha, ti ∈β, t∈υ(γi)}=[
i∈I
υ( a Iγi)
We shall now prove Theorem 24. By Lemma 30, it is enough to show that for anyhX, τi, and for any given basic positive termτ-check a Iγ, there exists a family of basic flat (τ 1 BXTrτ)-checks δ1, δ2, . . . , δm such that
λ−1υ( a Iγ) = [m i=1
υ(δi)
To achieve this, fix a basic positive term τ-check a Iγ, and take any rule ρ∈R, which has the conclusion of the form
f(x1, . . .xn) a It
for some construct fwith arity n, and such that tcan be obtained from γ by replacing each V ∈τ with some x∈Ξ. Since no variable occurs in
t more than once, this gives a function σ : Ξ → τ such that γ = t[σ].
Without loss of generality, assume that σ(x) =X if x does not occur in t.
Now for each 1≤i≤n take a test Vi ∈τ 1BXτ as follows:
• Ifxi does not occur in any premise ofρ, then takeVi =σ(xi)×BX.
• Ifxioccurs in a premisexi bi Iyi, then takeVi =X×υ( bi Iσ(yi)) Note that the syntactic restrictions of theTr-format ensure that the above definition is complete and unambiguous.
Having defined the testsVi, consider a basic flat τ 1BXτ-check δρ=fhV1, . . . , Vni
We will show thatυ(δρ) =ρ−1X υ( a Iγ). To this end, take any r =fhhx1, β1i, . . . ,hxn, βnii ∈Σ(X×BX) and check that the following are equivalent:
r passes δρ
⇐⇒ hxi, βii ∈Vi for all 1≤i≤n
⇐⇒ For each 1 ≤ i ≤ n, either xi does not occur in any premise and xi ∈σ(xi), or xi occurs in a premise xi bi Iyi and hbi, yii ∈βi for someyi ∈σ(yi)
⇐⇒ θ mapping each xi to xi, and yi to yi satisfies the conditions de-scribed in the proof of Theorem 9. Moreover, θ(x) ∈ σ(x) for all x∈Ξ.
⇐⇒ ha,t[θ]i ∈ρXr, andt[θ] passes γ.
⇐⇒ ρXr passes a Iγ.
This shows thatυ(δρ) = ρ−1X υ( a Iγ).
Now by definition ofλ from the family ofρX for ρ∈R, λ−1(υ( a Iγ)) =[
ρ
υ(ρX)
where the summation is made over all rules ρ with the conclusion as described above.
This completes the proof of Theorem 24.
Theorem 31. If R is in CTr-format, then
λ: Σ∗(Id×BCTr)→BCTrT∗ is a natural transformation inSet∗.
Proof. As before, we show that for anyhX, τi, for every test V ∈BT XCTrTX
there is a test V0 ∈ΣX(τ 1BXCTrτ) such that λ−1V =V0.
Definition 32. For a set of labelsQ⊆A, theQ-failure checkis denoted
Q6 I. Instead of A6 I, we will sometimes write 6 I. For any set X, a set β ∈BX passesthe Q-failure check if
β∩ { ha, ti : a∈Q}=∅
For any X, the test on BX associated to the Q-failure check will be denoted υ(Q6 I), and will be called the Q-failure test.
Lemma 33. A test V ∈BT XCTrTX is either the always true test BT X, or the A-failure test υ( 6 I), or a union of basic positive term τ-tests.
Proof. If a test V ∈ BT XCTrTXτ is not equal to BT X, then either V = whai◦BV0 for some V0 ∈TXτ, or V =wrA◦BV0 for someV0 ∈TXτ. In the former case, V is a union of basic positive term τ-tests, as shown in Lemma 30. In the latter case,
wrA◦BV0 ={∅}=υ( 6 I)
To prove Theorem 31, it is enough to consider single basic positive term τ-tests onBT X, and the A-failure test on BT X. For the positive tests, we proceed as in the proof of Theorem 24, except that when constructing the tests Vi we consider one additional case:
• Ifxi occurs inρ in a negative premise xi a6 I(and hence, it occurs in a premise xi b6 Ifor any b∈A), then take Vi =X×υ( 6 I).
The syntactic restrictions ofCTr-format ensure that the definition ofVi’s extended this way is complete and unambiguous.
The rest of the argument remains as in the case of Tr-format.
For the A-failure test υ( 6 I) on BT X, for any language construct f(x1, . . . ,xn) take a sequence of CTr-testing sets P1, . . . , Pkm that satisfy the condition described in the definition ofCTr-format. For each Pi and each variable xj, define a testVij ∈τ 1BXCTrτ as follows:
• If, for some a ∈ A, both xj a I and xj a6 I belong to Pi, then takeVij =∅.
• If, for all a ∈ A, xj a I ∈ Pi, and if for all b ∈ A, xj b6 I 6∈ Pi, then takeVij =X×υ( 6 I).
• If, for alla ∈A, xj a I 6∈ Pi, and if for some b∈A, xj b6 I∈Pi, then takeVij =X×υ( b IX).
Note that the definition of aCTr-testing set ensures that the above defi-nition is complete and unambiguous.
Now for anyPi consider the basic flatτ 1BXCTrτ-check δfi =fhVi1, . . . , Vini
Recall the definition of the functionfX in the proof of Theorem 9. We will now show that
kf
[
i=1
υ(dfi) =fX−1υ( 6 I) To this end, consider anyr ∈Σ(X×BS) of the form
r=ιmhhx1, β1i, . . . ,hxn, βnii
and assume thatfXr doesnotpass 6 I, i.e., thatfXr6=∅. This means that there exists a ruleρ∈Rwith sourcef(x1, . . . ,xn), and a substitution σ: Ξ→X such that
σxi =xi
∀i≤n∀j ≤mi.haij, σ(yij)i ∈βi
∀i≤n∀j ≤ni∀x∈X.hbij, xi 6∈βi wheremi, ni, aij, bij,yij are taken from ρ.
By the first part of condition 2 of CTr-format, there exists a sequence p1, . . . , pkf such that pi ∈ Pi and each pi is completed by some premise of ρ. Take any 1 ≤ i ≤ kf. In ρ there is a premise that completes pi. If pi is a positive semiliteral xj c I (for some xj, c), then βj 6= ∅, hencehxj, βji 6∈Vij and r does not pass dfi. Similarly, if pi is a negative semiliteral xj c6 I, then βj = ∅ and again hxj, βji 6∈ Vij and r does not pass dfi.
Conversely, assume that r does not pass dfi for any 1 ≤ i ≤ kf. This means that for each i, there is a j such that hxj, βji 6∈ Vij. For each 1≤i≤kf, take pi to be any element of Pi that has the respectivexj on the left-hand side. By the second part of condition 2 ofCTr-format, there exists a ruleρ∈R with sourcef(x1, . . . ,xn), such that each premise ofρ completes somepi. This means that there exists a substitutionσ : Ξ→X satisfying all the conditions mentioned above, hence fXr 6= ∅ and fXr does not pass 6 I.
From this, by definition ofλ as in the proof of Theorem 9, [
f∈Σ kf
[
i=1
υ(dfi) =λ−1υ( 6 I) This completes the proof of Theorem 31.
Theorem 34. If R is in Fl-format, then
λ : Σ∗(Id×BFl)→BFlT∗ is a natural transformation inSet∗.
Proof. As before, we show that for anyhX, τi, for every testV ∈BT XFl TX there is a test V0 ∈ΣX(τ 1BXFlτ) such that λ−1V =V0.
As before, we begin with a characterisation of tests in BT XFl TX:
Lemma 35. A test V ∈BT XFl TX is either the always true test BT X, or the Q-failure test υ( 6 I) for some Q ⊆ A, or a union of basic positive term τ-tests.
Proof. As in the proof of Lemma 33.
The proof proceeds much the same as in Theorem 31. For the positive tests V, we proceed as in the proof of Theorem 24, except that when constructing the testsVi we consider one additional case:
• If xi occurs in ρ in some negative premises, then take Vi = X × υ(Q6iI), where Qi =
a∈A : xi a6 I is a premise in ρ .
Again, the syntactic restrictions of Fl-format ensure that the definition of Vi’s extended this way is complete and unambiguous.
The rest of the argument remains as in the case of Tr-format.
For the Q-failure test υ(Q6 I) for some Q ⊆ A, we proceed as in the proof of Theorem 31, except that we construct the tests Vij in a slightly different manner:
• If, for some a ∈ A, both xj a I and xj a6 I belong to Pi, then takeVij =∅.
• If for some a ∈A, xj a I ∈ Pi, and if for all b ∈ A, xj b6 I6∈ Pi, then takeVij =X×υ(Qj6 I), where Qj ={a∈A : xj a I ∈Pi}.
• If, for alla ∈A, xj a I 6∈ Pi, and if for some b∈A, xj b6 I∈Pi, then takeVij =X×υ( b IX).
(note that the first and the third case are as in the case ofCTr-format).
Note that the definition of aFl-testing set ensures that the above defini-tion is complete and unambiguous.
The rest of the argument remains the same as in the case ofCTr-format.