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ólfsdóttir

BRICS Report Series RS-07-5 ISSN 0909-0878 February 2007 BRICS RS-07-5 Aceto et al.: On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt Copyright \begin{matrix}c \\ ◯ \end{matrix} 2007, Luca Aceto & Silvio Capobianco & Anna

Ingólfsdóttir. 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 subdirectory RS/07/5/

On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt

Luca Aceto  Silvio Capobianco

Anna Ingólfsdóttir 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 explicitly 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 Process Algebra (BPA), enriched with the deadlock constant δ (a special process, not doing anything) and the interrupt 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 more auxiliary operators: hence, it is not immediately clear whether this process algebra, modulo bisimilarity, is finitely axiomatizable by itself. This fact is not at all immediate, given the many examples [1, 2, 3, 4, 5, 13, 15, 16, 18] where a finite complete axiomatization does not exist.

∗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.

In this paper, we deal with the process algebra BPA_{int}, obtained from BPA by adding the interrupt operator and, as for the relation modeling “indistinguishability from an external observer”, we choose to work with complete 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 of regular 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 term t over BPA_{int}, there is a term u over BPA which is c.t.e. to t. Such u can be obtained from t via 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), BPA_{int} turns 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 BPA_{int} terms 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 BPA_{int} term to a BPAterm with a very special “shape”; and in fact, this “shape” is special enough to be characterizing, i.e., two BPA_{int} terms 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 BPA_{int} 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 BPA_{int}

We assume a nonempty alphabet Actof atomic actions, with typical elements a, b. The language for processes we shall consider in this paper, henceforth referred to as BPA_{int}, 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 | t ⊳ t ,

where x is a variable drawn from a countably infinite set Var and a is an action. In the above grammar, we use the symbol ⊳ for the interrupt operator. We shall use the meta-variables t, u, v to range over process terms, and write Var(t) for the collection of variables occurring in the term t. The size of a term is the number of operator symbols in it. A process term is closed if it does not contain any variables. As usual, we shall often write tu in lieu of t·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 BPA_{int} without the interrupt operator.

A substitution is a mapping from process variables to BPA_{int} terms. A substitution σ is closed if σ(x) is a closed term for every variable x. For every term t and substitution σ, the term obtained by replacing every occurrence of a variable x in t 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 ↦ p], where σ is a closed substitution and p is a closed BPA_{int} term, to stand for the substitution mapping x to p, and acting like σ on all of the other variables in Var. If a ∈ Act, we indicate by σ_{a} the closed substitution that replaces every variable with a, i.e.,

σ_{a}(x) = a ∀x ∈ Var .  (1)

In the remainder of this paper, we let a^{1} denote a, and a^{m+1} denote a(a^{m}). Moreover, we consider terms modulo associativity and commutativity of +. In other words, we do not distinguish t+u and u+t, nor (t+u)+v and t+(u+v). This is justified because + is associative and commutative with respect to the notion of equivalence we shall consider over BPA_{int}. (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 term t has + as head operator if t = t_{1} + t_{2} for some terms t_{1} and t_{2}. For example, a + b has + as head operator, but (a + b)a does not.

For k ≥ 1, we use a summation ∑_{i∈{1,...,k}} t_{i} to denote t_{1} + ⋯ + t_{k}. It is easy to see that every BPA_{int} term t has the form ∑_{i∈I} t_{i}, for some finite, nonempty index set I, and terms t_{i} (i ∈ I) that do not have + as head operator. The terms t_{i} (i ∈ I) will be referred to as the (syntactic) summands of t. For example, the term (a + b)a has only itself as (syntactic) summand.

The operational semantics for the language BPA_{int} is given by the labeled transition system

(BPA_{int}, {→^{a}| a ∈ Act}, {→^{a}✓ | a ∈ Act}) ,

where the transition relations →^{a} and the unary predicates →^{a}✓ are, respectively, the least subsets of BPA_{int} × BPA_{int} and BPA_{int} satisfying the rules in Table 1. Intuitively, a transition t →^{a} u means that the system represented by the term t can perform the action a, thereby evolving into u. The special symbol ✓ stands for (successful) termination; therefore the interpretation of the statement t →^{a}✓ is that the process term t can terminate by performing a. Note that, for every closed term p, there is some action a for which either p →^{a} p′ holds for some p′, or p →^{a}✓ does.

\overline{a →^{a}✓}

\frac{t →^{a}✓}{t + u →^{a}✓}  \frac{u →^{a}✓}{t + u →^{a}✓}  \frac{t →^{a} t′}{t + u →^{a} t′}  \frac{u →^{a} u′}{t + u →^{a} u′}

\frac{t →^{a}✓}{t · u →^{a} u}  \frac{t →^{a} t′}{t · u →^{a} t′ · u}

\frac{t →^{a}✓}{t ⊳ u →^{a}✓}  \frac{t →^{a} t′}{t ⊳ u →^{a} t′ ⊳ u}  \frac{u →^{a}✓}{t ⊳ u →^{a} t}  \frac{u →^{a} u′}{t ⊳ u →^{a} u′ · t}

Table 1: Transition Rules for BPA_{int}

The transition relations →^{a} naturally compose to determine the possible effects that performing a sequence of actions may have on a BPA_{int} term.

Definition 1.1 For a sequence of actions a_{1} ⋯ a_{k} (k ≥ 0), and BPA_{int} terms t, t′, we write t →^{a_{1}···a_{k}} t′ iff there exists a sequence of transitions

t = t_{0} →^{a_{1}} t_{1} →^{a_{2}} ⋯ →^{a_{k}} t_{k} = t′ .

Similarly, we say that a_{1} ⋯ a_{k} (k ≥ 1) is a complete trace of a BPA_{int} term t iff there exists a term t′ such that

t ⟶^{a_{1}···a_{k−1}} t′ →^{a_{k}}✓ .

If t ⟶^{a_{1}···a_{k}} t′ holds for some BPA_{int} term t′, or a_{1} ⋯ a_{k} is a complete trace of t, then a_{1} ⋯ a_{k} is a trace of t.

The depth of a term t, written depth(t), is the length of a longest trace it affords. Observe that such a trace is necessarily a complete trace.

The norm of a term t, denoted by norm(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(p ⊳ q) = depth(p) + depth(q)
norm(a) = 1
norm(p + q) = min{norm(p), norm(q)}
norm(pq) = norm(p) + norm(q)
norm(p ⊳ q) = norm(p) .

Note that the depth and the norm of each closed BPA_{int} term are positive.

Lemma 1.1 [Operational Correspondence] Assume that t is a BPA_{int} term, σ is a closed substitution and a is an action. Then the following statements hold:

1. If t →^{a}✓, then σ(t) →^{a}✓.

2. If t →^{a} t′, then σ(t) →^{a} σ(t′).

3. Assume that t is a BPA term. If σ(t) →^{a}✓, then either

(a) t →^{a}✓, or

(b) t = x and σ(x) →^{a}✓ for some variable x, or

(c) t = x + u and σ(x) →^{a}✓ for some variable t and term u.

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 term t.

The details are lengthy, but straightforward, and we therefore omit them. □

In this paper, we shall consider the language BPA_{int} modulo complete trace equivalence.

Definition 1.2 Two closed BPA_{int} terms p and q are complete trace equivalent, denoted by p ∼ q, if they have the same complete traces, i.e., if for every nonempty word w ∈ Act^{+}, w is a complete trace for p iff it is a complete trace for q. The relation ∼ will be referred to as complete trace equivalence.

It is evident that ∼ is an equivalence. There is more: ∼ is a congruence with respect to all the operators in the signature of BPA_{int}, that is, if t ∼ t′ and u ∼ u′, then t + u ∼ t′ + u′, tu ∼ t′u′, and t ⊳ u ∼ t′ ⊳ u′. This will follow from Lemma 2.1, at the beginning of next section. Observe that complete trace equivalent BPA_{int} terms have the same norm and depth.

Complete trace equivalence is extended to arbitrary BPA_{int} terms thus:

Definition 1.3 Let t, u be BPA_{int} terms. Then t ∼ u iff σ(t) ∼ σ(u) for every closed substitution σ.

For instance, we have that

x ⊳ y ∼ (x ⊳ y) + yx

because, as our readers can easily check, the terms p ⊳ q and (p ⊳ q) + qp have the same set of initial “capabilities”, i.e.,

p ⊳ q →^{a} r iff (p ⊳ q) + qp →^{a} r , for each a and r, and

p ⊳ q →^{a}✓ iff (p ⊳ q) + qp →^{a}✓, for each a .

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

An axiom system is a collection of equations t ≈ u over the language BPA_{int}. An equation t ≈ u is derivable from an axiom system E, notation E ⊢ t ≈ u, if it can be proved from the axioms in E using the rules of equational logic (viz. reflexivity, symmetry, transitivity, substitution and closure under BPA_{int} contexts):

t ≈ t \frac{t ≈ u}{u ≈ t} \frac{t ≈ u u ≈ v}{t ≈ v} \frac{t ≈ u}{σ(t) ≈ σ(u)}

\frac{t ≈ u t′ ≈ u′}{t + t′ ≈ u + u′} \frac{t ≈ u t′ ≈ u′}{tt′ ≈ uu′} \frac{t ≈ u t′ ≈ u′}{t ⊳ t′ ≈ u ⊳ u′} .

\begin{aligned}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) \end{aligned}

Table 2: Some Axioms for BPA_{int}

Definition 1.4 An equation t ≈ u over the language BPA_{int} is sound 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 BPA_{int} that 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 BPA_{int}. In fact, we give a complete, structural description of the complete traces of BPA_{int} terms: congruence of complete trace equivalence will be an easy consequence.

First of all, we observe that, given two closed terms t, u over BPA_{int} and a nonempty word w over Act, then w is a complete trace for t + u iff w is a complete trace for either t or u, while w is a complete trace for tu iff w = xy for some words x, y that are complete traces for t and u, respectively. In fact, there is a similar characterization for complete traces of t ⊳ u, but it’s a bit trickier.

Lemma 2.1 Let t and u be closed terms over BPA_{int}. Let w be a nonempty word over the alphabet Act. Then w is a complete trace for t ⊳ u iff there exist words x, y, z over Actsuch that

1. w = xyz,

2. z is nonempty,

3. xz is a complete trace for t, and

4. y is either empty or a complete trace for u.

Proof: Suppose t ⊳ u →^{w} ✓. Then

• either u does not initiate, so that t →^{w} ✓, or

• u initiates before t, so that u →^{y} ✓, then t →^{z} ✓ for some nonempty words y, z such that w = yz, or

• u initiates while t is running, so that t →^{x} t′ for some closed term t′, u →^{y} ✓, and t′ →^{z} ✓ for some nonempty words x, y, z such that w = xyz.

The reverse implication is trivial. □

Lemma 2.1allows one to give a language-theoretic characterization of closed terms over BPA_{int} modulo complete trace equivalence. Call CT (t) the set of complete traces of closed term t: 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 (t ⊳ u) = CT (t) ∪ ⋃_{rs∈CT (t),s≠ε}{r}CT (u){s}  (4)

hold. We recall that XY = {w : ∃x ∈ X, y ∈ Y : w = xy}.

Corollary 2.1 For terms over BPA_{int}, complete trace equivalence is a congruence.

Proof: Suppose t ∼ t′ and u ∼ u′. Let σ be a closed substitution: then σ(t) and σ(t′) have the same set of complete traces, and similarly for σ(u) and σ(u′). By (2), σ(t + u) = σ(t) + σ(u) has the same complete traces as σ(t′ + u′) = σ(t′) + σ(u′); similarly for σ(tu) and σ(t′u′) because of (3), and for σ(t ⊳ u) and σ(t′ ⊳ u′) because of (4). This is true for every closed substitution σ, thus t + u ∼ t′ + u′, tu ∼ t′u′, and t ⊳ u ∼ t′ ⊳ u′. □

As a consequence of Lemma 2.1 and our previous observations, we obtain the following equivalences.

Lemma 2.2 For every action a and closed terms t, u, v over BPA_{int}, 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. a ⊳ u ∼ a + ua;

8. at ⊳ u ∼ a(t ⊳ u) + uat;

9. (t + u) ⊳ v ∼ (t ⊳ v) + (u ⊳ v); and

10. t ⊳ (u + v) ∼ (t ⊳ u) + (t ⊳ v).

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. Suppose w is a complete trace for a ⊳ u. By Lemma 2.1, this is the same as saying that w = xyz so that z is nonempty, a →^{xz} ✓ and either y is empty or u →^{y} ✓. The first part is possible iff x is empty and z = a, thus either w = a or w = ya with u →^{y} ✓; by Lemma 2.1, this is the same as saying that w is a complete trace for a + ua. On the other hand, if a + ua →^{w} ✓, then either w = a or w = ya for some y such that u →^{y} ✓; in either case, w is a complete trace for a ⊳ u as well.

8. Suppose w is a complete trace for at ⊳ u. We can write w = xyz with z nonempty, at →^{xz} ✓, and either y empty or u →^{y} ✓. Two cases are possible: either x = ax′, or x is empty and z = az′. In the first case t →^{x′z} ✓, and either y empty or u →^{y} ✓, so that x′yz is a complete trace for t ⊳ u, and w = ax′yz is a complete trace for a(t ⊳ u); in the second case, w = yaz′ is a complete trace for uat. On the other hand, let w be a complete trace for a(t ⊳ u) + uat: then either a(t ⊳ u) →^{w} ✓, so that w = axyz with t →^{xz} ✓ and either y empty or u →^{y} ✓; or w = yax with u →^{y} ✓ and t →^{x} ✓. In either case, at ⊳ u →^{w} ✓.

9. Suppose w is a complete trace for (t + u) ⊳ v. This is the same as saying that w = xyz with z nonempty, either t →^{xz} ✓ or u →^{xz} ✓, and either y empty or v →^{y} ✓. This means that either t ⊳ v →^{w} ✓ or u ⊳ v →^{w} ✓.

10. Suppose w is a complete trace for t ⊳ (u + v). This is the same as saying that w = xyz with z nonempty, t →^{xz} ✓, and either y is empty or u →^{y} ✓ or v →^{y} ✓. This means that either t ⊳ u →^{w} ✓ or t ⊳ v →^{w} ✓. □

We can then state Theorem 2.1 Let a be an action and let x, y, z be variables. The following equations are sound for BPA_{int} modulo 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  a ⊳ y ≈ a + ya
I2.a  ax ⊳ y ≈ a(x ⊳ y) + yax
I3.1 (x + y) ⊳ z ≈ (x ⊳ z) + (y ⊳ z)
I3.2 x ⊳ (y + z) ≈ (x ⊳ y) + (x ⊳ z)

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. □

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 “simplest possible form” a BPA term can have, modulo complete trace equivalence.

Definition 2.1 A term t over BPA is in prenex normal form if there exists a finite nonempty set W ⊆ (Act∪ Var)^{+} such that

t = ∑_{w∈W} w ,  (5)

where the word α_{1} … α_{n} is 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 Let t be a term over BPA. There exists a term u over BPA in prenex normal form such that t ∼ u. Moreover, if t is closed, then u is closed as well.

Proof: By structural induction on t. The thesis is trivially true if either t = a for some a ∈ Act, or t = x for some x ∈ Var.

If t = t_{1} + t_{2} for some terms t_{1}, t_{2}, consider u_{1}, u_{2} in prenex normal form such that t_{1} ∼ u_{1} and t_{2} ∼ u_{2}. Put

u = ∑_{w∈W} w ,

where W is the set of all words w that appear as summands in either u_{1} or u_{2}. Observe that u can be constructed from u_{1} + u_{2} by repeatedly applying the idempotence rule A3. It is immediate to check that u is in prenex normal form, and that t ∼ u; moreover, if t is closed, then t_{1} and t_{2} are closed, so that u_{1} and u_{2}, and consequently u, are closed by inductive hypothesis.

If t = t_{1}t_{2} for some terms t_{1}, t_{2}, consider u_{1}, u_{2} in prenex normal form such that t_{1} ∼ u_{1} and t_{2} ∼ u_{2}. Put

u = ∑_{w∈W} w ,

where W is the set of all words w such that w = w_{1}w_{2} for two nonempty words w_{1}, w_{2} such that w_{1} is a summand of u_{1} and w_{2} is a summand of u_{2}. Observe that u can be constructed from u_{1}u_{2} by repeatedly applying the associativity laws A4.1 and A4.2, and the idempotence rule A3. It is straightforward to check that u is in prenex normal form, and that t ∼ u; moreover, if t is closed, then t_{1} and t_{2} are closed, so that u_{1} and u_{2}, and consequently u, are closed by inductive hypothesis. □

Lemma 2.3 states that, for every closed term t over BPA, there exists a closed term ν(t) over BPA in prenex normal form, such that t ∼ ν(t). We call ν(t) the prenex normal form of the term t. Observe that ν(t) is defined up to the order of its summands. Observe also that, to construct u from t in the proof of Lemma 2.3, we have only applied associativity of operators, commutativity and idempotence of nondeterministic choice, and distributivity of nondeterministic choice w.r.t. composition: that is, ν(t) can be constructed syntactically from t by means of axioms in Table 2.

Introduction of prenex normal forms allows us to prove

Lemma 2.4 Let t and u be closed terms over BPA. There exists a closed term v over BPA such that t ⊳ u ∼ v.

Proof: By induction on the size of t. Because of Lemma 2.3, it is not restrictive to suppose that t is in prenex normal form.

If t has size 1, then t = a for some action a. Then t ⊳ u = a ⊳ u ∼ a + ua. Suppose now that the thesis is proved every time that t has at most size n. Let

t have size n + 1. If t = t_{1} + t_{2}, then t ⊳ u ∼ t_{1} ⊳ u + t_{2} ⊳ u, with t_{1} and t_{2} having size at most n: by inductive hypothesis, t_{1} ⊳ u ∼ v_{1} and t_{2} ⊳ u ∼ v_{2} for suitable closed terms v_{1}, v_{2} over BPA, so that t ⊳ u ∼ v_{1} + v_{2} = v with v closed term over BPA. Otherwise t has only one summand, so, since it is in prenex normal form, it must have the form t = at′ for some action a and closed term t′ having size n: by inductive hypothesis, t′ ⊳ u ∼ v′ for some closed term v′ over BPA, so that t ⊳ u = at′ ⊳ u ∼ a(t′ ⊳ u) + uat′ ∼ v, with v = av′ + uat′ being a closed term over BPA. □

In turn, Lemma 2.4 paves the way to

Theorem 2.2 Let t be a closed term over BPA_{int}. Then t ∼ u for some closed term u over BPA.

In other words: for closed terms over BPA modulo complete trace equivalence, interrupt is a derived operator.

Proof: By induction on the structure of t.

Case 1: t = a. This poses no problem: simply put u = a.

Case 2: t = t_{1} + t_{2}. By inductive hypothesis, there exist closed terms u_{1}, u_{2} over BPA such that t_{1} ∼ u_{1} and t_{2} ∼ u_{2}. Then u = u_{1} + u_{2} is a closed term over BPA such that t ∼ u.

Case 3: t = t_{1}t_{2}. By inductive hypothesis, there exist closed terms u_{1}, u_{2} over BPA such that t_{1} ∼ u_{1} and t_{2} ∼ u_{2}. Then u = u_{1}u_{2} is a closed term over BPA such that t ∼ u.

Case 4: t = t_{1} ⊳ t_{2}. By inductive hypothesis, there exist closed terms u_{1}, u_{2} over BPA such that t_{1} ∼ u_{1} and t_{2} ∼ u_{2}. By Lemma 2.4, there exists a closed term u over BPA such that u_{1} ⊳ u_{2} ∼ u. Then t = t_{1} ⊳ t_{2} ∼ u_{1} ⊳ u_{2} ∼ u. □

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 is not associative modulo complete trace equivalence, so that we cannot regroup all of its instances on a single side. As a counterexample, let a be an action: then a^{4} is a complete trace for (a^{3} ⊳ a^{2}) ⊳ a, but not for a^{3} ⊳ (a^{2} ⊳ a).

Since every closed term over BPA_{int} is 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 complete axiomatization for BPA_{int}, 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 were characterizing 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 Let t and u be closed terms over BPA in prenex normal form. Then t ∼ u iff t and u have the same summands.

Proof: Suppose t ∼ u. Let w be a summand of t: then t →^{w} ✓ and u →^{w} ✓ as well. Thus one of the summands w′ of u satisfies w′ →^{w} ✓: but w′ is a closed term without summands, so the only possibility is w′ = w. This proves that every summand of t appears in u: by swapping the roles of t and u we find that they have the same summands.

The reverse implication is trivial. □

Theorem 2.3 The axioms in Table 2 form a ground complete axiomatization for BPA.

Proof: Let t and u be two closed terms over BPA such that t ∼ 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 prove t ≈ u. □

As a consequence of this fact, we obtain the main result of this section.

Theorem 2.4 If |Act| < ∞, then BPA_{int} has a finite ground complete axiomatization modulo complete trace equivalence.

Proof: Consider the family E of equations from Theorem 2.1: if |Act| = n, then |E| = 2n + 8. Let t and u be closed terms over BPA_{int} such that t ∼ u: we must show that E ⊢ t ≈ u.

As seen in Theorem 2.2, the equations in E allow us to reduce any closed term over BPA_{int} to a closed term over BPA: in particular, there exist closed terms t′, u′ over BPA such that E ⊢ t ≈ t′ and E ⊢ u ≈ u′. By the soundness of E, t′ ∼ u′: since the equations in Table 2 also appear in Theorem 2.1, from Theorem 2.3 we deduce E ⊢ t′ ≈ u′. Thus E ⊢ t ≈ u as well. □

3 The case of general terms

Having proved finite complete axiomatizability for c.t.e. over closed terms in the language BPA_{int}, 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 t over BPA such that t ∼ x ⊳ y if and only if |Act| = 1.

Proof: If Act= {a}, then by Lemma 2.3 and Theorem 2.2 the only closed substitutions are, up to complete trace equivalence, those of the form

σ(z) = ∑_{k∈K} a^{k} ,  (6)

where K is a nonempty finite set of positive integers. Therefore, if |Act| = 1, then x ⊳ y ∼ x + yx. In fact, let

σ(x) = ∑_{i∈I} a^{i} and σ(y) = ∑_{j∈J} a^{j} ;

then

σ(x + yx) = ∑_{i∈I} a^{i} + ∑_{j∈J} a^{j} ∑_{i∈I} a^{i} ∼ ∑_{i∈I} a^{i} + ∑_{i∈I,j∈J} a^{j+i}

and

σ(x ⊳ y) = (∑_{i∈I} a^{i}) ⊳ (∑_{j∈J} a^{j}) ∼ ∑_{i∈I,j∈J} a^{i} ⊳ a^{j}

both have as complete traces precisely the words of the form a^{i} for i ∈ I, and those of the form a^{j+i} for j ∈ J and i ∈ I.

If Act= {a, b, …}, then we prove that no BPA term is c.t.e. to x ⊳ y; closed substitutions of the form (1) will play a key role. Assume, towards a contradiction, that x ⊳ y ∼ t for some term t over BPA. By complete trace equivalence, σ_{a}(t) →^{a} ✓, which, by Lemma 1.1, is possible if and only if either t →^{a} ✓, or there exists a variable z such that z is a summand of t and σ_{a}(z) →^{a} ✓. But the latter is the only possibility, because if t →^{a} ✓, then σ_{a}[x ↦ a^{2}](t) →^{a} ✓ as well, while σ_{a}[x ↦ a^{2}](x ⊳ y) = a^{2} ⊳ a has norm 2, contradicting our assumption that t is c.t.e. to x ⊳ y; moreover, it cannot be just t = z, or σ_{a}[y ↦ b](z) would have ba as a complete trace, which is impossible. So t = z + u for some term u over BPA; if it were z ≠ x, we would get σ_{a}[x ↦ a^{2}](t) = a + σ_{a}[x ↦ a^{2}](u) →^{a} ✓, which we know to be a contradiction. Thus, if t ∼ x ⊳ y, then necessarily t ∼ x + u for some term u over BPA; it is not restrictive to suppose that u is in prenex normal form, and that the summand x does not occur in u.

We observe that u cannot contain actions. In fact, should u contain action a, let b ∈ Act\ {a}: then σ_{b}(x + u) has a complete trace containing a and σ_{b}(x ⊳ y) does not, contradicting our assumption that t is c.t.e. to x ⊳ y. Moreover, u cannot contain variables other than x and y: otherwise, if σ = σ_{a}[x ↦ b, y ↦ b], then σ(x + u) and σ(x ⊳ y) would yield a similar contradiction.

If x = y, then all the summands of u have the form x^{n} for some n > 1. Let then σ(x) = ab; it follows that a^{2}b^{2} = a(ab)b is a complete trace for σ(x ⊳ x) = ab ⊳ ab, but not for σ(x + u). This is a contradiction.

If x ≠ y, then u must contain both x and y. In fact, consider the closed substitution σ_{N,K} given by

σ_{N,K}(x) = a^{N} ; σ_{N,K}(y) = b^{K} ; σ(z) = a ∀z ∉ {x, y} .

Since x + u ∼ x ⊳ y, b^{K}a^{N} is a complete trace for σ_{N,K}(x + u) for all N and K, which is impossible if either x or y does not occur in u. Thus u is actually a sum of nonempty words over the alphabet {x, y}; since the only complete traces of σ_{a}[y ↦ b](x + u) must be a and ba, none of these words can contain xx, xy, or yy as a subword, plus y cannot be a summand of u. Then the only possibility is u = yx: however, aba is a complete trace for σ_{b}[x ↦ a^{2}](x ⊳ y) = a^{2} ⊳ b, but not for σ_{b}[x ↦ a^{2}](x + yx) = a^{2} + ba^{2}. This is a contradiction as well. □

Proposition 3.1puts an end to our hopes of finding an easy solution to the finite axiomatization problem for general terms over BPA_{int}; at the same time, however, it opens the way to such a solution in a special case. To better understand the possibilities 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, if t is a term over BPA and σ is a closed substitution, then the prenex normal form of σ(t), say ∑_{j∈J} t_{j}, 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, if t and u are terms over BPA such that t ∼ 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 the length of a word w over an alphabet A is the number |w| of characters (i.e., elements of A) occurring in w, while the number of occurrences of character a in word w is the number |w|_{a} of characters in w equal to a. Of course, |w| = ∑_{a∈A} |w|_{a}, and if w_{1} = w_{2}, then |w_{1}|_{a} = |w_{2}|_{a} for every a ∈ A.

Proposition 3.2 Let t and u be nonempty words over Act∪ Var.

1. If |Act| > 1 then t ∼ u iff t = u.

2. If Act= {a} then t ∼ u iff t is a permutation of u.

Proof: First of all, we recall that both points are true for closed 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. Suppose t ≠ u: then either |t| ≠ |u|, or t = λ_{1}αλ_{2}, u = λ_{1}βλ_{3}, with λ_{1}, λ_{2}, λ_{3} ∈ (Act∪ Var)^{∗}, α, β ∈ Act∪ Var, α ≠ β. 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, and b ∈ Act\ {a}, then σ_{b}(t) ≠ σ_{b}(u); otherwise, α and β are distinct variables, thus σ_{a}[β ↦ b](t) ≠ σ_{a}[β ↦ b](u). Therefore, if t ≠ u, then there exists a closed substitution σ such that σ(t) ≁ σ(u), so that t ≁ u.

We are now left with the proof of point 2 for general terms. Let σ be a closed substitution; let t a term with a single summand, let σ be a closed substitution, and let w_{1}, w_{2}, …, w_{n} ∈ Act∪ Var such that

t = w_{1}w_{2} … w_{n} .

By Theorem 2.2 and Lemma 2.3, for all j ∈ {1, 2, …, n} there exists a finite set I_{j} of integers such that

σ(w_{j}) ∼ ∑_{i_{j}∈I_{j}} a^{i_{j}}

Then, since complete trace equivalence is a congruence and distributivity laws apply modulo complete trace equivalence,

σ(w) ∼ σ(w_{1})σ(w_{2}) … σ(w_{n})
∼ ( ∑_{i_{1}∈I_{1}} a^{i_{1}} ) ( ∑_{i_{2}∈I_{2}} a^{i_{2}} ) … ( ∑_{i_{n}∈I_{n}} a^{i_{n}})
∼ ∑_{i_{1}∈I_{1},i_{2}∈I_{2},...,i_{n}∈I_{n}} a^{i_{1}}a^{i_{2}} … a^{i_{n}}
= ∑_{i_{1}∈I_{1},i_{2}∈I_{2},...,i_{n}∈I_{n}} a^{i_{1}+i_{2}+...+i_{n}}

which depends on the nature of the w_{j}’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 t is not a permutation of u, then either |t| ≠ |u| or there is a variable x such that |t|_{x} ≠ |u|_{x}, so that either σ_{a}(t) ≠ σ_{a}(u) or σ_{a}[x ↦ a^{2}](t) ≠ σ_{a}[x ↦ a^{2}](u); and again, t ≁ u. □

Proposition 3.2 suggests a strategy for finding an axiomatization for the terms over BPA_{int} when Act= {a}.

Consider an ordering Act∪ Var = {a, x_{1}, x_{2}, …, x_{n}, …}. Let w be a word over Act∪ Var and let n be the maximum index of a variable occurring in w. We define the normal form of w as

ν(w) = a^{|w|_{a}}x_{1}^{|w|_{x_{1}}} x_{2}^{|w|_{x_{2}}} … x_{n}^{|w|_{xn}} .  (7)

By Proposition 3.2, w ∼ ν(w).

Let now t be a term over BPA_{int}: by Proposition 3.1, t is complete trace equivalent to a term t′ over BPA, which, in turn, has a prenex normal form ∑_{w∈W} w. We can therefore say that the normal form of the term t is

ν(t) = ∑_{w∈W} ν(w) ,  (8)

where each summand in normal form is taken once per occurrence. For instance, the normal form of t = ya + xax + a ⊳ x is ν(t) = a + ax + ax^{2} + ay, while that of xy + yx is xy. We observe that ν(t) is unique, up to the order of summands, and that t ∼ ν(t).

Theorem 3.1 Suppose Act= {a}. Then two terms u, v over BPA_{int} are complete trace equivalent if and only if ν(t) = ν(u) up to the order of summands.

Proof: Let t and u be two terms over BPA_{int} such that t ∼ u, and let

ν(t) = ∑_{i=1}^{r} p_{i} and ν(u) = ∑_{j=1}^{s} q_{j}

be their normal forms. Let N be the maximum index of a variable in either the p_{i}’s or the q_{j}’s; then for each i and j we can write

p_{i} = a^{e_{0,i}}x_{1}^{e_{1,i}} … x_{N}^{e_{N,i}} and q_{j} = a^{f_{0,j}}x_{1}^{f_{1,j}} … x_{N}^{f_{N,j}} .

Let b be a positive integer greater than all of the e_{k,i}’s and the f_{k,j}’s; consider the substitution σ defined by

σ(x_{k}) = a^{b^{k}} ∀k ∈ ℕ .  (9)

Then, for all i and j, σ(p_{i}) = a^{α_{i}} and σ(q_{j}) = a^{β_{j}}, where

α_{i} = ∑_{k=0}^{N} e_{k,i}b^{k} and β_{j} = ∑_{k=0}^{N} f_{k,j}b^{k} ,

\begin{aligned}I0.1 & x ⊳ y & ≈ & x ⊳ y + x \\ I0.2 & x ⊳ y & ≈ & x ⊳ y + yx \\ I2 & xy ⊳ z & ≈ & x(y ⊳ z) + (x ⊳ z)y \\ I4 & (x ⊳ y) ⊳ z & ≈ & (x ⊳ y) ⊳ z + x ⊳ (y ⊳ z) \\ I5 & (x ⊳ y) ⊳ z + x ⊳ (z ⊳ y) & ≈ & (x ⊳ z) ⊳ y + x ⊳ (y ⊳ z) \end{aligned}

Table 3: A list of valid equations for BPA_{int}.

and since b is larger than all of the e_{k,i}’s and the f_{k,j}’s, the α_{i}’s are pairwise distinct, and so are the β_{j}’s.

Since t ∼ u, we have ν(t) ∼ ν(u) as well, so σ(ν(t)) ∼ σ(ν(u)). But a word w = a^{K} is a complete trace for σ(ν(t)) iff K = α_{i} for some i, and similarly, w is a complete trace for σ(ν(u)) iff K = β_{j} for some j: thus, for every i there must exist a j such that α_{i} = β_{j}, and vice versa. This, in turn, is only possible if for every i there exists j such that p_{i} = q_{j}, and vice versa; since the p_{i}’s are summands in a normal form, and so are the q_{j}’s, we conclude that r = s and the p_{i}’s are a permutation of the q_{j}’s, that is, ν(t) = ν(u) up to the order of summands.

The reverse implication is trivial. □

Theorem 3.2 If |Act| = 1 then BPA_{int} is finitely axiomatizable.

Proof: Consider the set E consisting of the axioms of Theorem 2.1 together with

\begin{aligned}CC & xy & ≈ & yx \\ DI & x ⊳ y & ≈ & x + yx \end{aligned}

(Observe that CC and DI are sound modulo complete trace equivalence iff |Act| = 1.) Let t and u be terms over BPA_{int} such that t ∼ u: we must prove that E ⊢ t ≈ u.

Consider the normal forms ν(t) and ν(u). Using equations CC and DI, it is not hard to prove that E ⊢ 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. □

4 Other valid equations

In this section, we will list some equations over BPA_{int}, and prove that they are all valid; plus, we will suggest a kind of “normal forms” for BPA_{int} terms. We use double quotes, because these, as we shall see, are not characterizing.

A list of valid equations for BPA_{int} is given in Table 3. We immediately observe that I0.1 and I0.2 are valid indeed, because, whatever t and u are, any complete trace for t or ut is also a complete trace for t ⊳ u

Proposition 4.1 Equation I2 in Table 3 is sound modulo complete trace equivalence.

Proof: We must show that, for every word w over the alphabet Act and every closed terms t, u, v over BPA_{int}, tu ⊳ v →^{w} ✓ if and only if t(u ⊳ v) + (t ⊳

v)u →^{w} ✓.

Suppose tu ⊳ v →^{w} ✓: this is the same as saying that w = xyz with z nonempty, tu →^{xz} ✓, and either y is empty or v →^{y} ✓. If t →^{x} ✓ and u →^{z} ✓, then t(u ⊳ v) →^{w} ✓; otherwise, either x = x′p with t →^{x′} ✓, or z = qz′ with t →^{xq} ✓, where p and q are suitable nonempty words. In the former case, u ⊳ v →^{pyz} ✓, so that t(u ⊳ v) →^{x′pyz} ✓ and x′pyz = w; in the latter case, u →^{z′} ✓ and t ⊳ v →^{xyq} ✓,

so that (t ⊳ v)u →^{xyqz′} ✓ and xyqz′ = w.

On the other hand, suppose t(u ⊳ v) + (t ⊳ v)u →^{w} ✓: then either t(u ⊳ v) →^{w} ✓ or (t ⊳ v)u →^{w} ✓. In the first case, w = rxyz with z nonempty, t →^{r} ✓, u →^{xz} ✓, and either y is empty or v →^{y} ✓. Then tu →^{rxz} ✓ and tu ⊳ v →^{rxyz} ✓; but rxyz = w. In the second case, w = xyzs with z nonempty, t →^{xz} ✓, u →^{s} ✓, and either y is empty or v →^{y} ✓. Then tu →^{xzs} ✓ and tu ⊳ v →^{xyzs} ✓; but xyzs = w. □

Observe how equation I2 generalizes I2.a to the case of a general concatenation of terms. In fact,

at ⊳ u ≈ a(t ⊳ u) + (a ⊳ u)t from I2 ,
≈ a(t ⊳ u) + (a + ua)t from I1.a ,
≈ a(t ⊳ u) + at + uat from A4.1 ,
≈ a(t ⊳ u) + uat  from I0.1 and A4.2 .

Proposition 4.2 Equation I4 in Table 3 is sound modulo complete trace equivalence.

Proof: We must show that, for every word w over the alphabet Act and every closed terms t, u, v over BPA_{int}, if t ⊳ (u ⊳ v) →^{w} ✓, then (t ⊳ u) ⊳ v →^{w} ✓.

Let t ⊳ (u ⊳ v) →^{w} ✓: then w = xyz with z nonempty, t →^{xz} ✓, and either y is empty or u ⊳ v →^{y} ✓. If y is empty, then w = xz is a complete trace for (t ⊳ u) ⊳ v; otherwise, y = pqr with u →^{pr} ✓ and either q is empty or v →^{q} ✓. Let

then x′ = xp, y′ = q, z′ = rz: then t ⊳ u →^{x′z′} ✓ and either y′ is empty or v →^{y′} ✓,

thus (t ⊳ u) ⊳ v →^{x′y′z′} ✓. But x′y′z′ = xpqrz = xyz = w. □

Equation I4 says that t ⊳ (u ⊳ v) is somewhat “less capable”, in terms of “possible terminating executions”, than (t ⊳ u) ⊳ v, something we had already seen after Theorem 2.2. The question arises naturally: how much is this “less”? Equation I5 provides a possible answer to this question.

Theorem 4.1 Equation I5 in Table 3 is sound modulo complete trace equivalence.

Proof: Suppose (t ⊳ u) ⊳ v →^{w} ✓. We know from Lemma 2.1 that w = xyz with t ⊳ u →^{xz} ✓ and either y is empty or v →^{y} ✓. From the same lemma we get xz = pqr with t →^{pr} ✓ and either q is empty or u →^{q} ✓. Thus four cases must be studied.

Case 1: y and q are both empty. In this case, the transition is entirely due to

t, thus t ⊳ (u ⊳ v) →^{w} ✓.

Case 2: y is empty and q is not. In this case, there is a transition t →^{p} t′, followed by u →^{q} ✓, then by t′ →^{r} ✓; plus, w = xz = pqr. This can be mimicked by t ⊳ (u ⊳ v) as follows:

t ⊳ (u ⊳ v) →^{p} t′ ⊳ (u ⊳ v) →^{q} t′ →^{r} ✓ ,

because if u →^{q} ✓ then u ⊳ v →^{q} ✓ as well.

Case 3: y is nonempty and q is empty. In this case, the transition is of the kind

(t ⊳ u) ⊳ v →^{x} (t′ ⊳ u) ⊳ v →^{y} t′ ⊳ u →^{z} ✓ ,

This cannot in general be mimicked by t ⊳ (u ⊳ v), because

t ⊳ (u ⊳ v) →^{x} t′ ⊳ (u ⊳ v) →^{y} ut ,

and ut might not have z as a complete trace. However, it can be mimicked by

t ⊳ v →^{x} t′ ⊳ v →^{y} t′ →^{z} ✓ ,

which is tolerable, because if t ⊳ v →^{w} ✓, then (t ⊳ u) ⊳ v →^{w} ✓ as well.

Case 4: y and q are both nonempty. This is the most complicated case, so we split it into subcases.

Subcase 4a: x = pq′, z = q′′r. This means that the execution of t is interrupted by that of u, which is in turn interrupted by that of v; that is, for some t′, u′,

(t ⊳ u) ⊳ v →^{p} (t′ ⊳ u) ⊳ v →^{q′} u′t′ ⊳ v →^{y} u′t′ →^{q′′} t′ →^{r} ✓ .

This can be mimicked by

t ⊳ (u ⊳ v) →^{p} t′ ⊳ (u ⊳ v) →^{q′} (u′ ⊳ v)t′ →^{y} u′t′ →^{q′′} t′ →^{r} ✓ .

Subcase 4b: x = pqr′, z = r′′. This means that the execution of t is first interrupted by that of u, then resumed, then suspended by that of v; that is,

(t ⊳ u) ⊳ v →^{p} (t′ ⊳ u) ⊳ v →^{q} t′ ⊳ v →^{r′} t′′ ⊳ v →^{y} t′′ →^{r′′} ✓ .

This cannot in general be mimicked by t ⊳ (u ⊳ v), because

t ⊳ (u ⊳ v) →^{p} t′ ⊳ (u ⊳ v) →^{q} t′ ,

and t′ might not have r′yr′′ as a complete trace.

Subcase 4c: x = p′, z = p′′qr. This means that the execution of t is first interrupted by that of v, then resumed, then suspended by that of u; that is,

(t ⊳ u) ⊳ v →^{p′} (t′ ⊳ u) ⊳ v →^{y} t′ ⊳ u →^{p′′} t′′ ⊳ u →^{q} t′′ →^{r} ✓ .

This cannot in general be mimicked by t ⊳ (u ⊳ v), because

t ⊳ (u ⊳ v) →^{p′} t′ ⊳ (u ⊳ v) →^{y} ut′ ,

and ut′ might not have p′′qr as a complete trace.

The problems come from subcases 4b and 4c. In fact, in (t ⊳ u) ⊳ v, the execution of t can either be first suspended by u, then resumed, then suspended by v; or be first suspended by v, then resumed, then suspended by u. On the contrary, in t ⊳ (u ⊳ v), if u interrupts t, then v can only interrupt u, and during this process, the execution of t cannot be resumed; while if v interrupts t, then t cannot be resumed until first v, then u are finished.

However, this behaviour can be mimicked by

(t ⊳ v) ⊳ u

by means of

(t ⊳ v) ⊳ u →^{p} (t′ ⊳ v) ⊳ u →^{q} t′ ⊳ v →^{r′} t′′ ⊳ v →^{y} t′′ →^{r′′} ✓

for case 4b, and

(t ⊳ v) ⊳ u →^{p′} (t′ ⊳ v) ⊳ u →^{y} t′ ⊳ u →^{p′′} t′′ ⊳ u →^{q} t′′ →^{r} ✓

for case 4c; plus, it also works in case 3. This means that we can write down

(t ⊳ u) ⊳ v ≼ (t ⊳ v) ⊳ u + t ⊳ (u ⊳ v)

where A ≼ B is a shortcut for CT (A) ⊆ CT (B). Moreover, by applying I4 to t ⊳ (v ⊳ u) and (t ⊳ v) ⊳ u, we can refine this inequality into

(t ⊳ u) ⊳ v + t ⊳ (v ⊳ u) ≼ (t ⊳ v) ⊳ u + t ⊳ (u ⊳ v)

But the roles of u an v are symmetrical on either side, thus we can swap these two terms and get the reverse inequality. □

Since, in general, (t ⊳ u) ⊳ v and t ⊳ (u ⊳ v) are not c.t.e., they should both be considered when looking for normal forms. For a term t containing a single summand, let us introduce a notion of leftmost term:

1. if the interrupt operator does not occur in t, then t is its own leftmost term;

2. if t = u ⊳ v, then the leftmost term of t is that of u.

For instance, the leftmost term of x ⊳ y, x ⊳ (y ⊳ z), and (x ⊳ y) ⊳ z, is always x, while the leftmost term of xy ⊳ z is xy.

Lemma 4.1 Every BPA_{int} term t can be written, modulo complete trace equivalence, as a sum of concatenations of singletons and sequences of interrupts where, in every subsequence, the leftmost term is a variable.

Proof: By induction on the structure of t. The cases t = a, t = x, and t = u + v with the thesis holding for both u and v obviously pose no problem.

Suppose t = uv with the thesis holding for v and v. Then

u≈ ∑_{i∈[1...n]} ∏_{j∈[1...n_{i}]} u_{i,j}

and

v ≈ ∑_{r∈[1...m]} ∏_{s∈[1...m_{r}]} v_{r,s}

with each u_{i,j} and v_{r,s} being either a singleton, or a sequence of interrupts where, in each subsequence, the leftmost term is a variable. Since concatenation is both left- and right-distributive modulo c.t.e. w.r.t. nondeterministic choice,

uv ≈ ∑_{\begin{matrix}i ∈ [1 … n] \\ r ∈ [1 … m] \end{matrix}} ( ∏_{j∈[1...n_{i}]} u_{i,j}) ( ∏_{s∈[1...s_{r}]} v_{r,s})

with each factor in each summand being either a singleton, or a sequence of interrupts where, in each subsequence, the leftmost term is a variable.

Suppose finally t = u ⊳ v with the thesis holding for u and v. Write u and v as in previous case, and put

v_{r} = ∏_{s∈[1...m_{r}]} v_{r,s} .

Since interrupt is both left- and right-distributive modulo c.t.e. w.r.t. nondeterministic choice,

u ⊳ v ≈ ∑_{\begin{matrix}i ∈ [1 … n] \\ r ∈ [1 … m] \end{matrix}} (( ∏_{j∈[1...n_{i}]} u_{i,j}) ⊳ v_{r}) .

But by repeatedly applying I2 we find

( ∏_{j∈[1...n_{i}]} u_{i,j}) ⊳ v_{r} ≈ ∑_{j∈[1...n_{i}]} u_{i,1} … u_{i,j−1} (u_{i,j} ⊳ v_{r}) u_{i,j+1} … u_{i,n_{i}}

where each factor in any of the right hand summands is either a singleton or a sequence of interrupts where, in each subsequence, the leftmost term is surely a singleton, but possibly not a variable. However:

• if u_{i,j} is a variable, then the thesis is still satisfied;

• if u_{i,j} is a sequence of interrupts, then again the thesis is satisfied by inductive hypothesis;

• finally, if u_{i,j} is a constant, then u_{i,j} ⊳ v_{r} = u_{i,j} + v_{r}u_{i,j}, and the thesis keeps on being satisfied, again by inductive hypothesis.

From this the thesis follows. □

The terms in the thesis of Lemma 4.1 are tentative candidates as normal forms for BPA_{int} terms. However, from that point of view, x ⊳ y and x ⊳ y + yx + x are different forms; but from what we have seen until now it is obvious that they are complete trace equivalent, so that these forms are unfortunately not characterizing. To solve these problem, a theory of “reduction” of terms should most probably be developed. At the time of the writing, we do not know whether the collection of equations in Theorems 2.1 and 3 is complete for complete trace equivalence over BPA_{int}.

A thing to do is probably to study the terms of the form x ⊳ t, which, because of Lemma 4.1, seem to be good candidates for basic constituents of normal forms. The idea should be that, if x ⊳ t ∼ y ⊳ u, then x = y and t ∼ u.

Let t and u be terms over BPA_{int}, not necessarily closed; let x and y be variables. Suppose x ⊳ t ∼ y ⊳ u: then x = y, otherwise, if σ(x) = a and σ(y) = b, then σ(x ⊳ t) →^{a} ✓ and σ(y ⊳ u) ↛^{a} ✓. Moreover, the maximum length of a complete trace for σ(t) and σ(u) must be the same: otherwise, by joining two complete traces of maximum length for either σ(t) or σ(u) and σ(x), we would get a complete trace for either σ(x ⊳ t) or σ(x ⊳ u), but not both. Lastly, t and u contain the same variables: otherwise, if N is larger than the length of any summand in t and u, then by substituting with b^{N} a single variable that does not appear in both t and u, and with a all other variables, we get two non-c.t.e. closed terms.

We are now left with the task of checking whether t ∼ u. This is not immediate, because, in general, t ⊳ u ∼ t ⊳ v does not imply u ∼ v: as a counterexample, put t = u = a + a^{2} and v = a^{2}.

Suppose x does not occur in t (and u). Suppose there exists a closed substitution σ such that σ(t) and σ(u) are not complete trace equivalent. Then σ[x ↦ a](x ⊳ t) ≈ a + σ(t)a and σ[x ↦ a](x ⊳ u) ≈ a + σ(u)a are not complete trace equivalent, because if (for example) w is a complete trace for σ(t) and not for σ(u), then wa is a complete trace for a + σ(t)a and not for a + σ(u)a.

Suppose now x does occur in t (and u). Again, suppose there exists a closed substitution σ such that σ(t) and σ(u) are not complete trace equivalent; in particular, let w ∈ Act^{+} be a complete trace for σ(t) and not for σ(u). How can we prove that there exists a closed substitution σ′ such that σ′(x ⊳ t) and σ′(x ⊳ u) are not complete trace equivalent?

We can reformulate our problem in terms of language theory. Call X the language of complete traces of σ(x), Y that of σ(t), and Z that of σ(u): then X, Y, and Z are finite languages. Saying that σ(x ⊳ t) ∼ σ(x ⊳ u), is then equivalent to saying that

X ∪ ⋃_{rs∈X,s≠ε} rY s = X ∪ ⋃_{rs∈X,s≠ε} rZs  (10)

for all X. We can then state

Conjecture 1 Suppose that, for every finite language X, equation (10) has a solution (Y, Z) with Y and Z finite. Then, for every finite language X, there is only one such solution.

If Conjecture 1 is true, then σ(x ⊳ t) ∼ σ(x ⊳ u) for all σ implies σ(t) = σ(u) for all σ.

References

[1] L. Aceto, W. Fokkink, R. van Glabbeek, and A. Ingolfsdottir, Nested semantics over finite trees are equationally hard, Information and Computation, 191 (2004), pp. 203–232.

[2] L. Aceto, W. Fokkink, and A. Ingolfsdottir, A menagerie of non-finitely based process semantics over BPA*—from ready simulation to completed traces, Mathematical Structures in Computer Science, 8 (1998), pp. 193–230.

[3] L. Aceto, W. Fokkink, A. Ingolfsdottir, and B. Luttik, CCS with Hennessy’s merge has no finite equational axiomatization, Theoretical Comput. Sci., 330 (2005), pp. 377–405.

[4] L. Aceto, W. Fokkink, A. Ingolfsdottir, and B. Luttik, Finite Equational Bases in Process Algebra: Results and Open Questions, in Processes, Terms, and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday A. Middeldorp, V. van Oostrom, F. Raamsdonk, R. Vrijer eds. vol. 3838 of Lecture Notes in Computer Science, Springer Verlag (2005), pp. 338–367.

[5] L. Aceto, W. Fokkink, A. Ingolfsdottir, and S. Nain, Bisimilarity is not Finitely Based over BPA with Interrupt, Theoretical Computer Science, 366(1–2):60–81, 2006. An extended abstract of this paper appeared in J. Fiadeiro, N. Harman, M. Roggenbach, and J. Rutten, eds., Proc. 1st Conference on Algebra and Coalgebra in Computer Science (CALCO’05), vol. 3629 of Lecture Notes in Computer Science, Springer Verlag (2005), pp. 52–66.

[6] J. C. Baeten and J. Bergstra, Mode transfer in process algebra, Report CSR 00–01, Technische Universiteit Eindhoven, 2000. This paper is an expanded and revised version of [9].

[7] J. C. Baeten, J. Bergstra, and J. W. Klop, Syntax and defining equations for an interrupt mechanism in process algebra, Fundamenta Informaticae, IX (1986), pp. 127–168.

[8] , Decidability of bisimulation equivalence for processes generating context-free languages, J. Assoc. Comput. Mach., 40 (1993), pp. 653–682.

[9] J. Bergstra, A mode transfer operator in process algebra, Report P8808, Programming Research Group, University of Amsterdam, 1988.

[10] J. Bergstra and J. W. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

[11] ISO, Information processing systems – open systems interconnection – LO-TOS – a formal description technique based on the temporal ordering of observational behaviour ISO/TC97/SC21/N DIS8807, 1987.

[12] S. Mauw, PSF – A Process Specification Formalism, PhD thesis, University of Amsterdam, Dec. 1991.

[13] R. Milner, Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

[14] R. Milner, M. Tofte, R. Harper, and D. MacQueen, The Definition of Standard ML (Revised), MIT Press, 1997.

[15] F. Moller, The importance of the left merge operator in process algebras, in Proceedings 17^{th} ICALP, Warwick, M. Paterson, ed., vol. 443 of Lecture Notes in Computer Science, Springer-Verlag, July 1990, pp. 752–764.

[16] , The nonexistence of finite axiomatisations for CCS congruences, in Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, 1990, pp. 142–153.

[17] D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.

[18] P. Sewell, Nonaxiomatisability of equivalences over finite state processes, Annals of Pure and Applied Logic, 90 (1997), pp. 163–191.

Recent BRICS Report Series Publications

RS-07-5 Luca Aceto, Silvio Capobianco, and Anna Ingólfsdóttir. On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt. February 2007. 26 pp.

RS-07-4 Kristian Støvring and Søren B. Lassen. A Complete, Co-Inductive Syntactic Theory of Sequential Control and State. February 2007. 36 pp. Appears in the proceedings of POPL 2007, p. 161–172.

RS-07-3 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. Ready To Preorder: Get Your BCCSP Axiomatization for Free! February 2007. 37 pp.

RS-07-2 Luca Aceto and Anna Ingólfsdóttir. Characteristic Formulae: From Automata to Logic. January 2007. 18 pp.

RS-07-1 Daniel Andersson. HIROIMONO is NP-complete. January 2007. 8 pp.

RS-06-19 Michael David Pedersen. Logics for The Applied π Calculus. December 2006. viii+111 pp.

RS-06-18 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. dec 2006. iii+39 pp. Extended version of an article to appear in TCS. Revised version of BRICS RS-05-22.

RS-06-17 Olivier Danvy and Kevin Millikin. A Rational Deconstruction of Landin’s J Operator. December 2006. ii+37 pp. Revised version of BRICS RS-06-4. A preliminary version appears in the proceedings of IFL 2005, LNCS 4015:55–73.

RS-06-16 Anders Møller. Static Analysis for Event-Based XML Processing. October 2006. 16 pp.

RS-06-15 Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. October 2006. ii+28 pp. Revised version of BRICS RS-05-16.

RS-06-14 Giorgio Delzanno, Javier Esparza, and Jiří Srba. Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. July 2006. 31 pp. To appear in ATVA ’06.