BRICS
Basic Research in Computer Science
On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt
Luca Aceto
Silvio Capobianco Anna Ing´olfsd´ottir
BRICS Report Series RS-07-5
BRICSRS-07-5Acetoetal.:OntheExistenceofaFiniteBaseforCompleteTraceEquivalenceoverBPAwith
Copyright c2007, Luca Aceto & Silvio Capobianco & Anna Ing´olfsd´ottir.
BRICS, Department of Computer Science University of Aarhus. All rights reserved.
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.
See back inner page for a list of recent BRICS Report Series publications.
Copies may be obtained by contacting:
BRICS
Department of Computer Science University of Aarhus
IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark
Telephone: +45 8942 9300 Telefax: +45 8942 5601 Internet: BRICS@brics.dk
BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:
http://www.brics.dk ftp://ftp.brics.dk
This document in subdirectoryRS/07/5/
On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt
Luca Aceto Silvio Capobianco Anna Ing´olfsd´ottir
Department of Computer Science, Reykjav´ık University, Kringlan 1, IS-103, Reykjav´ık, Iceland
Email: luca@ru.is,silvio@ru.is,annai@ru.is∗
Abstract
We study Basic Process Algebra with interrupt modulo complete trace equivalence. We show that, unlike in the setting of the more demanding bisimilarity, a ground complete finite axiomatization exists. We explicitly give such an axiomatization, and extend it to a finite complete one in the special case when a single action is present.
Introduction
Mode switching is a desirable feature of programming and verification languages (see [7, 9, 11, 12, 14]). Actually, interrupts in operating systems and exception handling in virtual machines fall under this category, and similar behaviour is ex- plicitly required for control programs and embedded systems.
From the theoretical viewpoint of process algebra, representation of mode switching translates into the isolation of suitable operators on terms. Baeten and Bergstra [6] (reprising Bergstra [9]) discuss some of these operators for Basic Pro- cess Algebra (BPA), enriched with thedeadlock constant δ(a special process, not doing anything) and theinterrupt and disrupt operators. For that language, they construct a complete axiomatization modulo bisimilarity [13, 17], which is finite if the set of actions is finite. However, that axiomatization is based on the use of four moreauxiliary operators: hence, it is not immediately clear whether this process algebra, modulo bisimilarity, is finitely axiomatizableby itself. This fact is not at
∗The work of the authors has been partially supported by the project “The Equational Logic of Parallel Processes” (nr. 060013021) of The Icelandic Research Fund.
all immediate, given the many examples [1, 2, 3, 4, 5, 13, 15, 16, 18] where a finite complete axiomatization does not exist.
In this paper, we deal with the process algebra BPAint, obtained from BPA by adding the interrupt operator and, as for the relation modeling “indistinguishability from an external observer”, we choose to work withcomplete trace equivalence (briefly, c.t.e.) instead of the more demanding bisimilarity. Basically, a sequence of actions is a complete trace for a closed term, if it “leads the term to termination”;
two terms are c.t.e. if they have exactly the same complete traces.
Since equivalence classes of terms modulo complete trace equivalence can be described in the language ofregular expressions, it is possible to deal with them via language-theoretical techniques. This is precisely the way we find the first of our main results: interrupt is a derived operator for closed terms, modulo c.t.e; that is, for every closed termtover BPAint, there is a termuover BPA which is c.t.e. to t. Suchucan be obtained fromtvia application of instances of a finite number of axioms. Therefore, since BPA has a finite ground complete axiomatization modulo c.t.e. (as will be shown in the paper), BPAintturns out to have one as well. This theorem is in sharp contrast with the negative result proved in [5], to the effect that bisimilarity has no finite axiomatization over closed BPAintterms even in the presence of a single action.
The technical analysis of c.t.e. becomes more complex when we consider terms including variables. In fact, as in the setting of bisimilarity [5], interrupt is not a derived BPA operator modulo complete trace equivalence. This rule has precisely one exception, modulo c.t.e.:when the set of actions is a singleton. In this special case, not only we are able to remove every occurrence of the interrupt operator, but we also can reduce each BPAintterm to a BPA term with a very special “shape”; and in fact, this “shape” is special enough to becharacterizing, i.e., two BPAintterms are c.t.e. if and only if they can be reduced to the same “specially shaped” term.
Again, this will be achieved syntactically by adding a finite number of axioms to the ones we had found earlier, which yields a finite complete axiomatization for BPAint modulo c.t.e. in the presence of a single action. When the set of actions is not a singleton, we have isolated a collection of valid equations. However, the details involved in (dis)proving the completeness of that set of equations have so far defeated us.
The paper is divided as follows. In Section 1 we sketch the framework we are working with. In Section 2 we prove our results for closed terms. In Section 3 we state and prove our result for general terms with a single action. In Section 4 we introduce some additional sound equations we have found, and give hints and suggestions for future research in the field.
1 Preliminaries
We begin by introducing the basic definitions and results on which the technical developments to follow are based. The interested reader is referred to [6, 10] for more information.
1.1 The Language BPAint
We assume a nonempty alphabetActof atomic actions, with typical elementsa, b. The language for processes we shall consider in this paper, henceforth referred to as BPAint, is obtained by adding the interrupt operator from [6] to Bergstra and Klop’s BPA [10]. This language is given by the following grammar:
t::=x|a|t·t|t+t|tt ,
wherexis a variable drawn from a countably infinite set Var and ais an action.
In the above grammar, we use the symbol for theinterrupt operator. We shall use the meta-variablest, u, vto range over process terms, and writeVar(t)for the collection of variables occurring in the termt. Thesize of a term is the number of operator symbols in it. A process term isclosed if it does not contain any variables.
As usual, we shall often writetuin lieu oft·u, and we assume that·binds stronger than both+and , while binds stronger than+. In this paper we will also consider the language BPA, which is constructed as BPAint without the interrupt operator.
A substitution is a mapping from process variables to BPAintterms. A substi- tutionσis closed ifσ(x)is a closed term for every variablex. For every termtand substitutionσ, the term obtained by replacing every occurrence of a variablexint with the termσ(x)will be writtenσ(t). Note thatσ(t)is closed, if so isσ. In what follows, we shall use the notationσ[x 7→ p], whereσ is a closed substitution and pis a closed BPAintterm, to stand for the substitution mappingxtop, and acting likeσon all of the other variables inVar. Ifa∈Act, we indicate byσathe closed substitution that replaces every variable witha, i.e.,
σa(x) =a ∀x∈Var . (1)
In the remainder of this paper, we let a1 denote a, andam+1 denote a(am). Moreover, we consider terms modulo associativity and commutativity of+. In other words, we do not distinguisht+uandu+t, nor(t+u)+vandt+(u+v). This is justified because+is associative and commutative with respect to the notion of equivalence we shall consider over BPAint. (See axioms A1, A2 in Table 2 on page 7.) In what follows, the symbol=will denote equality modulo associativity and commutativity of+.
We say that a termthas+as head operator ift =t1+t2 for some termst1
andt2. For example,a+bhas+as head operator, but(a+b)adoes not.
Fork≥1, we use asummationP
i∈{1,...,k}tito denotet1+· · ·+tk. It is easy to see that every BPAint term thas the form P
i∈Iti, for some finite, nonempty index setI, and termsti(i∈I) that do not have+as head operator. The termsti (i∈I) will be referred to as the(syntactic) summands oft. For example, the term (a+b)ahas only itself as (syntactic) summand.
The operational semantics for the language BPAintis given by the labeled tran- sition system
BPAint,na
→|a∈Act o,na
→X|a∈Act o ,
where the transition relations→a and the unary predicates →a Xare, respectively, the least subsets of BPAint ×BPAint and BPAint satisfying the rules in Table 1.
Intuitively, a transitiont→a umeans that the system represented by the term tcan perform the action a, thereby evolving into u. The special symbol Xstands for (successful) termination; therefore the interpretation of the statementt→Xa is that the process termtcan terminate by performinga. Note that, for every closed term p, there is some actionafor which eitherp→a p0holds for somep0, orp→Xa does.
a→Xa t→Xa
t+u→Xa
u→Xa t+u→Xa
t→a t0 t+u→a t0
u→a u0 t+u→a u0 t→Xa
t·u→a u
t→a t0 t·u→a t0·u t→Xa
tu→Xa
t→a t0 tu→a t0u
u→Xa tu→a t
u→a u0 tu→a u0·t
Table 1: Transition Rules for BPAint
The transition relations→a naturally compose to determine the possible effects that performing a sequence of actions may have on a BPAintterm.
Definition 1.1 For a sequence of actionsa1· · ·ak(k ≥0), and BPAinttermst, t0, we writeta1→···ak t0iff there exists a sequence of transitions
t=t0→a1 t1 → · · ·a2 →ak tk=t0 .
Similarly, we say thata1· · ·ak(k ≥ 1) is a complete trace of a BPAinttermtiff there exists a termt0such that
ta1−→···ak−1 t0→Xak .
Ifta−→1···akt0holds for some BPAinttermt0, ora1· · ·akis a complete trace oft, thena1· · ·akis atrace oft.
Thedepth of a termt, writtendepth(t), is the length of a longest trace it affords.
Observe that such a trace is necessarily a complete trace.
Thenorm of a termt, denoted bynorm(t), is the length of its shortest complete trace; this notion stems from [8].
The depth and the norm of closed terms can also be characterized inductively thus:
depth(a) = 1
depth(p+q) = max{depth(p),depth(q)}
depth(pq) = depth(p) +depth(q) depth(pq) = depth(p) +depth(q)
norm(a) = 1
norm(p+q) = min{norm(p),norm(q)}
norm(pq) = norm(p) +norm(q) norm(pq) = norm(p) .
Note that the depth and the norm of each closed BPAintterm are positive.
Lemma 1.1 [Operational Correspondence] Assume thattis a BPAintterm,σis a closed substitution andais an action. Then the following statements hold:
1. Ift→Xa , thenσ(t)→Xa . 2. Ift→a t0, thenσ(t)→a σ(t0).
3. Assume thattis a BPA term. Ifσ(t)→X, then eithera (a) t→Xa , or
(b) t=xandσ(x)→Xa for some variablex, or
(c) t=x+uandσ(x) →Xa for some variabletand termu.
Proof: Statements 1 and 2 are proved by induction on the proof of the relevant transitions. Statement 3 is proved by induction on the structure of the termt.
The details are lengthy, but straightforward, and we therefore omit them. 2
In this paper, we shall consider the language BPAintmodulo complete trace equiv- alence.
Definition 1.2 Two closed BPAint terms p and q are complete trace equivalent, denoted byp∼q, if they have the same complete traces, i.e., if for every nonempty wordw∈Act+,wis a complete trace forpiff it is a complete trace forq.
The relation∼will be referred to ascomplete trace equivalence.
It is evident that∼is an equivalence. There is more: ∼is acongruence with respect to all the operators in the signature of BPAint, that is, ift ∼ t0 andu ∼ u0, then t+u∼t0+u0,tu∼t0u0, andtu∼t0 u0. This will follow from Lemma 2.1, at the beginning of next section. Observe that complete trace equivalent BPAint
terms have the same norm and depth.
Complete trace equivalence is extended to arbitrary BPAintterms thus:
Definition 1.3 Lett, u be BPAint terms. Then t ∼ u iffσ(t) ∼ σ(u) for every closed substitutionσ.
For instance, we have that
xy∼(xy) +yx
because, as our readers can easily check, the termsp q and(p q) +qphave the same set of initial “capabilities”, i.e.,
pq→a riff(pq) +qp→a r , for eachaandr, and pq →Xa iff(pq) +qp→X,a for eacha .
It is natural to expect that the interrupt operator cannot be defined in the language BPA modulo complete trace equivalence. With a single, remarkable exception, this expectation will be confirmed by Proposition 3.1.
1.2 Equational Logic
Anaxiom system is a collection of equationst≈uover the language BPAint. An equationt≈uis derivable from an axiom systemE, notationE `t≈u, if it can be proved from the axioms inEusing the rules of equational logic (viz. reflexivity, symmetry, transitivity, substitution and closure under BPAintcontexts):
t≈t t≈u u≈t
t≈u u≈v t≈v
t≈u σ(t)≈σ(u) t≈u t0 ≈u0
t+t0 ≈u+u0
t≈u t0≈u0 tt0 ≈uu0
t≈u t0 ≈u0 tt0≈uu0 .
A1 x+y ≈ y+x A2 (x+y) +z ≈ x+ (y+z)
A3 x+x ≈ x
A4.1 (x+y)z ≈ (xz) + (yz) A4.2 x(y+z) ≈ (xy) + (xz)
A5 (xy)z ≈ x(yz)
Table 2: Some Axioms for BPAint
Definition 1.4 An equationt≈uover the language BPAintissound with respect to∼iff t ∼ u. An axiom system is sound with respect to∼iff so is each of its equations.
An example of a collection of equations over the language BPAintthat are sound with respect to∼is given in Table 2. Those equations stem from [10]. Equations dealing with the interrupt operator in the setting of bisimulation semantics using auxiliary operators are offered in [6].
2 A ground complete finite axiomatization for BPA
int We start by proving that complete trace equivalence is a congruence over BPAint. In fact, we give a complete, structural description of the complete traces of BPAintterms: congruence of complete trace equivalence will be an easy consequence.
First of all, we observe that, given two closed terms t, u over BPAint and a nonempty wordwoverAct, thenwis a complete trace fort+uiffwis a complete trace for either t oru, while w is a complete trace for tu iff w = xy for some wordsx, y that are complete traces for t and u, respectively. In fact, there is a similar characterization for complete traces oftu, but it’s a bit trickier.
Lemma 2.1 Lettandube closed terms over BPAint. Letwbe a nonempty word over the alphabetAct. Thenwis a complete trace fortuiff there exist wordsx, y,zoverActsuch that
1. w=xyz, 2. zis nonempty,
3. xzis a complete trace fort, and
4. yis either empty or a complete trace foru.
Proof: Supposetu→w X. Then
• eitherudoesnot initiate, so thatt→w X, or
• uinitiates beforet, so that u →y X, thent →z Xfor some nonempty words y,zsuch thatw=yz, or
• uinitiates whiletis running, so thatt→x t0for some closed termt0,u→y X, andt0 →z Xfor some nonempty wordsx,y,zsuch thatw=xyz.
The reverse implication is trivial. 2
Lemma 2.1 allows one to give a language-theoretic characterization of closed terms over BPAintmodulo complete trace equivalence. Call CT(t)the set of complete traces of closed termt: then Lemma 2.1 states that the equalities
CT(t+u) = CT(t)∪CT(u), (2)
CT(tu) = CT(t)CT(u), and (3)
CT(tu) = CT(t)∪ [
rs∈CT(t),s6=ε
{r}CT(u){s} (4)
hold. We recall thatXY ={w:∃x∈X, y∈Y :w=xy}.
Corollary 2.1 For terms over BPAint, complete trace equivalence is a congruence.
Proof: Supposet ∼ t0 and u ∼ u0. Let σ be a closed substitution: then σ(t) andσ(t0)have the same set of complete traces, and similarly forσ(u)andσ(u0). By (2),σ(t+u) = σ(t) +σ(u) has the same complete traces asσ(t0 +u0) = σ(t0) +σ(u0); similarly for σ(tu) and σ(t0u0) because of (3), and for σ(t u) and σ(t0 u0) because of (4). This is true for every closed substitution σ, thus t+u∼t0+u0,tu∼t0u0, andtu∼t0 u0. 2 As a consequence of Lemma 2.1 and our previous observations, we obtain the following equivalences.
Lemma 2.2 For every actionaand closed termst,u,vover BPAint, the following hold:
1. t+u∼u+t;
2. t+ (u+v)∼(t+u) +v;
3. t+t∼t;
4. (t+u)v∼tv+uv; 5. t(u+v)∼tu+tv;
6. (tu)v∼t(uv);
7. au∼a+ua;
8. atu∼a(tu) +uat;
9. (t+u)v∼(tv) + (uv); and 10. t(u+v)∼(tu) + (tv).
Proof: We must show that, for any of the formulas above and for any word w over Act, w is a complete trace for the left-hand side iff it is for the right-hand side. Thanks to equations (2), (3), and (4), this is basically an exercise in sentence rewriting; only the last four identities require a greater amount of caution.
7. Supposewis a complete trace fora u. By Lemma 2.1, this is the same as saying thatw = xyz so that zis nonempty, a →xz Xand eithery is empty or u →y X. The first part is possible iff xis empty and z = a, thus eitherw = a orw = ya with u →y X; by Lemma 2.1, this is the same as saying thatw is a complete trace fora+ua. On the other hand, ifa+ua →w X, then eitherw=a orw =yafor someysuch thatu →y X; in either case,wis a complete trace for auas well.
8. Supposew is a complete trace for at u. We can write w = xyzwith z nonempty, at →xz X, and either y empty or u →y X. Two cases are possible:
eitherx =ax0, orxis empty andz = az0. In the first caset x→0z X, and eithery empty oru→y X, so thatx0yzis a complete trace for tu, andw =ax0yz is a complete trace fora(tu); in the second case,w =yaz0 is a complete trace for uat. On the other hand, letwbe a complete trace fora(tu) +uat: then either a(tu) →w X, so thatw=axyz witht →xz Xand eitheryempty oru→y X; or w=yaxwithu→y Xandt→x X. In either case,atu→w X.
9. Supposewis a complete trace for(t+u) v. This is the same as saying thatw =xyz withznonempty, eithert →xz Xoru →xz X, and either yempty or v→y X. This means that eithertv→w Xoruv→w X.
10. Supposewis a complete trace fort(u+v). This is the same as saying thatw=xyzwithznonempty,t→xz X, and eitheryis empty oru→y Xorv→y X.
This means that eithertu→w Xortv →w X. 2
We can then state
Theorem 2.1 Letabe an action and letx,y,zbe variables. The following equa- tions are sound for BPAintmodulo complete trace equivalence:
A1 x+y ≈ y+x
A2 x+ (y+z) ≈ (x+y) +z
A3 x+x ≈ x
A4.1 (x+y)z ≈ xz+yz A4.2 x(y+z) ≈ xy+xz
A5 (xy)z ≈ x(yz)
I1.a ay ≈ a+ya
I2.a axy ≈ a(xy) +yax I3.1 (x+y)z ≈ (xz) + (yz) I3.2 x(y+z) ≈ (xy) + (xz)
Proof: Letσbe a closed substitution. Applyσto both sides of any of the equations above: then left-hand and right-hand members are complete trace equivalent by Lemma 2.2. This is true for all closed substitutions, which proves the theorem. 2 Observe that, for every action a, there is one equation of the form I1.a and one equation of the form I2.a, so that those equations are infinitely many if Act is infinite.
We now argue that the interrupt operator can be eliminated from closed terms.
To be able to support our thesis, we do a little digression, and try to find the “sim- plest possible form” a BPA term can have, modulo complete trace equivalence.
Definition 2.1 A termtover BPA is inprenex normal form if there exists a finite nonempty setW ⊆(Act∪Var)+such that
t= X
w∈W
w , (5)
where the wordα1. . . αnis identified with the termα1·. . .·αn.
In other words, a term is in prenex normal form if the nondeterministic choice operator only appears at the topmost level.
Lemma 2.3 Lettbe a term over BPA. There exists a termuover BPA in prenex normal form such thatt∼u. Moreover, iftis closed, thenuis closed as well.
Proof: By structural induction ont. The thesis is trivially true if either t=afor somea∈Act, ort=xfor somex∈Var.
Ift = t1 +t2 for some termst1,t2, consider u1, u2 in prenex normal form such thatt1 ∼u1andt2 ∼u2. Put
u= X
w∈W
w ,
whereW is the set of all words w that appear as summands in either u1 oru2. Observe thatucan be constructed fromu1+u2 by repeatedly applying the idem- potence ruleA3. It is immediate to check thatuis in prenex normal form, and that t ∼ u; moreover, iftis closed, then t1 andt2 are closed, so thatu1 andu2, and consequentlyu, are closed by inductive hypothesis.
Ift=t1t2 for some termst1,t2, consideru1,u2in prenex normal form such thatt1 ∼u1andt2 ∼u2. Put
u= X
w∈W
w ,
whereW is the set of all wordswsuch that w =w1w2 for two nonempty words w1,w2 such thatw1is a summand ofu1andw2 is a summand ofu2. Observe that ucan be constructed fromu1u2by repeatedly applying the associativity lawsA4.1 andA4.2, and the idempotence ruleA3. It is straightforward to check thatuis in prenex normal form, and thatt ∼ u; moreover, iftis closed, thent1 andt2 are closed, so thatu1 andu2, and consequentlyu, are closed by inductive hypothesis.
2
Lemma 2.3 states that, for every closed termtover BPA, there exists a closed term ν(t)over BPA in prenex normal form, such thatt∼ν(t). We callν(t)theprenex normal form of the termt. Observe thatν(t)is defined up to the order of its sum- mands. Observe also that, to constructufromtin the proof of Lemma 2.3, we have only applied associativity of operators, commutativity and idempotence of nonde- terministic choice, and distributivity of nondeterministic choice w.r.t. composition:
that is,ν(t)can be constructedsyntactically fromtby means of axioms in Table 2.
Introduction of prenex normal forms allows us to prove
Lemma 2.4 Lettandube closed terms over BPA. There exists a closed term v over BPA such thattu∼v.
Proof: By induction on the size oft. Because of Lemma 2.3, it is not restrictive to suppose thattis in prenex normal form.
Ifthas size 1, thent=afor some actiona. Thentu=au∼a+ua. Suppose now that the thesis is proved every time thatthas at most sizen. Let thave sizen+ 1. If t = t1+t2, thent u ∼ t1 u+t2 u, witht1 and
t2having size at mostn: by inductive hypothesis,t1 u ∼ v1and t2 u ∼ v2
for suitable closed termsv1,v2 over BPA, so that t u ∼ v1 +v2 = v withv closed term over BPA. Otherwisethas only one summand, so, since it is in prenex normal form, it must have the formt = at0 for some action aand closed term t0 having sizen: by inductive hypothesis,t0 u∼ v0 for some closed termv0 over BPA, so thattu=at0 u∼a(t0 u) +uat0 ∼v, withv=av0+uat0being
a closed term over BPA. 2
In turn, Lemma 2.4 paves the way to
Theorem 2.2 Lettbe a closed term over BPAint. Thent∼ufor some closed term uover BPA.
In other words: for closed terms over BPA modulo complete trace equivalence, interrupt is a derived operator.
Proof: By induction on the structure oft.
Case 1: t=a. This poses no problem: simply putu=a.
Case 2: t=t1+t2. By inductive hypothesis, there exist closed termsu1,u2 over BPA such thatt1 ∼u1andt2 ∼u2. Thenu=u1+u2is a closed term over BPA such thatt∼u.
Case 3:t=t1t2. By inductive hypothesis, there exist closed termsu1,u2over BPA such thatt1 ∼ u1 andt2 ∼ u2. Thenu = u1u2 is a closed term over BPA such thatt∼u.
Case 4:t=t1 t2. By inductive hypothesis, there exist closed termsu1,u2 over BPA such thatt1∼u1andt2∼u2. By Lemma 2.4, there exists a closed term uover BPA such thatu1 u2∼u. Thent=t1 t2 ∼u1u2 ∼u. 2 Observe that, to prove Lemma 2.4 (and thus Theorem 2.2 as well), we use only leftwise distributivity. This is interesting, because the interrupt operator isnot associative modulo complete trace equivalence, so that we cannot regroup all of its instances on a single side. As a counterexample, letabe an action: thena4 is a complete trace for(a3a2)a, but not fora3 (a2 a).
Since every closed term over BPAintis c.t.e. to a closed term over BPA in light of Theorem 2.2, we can think of reducing the problem of finding a ground com- plete axiomatization for BPAint, modulo c.t.e., to that of finding a ground complete axiomatization for BPA, modulo c.t.e. This would be allowed by prenex normal form, if they werecharacterizing for closed terms over BPA modulo complete trace equivalence, that is, if it were true that two closed terms over BPA having the same complete traces, also have the same prenex normal form.
And this is precisely the content of
Lemma 2.5 Lettand ube closed terms over BPA in prenex normal form. Then t∼uifftanduhave the same summands.
Proof: Supposet ∼ u. Let wbe a summand oft: thent →w Xand u →w Xas well. Thus one of the summands w0 ofu satisfies w0 →w X: but w0 is a closed term without summands, so the only possibility isw0 =w. This proves that every summand oftappears inu: by swapping the roles oftanduwe find that they have the same summands.
The reverse implication is trivial. 2
Theorem 2.3 The axioms in Table 2 form a ground complete axiomatization for BPA.
Proof: Lettandube two closed terms over BPA such thatt∼u, and letν(t)and ν(u)be their prenex normal forms. By using the axioms in Table 2 we can prove t ≈ ν(t)and u ≈ ν(u). But two terms in prenex normal form that are complete trace equivalent, are also equal up to the order of their summands: thus, by using the axioms in Table 2 we can also proveν(t) ≈ ν(u). This, in turn, allows us to
provet≈u. 2
As a consequence of this fact, we obtain the main result of this section.
Theorem 2.4 If|Act|<∞, then BPAinthas a finite ground complete axiomatiza- tion modulo complete trace equivalence.
Proof: Consider the familyE of equations from Theorem 2.1: if|Act|=n, then
|E|= 2n+ 8. Lettandube closed terms over BPAintsuch thatt∼u: we must show thatE`t≈u.
As seen in Theorem 2.2, the equations inEallow us to reduce any closed term over BPAintto a closed term over BPA: in particular, there exist closed termst0,u0 over BPA such thatE ` t≈t0and E `u ≈u0. By the soundness ofE,t0 ∼u0: since the equations in Table 2 also appear in Theorem 2.1, from Theorem 2.3 we
deduceE `t0 ≈u0. ThusE`t≈uas well. 2
3 The case of general terms
Having proved finite complete axiomatizability for c.t.e. over closed terms in the language BPAint, we want to obtain a similar result for general terms. However, the technique we used to prove Theorem 2.4 does not work in the broader case, because, as we announced in Subsection 1.1, interrupt is not a derived operator, except for a very special case.
Proposition 3.1 Let x and y be variables. Then there exists a term tover BPA such thatt∼xyif and only if|Act|= 1.
Proof: IfAct={a}, then by Lemma 2.3 and Theorem 2.2 the only closed substi- tutions are,up to complete trace equivalence, those of the form
σ(z) = X
k∈K
ak, (6)
whereKis a nonempty finite set of positive integers. Therefore, if|Act|= 1, then xy∼x+yx. In fact, let
σ(x) =X
i∈I
ai andσ(y) =X
j∈J
aj ; then
σ(x+yx) =X
i∈I
ai+X
j∈J
ajX
i∈I
ai ∼X
i∈I
ai+ X
i∈I,j∈J
aj+i and
σ(x y) = X
i∈I
ai
!
X
j∈J
aj
∼ X
i∈I,j∈J
ai aj
both have as complete traces precisely the words of the formaifori∈I, and those of the formaj+iforj∈J andi∈I.
IfAct={a, b, . . .}, then we prove that no BPA term is c.t.e. toxy; closed substitutions of the form (1) will play a key role. Assume, towards a contradiction, thatxy∼tfor some termtover BPA. By complete trace equivalence,σa(t)→a X, which, by Lemma 1.1, is possible if and only if either t →a X, or there exists a variable z such that z is a summand of t and σa(z) →a X. But the latter is the only possibility, because ift →a X, then σa[x 7→ a2](t) →a Xas well, while σa[x 7→ a2](x y) =a2 ahas norm 2, contradicting our assumption thattis c.t.e. tox y; moreover, it cannot be justt=z, orσa[y7→ b](z)would haveba as a complete trace, which is impossible. Sot=z+ufor some termuover BPA;
if it werez6=x, we would getσa[x 7→a2](t) =a+σa[x7→a2](u) →a X, which we know to be a contradiction. Thus, ift∼xy, then necessarilyt∼x+ufor some termu over BPA; it is not restrictive to suppose thatuis in prenex normal form, and that the summandxdoes not occur inu.
We observe thatucannot contain actions. In fact, shouldu contain actiona, letb∈Act\ {a}: thenσb(x+u)has a complete trace containingaandσb(xy) does not, contradicting our assumption thattis c.t.e. toxy. Moreover,ucannot
contain variables other thanxand y: otherwise, ifσ = σa[x 7→ b, y 7→ b], then σ(x+u)andσ(xy)would yield a similar contradiction.
Ifx = y, then all the summands ofuhave the formxn for somen > 1. Let thenσ(x) =ab; it follows thata2b2=a(ab)bis a complete trace forσ(xx) = abab, but not forσ(x+u). This is a contradiction.
If x 6= y, then u must contain both x and y. In fact, consider the closed substitutionσN,K given by
σN,K(x) =aN ; σN,K(y) =bK ; σ(z) =a∀z6∈ {x, y}.
Sincex+u ∼x y,bKaN is a complete trace for σN,K(x+u)for allN and K, which is impossible if eitherxory does not occur inu. Thusu is actually a sum of nonempty words over the alphabet{x, y}; since the only complete traces ofσa[y 7→ b](x+u)must beaandba, none of these words can containxx,xy, oryyas a subword, plusycannot be a summand ofu. Then the only possibility is u =yx: however,abais a complete trace forσb[x 7→ a2](x y) = a2 b, but not forσb[x7→a2](x+yx) =a2+ba2. This is a contradiction as well. 2 Proposition 3.1 puts an end to our hopes of finding an easy solution to the finite axiomatization problem for general terms over BPAint; at the same time, however, it opens the way to such a solution in a special case. To better understand the pos- sibilities left, and possibly use an approach based on normal forms for the special case, we need a deeper insight on the properties of prenex normal forms.
We start by observing that, iftis a term over BPA andσis a closed substitution, then the prenex normal form ofσ(t), sayP
j∈Jtj, is a sum of objects that can be seen both as closed terms over BPA and as words over actions, such that the word is the only complete trace for the term. It follows that, iftand uare terms over BPA such thatt∼u, then the “shape” ofν(σ(t))andν(σ(u))must be the same for every closed substitutionσ. The most natural thing to do is to ask oneself whether this “equality of shape” must be true for the terms themselves.
We recall that thelength of a wordwover an alphabetAis the number|w|of characters (i.e., elements ofA) occurring inw, while thenumber of occurrences of characterain wordwis the number|w|aof characters inwequal toa. Of course,
|w|=P
a∈A|w|a, and ifw1=w2, then|w1|a=|w2|afor everya∈A.
Proposition 3.2 Lettandube nonempty words overAct∪Var. 1. If|Act|>1thent∼uifft=u.
2. IfAct={a}thent∼uifftis a permutation ofu.
Proof: First of all, we recall that both points are true forclosed terms. This fact will be used later on in the proof. Also, substitutions of the form (1) will play a key role.
We now prove point 1 for general terms. Of course, only the “only if” part needs to be proved. Supposet 6= u: then either |t| 6= |u|, ort = λ1αλ2, u = λ1βλ3, withλ1, λ2, λ3 ∈(Act∪Var)∗,α, β ∈Act∪Var,α 6=β. In the former case, σa(t) and σa(u) are closed words of different length. In the latter, if one betweenα andβ is action a, andb ∈ Act\ {a}, thenσb(t) 6=σb(u); otherwise, α and β are distinct variables, thus σa[β 7→ b](t) 6= σa[β 7→ b](u). Therefore, ift 6= u, then there exists a closed substitution σ such thatσ(t) 6∼ σ(u), so that t6∼u.
We are now left with the proof of point 2 for general terms. Letσbe a closed substitution; letta term with a single summand, letσbe a closed substitution, and letw1, w2, . . . , wn∈Act∪Var such that
t=w1w2. . . wn.
By Theorem 2.2 and Lemma 2.3, for allj ∈ {1,2, . . . , n}there exists a finite set Ij of integers such that
σ(wj)∼ X
ij∈Ij
aij
Then, since complete trace equivalence is a congruence and distributivity laws ap- ply modulo complete trace equivalence,
σ(w) ∼ σ(w1)σ(w2). . . σ(wn)
∼
X
i1∈I1
ai1
X
i2∈I2
ai2
. . . X
in∈In
ain
!
∼ X
i1∈I1,i2∈I2,...,in∈In
ai1ai2. . . ain
= X
i1∈I1,i2∈I2,...,in∈In
ai1+i2+...+in
which depends on the nature of the wj’s, but not on their order. Thus, if t is a permutation of u, then σ(t) ∼ σ(u) whatever the closed substitution σ, i.e., t ∼ u. On the other hand, if tis not a permutation of u, then either |t| 6= |u|
or there is a variable x such that |t|x 6= |u|x, so that either σa(t) 6= σa(u) or σa[x7→a2](t)6=σa[x7→a2](u); and again,t6∼u. 2 Proposition 3.2 suggests a strategy for finding an axiomatization for the terms over BPAintwhenAct={a}.
Consider an orderingAct∪Var ={a, x1, x2, . . . , xn, . . .}. Letwbe a word overAct∪Var and letnbe the maximum index of a variable occurring inw. We define thenormal form ofwas
ν(w) =a|w|ax|w|1 x1x|w|2 x2. . . x|w|n xn . (7) By Proposition 3.2,w∼ν(w).
Let nowtbe a term over BPAint: by Proposition 3.1,tis complete trace equiv- alent to a term t0 over BPA, which, in turn, has a prenex normal formP
w∈Ww. We can therefore say that thenormal form of the termtis
ν(t) = X
w∈W
ν(w), (8)
where each summand in normal form is taken once per occurrence. For instance, the normal form oft=ya+xax+axisν(t) =a+ax+ax2+ay, while that ofxy +yxisxy. We observe thatν(t)is unique, up to the order of summands, and thatt∼ν(t).
Theorem 3.1 SupposeAct={a}. Then two termsu,vover BPAintare complete trace equivalent if and only ifν(t) =ν(u)up to the order of summands.
Proof: Lettandube two terms over BPAintsuch thatt∼u, and let ν(t) =Xr
i=1
piandν(u) =Xs
j=1
qj
be their normal forms. LetNbe the maximum index of a variable in either thepi’s or theqj’s; then for each iandjwe can write
pi =ae0,ixe11,i. . . xeNN,i andqj =af0,jxf11,j. . . xfNN,j .
Letbbe a positive integer greater than all of theek,i’s and thefk,j’s; consider the substitutionσdefined by
σ(xk) =abk ∀k∈N. (9) Then, for alliandj,σ(pi) =aαi andσ(qj) =aβj, where
αi = XN k=0
ek,ibkandβj = XN k=0
fk,jbk,
I0.1 xy ≈ xy+x
I0.2 xy ≈ xy+yx
I2 xy z ≈ x(yz) + (xz)y
I4 (xy)z ≈ (xy)z+x(yz) I5 (xy)z+x(zy) ≈ (xz)y+x(yz)
Table 3: A list of valid equations for BPAint.
and sincebis larger than all of theek,i’s and thefk,j’s, theαi’s are pairwise distinct, and so are theβj’s.
Sincet∼u, we haveν(t)∼ν(u)as well, soσ(ν(t))∼σ(ν(u)). But a word w=aKis a complete trace forσ(ν(t))iffK=αifor somei, and similarly,wis a complete trace forσ(ν(u))iffK = βj for some j: thus, for everyithere must exist aj such thatαi = βj, and vice versa. This, in turn, is only possible if for everyithere existsjsuch thatpi =qj, and vice versa; since thepi’s are summands in a normal form, and so are theqj’s, we conclude thatr = sand thepi’s are a permutation of theqj’s, that is,ν(t) =ν(u)up to the order of summands.
The reverse implication is trivial. 2
Theorem 3.2 If|Act|= 1then BPAintis finitely axiomatizable.
Proof: Consider the setEconsisting of the axioms of Theorem 2.1 together with
CC xy ≈ yx
DI xy ≈ x+yx
(Observe thatCCandDIare sound modulo complete trace equivalence iff|Act|= 1.) Lettandube terms over BPAintsuch thatt∼u: we must prove thatE `t≈u. Consider the normal formsν(t)and ν(u). Using equations CCand DI, it is not hard to prove thatE ` t ≈ ν(t)and E ` u ≈ ν(u). But the normal forms of two terms over BPA that are equivalent modulo complete trace equivalence are equal by Theorem 3.1; thus,E ` ν(t) ≈ ν(u). This allows us to conclude that
E`t≈u. 2
4 Other valid equations
In this section, we will list some equations over BPAint, and prove that they are all valid; plus, we will suggest a kind of “normal forms” for BPAint terms. We use double quotes, because these, as we shall see, are not characterizing.
A list of valid equations for BPAintis given in Table 3. We immediately observe that I0.1 and I0.2 are valid indeed, because, whatevertand uare, any complete trace fortorutis also a complete trace fortu
Proposition 4.1 Equation I2in Table 3 is sound modulo complete trace equiva- lence.
Proof: We must show that, for every word w over the alphabet Act and every closed termst, u, v over BPAint, tu v →w Xif and only ift(u v) + (t v)u→w X.
Suppose tu v →w X: this is the same as saying that w = xyz with z nonempty,tu→xz X, and either yis empty orv →y X. Ift→x Xandu →z X, then t(u v) →w X;otherwise, eitherx =x0pwitht →x0 X, orz =qz0 witht →xq X, wherepand qare suitable nonempty words. In the former case, u v pyz→ X, so thatt(uv) x0→pyzXandx0pyz=w; in the latter case,u→z0 Xandtvxyq→ X, so that(tv)uxyqz→0 Xandxyqz0 =w.
On the other hand, suppose t(u v) + (t v)u →w X: then eithert(u v) →w Xor(tv)u→w X. In the first case,w=rxyzwithznonempty,t→r X, u→xz X, and eitheryis empty orv →y X. Thentu rxz→ Xandtu vrxyz→ X; but rxyz=w. In the second case,w =xyzswithznonempty,t→xz X,u→s X, and eitheryis empty orv →y X. Thentuxzs→ Xandtuvxyzs→ X; butxyzs=w. 2 Observe how equationI2generalizesI2.ato the case of a general concatenation of terms. In fact,
atu ≈ a(tu) + (au)t from I2,
≈ a(tu) + (a+ua)t from I1.a ,
≈ a(tu) +at+uat from A4.1,
≈ a(tu) +uat from I0.1 and A4.2.
Proposition 4.2 Equation I4in Table 3 is sound modulo complete trace equiva- lence.
Proof: We must show that, for every word w over the alphabet Act and every closed termst,u,vover BPAint, ift(uv)→w X, then(tu)v→w X.
Lett (uv) →w X: thenw = xyzwith znonempty, t →xz X, and either y is empty oru v →y X. Ify is empty, then w = xz is a complete trace for (tu)v; otherwise,y=pqrwithu→pr Xand eitherqis empty orv→q X. Let thenx0 =xp,y0 =q,z0 =rz: thentux→0z0Xand eithery0is empty orv→y0 X, thus(tu)vx0→y0z0 X. Butx0y0z0 =xpqrz=xyz=w. 2
Equation I4 says that t (uv) is somewhat “less capable”, in terms of
“possible terminating executions”, than(tu) v, something we had already seen after Theorem 2.2. The question arises naturally: how much is this “less”?
EquationI5provides a possible answer to this question.
Theorem 4.1 EquationI5in Table 3 is sound modulo complete trace equivalence.
Proof: Suppose(tu) v →w X. We know from Lemma 2.1 thatw = xyz witht u →xz Xand either yis empty orv →y X. From the same lemma we get xz =pqrwitht →pr Xand eitherqis empty oru→q X. Thus four cases must be studied.
Case 1:yandqare both empty. In this case, the transition is entirely due to t, thust(uv)→w X.
Case 2: y is empty and q is not. In this case, there is a transition t →p t0, followed byu→q X, then byt0 →r X; plus,w=xz=pqr. This can be mimicked byt(uv)as follows:
t(uv)→p t0 (uv)→q t0 →r X, because ifu→q Xthenuv→q Xas well.
Case 3: yis nonempty and q is empty. In this case, the transition is of the kind
(tu)v→x (t0 u)v→y t0u→z X, This cannot in general be mimicked byt(uv), because
t(uv)→x t0 (uv)→y ut ,
andutmight not havezas a complete trace. However, it can be mimicked by tv→x t0 v→y t0 →z X,
which is tolerable, because iftv→w X, then(tu)v→w Xas well.
Case 4: yand q are both nonempty. This is the most complicated case, so we split it into subcases.
Subcase 4a:x=pq0,z=q00r. This means that the execution oftis interrupted by that ofu, which is in turn interrupted by that ofv; that is, for somet0,u0,
(tu)v→p (t0 u)v→q0 u0t0 v→y u0t0 →q00 t0 →r X. This can be mimicked by
t(uv)→p t0(uv)→q0 (u0 v)t0 →y u0t0 →q00 t0→r X.
