A Conservative Look at Term Deduction Systems withVariable Binding WanFokkink Department of Philosophy UtrechtUniversity Heidelberglaan 8, 3584 CS Utrecht, The Netherlands fokkink@phil.ruu.nl ChrisVerhoef Department of Mathematics and Computing Science Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands chrisv@win.tue.nl Abstract We set up a formal framework to describe term deduction systems, such a* *s tran- sition system specifications in the style of Plotkin,and conditional term * *rewriting systems. This framework has the power to express many-sortedness, general * *bind- ing mechanisms and substitutions,among other notions such as negative prem* *ises and unary predicates on terms. The framework is used to present a conservativity format in operational* * se- mantics, which statessufficient criteria to ensure that the extension of a* * transition system specification with new rules does not affect the behaviour of the o* *riginal terms. Furthermore,we show how general theorems in structured operational sema* *n- tics can be transformed into results in conditional term rewriting. We ap* *ply this approach to the conservativity theorem,which yields a result that is usefu* *l in the field of abstract data types. 1 Introduction A current method to provide pro cess algebras and specification languages with * *an oper- ational semantics is based on the use of structured operational semantics from * *Plotkin [34]. Given a set of states, the transitions between these states are obtained * *inductively from a transition system specification (TSS), which consists of transition rule* *s. Deducing desirable properties for transition systems generated by some TSS is* * often a technical and mechanic labour. Therefore, in recent years several general the* *ories for TSSs have been developed, for instance to discover which TSSs satisfy a cer* *tain congruence property [38; 11; 22; 21; 13; 4; 41; 16; 24; 10], or to study the me* *aning of negative premises [21; 13; 20], or to find which extensions of TSSs are operati* *onally conservative [22; 21; 13; 40].Our paper is devoted to this last topic. 1 Over and over again, process theories such as CCS[ 29], CSP[ 23]and ACP[ 8]ha* *ve been extended with new features, andthe original TSSs, which provide the semant* *ics for these process algebras,were extended with rules to describe these features.* *A ques- tion that arises naturally is whether or not such an extension influences the t* *ransition systems of terms in the originaldomain. Usually, it is desirable that an exten* *sion is (operationally) conservative, meaning that the provable transitions for an orig* *inal term are the same both in the original and in the extended TSS. Groote and Vaandrager [22] were the first to propose (in theorem 7.6) syntact* *ic re- strictions for the original TSSand for its extension, which automatically yield* * that the extension is operationally conservative. The restrictions are: all rules m* *ust be `tyft/tyxt',and the original rules must be `pure' and `well-founded' (see [22]f* *or the def- initions),and the rules in the extension must contain some new operatorin their* * source, i.e., in the left-hand side of their conclusion. Groote [21] adapted this conse* *rvativity format to the setting with negative hypotheses. Bol and Groote [13] showed that* * the tyft/tyxt restriction can be omitted. Finally, Verhoef[40]proposed more general syntactic criteria which ensure ope* *rational conservativity. Verhoef's criteria allow, under certainconditions, that a rule* * in the extension has an original term as its source. Examples of extensions that are w* *ithin the scope of Verhoef's criteria, but that donot fit the previous formats, are the e* *xtension of CCSwith time from Moller and Tofts [32],and BPA withdiscrete time from Baeten and Bergstra [3]. (In the current version of BPA with discrete time, the operat* *ional semantics has been adapted in such a way that the extension with discrete time * *is no longer operationally conservative over BPA.) In many practical cases, the format from [40]cannot yetb eapplied, due to the* * use of a typed signature,or the presence of some variable binding mechanism in the tra* *nsition rules. Familiar examples of such binding mechanisms are the expressionx:t from the -calculus, where the variable x is bound in the term t, and the construct t* *[s=x], where occurrences of the variable x in the term t are replaced by the term s. T* *his paper proposes a generalization of the conservativity format to transition rule* *s which may contain types and avariable binding mechanism. The syntactic requirements f* *rom Verhoef's format are generalized tothis setting. These generalizations make hea* *vy use of two different notions of free variables in terms; these notions will be intr* *oduced in due course. The syntactic criteria `pure' and `well-founded'on original rules w* *ill be relaxed to a more natural formulation, which we will call source-dependency. Wefound that several concepts in the setting of operational semantics with va* *riable binding,which seem to be intuitively clear at first sight,turn out to be ambigu* *ous when studied carefully.In order to obtain a formal framework in which transition rul* *eswith a variable binding mechanism can be expressed rigorously, we will elab orately * *discuss the preliminaries,presenting examples and introducing new notions on the way. M* *ost notably,we distinguish between actual and formal variables, following conventio* *ns from programming languages, and we formalize the construct t[s=x] in transition rule* *s. There is a strong link between the world of structured operational semantics * *and that of conditional term rewriting. Both fields deal with what can be viewed as* * `term deduction systems'.Terms are built from a set of function symbols,and binary re* *lations on terms (transitions versus rewrite steps) are defined by means of proof rules* * (transition 2 rules versus conditional rewrite rules). Such a rule,together with the validity* *,or non- validity, of a number of relationsb etween terms, may imply the validity of ano* *ther relation between terms. Hence,theorems in structured operational semantics also* * apply to the field of conditional rewriting. The link was already noted, but not expl* *oited, by Groote and Vaandrager [22](in example 3.5). We show that our conservativity res* *ults constitute useful lemmas in the field of conditional rewriting.Most notably, th* *e results are applicable in the field of abstract data types,which are often specified as* * modules of conditional term rewriting systems. Acknowledgements. We have benefited from technical discussions with Bard Bloom, Pedro D'Argenio, Arie van Deursen, Rob van Glabb eek, Douglas Howe, Aart Middel- dorp, Davide Sangiorgi, and Frits Vaandrager. 2 The Formal Framework In this section we recall some notions concerning general theoryof structured o* *pera- tional semantics, and we intro duce some new matters, interspersed with example* *s.We incorporate the notions of negative hypotheses from Groote [21] and predicates * *from Baeten and Verhoef [4]. We define a framework in which it is possible to expres* *s bind- ing mechanisms and substitutions. To thatend we will introduce two different ki* *nds of terms: actual ones and formal ones. Before we continue with the definitions,we * *give some intuition about those signatures and the framework. Some intuitions In many programming languages there are so-called actual param- eters and formal parameters. The formal parameters are used to define procedure* *sor functions; the actual parametersare the "real" variables to be used in the main* * program. In the main program the formal parameters are bound by the actual parameters. W* *hen discussing procedures on a conceptual level,it is often useful to introduce a n* *otational distinction between formal and actual parameters;see, for instance, [42].We wil* *l do the same in this paper: we think of a transition rule as a pro cedure to establish * *a transition relation by means of substituting (actual) terms for the (formal) variables. Si* *nce we will discuss transition rules on a conceptual level,we will make a clear distinction* * between actual and formal variables. Transition rules are built from terms that may con* *tain formal variables, and proofs for transitions are obtained by substituting actua* *l terms for formal variables in transition rules. We illustrate with the (nonsense) transition rule below that it is useful to * *make a notational distinction between actual and formal variables. y[x=x]!a z __________ y!b z Application of a substitution oe to this transition rule yields oe(y)[oe(x)=x]!a oe(z) __________________ oe (y)!boe (z ) 3 For instance, if oe(x) =c and oe(y )= x and oe(z) = d, then we obtain c!a d ______ x!b d We make two observations. 1. The expression y[x=x] is not asubstitution (for then it would equal y), bu* *t a syntactic construct with a suggestive form. We will call it a substitution* * harness. Only after application ofa substitution oe, the result oe(y)[oe(x)=x] can * *be evaluated to a term. 2. Substitutions only applyto part of the variables that occur in a transitio* *n rule. In order to distinguish such variables in a transition rule, we call them * *formal, and we mark them withan asterisk (*). Hence, the transition rule above takes the following form: y [x =x]!a z ____________ y! b z where x and x are unrelated. The distinctionof formal variables in structured operational semantics with v* *ariable binding was also propagatedindependently by Sangiorgi [36]and by Howe [24]. The* *re, they are called `meta-variables'. Now that we have an idea of the framework, we will first intro duce the notio* *n of actual terms (as opposed to formal terms), in which it is possible to express v* *ariable binding. Binding mechanisms exist in many and diverse forms, so we have chosen * *to describe these mechanisms as general as possible, in a notationally convenient * *way. We use a notational approach based on [2]; it is the notation for terms inthe Nupr* *l proof development system, see[14]. Our choice for the Nuprl notation, instead of for * *example the -calculus [6], is simply a matter of taste. 2.1 The actual world In this section we describe theactual world, which contains actual terms,actual* * sub- stitutions, and so forth. In the sequel, "Owill denote a sequence O1: :O:k, and* * "Oia sequence Oi1: :O:ik,with k 0. We note here that we do not need this k to be a finite number; infact, our results are also valid if k is an arbitrary cardinal* * number. However,since we did not find any applications for infinite cardinals, and sinc* *e we want to focus the discussion on more important and less trivial matters, we refrain * *from this generalization. Definition 2.1A (many-sorted) signature consists of a non-empty set of sorts, a set V of sorted actual variables v; w; x; y; z; : :,:and a set of function symb* *ols f :"S1:S1 "Sn:Sn ! S; where the Sijand the Siand S are sorts. 4 A function symbol of arity zero is called a constant. Definition 2.2 Let bea signature. The collection T() of (open) actual termss; * *t; : : : over is defined as the least set satisfying: -each actual variable from V is in T(), -for each function f : "S1:S1 "Sn:Sn ! S, f("x1:t1; : :;:"xn:tn) is an a* *ctual term of sort S, where - the actual terms ti are ofsort Si, - each "xiis a sequence of distinct actual variables xi1::x:imi,with xi* *jof sort Sij. We say that the actual variables "xiare bound in the ith argument of f . Definition 2.3 Free occurrences of actual variables in actual terms are defined* * as ex- pected: -x occurs free in x, -if x occurs free in ti, and x 62 f"xig, then x occurs freein f ("x1:t1; : * *:;:"xn:tn). As usual, an actual term is called closed if it does not contain any free occur* *rences of actual variables. In the sequel, T () denotes the collection of closed actua* *l terms p; q; : :o:ver. The notion of a substitution is also defined as expected. Definition 2.4 An actualsubstitution is a sort preserving mapping oe : V ! T(), where sort preserving means that x and oe(x) are always of the same sort. A sub* *stitution extends to a mapping from terms to terms as usual;the term oe(t) is obtained by* * replacing each free occurrence of a variable x in t by oe(x). As usual, _[t=x] is the postfix notation for the substitution that maps x to * *t and is inert otherwise. Such postfix denoted substitutions will be called explicit actual su* *bstitutions (as opposed to implicit actual substitutions oe). In the definition of substitutions on actual terms there is a well-known comp* *lication. Namely, consider a term oe(t), and let x occur free in t.After x in t has been * *replaced by oe(x), variables ythat occur in oe(x) are suddenly bound in subterms such as f(* *y:s) of t. A solution for this problem,which originates from the -calculus, is to allow un* *restricted substitution by applying ff-conversion, that is, byrenaming bound variables. I* *n the sequel, actual terms are considered modulo ff-conversion, and when a substituti* *on is applied, bound variables are renamed. Stoughton [39] presented a nice treatment* * of this technique. Remark 2.5 Bloom and Vaandrager [12]develop a framework for transition rules * *with types and a binding mechanism, in whichthey make a clear distinction between so* *rts for processes and sorts for data. We have chosen not to adopt this distinction,* * since it is not of interest for the question whether an extension of transition rules in* *fluences the behaviour of original process terms. We consider data as processes that do not * *display any behaviour. 5 2.2 The formal world We argued that it is often a good idea to distinguish between formal and actual* * variables, when discussing transition ruleswith variable bindings and substitutions on an * *abstract level. This isalso convenient in order to distinguish the variables towhich a s* *ubstitution applies. We introduce the notion of a formal term t ,being an actual term with * *possible occurrences of formal variables and substitution harnesses. Assume a signature , consisting of a non-empty set of sorts, a set V of varia* *bles, and a set of function symbols.The set V of formalvariables is defined as fx j * *x 2 V g, where x and x are of the same sort. Definition 2.6The collection F() of formal terms over a signature is the least* * set satisfying: - each actual variable from V is in F(), - each formal variable from V is in F(), - for each functionsymbol f : "S1:S1 "Sn:Sn ! S, f("x1:t1; : :;:"xn:tn) * *is a formal term of sort S, where - the formal terms tiare of sort Si, - each "xiconsists of distinct actual variables in Vof sorts "Si. - If s and t areformal terms of sorts S0 and S1 respectively,and x 2 V is * *of sort S1, then t [s =x] is a formal term of sort S0. Definition 2.7A formal substitution is a sort preserving mapping oe : V ! T(). It extends to a mapping oe : F() ! T() as expected; the term oe (t) is obtained from t by replacing each formal variable x in t by oe (x ), after which the s* *ubstitution harnesses become explicit actual substitutions. The result evaluates toa term i* *n T(). Example 2.8 An example of a formal term is y [z =x],which evaluates to the act* *ual term a after application of a formal substitution oe with oe (y ) = x and oe (* *z) = a. Namely,the implicit formal substitution oe turns the substitution harness y [z * *=x] into the actual term x[a=x], where_[a=x] is an explicit actual substitution, which e* *valuates to a. Summarizing the various substitutions At this point we have introduced all the substitutions and the substitution harness. We summarize the various notions, * *and briefly discuss their differences. There are four notions in two worlds: the i* *mplicit and explicit actual substitutions (which are semantically the same), and the fo* *rmal substitutions and the substitution harnesses. fflImplicit actual substitutions oe and explicit actual substitutions_[t=x] * *both denote mappings from actual variables to actual terms. fflFormal substitutions oe are mappings from formal variables to actual ter* *ms. 6 fflA substitution harness t [s =x] is nota substitution, but a piece of synt* *ax with a suggestive form. Ifwe apply a formal substitution oe to it, the result* * isan expression oe (t )[oe (s )=x], containing an explicit actual substitution,* * so that it can be evaluated to an actual term. Substitution harnesses are used to formulate ina precise way how a formal sub* *stitution is to act on a transition rule. The actual and formal substitutions are used to* * move from transition rules to a proof tree. 2.3 Actual and formal transition rules We now know what the framework looks likemore or less. We have described the intuition behind the use of structured operational semantics with variable bind* *ing and substitution harnesses. We shall now formalize what that intuition is,in order * *to be able to discuss the theory of structured operational semantics on anabstract le* *vel, and to give a rigorous presentation of our conservativity result. Before we present the formal definitions ofstructured operational semantics, * *first we consider as an example the well-known recursive -construct, which combines form* *al variables, a binding mechanism and a substitution harness. This transition rul* *ewill serve as a running example. Example 2.9 Intuitively, the term x:p executes p until itencounters an expres* *sion x, in which case it starts to executex:p again. This intuition can be expressed* * in the following transition rule, which we will call the -rule: y [x:y =x]!a z _______________ x:y! a z We recall that formal variables are markedwith an asterisk (*) in order to avoi* *d no- tational confusion. Note that the variable x in the -rule does not carry an ast* *erisk, because we want to bind actual variables to actualterms in the end. For the -co* *nstruct we have x:ax!a x:ax where a_ is the well-known action prefix operator from CCS. The -rule is a reci* *pe to achieve transitions like the one above.We derive this transition from the -rule* * together with the well-known rule for the prefix operator: aw! aw . After application of* * a formal substitution oe to the -rule with oe (y ) = ax and oe (z ) = x:ax, the hypothe* *sis takes the form ax[x:ax=x]!a x:ax,which evaluates to ax:ax!a x:ax. Since this is an instance of the rule for the prefix operator, with x:ax for w ,we may conclu* *de that the oe instantiation of the conclusion of the -rule is valid: x:ax!a x:ax. Now, we will introduce the basic notions of structured operational semantics.* * We assume a signature , and a set D of relation and predicate symbols R; S; :.: : Definition 2.10 Let t0; : :;:tn be terms over some signature. -For R a relation, the expression t0R(t1; : :;:tn1 )tn is a positive transi* *tion. 7 - For Ra predicate, the expression t0R(t1;: :;:tn1 ) is a positivetransition. - For Ra relation or a predicate, the expression t0:R(t1; : :;:tn1) is a neg* *ative transition. A transition is cal led closed if it involves only closed actual terms. Weallow the possibility to attach terms to relations and predicates,because o* *f the fact that nowadays many transition rules use parametrized labels. We will see an exa* *mple of such a parametrized label, inthe setting of the ss-calculus from Milner, Par* *row and Walker[31], in example 2.14. Definition 2.11An actual (transition) rule is an expression of the form H=c,whe* *re H is a collection of positive and negative transitions over an actualsignature,* * and c is a positive transition over an actual signature. Example 2.12 An example of an actual rule that we met already is ax:ax!a x:ax _______________ x:ax!a x:ax It can be deduced from the -rule, see example 2.9, which is an example of a for* *mal rule. Actual transition rules are deduced by means of formal transition rules. The * *formal rules are the ones that wemeet in the literature; they are the recipes that all* *ow usto deduce the transition relation.We recall that it is our aim to make this recipe* * practice (more) precise, in order to be able to discuss properties of such rules on an a* *bstract level. Definition 2.13A formal (transition) rule is an expression of the form H =c, wh* *ere - H is a collection hypotheses of the form t0R(t1; : :;:tn1 )tn and t0R(t1; * *: :;:tn1 ) andt0:R(t1; : :;:tn1 ), - c is the conclusion of the form t0R(t1; : :;:tn1 )tn ort0R(t1; : :;:tn1 ), where t0; :;::tn are formal terms. A transition system specification (TSS) is a collection of formal rules. Wegive an intricate example of a formal transition rule PREfrom the ss-calcul* *us, which incorporates bound variables and parametrized labels. Example 2.14 Assume two sorts Port of port names and Process of processes. For actual variables x andy of sort Port we have the following transition rule: PRE x(y):v x(y)!v 8 where v is a formal variable of sort Process. The rule PREexpresses that term * *x(y):p sends port name y via port x,and proceeds as p. There is a subtle distinction b* *etween the two occurrences of y in PRE; in x(y):v it is a binder of v , whilein the la* *bel it is a free parameter. A notation of PRE in the vein of thispaper would be send(x;y:v ) (x;y)!v From PRE we can deduce x(y):t x(w)!t[w=y] for actual terms t of sort Process wh* *ich do not contain any free occurrence of the actual variable w of sort Port. Namel* *y,PRE yields x(w):t[w=y] x(w)!t[w=y], and if w does not occur free in t, then x(w ):t* *[w=y ]is ff-convertible to x(y):t. In example 2.9 we already saw that a TSSis used to prove that certain transit* *ions hold. Now we give the precise definition of apro of from a TSS. Definition 2.15 A proof from a TSS T of an actual rule H=c consists of an upwar* *dly branching tree in which all upward paths are finite, where the nodes of the tre* *e are labelled by transitions such that: fflthe root has label c, fflif some node has label l, and K is the set of labels of nodes directly ab* *ove this node, then 1. either K= ;, and l 2 H, 2. or K=lis a formal substitution instance of a formal rule in T. A proof is called closed if all its labels are closed transitions. Example 2.16 In example 2.9 we saw that the transition x:ax!a x:ax can be pro* *ved from the TSS containing the rule for prefixing from CCS and the-rule. This proo* *f is depicted in Figure 1. Remark 2.17 Provability of an actual rule may depend in an essential way on t* *he fact that terms are considered modulo ff-conversion. For example, this was the * *case in example 2.14, where the transition x(y):t x(w)!t[w=y], with w 6=y not free in t* *, could only be proved by ff-conversion of x(y):t to x(w):t[w=y]. 2.4 On substitution instances of pro ofs Due to the fact that substitution harnesses are allowed too ccurin formal rules* *, the actual substitution instance of a proof need not be a proof again. This complic* *ation may arise in case the proof involves formal rules thatcontain two kinds of occu* *rrences of one formal variable: one in a free context and the other in a bound context.* * We give an example. 9 8 >>> ; >>> < instance of prefixing rule > >>> >>: a:x:ax!a x:ax 9>> >>> = >>>instance of -rule >>; x:ax!a x:ax Figure 1: A proof for x:ax!a x:ax Example 2.18 Let a and b be constants, andassume a predicate #. Consider the T* *SS that consists of the following formal rules: y [a=x]# y # a# ________ ________ y # y [b=x]# Note that in the last two rules, the formal variable y occurs b oth in a free * *and in a bound context. By substitutingx for y in the last two formal rules, we obtain the actual ru* *les a#=x# and x #=b # respectively. Hence, the transitionb # is provable from the TSS. Ho* *wever, it is not hard to see that theredo es not exist a closed proof for b#. 2.5 Stable models Up to now we have ignored the presence of negative hypotheses in the hypotheses* * of the rules in a TSS. It is well-known that when there are negative hypotheses around* * it is no longer straightforwardto define a sensible transition relation. We will use the* *notion of a stablemodel for a TSS, which stems from Gelfond and Lifschitz [18], in the se* *tting of logic programming,and which was adapted to structured operational semantics by * *Bol and Groote [13]. See Van Glabbeek [20] foran overview of other possibilities to* * give meaning to negative hypotheses in a TSS. We follow the approach in [20]and we a* *dapt it to the present situationwith predicates around. Definition 2.19A collection of negative transitions H holds for a set of positi* *ve tran- sitions M, denoted by Mj= H, if for each t:R(t1; : :;:tn1 ) 2 H wehave - either t0R(t1; : :;:tn1 )tn62 M for all actual terms tnif R is a relation. - or t0R(t1; : :;:tn1 ) 62 M if Ris a predicate. Definition 2.20A collection of positive transitions M is a stable model for a T* *SST , if the elements of M areexactly those positive transitions c for which there ex* *ists an actual rule H=c such that: 10 fflthere is a proof from T forH =c, fflH contains only negative transitions, fflM j= H. Similarly, we can define the notion of a closed stable model for a TSS. Definition 2.21 A col lection of closed positive transitions M is a closed stab* *le model for a TSS T, if the elements of M are exactly those closed positive transitions* * c for which there exists an actual rule H=c such that: fflthere is a closed proof fromT for H=c, fflH contains only closed negative transitions, fflM j= H. There exist TSSs which allow several (closed) stable models. Example 2.22 Assume two constants a and b, and a predicate R. The TSS that consists of the formal rules b:R=aR and a:R=bR allows two stable models, namely faRg and fbRg. The following example shows that the closedtransitions in a stable model of a* * TSS do not always make out a closed stable model of this TSS. Example 2.23 The TSSin example 2.18 allows one stable model faR;bRg and one closed stable model faRg. The closed transition bR isnot present in the closed * *stable model since it cannot be deduced by a closed proof. We will prove a conservativity result both for stable models and for closed s* *table models. Due to the fact that the substitution instance of a proof from a TSS i* *s not always a proof from this TSS, the conservative extension theorem for stable mod* *els does not immediately imply the same result for closed stable models. Fortunatel* *y, the conservative extension theorems for the open and for the closed case can be pro* *ved in exactly the same way,the only difference being that the proofs involve open and* * closed actual terms respectively. Remark 2.24 Van Glabbeek [20] argues that the best way to give meaning to TSSs with negative hypotheses is through the notion of completeness. For this purpos* *e, the notion of provability is extended in order to allow the derivation of negative * *transitions. Then, a TSS is said to be complete if for eachclosed transition p!a p0, the TSS* *can prove either p!a p0or its negation p6a!p0. Our conservativity result for closed stable models applies to complete TSSs a* *s well. Namely, if a TSS is complete, then it allows a unique closed stable model, whic* *h consists of the closed transitions that are provable from the TSS, see [20]. 11 3 A General Conservative Extension Theorem In this section,we present our theorem concerning conservative extensions. Firs* *t,we define in a precise waywhat is a conservative extension; wedistinguish between * *closed and open conservative extensions. Then a string of technical definitions will l* *ead to the formulation of the main theorem. 3.1 Well-defined sums In order to be able to combine two TSSs, we need to know that the functionsymbo* *ls in the intersection of their signatures have the same functionality in both sig* *natures. Furthermore,if a relation or predicate symbol occurs in the two TSSs,then it sh* *ould be either a relation or a predicatesymbol in both TSSs. Therefore, we introduce* * the notion of a well-defined sum oftwo TSSs. Definition 3.1 fflLet 0 and 1 be signatures. Their sum (or union) 01 is well-defined if each function symbol and each variable in 0" 1 has thesame functionality in both signatures. fflLet D0 and D1 be sets of relations and predicates symbols. The sum (or u* *nion) D0D1is well-defined if each element in D0"D1is either a relation or a pred* *icate in both col lections. fflLet T0 and T1 be TSSs over (0; D0) and (1; D1) respectively. Their sum (or union) T0 T1 is well-defined if both 0 1and D0 D1are well-defined. 3.2 Conservative extension In the remainder of this sectionwe assume two TSSs T0 and T1 over (0;D0) and (1;D1) respectively, where T0T1 is well-defined. Definition 3.2T0 T1 is an open (operationally) conservative extension of T0 if * *for each stable model M for T0 T1, the collection ft0R(t1; : :;:tn1 )tn; t0R(t1; : :;:tn1 ) 2 M j t02 T(0)g is a stable model for T0. Definition 3.3T0 T1 is a closed (operationally) conservativeextension of T0 if * *for each closed stable model M for T0 T1, the collection fp0R(p1; : :;:pn1 )pn; p0R(p1; : :;:pn1) 2 M j p0 2T (0)g is a closed stable modelfor T0. Before we can formulate under what conditions T0 T1is both a closed and an op* *en conservative extension of T0, first we need to present several auxiliary defini* *tions. 12 3.3 New formal terms and new relations A formal term in F(1) is called newif it incorporates a function symbol from 1n0 outside its substitution harnesses. This is stated more precisely in the defini* *tion below. Definition 3.4 The formal terms in F(1) that are new are defined inductively as follows: -f("x1:t1; : :;:"xn:tn) is new if f2 1n0, or if some tiis new, -t [s =x] is new if t is new. Example 3.5 Let 0 = fa;fg and 1 = fbg,where a; b are constants and f is of ar* *ity one. Then f(x:b[a=y]) is new, but f(x:a[b=y]) is not new. Definition 3.4 is motivated by the following observation. Lemma 3.6 t is new ) oe (t ) 62T(0). Proof. By induction on the size of t . Definition 3.7 Relations and predicates are called new if they are in D1nD0. 3.4 The collections FV (t ) and EV (t ) F V(t ) denotes the collection of formal variables that occur in the formal ter* *m t . Definition 3.8 The collectionsF V(t ) are defined inductivelyas fol lows. F V(x ) = x , F V (f("x1:t1; : :;:"xn:tn)) = F V(t1) [ : :[:F V (tn), F V (t [s =x]) = FV (t ) [ F V(s ). Example 3.9 FV(f(v:x [y =w])) = fx ; yg. Lemma 3.10 For formal terms t 2 F(0) we have oe (x ) 2 T(0) for alxl 2 FV(t ) ) oe (t ) 2 T(0): Proof. By induction on the size of t . The converse of lemma 3.10 does not hold. Namely, if oe (t ) 2 T(0),then it is * *possible for formal variables y that occur inside a substitution harness in t that oe (y* * ) 62 T(0). This is illustrated by the following example. Example 3.11 Let 0 = fagand 1 = fbg, where a and b are constants, and let oe (x ) = a and oe (y ) = b. Thenoe (x [y =z]) = a 2 T(0), but oe (y ) = b 62 T* *(0). 13 In order to obtain a result converse to lemma 3.10, we define a second, more re* *strictive collection EV(t ) of formal variables in a formal term t , which does not take * *into account formal variables that occur inside a substitution harness. Definition 3.12The collections EV (t )are defined inductively as follows. EV(x ) = x , EV(f ("x1:t1; : :;:"xn:tn)) = EV(t1) [ : :[:EV (tn), EV(t [s =x]) = EV (t ). Example 3.13 EV (f(v:x [y =w])) = fx g. The definition of EV(t ) is motivated by the following observation, which isthe* * converse of lemma 3.10, with FV replaced by EV. Lemma 3.14 oe (t ) 2 T(0) ) oe (x) 2 T(0) for all x 2EV (t ). Proof. By induction on the size of t . 3.5 Source-dependency Definition 3.15The formal term at the left-hand side of the conclusion of a for* *mal rule is called the source of the formal rule. Weadapt the syntactic criterion `pure and well-founded' for transition rules * *from Groote and Vaandrager [22] to a more liberal form, which we call source-depende* *ncy. This definition uses the two distinct notions FV and EV of formal variables i* *n for- mal terms. In the setting without variable bindings,this notion was also discov* *ered independently by Van Glabbeek [19]and by Howe [24]. Definition 3.16For a formal rule r , its collection of source-dependent formal * *vari- ables SV(r ) is defined inductively as follows. - If t is the source of r , then EV(t ) SV (r). - If t0R(t1; : :;:tn1 )tn is a hypothesis of r and FV (t0) SV (r ), thenEV* * (ti) SV(r ) for i = 1; : :;:n. - If t0R(t1; : :;:tn1 ) is a hypothesis of r and FV (t0) SV (r ), then EV (* *ti) SV(r ) for i = 1; : :;:n 1. r is source-dependent if the formal variables that occur in r are all in SV (r). Example 3.17 We display the -rule, which was introduced in example 2.9. y [x:y =x]!a z _______________ x:y !a z 14 The variables in the -rule are all source-dependent. Namely,y and z are the o* *nly formal variables that occur in the -rule. Since EV(x:y ) = fy g, we find that y* * is source-dependent. Since F V (y [x:y =x]) = F V (y ) [ F V(x:y ) = fy g; and since the -rule contains a premise y [x:y =x]!a z ,and since EV (z ) = fzg,* * it follows that z is source-dependent. We will see later on that source-dependencyis an essential ingredient of the * *conser- vativity theorem. Namely,in order to conclude that an extended TSS is operation* *ally conservative over an original TSS, it is necessary that the rules in the origin* *al TSS are source-dependent. In practical cases, this criterion is sometimes neglecte* *d. For example, Nicollin and Sifakis [33] consider an extended TSS in which each rule * *in the extension contains a new operator in its source,and from this fact they conclud* *e that the extension is operationally conservative. In general however, this character* *istic is not sufficient, as is shown in the next example. Example 3.18 Let 0 =fag and 1 = fbg, where a and b are constants, and let # be a predicate. Consider the TSS over 0 that consists of the rule x #=a#. Note tha* *t the formal variable x in this rule is not source-dependent. Extend this TSS withth* *e rule b #, which contains the new constant b in its source. Then a# holds in the exte* *nded TSS, but not in the original one, so this extension is not operationallyconserv* *ative. 3.6 The formal rule ae(r ) Definition 3.19 For each formal rule r in T0T1, ae(r ) denotes the formal rule* * that consists of the conclusion from r ,together with those hypotheses from r for w* *hich the term at the left-hand side is in F(0). Example 3.20 Let 0 =fag and 1 = fbg, where a and b are constants, andlet # and " be predicates. If r is the rule a# b # ________ b" then ae(r ) is a# =b". Note that if r 2 T0, then ae(r ) = r , simply because in this case all terms i* *n r are in F(0). 3.7 The main theorem Recall that we assume two TSSs T0 and T1 over(0; D0) and (1;D1) respectively, where T0 T1 is well-defined. Theorem 3.21 formulates sufficient criteria for T0* * T1 to be a closed conservative extension of T0. As a corollarywe will find that th* *e same criteria ensure that T0 T1is an open conservative extension of T0. 15 Theorem 3.21 Under the following conditions, T0T1 is a closed conservative ex* *ten- sion of T0: 1. T0is source-dependent, 2. for each r 2 T1, ffleither the source of r is new, fflor r has a hypothesis ofthe form t0R(t1; : :;:tn1 )tn or t0R(t1; : :* *;:tn1 ), where - t02 F(0), - FV (t0) SV (ae(r )), - R orone of the terms t1; : :;:tn is new. In the proof of thisconservativity theorem we will apply induction on the sou* *rce- distance of a formal variable x in a formal rule r, being the minimal number o* *f steps it takes to deduce that x is source-dependent in r . Definition 3.22Assume a formal rule r . For a formal variable x 2 SV (r), its sourcedistance sd(r ; x) in r is defined as follows. - If t is the source of r and x 2EV (t ),then sd(r ;x ) n holds for all na* *turals n. - If t0R(t1; : :;:tn1 )tn is a hypothesis of r , and sd(r ;x ) n holds for * *all x 2 FV (t0), then sd(r ;y ) n + 1 holds for all y 2 EV (t1) [ ::[:EV (tn). - If t0R(t1; : :;:tn1 ) is a hypothesis of r ,and sd(r ; x) n holds for all* * x 2 FV (t0), then sd(r ;y ) n + 1 holds for all y 2 EV (t1) [ ::[:EV (tn1 ). Finally, sd(r ;x ) = n if n is the smallest number such that sd(r ; x) n. Proof of theorem 3.21. Fix a closed stable model M for T0 T1. We show that N =fp0R(p1; : :;:pn1 )pn; p0R(p1; : :;:pn1 ) 2 M jp0 2T (0)g is a closed stable model for T0. 1. Assume that there is a closed proof from T0 for a closed actual rule H=c,w* *here H contains only negative transitions, and N j= H. We show that c 2 N. Since T0 proves H=c, clearly H and c involve only actual terms from T(0). Furthermore,the closed proof for H=c from T0 is also a proof from T0T1. Consider a p0:R(p1; : :;:pn1 ) in H. Since Nj= H,either p0R(p1; : :;:pn1 )* *pn 62 N for all actualterms pn 2T (01) (if R is a relation),or p0R(p1; : :;:pn1 * *) 62 N (if R is a predicate). Since H involves only actual terms from T (0), in particular p02 T(0). Thus,by definition of N, either p0R(p1; : :;:pn1 )pn6* *2 M for all pn2 T(0 1), or p0R(p1; : :;:pn1 ) 62 M, respectively. Hence, we may 16 conclude that M j= H. Since M is a closed stable model for T0 T1, and there is a closed proof from T0 T1for H=c, this implies c 2 M. Since c contains only actual terms from T(0), in particular its left-hand sid* *e is in T (0), and so c 2 N . 2.Fix a transition p0R(p1; : :;:pn1 )pn in N. We show that there is a closed pr* *oof from T0 for an actual rule H=p00R(p01;: :;:p0n1)p0n,where H consists of negat* *ive transitions and N j=H and p0iis ff-convertible to pi for i = 1; : :;:n. (Simi* *larly it can be proved that for each transition p0R(p1; : ::;pn1 ) in N there is ac* *losed proof from T0 for an actual rule H=p00R(p01; : :;:p0n1), where Hconsists of n* *egative transitions and N j=H.) Since N M, the transition p0R(p1; : :;:pn1 )pnis also in M, which is a stable model for T0 T1. So there exists a closed proof P from T0 T1 for a closed actual rule H=p00R(p01; : :;:p0n1)p0nwhere H consists of negative transitions* *, and M j= H and p0iis ff-convertible to pi for i = 1; : :;:n. SinceN M, M j= H implies N j=H. Remains to prove that P is a proof from T0, which we will do by ordinal induction A on the length of P. Let P have length ff,and suppose that we have already proved the case for ord* *inals smaller than ff. The last step in Pis constituted by a formal rule r 2 T0T1wi* *th a conclusion of the form t0R(t1; : :;:tn1 )tn together with a formal substitu* *tion oe : V ! T (01), where oe (t0) = p00. First, we show that oe (x ) 2 T (0) for all x 2 SV(ae(r )),by induction B on * *the source distance of x inae(r ) (see definition 3.22). (a) sd(ae(r); x ) = 0. This means that x 2 EV(t0). Since oe (t0) = p00is in T(0), lemma 3.14 yieldsoe (x ) 2 T(0). (b) sd(ae(r); x ) = k+1. By definition there is a hypothesis s0S(s1; : :;:sm1 )sm ors0S(s1; : :;* *:sm1 ) of ae(r) such that x 2 EV(si) for some i = 1; : :;:m and sd(ae(r); y ) * * k for ally 2 FV (s0). Induction Bimplies that oe (y ) 2 T (0)for all y 2 FV(s0). Furthermore, definition 3.19 of ae(r ) ensures thats0 2 F(0), so lemma 3.10 yields oe (s0) 2 T (0). The transitionoe (s0S(s1; : :;:sm1 )s* *m) or oe(s0S (s1; : :;:sm1 ) is proved by a strict sub-proof of P,so then o* *rdinal induction A implies that T0 proves this transition. In particular,oe (si* *) 2 T(0) for i = 1; : :;:m. Since x 2 EV(si) for some i = 1; : :;:m, lemma 3.14 yields oe (x ) 2 T (0). Next, we show that r is in T0. Suppose not, so let r 2 T1; we deduce a con- tradiction. Since oe (t0) = p00is in T(0), lemma 3.6 implies that t0is not ne* *w. Then by assumption there is a hypothesis in r of the form s0S(s1; : :;:sm1 )* *sm or s0S(s1; : :;:sm1 ), where either S or some sifor i = 1; : :;:mis new, and s0 2F(0), and FV (s0) SV(ae(r )). 17 If siis new for some i = 1; : :;:m,then lemma 3.6 says that oe (si) 62 T(0* *). Hence, since either Sis new or oe (si) 62 T(0) for some i = 1; : :;:m, the sub-pr* *oof of P of H=oe (s0S(s1; : :;:sm1 )sm ) or H=oe (s0S(s1; : :;:sm1 )) cannot be a p* *roof from T0. So according to ordinal induction A, oe (s0)62 T (0). Sinces02 F(0), l* *emma 3.10 yields oe (x )62 T (0) for some x 2 FV (s0) SV(ae(r )). Contradictio* *n. So apparently r is in T0. Then ae(r ) = r (see Section 3.6),so oe (x ) 2* * T(0) for all x 2 SV(r ). By assumption T0 is source-dependent,so the formal variabl* *es in r are all in SV (r ).Hence, oe (x ) 2 T (0) for all x in r . Thus,oe (r ) involves only actual terms in T(0). In particular,for each po* *sitive hypothesis h in r , the left-hand side of oe (h ) is in T (0). Then induct* *ion A says that the sub-proof of P for H=oe (h ) is a proof from T0. Since the l* *ast step (with r and oe ) is in T0 too, Pis a proof from T0. * * 2 Under the conditions from theorem 3.21, T0 T1 is not only aclosed conservative extension,but also an open conservative extension of T0.We formulate this in th* *e next corollary. Corollary 3.23 Under the conditions from theorem 3.21, T0T1 is an open conserva- tive extension of T0. Proof sketch. Consider free occurrences of actual variables in actual terms as * *con- stants. Then open actual terms and proofs become `closed', so that the conserva* *tivity result for closed stable models applies. 2 4 Applications In this section we will give the reader an idea of the range of applications of* * our results. For a start,we wish to mention that Baeten and Verhoef [5] and Aceto,Bloom and Vaandrager[1]give several applications of our conservativity result in the case* * of oper- ational semantics without types and binding mechanisms. Some systems with varia* *ble binding mechanisms to which our results can be applied are CCS from Milner [29]* *, CSP from Hoare [23], the ss-calculus from Milner, Parrow and Walker [31], andACP wi* *th real-time as proposed by Fokkink and Klusener [17], to mention a few. First, we will focus on a process algebra application with both types and var* *iable binding: the ss-calculus. Then we will devote our attention to the formulation * *of our results in conditional term rewriting; here also we will give examples. 4.1 An application in the ss-calculus We show how our conservativity results can be applied to a TSS fromthe literatu* *re that incorporates both types and variable binding. Weopt for the ssI -calculus* * from Sangiorgi[37], which is a subset of the full ss-calculus. Basically, one could * *say that the ssI-calculus is made out of CCScombined with ff-conversion. The transition rule* *s for the ss-calculus as defined in [30]satisfy our criteria too, so our conservativi* *ty results can be applied to this formalism just aswell. However, we prefer ssI over ss here, * *because it 18 has a simpler operational semantics, and we want to keep this exposition as smo* *oth as possible. We already encountered the ssI-calculus,and its transition rule PRE, briefly * *in ex- ample 2.14. We will now explain its syntax and semantics in more detail. Recall* * that there are two sorts Port and Process. Process terms are defined by the followin* *g BNF grammar: t ::= 0 j x(y):t j x(y):t j t + t j tjt j x t where 0 and t are terms of sort Process,and x and y areactual variables of sort* * Port. As usual, t + t0denotes the alternativecomposition an tjt0the communication merge.* * The process x(y):t sends, and the process x(y):t reads, port name y via port x and * *proceeds as t. In both expressions, the x is free, and the yis bound in t. Finally, x * *t expresses that the port name x is made local in t, that is, the x is bound in t. __________________________________________________________________ _ _ __v__x(y)!v0__ PRE x(y):v x(y)!v SUM x(y) _ v +w ! v0 _ _ _ v__x(y)!v0___ynot_free_in_w v__x(y)!v0___w__x(y)!w0_ PAR x(y) COM | 0 0 _ v jw ! v0jw v jw ! y (v jw ) _ _ _ ___v__x(y)!v0____ RES x(y) z62 fx;yg _ z v ! z v0 _ ___________________________________________________________________ Table 1: Operational semantics of the ssI -calculus The operational semantics of the ssI-calculus is presented in Table 1, where * *x; y; zare actual variables of sort Port, and v; v0 ; w ; w0 are formal variables of sort * *Process. In order to keep Table 1 clean,the versions of PRE and SUM and PAR and RES with label x(y) instead of x(y), and the symmetric versions of SUM and PAR and COM, have not been included. We already encountered the rule PRE in example 2.14. Recall from that example that the y is a free parameter in the labels,but that it is a binder of v in th* *e source of PRE. The variables in the rules in Table 1 are all source-dependent. As an example* *, we show that this is the case for the rule COM. This rule saysthat if v sends por* *t name y along port x, pro ceeding as v0 ,and if w reads port name yalong port x, pro* *ceeding as w0 , then their merge can communicate, proceeding as the merge of v0 and w0,* * in which the port name y is made local, i.e., is bound in both arguments. The vari* *ables in COM are all source-dependent: -v and w occur in the source, so they are source-dependent, 19 - in the hypotheses v x(y)!v0 and w x(y)!w0, the left-hand sides v and w a* *re source-dependent,so the right-hand sides v0 and w0 are source-dependent, r* *e- spectively. The side condition `y not free in w ' in PAR can be encoded as a predicatein a collection of source-dependent transition rules. This easy exercise is left to * *the reader. (See Baeten and Verho ef [4] and Verhoef [41] for many examples how to encode s* *ide conditions as predicates.) Hence,the operational semantics for the ssI-calculus* * can be represented by a source-dependent TSS T0. Theorem 3.21 andcorollary 3.23 imply that a well-defined sum T0T1is both a cl* *osed and an open conservative extension of the TSS T0 for the ssI-calculus if eachru* *le r in T1satisfies one of two syntactic criteria: - either the source of r is new, - or one of the hypothesesof r has a special form, see theorem 3.21. These two criteria cover types of extensions that are common in the literature.* * The first criterion can deal with the casethat a rule in the extension T1 describes theb * *ehaviour of a new function symbol,because in general this new function symbol will be pr* *esent in the source of such a rule. The second criterion is often fulfilled if a func* *tion symbol in the original signature adoptsa new meaning when applied to new terms. Remark 4.1 In the ssI-calculus, port names are not processes,but data that are* * used to parametrize processes. Since we do not distinguish between processes and dat* *a, in our setting port names are considered to be processes too. This means that * *our conservativity results are slightly stronger than necessary, namely, that behav* *iour of both processes (interesting) and port names (not so interesting) is not influen* *ced by transition rules which satisfy one of the two criteria above. 4.2 Application to conditional term rewriting There is a strong link between the world of structured operational semantics an* *d that of conditional term rewriting.Both fields deal with what can be viewed as `term de* *duction systems'. Terms are built from a set of function symbols,and binary relations o* *n terms (transitions versus rewritesteps) are defined by means of proof rules (transiti* *on rules versus conditional rewriterules). Such a rule, togetherwith the validity,or non* *-validity, of a number of relations between terms, may imply the validity of another relat* *ion betweenterms. There is only one real distinction: in conditional rewriting,provability is c* *losed under context,in other words, if s ! t is provable,then C[s] ! C[t] is provable. The * *set of transitions provable from a TSS does not have to satisfythis characteristic, so* * in general a TSS cannotb eexpressed as a conditional term rewriting system (CTRS). However, we will see that the reverse transposition is possible, that is, for each CTRSt* *here is an equivalent TSS. Essentially, this transformation is obtained by adding so-calle* *d context rules for all function symbols. 20 Hence, theorems in structured operational semantics also apply to the field o* *f con- ditional rewriting. This link was already noted,but not exploited, by Groote a* *nd Vaandrager [22]. They refrain from transposing their results to conditional rew* *riting because it would yield lemmas that do not serve any practical purpose. We show in this section that our conservativity results do constitute useful * *lemmas in the field of conditional rewriting. They formulate sufficient syntactic requ* *irements for CTRSs R0 and R1 to ensure that the rewrite relation induced by R0 on origin* *al terms will not be affected if R0 is extended with R1. This result is applicabl* *e in the field of abstract data types, which are often specified by means of modules of * *CTRSs. In abstract data typing there is a long tradition in modular specifying systems* *. In fact, modular specifying means extending conservatively,in our terminology;see [7]for* * more information. Our conservativity theorem servesas an example how theorems from structured o* *p- erational semantics can be transposed to conditional rewriting. In order to kee* *p this exposition clean, we will not include important features from the previous sect* *ions,such as variable binding, substitution harnesses, formal variables, predicates, and * *negative conditions. These features are certainly relevant for the field ofconditional r* *ewriting. For instance, it is well-known that the -calculus can be viewed as a term rewri* *ting system, which involves variable binding.Take for example the rule for fi-reduct* *ion: (x:M)N ! M[x := N]: We can argue, analogously to the SOScase, that the substitution at the right-ha* *nd side is not a real substitution, but a substitution harness. Even so, negative condi* *tions are relevant for conditional rewriting,and have been studied for instance by Kaplan* * [26]. In order to find out how the conservativity results apply to CTRSs with variable b* *indings and negative conditions, the reader is referred to the previoussections. Remark 4.2 In structured operational semantics we allowed negative premises o* *f the form s6! for relations! , see definition 2.10. This construct expresses that* * there does not exits a relation s! t for any t, or inother words, 8x (s6! x), where x is * *a fresh variable. In order to make these expressions suited for conditional rewriting, * *they areto be generalized to the form 8x1; : :;:xn (s6! t), where x1; : :;:xnare the varia* *bles that occur in t but not in s; see Vande Pol [35]for more detailed information. CTRSs* * with such negative conditions can be given a meaning following Van Glabbeek [20]. We define the necessary preliminaries concerning conditional term rewriting a* *nd dis- cuss the connection with our results. We will provide some examples from the te* *rm rewriting literature to exemplify the results. For detailed information on cond* *itional rewriting we refer to Kaplan [25]and Bergstra and Klop [9]. Bergstra and Klop [9]classify the various kinds of CTRSs that occur in the li* *terature into four types: I (or `semi-equational'), II(or `join'), III, and IIIn (or `no* *rmal'). These types differ in the meaning that is given to the conditions thato ccur the rewr* *ite rules. In this section, we will focus on CTRSs of type III. A CTRS of any of the other th* *ree types can always be transformed into a CTRSof type III. We will see that our conserva* *tivity results are useful for CTRSs of the types II and IIIand II In. The transformati* *on of 21 type Ito type III yields infinite CTRSs that are outside thescope of our conser* *vativity results. Definition 4.3A conditional term rewriting system (CTRS) of type IIIis a pair (* *;R) with a (formal) signature and R a set of conditional rewrite rules of the form l! r ( s1i t1; : :;:sn i tn; where l; r; si; ti are terms over the signature . The expressions sii ti are c* *alled the conditions of the rewrite rule, and i denotes the transitive-reflexive clos* *ure of the one-step rewrite relation !. A rewrite rule without conditions will be written as l !r, provided that no con* *fusion can arise. Remark 4.4 On a conditional rewrite rule we often see the the followingthree c* *ondi- tions. A. The left-hand side lis not a variable. B. The variables that occur in the right-hand side r also occur in the left-h* *and side l. C. No extra variables occur in the conditions. Restrictions A and B are quite natural in the unconditional case, because then * *theyare essential in order to obtain termination. According to Middeldorp [27],restrict* *ion C is often imposed to prevent severe complications of a technical nature. Weleave out these restrictions, because our results do not require to impose * *them. However,we will see that for CTRSs of types IIand IIIn, the conditions of the c* *onser- vativity theorem translate to the restrictions B and C. In the previoussections, on structured operational semantics, we allowed nega* *tive premises in the transition rules. In order to give meaning to TSSs, we introdu* *ced the notion of a `stable model', from Gelfond and Lifschitz [18], see definition 2.2* *0. Since in this part on conditional rewriting we have abstracted from negative conditio* *ns,it is much easier to givemeaning to CTRSs. Recall that i denotes the transitive-refle* *xive closure of !. Definition 4.5s ! t is provable from a CTRS if there exists a rule l ! r ( s1i t1; : :;:sn itn in the CTRS, a substitution oe, and acontext C[ ] such that s j* * C[oe(l)] and t j C[oe(r)] and oe(si) i oe(ti) is provable from the CTRS for i = 1; : :;:* *n. Before we continue, we give an example of a CTRS, taken from [15], which will* * serve as a running example to demonstrate our conservativity result. Example 4.6 The following CTRS of type II Iis built from two modules N0and N1. The CTRSN0 implements addition on natural numbers. It assumes the sort Nof natu* *ral 22 numbers, together with the constant 0, the successor function S : N ! N, and ad* *dition A : N N ! N. The CTRS N0consists of the following two rules: ae A(0;x) ! x A(S(x);y) ! S(A(x; y)) The CTRS N1implements the Fibonacci numbers. It assumes the sorts N and N N, the constant 0, and the functions S and A and Fib: N ! N N. TheCTRS N1consists of the following two rules: ae Fib(0) ! (0;S(0)) Fib(S(x)) ! (z; A(y; z)) ( Fib(x) i (y; z) The CTRS N1is considered difficult, because the variables y and z do not occur * *in the left-hand side of the rule. Later on we will see thatour conservativity format * *applies to N0 N1 without any problem. Our conservativity results make heavy use of the notion of source-dependency,* *which was introduced for TSSs in definition 3.16. We transpose this definition to CTR* *Ss of type III. Definition 4.7 Assume a conditional rewrite rule of type III: l ! r( s1i t1; : :;:sni tn: We define inductively what are the source-dependent variables of this rule. fflThe variables in l are source-dependent. fflIf the variables in siare all source-dependent,then the variables in tiar* *e source- dependent, for i = 1; : :;:n. A conditional rewrite rule oftype III is source-dependent if all the variables * *in the rule are source-dependent. A CTRSof type III is source-dependent if all its rules ar* *e so. Example 4.8 We show that the CTRS N0 N1in example 4.6 is source-dependent. The first three rules are trivial because they do not have conditions, and they* * satisfy restriction B in remark 4.4: the variablesthat occur in the right-hand side als* *o occur in the left-hand side. The fourth rule incorporates three variables: x; y, and * *z. Since l =Fib(S(x)), it follows that x is source-dependent. Since x is the only variab* *le in the left-hand side Fib(x)of the condition, the variables in theright-hand side (y; * *z) are also source-dependent. So the fourth rule is source-dependent too. We briefly discuss the three types I, IIand IIIn for CTRSs from [9], and how * *they can be transformed to type III CTRSs. We will find that if a CTRS oftype II or * *IIIn satisfies requirements B and C of remark 4.4, then its transformation to type I* *II is source-dependent. 23 fflIn type IIIn, conditionsare conjuncts of expressions s i t where t is a g* *round normal form. Inparticular, terms at the right-hand sides of conditions are* * closed, so it follows that the only source-dependent variables in type IIIn rules * *are the ones in the left-hand side of the rule. Hence, a ruleof type IIIn is sourc* *e-dependent if it satisfies requirements B and C of remark 4.4, which together ensure * *that all variables in therule occur in the left-hand side. fflIn type II, conditions are conjuncts of expressions s # t, which denote t* *hat both s and t reduce to a term u.This can be formulated in type III style: s i y a* *ndt i y where y is a fresh variable. Since the y is fresh, by definition it does * *not occur in any of the conditions. So again,the only source-dependent variables in* * type II rulesare the ones in the left-hand side of the rule. Hence, a rule of t* *ype II is source-dependent if it satisfies requirements B and C of remark 4.4. fflFinally, intype I, conditions are conjuncts of expressions s = t, which d* *enote that s rewrites to t if the rewrite rules may be applied both from left to* * right and from right to left. There is a laborious way toexpress a rule of type* * I in infinitely many rulesof type III. However, the rules that are thus obtaine* *d are not source-dependent,so that the conservativity results do not apply. The foll* *owing example, due to Aart Middeldorp [28], features type I CTRSs R0and R1, where R0satisfies requirements A, B, and C of remark 4.4, and in each rule in R1* * the term at the left-hand side contains a new function symbol, such that R0R1 * *is neither a closed nor an op enconservative extension of R0. Example4.9 Let 0 =fa; b; f g and 1 = fa; b; cg, where a;b; c are constan* *ts and f is of arity one. Let R0 consist of thefollowing rule: f(x) ! x ( x = a Furthermore,let R1 consist of the following two rules: n c ! a c ! b Then f(b) ! b is provable from R0 R1, but not from R0. 4.3 The conservativity theorems in conditional rewriting In this subsection we discuss the conservativity theorems in conditional rewrit* *ing. Definition 4.10Let (0; R0) and (1; R1) be two CTRSs of type III. R0 R1 is a closed/open conservative extension of R0 if for every closed/open term s over 0* *, s rewrites to a term t inthe original system R0 if and only if s rewrites to t in* * the extended system R0R1. In theorem 3.21and corollary 3.23 we formulated under which conditions an ext* *ension of a TSSis both closed and open conservative. Here,we transpose these results t* *o the setting of conditional rewriting. One of the clauses in theorem 3.21 leaves the* * possibility 24 for a rule in the extension to have an original term at theleft-hand side. We l* *eave out this clause here, in order to keep this exposition simple, and because we did n* *ot find an application of it in conditional rewriting. Theorem 4.11 Assume two type IIICTRSs (0; R0) and (1; R1). If R0 is source- dependent, and if in each rule in R1, the term at the left-hand side contains a* * function symbol from 1n0, then R0R1 is both a closed andan open conservative extension of R0. Proof. We show how a type III CTRSs can be translated into an equivalent TSS. Then we transform R0 and R0 R1 intoequivalent TSSs, and show that theop enand closed conservativity theorems for TSSs, theorem 3.21 and corollary 3.23, apply. Assume a CTRS (;R) of type III. We construct a TSS T such that Rproves a rewrite step s ! t if and only T proves the transition s ! t. Each conditional * *rule l ! r( s1 i t1; : :;:sni tn in R can be expressed as atransition rule in T : fs1i t1; : :;:sn i tng ____________________: l !r Furthermore,in order to define the transitive-reflexive closure i of ! that o* *ccurs in the conditions, we need two more transition rules in T: x ! y yi z x i x and ____________: x i z The first transition rule is clearly source-dependent. In the second rule, x is* * source- dependent because it occurs in the source, so the condition x ! y ensures that * *y is source-dependent, so finally the condition y iz ensures that z is source-depend* *ent. Note that both rules do not satisfy requirement Ain remark 4.4, i.e., their sou* *rces are single variables. If the notions of provability in aCTRS and a TSS would coincide, we would now* * be ready with the translation. However, there is one essential distinction: in con* *ditional rewriting, provability is closed under context, that is, if s ! t is provable t* *hen C[s] ! C[t] is provable. In order to bridge this gap,we add context rules to T for all* * function symbols f 2: xi! y _____________________________________; i = 1; : :;:n: f(x1; : :;:xi; : :;:xn) ! f(x1; : :;:y; : :;:xn) These context rules are source-dependent. Namely, the variables x1; : :;:xn occ* *ur in the source, so they are source-dependent, and the condition xi! y ensures that * *y is source-dependent. It is not hard to see that R proves a rewrite step s ! t if and only if T pro* *vesthe transition s ! t. We apply the strategy described above in order to translate R0 and R0 R1 into equivalent TSSs T0and T0 T1, respectively. 25 1. T0 consists of the transformations of the conditional rules in R0 into tra* *nsition rules, together with thetwo transition rules for i, and the context rules * *for function symbols in 0. 2. T1 contains the transformations of the conditional rules in R1 into transi* *tion rules, together with the context rules for function symbols in 1n0. We verify thatT0 and T1 meet the requirements from theorem 3.21. 1. Since the conditional rules in R0 are source-dependent,it follows that the* *ir trans- formations into transition rules are source-dependent. Moreover, the trans* *ition rules for i and the context rules are source-dependent. Hence, the TSS T0* * is source-dependent. 2. Since each conditional rule in R1 contains afunction symbol from 1n0in its* * left- hand side,the same holds for their transformations into transition rules. * *Moreover, each context rulefor a function symbol in 1n0contains this function symbol* * in itssource. So according to theorem 3.21 andcorollary 3.23, T0 T1is both a closed and an op* *en conservative extension of T0. Since R0 and R0 R1are equivalent with T0 and T0 T1 respectively,it follows that R0R1 is both a closed and an open conservative ext* *ension of R0. 2 Example 4.12 We show that the conservativity theorem 4.11 applies to the CTRSN0 N1 from example 4.6. Recall from example 4.8 that N0 and N1 are source-dependen* *t. Since N0is source-dependent, and since the left-hand sides of the two rules i* *n N1 both contain the function symb ol Fib,theorem 4.11 yields that N0 N1is a closed* * and an open conservative extension of N0. Furthermore, N0 N1is source-dependent, so we can extend this CTRSin a conser- vative way, as long as we make sure that the rules in the extension have a new * *function symbol in their left-hand sides.For example, letthe CTRS N2implement multiplica* *tion M : N N ! N as follows. ae M(0;x) ! 0 M(S(x);y) ! A(M (x; y); y) Since the new function symbol Moccurs in the left-hand sides of the two rules o* *f N2, it follows that N0 N1 N2is a conservative extension ofN0 N1. 5 Conclusions In this paper we set up a formalframework to describe term deduction systems su* *ch as appear in structured operational semantics in the style of Plotkin and in co* *nditional term rewriting. This framework has the power to express many-sortedness,general binding mechanisms and substitutions, among other notions such as negative prem* *ises and unary predicates on terms.This framework can serve as a platform to prove g* *eneral statements concerning such systems. 26 We discussed one such result for transition system specifications, known as c* *onser- vativity. Theconservativity theorem that we proved states under which circumsta* *nces the extension of a transition system specification with new rules does not affe* *ct the behaviour of the original terms. This subject is important because many existin* *g op- erational semantics are extended with new features describing real-time or mobi* *lity, to mention a few, and this should preferably be done conservatively. Furthermore, we presented a general strategy to translate theorems in structu* *red operational semantics to conditional term rewriting systems. In particular, we * *have applied this approach to the conservativity theorem, which yields a result that* * is useful for abstract data terms, when specified as modules of conditional term rewritin* *g systems. We showed that these conservativity results are applicable to many and divers* *e process algebras and conditional term rewriting systems. For example, we have seen that* * they can be applied successfully in the setting of the ss-calculus. References [1] L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOS rules into equations. Information and Computation, 111(1):1-52, 1994. [2] S.F. Allen, R.L. Constable, D.J. Howe, and W.E. Aitken.The semantics of ref* *lected proof. In ProceedingsLICS'90, pp. 95-197. IEEE Computer Society Press, 1990. [3] J.C.M. Baeten and J.A. Bergstra. Discrete time process algebra. In Procee* *dings CONCUR'92, LNCS 630, pp. 401-420. Springer,1992. Revised version to appear in Formal Aspectsof Computing. [4] J.C.M. Baeten and C. Verhoef. A congruence theorem for structured operation* *al semantics with predicates. In Proceedings CONCUR'93, LNCS 715, pp.477-492. Springer, 1993. [5] J.C.M. Baeten and C. Verhoef. Concrete process algebra. In S. Abramsky,D.M. Gabbay, and T.S.E. Maibaum, eds., Handbook of Logic in Computer Science,Vol- ume IV, Syntactical Methods, pp. 149-268. Oxford University Press, 1995. [6] H.P. Barendregt. The Lambda Calculus - Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics103. North-Holland, 1984. Revised edition. [7] J.A. Bergstra, J. Heering, and P. Klint, editors. Algebraic Specification. * *ACM Press in cooperation with Addison Wesley, 1989. [8] J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60(1/3):109-137, 1984. [9] J.A. Bergstra and J.W. Klop. Conditional rewrite rules: confluence and term* *ina- tion. Journal of Computer and System Sciences, 32:323-362, 1986. 27 [10]B. Bloom. Structural operational semantics for weak bisimulations. Theoreti* *cal Computer Science, 146(1/2):25-68, 1995. [11]B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced. Journal* * of the ACM, 42(1):232-268, 1995. [12]B. Bloom and F.W. Vaandrager. SOSrule formats for parameterized and state- bearing processes. Unpublished manuscript, 1995. [13]R.N. Bol and J.F. Groote. The meaning of negative premises in transition sy* *stem specifications. In Proceedings ICALP'91, LNCS 510, pp. 481-494. Springer, 1* *991. [14]R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J.Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, * *and S.F.Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall International, 1986. [15]N. Dershowitz, M. Okada, and G. Shivkumar. Confluence of conditional rewri* *te systems. In Proceedings CTRS'87, LNCS 308,pp. 31-44. Springer, 1987. [16]W.J. Fokkink and R.J.van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Technical Note CS-95-17, Stanford University, 1995. Toapp ear in Informatio* *n and Computation. [17]W.J. Fokkink and A.S.Klusener. An effective axiomatization for real time AC* *P. Report CS-R9542, CWI, Amsterdam, 1995. To appear in Information and Com- putation. [18]M. Gelfond and V. Lifschitz. The stable model semantics for logic programmi* *ng. In Proceedings 5th Conference on LogicProgramming, pp. 1070-1080. MIT press, 1988. [19]R.J. van Glabbeek. Full abstraction in structural operational semantics. In* * Pro- ceedingsAMAST'93, Workshops in Computing, pp. 77-84. Springer, 1993. [20]R.J. van Glabbeek. The meaning ofnegative premises in transition system spe* *ci- fications II. Technical Note CS-95-16, Stanford University, 1995. [21]J.F. Groote. Transition system sp ecifications with negative premises. Theo* *retical Computer Science, 118(2):263-299, 1993. [22]J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisim* *u- lation as a congruence. Information and Computation, 100(2):202-260, 1992. [23]C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall Internation* *al, 1985. [24]D.J. Howe. Proving congruence of bisimulation in functionalprogramming lan- guages. Technical Report, AT&T Bell Laboratories, 1995. 28 [25]S. Kaplan. Conditional rewrite rules. Theoretical Computer Science, 33(2):1* *75-193, 1984. [26]S. Kaplan. Positive/negative conditional rewriting. In Proceedings CTRS'87,* *LNCS 308, pp. 129-143. Springer, 1987. [27]A. Middeldorp. Modular properties of conditional term rewriting systems. In* *for- mation and Computation, 104(1):110-158, 1993. [28]A. Middeldorp. Personal communication, October 1995. [29]R. Milner. Communication andConcurrency. Prentice Hall International, 1989. [30]R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. In * *Pro- ceedings CONCUR'91, LNCS527, pp. 45-60. Springer, 1991. [31]R. Milner, J. Parrow, and D. Walker. Acalculus of mobile processes, part I * *+ II. Information and Computation, 100(1):1-77, 1992. [32]F. Moller and C. Tofts. A temporal calculusof communicating systems. In Pro- ceedings CONCUR'90, LNCS458, pp. 401-415. Springer, 1990. [33]X. Nicollin and J. Sifakis. The algebra of timed processes, ATP: theory and application. Information and Computation, 114(1):131-178, 1994. [34]G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University, 1981. [35]J.C. van de Pol. Semantics of priority rewrite systems by means of transiti* *on system specifications. Unpublished manuscript, 1995. [36]D. Sangiorgi. The lazy lambda calculus in a concurrency scenario. Informa* *tion and Computation, 111(1):120-153, 1994. [37]D. Sangiorgi. ssI: A symmetric calculus based on internal mobility. In Proc* *eedings TAPSOFT'95, LNCS 915, pp. 172-186. Springer, 1995. [38]R. de Simone. Higher-level synchronising devices in meije-SCCS. Theoretic* *al Computer Science, 37:245-267, 1985. [39]A. Stoughton. Substitution revisited. Theoretical Computer Science, 59:317-* *325, 1988. [40]C. Verhoef. A general conservative extension theorem in process algebra. In* * Pro- ceedings PROCOMET'94, IFIP Transactions A-56, pp. 149-168. Elsevier, 1994. [41]C. Verhoef. Acongruence theorem for structured operational semantics with p* *red- icates and negative premises. Nordic Journal of Computing, 2(2):274-302, 19* *95. [42]D.A. Watt. Programming Concepts andParadigms. Prentice Hall International, 1990. 29