• Ingen resultater fundet

BRICS Basic Research in Computer Science


Academic year: 2022

Del "BRICS Basic Research in Computer Science"


Hele teksten



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



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:


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


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.


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


→|a∈Act o,na

→X|a∈Act o ,

where the transition relationsa 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


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


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 relationsa 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=t0a1 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 relationwill be referred to ascomplete trace equivalence.

It is evident thatis 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 toiff t u. An axiom system is sound with respect toiff so is each of its equations.

An example of a collection of equations over the language BPAintthat are sound with respect tois 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 BPAint

terms: 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)∪ [


{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 x0z 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 , (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 ,

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 ,

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.


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


ak, (6)

whereKis a nonempty finite set of positive integers. Therefore, if|Act|= 1, then xy∼x+yx. In fact, let

σ(x) =X


ai andσ(y) =X


aj ; then

σ(x+yx) =X






ai X


ai+ X


aj+i and

σ(x y) = X









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,


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 σa7→ b](t) 6= σa7→ 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, . . . , wnAct∪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



Then, since complete trace equivalence is a congruence and distributivity laws ap- ply modulo complete trace equivalence,

σ(w) σ(w1)σ(w2). . . σ(wn)







. . . X






ai1ai2. . . ain

= X



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), (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


piandν(u) =Xs



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



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) x0pyzXandx0pyz=w; in the latter case,u→z0 Xandtvxyq X, so that(tv)uxyqz0 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: thentux0z0Xand eithery0is empty orv→y0 X, thus(tu)vx0y0z0 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 t0r X.



of the expressive completeness of this property language with respect to tests. More precisely, we study whether all properties that are testable can

With this relaxation we have been able to define complexity in this model using restricted classes of real numbers and functions.. Interval arithmetic [7], can be used as the

We have presented a wavelet based 3D compression scheme for very large volume data supporting fast random access to individual voxels within the volume. Experiments on the CT data

We give an algorithm list- ing the maximal independent sets in a graph in time proportional to these bounds (ignoring a polynomial factor), and we use this algorithm to

Chromatic Number in Time O(2.4023 n ) Using Maximal Independent Sets. Higher Dimensional

More pre- cisely, it is proven ibidem that, in the presence of at least two actions, the process (a, a) ∗ (a, b) cannot be expressed, modulo bisimulation equivalence, in ACP [4], and

  For  Dewey,  and  for  the  jazz  community,  learning  is  ubiquitous  and  continuous.  This  would  be  a  non-controversial  position  if 

semantics [10] in that processes denote downwards-closed sets of computa- tion paths and the corresponding notion of process equivalence, called path equivalence, is given by

‡ Supported by a grant from the Danish Research Council... is that two programs are related by a standard denotational interpretation if, in some precise sense, they afford the

Consequently, two of the translators (no. 8 and 10) were aware that they were participating in a research project, but they were not informed of the purpose of the study.

Translation-theoretical papers were only included in this cate- gory if the research could be situated within translation technology research – dealing with (aspects of)

Interviewee: Yes, If I could, do that. Interviewer: If you think that it would be able to make consumers do that or contribute to it. Interviewee: I don't think it's AI that does

This interpretation is by no means applicable to the villain alone (if this were the case, its validity for the drama would be very restricted); ultimately it is an (albeit

In that reference, a finite, complete equational axiomatization of strong bisimulation equivalence has been given for T(BCCS) p ∗ (A τ ), i.e., the language of closed terms obtained

This means that even if the empirical research showed that there was a distinct difference in terms of ROAE and ROAA in section 6.1, between boards with no women and those with,

13 This made it possible to make the theoretical choices that were representative for this type of information, based on the research objectives that were made

In theoretical terms, this implies that the utility model can be subsumed by the two other models, where income influences trust in the political establishment,

If there were to be a common European non-financial reporting standard applied by companies under the scope of the NFRD, to what extent do you think it would be important that such

Refining a basic result of Alexander, we show that two flag simplicial complexes are piecewise linearly homeomorphic if and only if they can be connected by a sequence of

When the sea heaves and is rough, the seething waves in their turbulence form pictures resembling creatures; it would seem as if it were these

This gives a cleaner semantics to the restriction phenomenon, and further- more avoids the state-space explosions mentioned above. According to [28], we can guarantee that the

4 well it begins to look as if the black boxes were effortlessly gliding through space as a result of their own impetus‖ (1987, p. To trace black boxes that form around

We have seen that these sets are power closed and root closed, where a subset of a ring is said to be root closed if whenever it contains a positive power of an element, it