ISSN 0249­6399 ISRN INRIA/RR­­4395­­FR+ENG apport de recherche THÈME 1 INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 James J. Leifer N° 4395 March 2002 Unité de recherche INRIA Rocquencourt Domaine de Voluceau, Rocquencourt, BP 105, 78153 Le Chesnay Cedex (France) Téléphone : +33 1 39 63 55 11 --- Télécopie : +33 1 39 63 53 30 Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 James J. Leifer Th‘eme 1 --- R’eseaux et syst‘emes Projet Moscova Rapport de recherche n° 4395 --- March 2002 --- 48 pages Abstract: This paper is the second in a series of two. It relies on its companion, Part 1, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive systems and how to prove congruence results for operational equiv­ alences and preorders defined above those transitions. The purpose of this paper is (i) to show that the hypotheses required of functorial reactive systems from Part 1, for example the sliding properties of IPO (idem pushout) squares, are indeed satisfied for functors of a general form; (ii) to illustrate an example of a functorial reactive system based on Milner's action calculi, which satisfy the RPO (relative pushout) hypothesis required in the proofs of congruence from Part 1. Key­words: labelled transition, structural congruence, bisimulation, action calculi, pushout Synth‘ese de transitions ’etiquet’ees et de congruences op’erationnelles pour les syst‘emes r’eactifs, deuxi‘eme partie R’esum’e : Cet article forme le second d'une s’erie. Le lecteur est renvoy’e ‘a l'article associ’e (premi‘ere partie) pour un expos’e de la motivation du probl‘eme auquel s'attaque cette s’erie, ‘a savoir comment synth’etiser des transitions ’etiquet’ees pour des syst‘emes r’eactifs et com­ ment prouver des r’esultats de congruence pour des ’equivalences et pr’eordres op’erationnels d’efinis sur ces transitions. Le but de cet article est, premi‘erement, de montrer que les hy­ poth‘eses de la d’efinition des syst‘emes r’eactifs fonctoriels de premi‘ere partie, par exemple les propri’et’es de glissement des diagrammes d'IPO (``idem pushout''), sont bien satisfaites pour des foncteurs d'une certaine forme g’en’erale ; deuxi‘emement, d'illustrer un exemple de syst‘eme r’eactif fonctoriel bas’e sur les ``action calculi'' de Milner, qui v’erifient les hy­ poth‘eses de RPO (``relative pushout'') des preuves de congruence de premi‘ere partie. Mots­cl’es : transition ’etiquet’ee, congruence structurelle, bisimulation, action calculi, somme amalgam’ee Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 1 Contents 1 Introduction 2 1.1 Motivation and goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Recapitulation of key definitions and theorems 5 3 Sliding IPO squares 8 3.1 Introduction and motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Properties of A . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.3 Construction of “ C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.4 Operations on “ C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.5 Construction of C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.6 Construction of F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.7 Replacing precategories with bicategories . . . . . . . . . . . . . . . . . . . 19 4 Action graph contexts 22 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.2 Action calculi reviewed . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.3 Examples and a problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.4 Closed shallow action graphs . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.5 The well­supported precategory A­Ixt of arities and raw contexts . . . . . 32 4.6 Constructing a functorial reactive system . . . . . . . . . . . . . . . . . . . 37 5 Conclusions and future work 40 Bibliography 46 RR n° 4395 2 J.J. Leifer 1 Introduction 1.1 Motivation and goals This paper is the second in a series of two. I rely on its companion [Lei02], referred to as Part 1 throughout, to motivate the central problem addressed by the series, namely: how to synthesise labelled transitions for reactive systems and how to prove congruence results for operational equivalences and preorders defined above those transitions. Thus, the present paper uses Part 1 as a base, sacrificing self­containedness in order to avoid repetition, though the key definitions are recapitulated here in Section 2. The purpose of this paper is to twofold: (i) to show that the hypotheses required of functorial reactive systems from Part 1 are indeed satisfied for functors of a general form; (ii) to illustrate an example of a functorial reactive system, namely action graphs, which satisfy the RPO (relative pushout) hypothesis required in the proofs of congruence from Part 1. Of the two, goal (i) is more critical since the techniques employed for generating the functor and proving the relevant properties are widely applicable. The argument does not fit neatly within standard category theory, though, and requires the use of precategories --- which have a partial composition operator, unlike the total one of categories. It seems possible that this work could be recast by replacing precategories with bicategories. One of the primary reasons for presenting (i) in detail is to expose this potential recasting as a challenge to the (enriched) category theory community. This question is discussed in detail in Subsection 3.7. For goal (ii), I introduce action graphs (a subclass of Milner's action calculi). The main motivation for defining these is to show that the properties required of them in the definition of a functorial reactive system follow smoothly from the work on goal (i). The proof of the existence of RPOs, by contrast, requires highly combinatorial manipulations of graph contexts and embeddings. For the sake of brevity, I omit this proof, pointing instead to its full treatment in my Ph.D. [Lei01b]. 1.2 Outline The outline of this paper is as follows: Section 2: This section recapitulates the key definitions from Part 1 needed in the present paper. INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 3 Section 3: As mentioned above in (i) the proofs of congruence in Part 1 rest on some hypotheses about the functor F . The most important one of these is that F allows an IPO square upstairs to ``slide'' so as to leave the F­image of the square invariant. This section eases the burden of showing that these hypotheses are satisfied by giving an abstract way of generating a functor satisfying them from simpler data. The section starts by assuming the existence of a well­supported precategory A, which is like a category but lacks some arrow compositions and has extra structure for extracting and renaming the support of an arrow. The motivation for this comes from the raw contexts in Section 4 for which composition of two contexts is not defined unless their node sets (supports) intersect trivially. I derive from A two categories and a functor between them. The upstairs category is formed from A by adding extra information to the objects, so as to make composition total. The downstairs category is formed by quotienting away the supports. The functor F maps arrows to their quotient equivalence classes. By reasoning abstractly, I show that F allows IPO sliding and has all of the other properties required of functorial reactive systems (see Definition 2.5). By instantiating these results, as in Section 4 for example, one gets ``for free'' a functorial reactive system provided that one starts with a well­supported precategory, a light burden. Section 4: This section gives a significant example of a family of functorial reactive sys­ tems. The contexts are derived from closed, shallow action graphs, those with no nesting and no free names. Their graph structure includes forked and discarded wiring connecting interfaces on each node and on the inside and outside of each context. By instantiating the results of the preceding section, we construct a func­ torial reactive system with the following properties: the downstairs category does not distinguishes the occurrences of controls, as desired when modelling agents of a process calculus; the upstairs one does distinguish them, thus providing su#cient RPOs. Section 5: The section sets out the main open questions, whose solutions are critical to the application of this work to a wide variety of process calculi. 1.3 Acknowledgements I thank Robin Milner (my Ph.D. supervisor) for his inspiration and warmth. I learned more about the ways of doing research and the style of presenting it from him than anyone else. I had extensive and valuable discussions with Luca Cattani and Peter Sewell. Many colleagues provided suggestions, for which I am grateful: Tony Hoare, Martin Hyland, Philippa Gardner, Michael Norrish, Andy Pitts, John Power, Edmund Robinson, and Lucian Wischik RR n° 4395 4 J.J. Leifer I was supported by the following funding sources: EPSRC Research Grant GR/L62290 and an NSF Graduate Research Fellowship. INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 5 m f 0 f 1 g 0 g 1 1(1) m f 0 f 1 g 0 g 1 h 0 h 1 h 1(2) m f 0 f 1 g 0 g 1 h 0 h 1 h h # h # 0 h # 1 kk 1(3) Figure 1: Construction of an RPO 2 Recapitulation of key definitions and theorems This section recalls the key definitions and theorems from Part 1 needed in this paper. The original motivation and explanation of each is not repeated, but can be found by following each pointer into Part 1. Definition 2.1 (RPO --- see Definition 2.4 in Part 1) In any category C, consider a commuting square (Figure 1(1)) consisting of g 0 f 0 = g 1 f 1 . An RPO is a triple h 0 , h 1 , h satisfying two properties: commutation: h 0 f 0 = h 1 f 1 and hh i = g i for i = 0, 1 (Figure 1(2)); universality: for any h # 0 , h # 1 , h # satisfying h # 0 f 0 = h # 1 f 1 and h # h # i = g i for i = 0, 1, there exists a unique mediating arrow k such that h # k = h and kh i = h # i (Figure 1(3)). # Terminology: A triple, such as h # 0 , h # 1 , h # given above, that satisfies the commutation property, i.e. h # 0 f 0 = h # 1 f 1 and h # h # i = g i for i = 0, 1, is often called a candidate. Thus an RPO triple is a candidate for which there is a unique mediating arrow from it to any other candidate. Definition 2.2 (IPO --- see Definition 2.5 in Part 1) The commuting square in Figure 1(1) is an IPO if the triple g 0 , g 1 , id m is an RPO. # # # # # m m # f 0 f 1 g 0 g 1 2 Proposition 2.3 (IPOs in a full subcategory --- see Proposition 2.10 in Part 1) Let m,m # be objects of C and let C # be a full subcategory of C satisfying the following property: obj C # # {n # obj C / #h # C(m,n) & #h # # C(n, m # )} . Suppose the square in Figure 2 commutes, where f i , g i # C # for i = 0, 1. Then the square is an IPO in C i# it is an IPO in C # . # RR n° 4395 6 J.J. Leifer Definition 2.4 (reactive system--- see Definition 2.1 in Part 1) A reactive system consists of a category C with added structure. We let m,n range over objects. C has the following extra components: ˆ a distinguished object 0 (not necessarily initial); ˆ a set of reaction rules called Reacts # # m#objC C(0, m) 2 , a relation containing pairs of agents with common codomain; ˆ a subcategory D of C, whose arrows are the reactive contexts, with the property that D 1 D 0 # D implies D 1 , D 0 # D. # Notation: a, b # C range over arrows with domain 0, called agents, and C, D,F # C range over arbitrary arrows (contexts). Definition 2.5 (functorial reactive system--- see Definition 3.1 in Part 1) Let C be a reactive system. A functorial reactive system over C consists of a functor F : “ C C which maps a distinguished object # # obj “ C to 0 (the distinguished object of C) and which satisfies the following properties. F lifts agents: for any a : 0 m there exists a : # m such that F(a) = a. F creates isos: if F(C) is an iso then C is an iso. F creates compositions: if F(C) = C 1 C 0 , there exist C 0 , C 1 # “ C such that C = C 1 C 0 and F(C i ) = C i for i = 0, 1. # # # # C F # F C # 3 C 0 F # 0 F 0 C # 0 4 F allows IPO sliding: for any IPO square as in Figure 3 and any arrow F # 0 with F(F # 0 ) = F(F # ) there exist C 0 , C # 0 , F 0 forming an IPO square as in Figure 4 with F(C 0 ) = F(C) F(C # 0 ) = F(C # ) F(F 0 ) = F(F) . # Notation: Uppercase teletype characters denote arrows in “ C and lowercase teletype characters (a, l, . . .) denote arrows with domain # in “ C. The F images of these are agents in C. The special domain requirement of a, l, . . . is left tacit throughout: thus (#l # “ C. . . .) means (#l # “ C. Dom l = # & . . .). # # # # a l F D 5 Definition 2.6 (F has all redex­RPOs--- see Definition 3.4 in Part 1) A functorial reactive system F : “ C C has all redex­RPOs if any square, such as in Figure 5, has an RPO, provided that F(D) # D and that there exists r # C such that (F(l), r) # Reacts. # INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 7 Proposition 2.7 (characterisation of --- see Proposition 3.2 in Part 1) a a # i# there exist a, l, D # “ C and r # C such that a = Dl and a # = F(D)r F(D) # D (F(l), r) # Reacts F(a) = a . # RR n° 4395 8 J.J. Leifer 3 Sliding IPO squares 3.1 Introduction and motivation Part 1 presents a series of congruence proofs, each one for a di#erent operational equiv­ alence. The theme throughout is the separation of ``reactive system'' into two categories with a functor F between them: the domain of F , i.e. “ C, is a category in which RPOs and IPOs exist; the codomain of F , i.e. C, is a category containing (i) the agents that perform reactions and labelled transitions and (ii) the agent contexts that serve as the labels and specify the closure condition for congruence. This separation is useful because the category for which we prove a congruence result is typically not one in which RPOs exist, as I show in the next section when considering categories of graph contexts. Thus functorial reactive systems are a powerful generalisation of reactive systems. This separation imposes a burden, though, in the form of the list of requirements given in Definition 2.5, i.e.: F lifts agents, creates isos, creates compositions, and allows IPO sliding. The motivation for the current section is to alleviate this burden by showing that all of these properties follow directly if we construct “ C, C, and F from a precategory A in a particular way. The assumption is that A is easier to construct than the others. (The next section gives a concrete instance of A.) Precategories are defined formally below. By way of motivation, though, let us look informally at an example we have in mind when deriving F : “ C C from A. A precate­ gory is just like a category but has a composition operation that is partial, i.e. not always defined. For example, consider a precategory A of ``raw contexts''. For the purpose of this example, take the objects to be natural numbers (representing the number of ports in an interface). Take the arrows m n to be just like normal graphs but with some added structure, namely an inner and outer interface. An arrow is thus a doughnut­shaped graph consisting of a set of nodes (which we call the support) and an arc relation; the arcs link nodes to one another and to the interface ports; m (ordered) interface ports sit on the inside ``hole'' and n (ordered ones) on the outside. (These are simpler than the graph con­ texts that appear in the next section.) Composition consists of placing one raw context inside the hole of another and joining together common ports. To see how this works, consider arrows A 0 : 1 2 and A 1 : 2 3: A 1 = v 1 v 2 A 0 = v 0 INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 9 Then their composition, which we denote A 1 # A 0 : 1 3, is as follows: A 1 # A 0 = v 2 v 0 v 1 This example reveals why composition is partial in A. If we form A # 0 from A 0 by renaming the node v 0 by v 2 then the supports of A # 0 and A 1 are not disjoint. Thus the composition A 1 # A # 0 is undefined since there is no clear choice for the support of the composite. There are several possible ways of building a true category (i.e. with a total composition relation) from the data provided by A. Two possible ways are as follows: ˆ We can construct a category “ C whose objects are pairs (m, U) where m is an object of A (in this case a natural number) and U is a set. An arrow (m 0 , U 0 ) (m 1 , U 1 ) consists of an A­arrow A : m 0 m 1 for which U 0 # U 1 and U 1 \ U 0 is equal to the support of A. Thus we can incorporate A 1 (given above) into many possible arrows in “ C, e.g. (2, #) A 1 (3, {v 1 , v 2 }) and (2, {w}) A 1 (3, {w, v 1 , v 2 }). As a result composition is always well­defined: if (m i , U i ) A i (m i+1 , U i+1 ) are “ C­arrows for i = 0, 1 then the supports of A 0 and A 1 are disjoint. ˆ We can construct a category C, whose objects are the objects of A and whose arrows are #­equivalence classes of A­arrows. Two A­arrows are #­equivalent i# they are graph­isomorphic, i.e. have (potentially) di#erent supports but look like the same graphs. Composition for this category is also well­defined since it is always possible when composing arrows to find representatives of each equivalence class with disjoint supports. One might consider a third way, i.e. to use the arrows of A but rename the supports so as to make them disjoint when composing arrows; but this yields a bicategory, since composition is not associative. I consider this possibility in detail in Subsection 3.7. What is the relationship between “ C and C? There is a simple functor F which discards the set component of each “ C­object (i.e. F : (m, U) ## m) and maps each arrow to its #­equivalence class. As we see later in this section, this functor has all of the desired properties listed earlier, e.g. F allows IPO sliding. The rest of this section repeats the above constructions in full formality. 3.2 Properties of A First we formally define a precategory (see [MSS00]): RR n° 4395 10 J.J. Leifer Definition 3.1 (precategory) A precategory A consists of similar data to that of a category: a collection of objects m, n, . . .; a collection of arrows A(m,m # ) between objects m and m # ; an identity arrow id m # A(m,m) for all m; and a partial composition operation, which we write here as # : A(m 1 , m 2 ) × A(m 0 , m 1 ) # A(m 0 , m 2 ) on arrows. Identity: composition with an identity arrow is always well­defined, i.e. for all A : m 0 m 1 , we have that id m 1 # A = A = A # id m 0 and both compositions are defined. Associativity: if A 2 # A 1 and A 1 # A 0 are defined then either both A 2 # (A 1 # A 0 ) and (A 2 # A 1 ) # A 0 are undefined or both are defined and equal. # Next we define some special properties of a precategory. These properties form a specification (used in Section 4) which any precategory is required to satisfy in order to make use of the constructions and propositions of this section. Definition 3.2 (well­supported precategory) A is a well­supported precategory i# it is a precategory and it satisfies the following properties: ˆ A has a support function |·| that maps an arrow to a set such that A 1 # A 0 is defined i# |A 1 | # |A 0 | = # and DomA 1 = CodA 0 . The support function satisfies additionally two axioms: |A 1 # A 0 | = |A 1 | # |A 0 | (provided A 1 # A 0 is defined) Supp­comp |id m | = # . Supp­id ˆ For any arrow A # A(m 0 , m 1 ) and any injective map # for which Dom # # |A|, there exists an arrow # # A # A(m 0 , m 1 ), which is called the support translation by # of A, where: # # id m = id m Trans­id­r # # (A 1 # A 0 ) = # # A 1 # # # A 0 Trans­comp­r Id |A| # A = A Trans­id­l (# 1 # # 0 ) # A = # 1 # (# 0 # A) Trans­comp­l # 0 # |A| = # 1 # |A| implies # 0 # A = # 1 # A Trans­res |# # A| = #|A| . Trans­supp A note about Trans­comp­r: Since # is injective, Trans­supp implies that the LHS is defined i# the RHS is defined. (These axioms are similar to those of Honda's Rooted P­Sets [Hon00], though his application concerns free names and renaming.) # INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 11 3.3 Construction of “ C We now turn to problem of building a genuine category from a well­supported precategory A. The idea is to enrich the object structure with enough data so that composition is always defined. This construction is captured in the following definition: Definition 3.3 (track) Given a well­supported precategory A, the track of A is a category “ C. An object of “ C is a profile: a pair (m, U) where m is an object of A and U is a set. We let p range over profiles and adopt the firm convention that the components of a profile p are always written (m, U) with suitable decoration, e.g. p # = (m # , U # ) and p i = (m i , U i ). An arrow p 0 A p 1 consists of an arrow A # A(m 0 , m 1 ) such that U 0 # U 1 and |A| = U 1 \ U 0 . We always include the profiles when referring to an arrow of “ C since di#erent “ C­arrows can be constructed from the same A­arrow, each with di#erent profiles. The identities of “ C are defined by id p “ = p id m p. Composition is defined in terms of the underlying composition in A: p 0 A 0 p 1 A 1 p 2 “ = p 0 A 1 #A 0 p 2 . # Proposition 3.4 If “ C is the track of A then “ C is a category. Proof Composition is well­defined: if p i A i p i+1 are arrows for i = 0, 1, then |A 1 | # |A 0 | = (U 2 \ U 1 ) # (U 1 \ U 0 ) = #, so A 1 # A 0 is defined. Furthermore, U 0 # U 1 # U 2 and U 2 \ U 0 = (U 2 \ U 1 ) # (U 1 \ U 0 ) = |A 1 | # |A 0 | = Supp­comp |A 1 # A 0 | , so p 0 A 1 #A 0 p 2 is an arrow of “ C as desired. The identity arrows are well­defined: By Supp­id, |id m | = #, so for any p = (m, U ), p id m p is an arrow of “ C. Composition is associative and respects identities: Immediate because these same properties hold in A. # 3.4 Operations on “ C In order to motivate the following results, let us recall the intuitions about the functor F (defined formally later): F maps p 0 A p 1 to an isomorphism equivalence class of A and throws away the set data contained in the profiles p 0 , p 1 . To prove that F allows IPO sliding, we require two things. (i) We have to understand how two “ C­arrows are related when they have the same F image, i.e. F(p 0 A p 1 ) = F(p # 0 A # p # 1 ). (ii) From the first piece of information, we have to slide similarly an IPO square whose left leg is p 0 A p 1 to one whose left leg is p # 0 A # p # 1 . RR n° 4395 12 J.J. Leifer For (i), it is clear that we can perform some profile translation (defined precisely later) on p 0 A p 1 to replace the set components of p 0 and p 1 and then perform a support transla­ tion on the resulting arrow to arrive at p # 0 A # p # 1 . If these two operations (profile translation and support translation) are iso functors (and thus preserve categorical constructions) then we can accomplish (ii). These two operations are not in fact iso functors on the whole of “ C but they are on certain convex subcategories, as defined next. Fortunately, the subcategories in question are rich enough to be proxies for “ C with respect to IPO squares, as shown in the result immediately following the definition: Definition 3.5 (convex subcategories of “ C) For any sets U 0 # U 1 , we write “ CU 0 ,U 1 for the convex subcategory of “ C w.r.t. U 0 , U 1 , namely the full subcategory of “ C formed by taking only those profiles (m, U) for which U 0 # U # U 1 . # # # # # p p 0 p 1 p 2 A 0 A 1 B 0 B 1 6 Proposition 3.6 Suppose that Figure 6 commutes in “ C. Then it is an IPO in “ C i# it is an IPO in “ CU,U 2 . Proof For any pair of arrows p C p # C # p 2 , we have that U # U # # U 2 , so p # # obj “ CU,U 2 (Definition 3.5) hence “ CU,U 2 satisfies the hypothesis of Proposition 2.3, whence the result follows. # Now we now define precisely profile translation and establish that it is an iso functor: Proposition 3.7 (profile translation is an iso functor) If W 1 = W 0 #W and W # 1 = W # 0 # W then the following operation, called profile translation, induces an isomorphism of categories H : “ CW 0 ,W 1 “ CW # 0 ,W # 1 , H : (m, W 0 # V ) ## (m, W # 0 # V ) for V # W H : (p 0 A p 1 ) ## H(p 0 ) A H(p 1 ) . Proof H is well­defined on arrows: Suppose that (p 0 A p 1 ) # “ CW 0 ,W 1 where U i = W 0 # V i , i = 0, 1 for some V 0 # V 1 # W . Now, W # 0 # V 0 # W # 0 # V 1 and (W # 0 # V 1 ) \ (W # 0 # V 0 ) = V 1 \ V 0 = |A| so (H(p 0 ) A H(p 1 )) # “ CW # 0 ,W # 1 as desired. H is a functor: Consider the action of H on identities: H(id p ) = H(p id m p) = H(p) id m H(p) = id H(p) and on compositions: H(p 0 A 0 p 1 A 1 p 2 ) = H(p 0 A 1 #A 0 p 2 ) = H(p 0 ) A 1 #A 0 H(p 2 ) = H(p 0 ) A 1 H(p 1 ) A 0 H(p 2 ) INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 13 H is an isomorphism of categories: By symmetry, the map H # : “ CW # 0 ,W # 1 “ CW 0 ,W 1 defined by H # : (m, W # 0 # V ) ## (m, W 0 # V ) for V # W H # : (p 0 A p 1 ) ## H # (p 0 ) A H # (p 1 ) . is also a functor and clearly inverts H, as desired. # Finally we lift the support translation operation from A to “ C in a straightforward way. This definition induces a functor on convex subcategories of “ C Proposition 3.8 (support translation is an iso functor) Given W 0 # W 1 and an injection # with Dom # # W 1 , the following operation, called support translation, induces an isomorphism of categories # # (·) : “ CW 0 ,W 1 “ C#W 0 ,#W 1 , # # (m, U) “ = (m, #U) # # (p 0 A p 1 ) “ = # # p 0 # # A # # p 1 , where # # A is the support translation by # of A in A. Proof # # (·) is well­defined on arrows: Suppose that (p 0 A p 1 ) # “ CW 0 ,W 1 . Then W 0 # U 0 # U 1 # W 1 # Dom #. Thus #U 0 # #U 1 and #U 1 \ #U 0 = # injective #(U 1 \ U 0 ) = #|A| = Trans­supp |# # A| , so # # (·) maps an arrow to an arrow. # # (·) is a functor: By Trans­id­r and Trans­comp­r, # # (·) preserves identities and compositions, so is a functor. # # (·) is an iso functor: Note that # has an inverse # -1 : Im # # Dom #. Furthermore, # -1 # (·) : “ C#W 0 ,#W 1 “ CW 0 ,W 1 is a functor for the same reasons (given above) that # # (·) is. By Trans­comp­ l and Trans­id­l, the functors # # (·) and # -1 # (·) invert each other, so # # (·) is an isomorphism of categories, as required. # 3.5 Construction of C We now turn to the construction of C, which was described informally in Subsection 3.1. Recall that the arrows of C are equivalence classes of arrows of A. In this subsection we make precise the underlying equivalence relation and the construction of C and verify that C is a well­defined category. RR n° 4395 14 J.J. Leifer Definition 3.9 (#­equivalence for A) Given two arrows A, A # : m 0 m 1 in A, we say that they are #­equivalent, written A # A # , i# there exists a bijection # : |A| ## |A # | such that # # A = A # . By Trans­id­l and Trans­comp­l, # is an equivalence relation. # Now the construction of C is straightforward: Definition 3.10 (support quotient) Given a well­supported precategory A, the sup­ port quotient of A is a category C. The objects of C are the objects of A. The arrows m 0 m 1 of C are #­equivalence classes of arrows in A: C(m 0 , m 1 ) “ = {[A] # / A # A(m 0 , m 1 )} . Identities: id m # C(m,m) “ = [id m ] # . Composition: if A 1 # A 0 is defined in A then [A 1 ] # [A 0 ] # “ = [A 1 # A 0 ] # . # This definition yields a well­defined category: Proposition 3.11 If C is the support quotient of A then C is a category. Proof Composition is total: Consider any two arrows in C such as [A i ] # : m i m i+1 for i = 0, 1. Let W be a fresh set in bijection with |A 1 |, as witnessed by # : |A 1 | ## W . Then # # A 1 # A 0 is defined since |# # A 1 | # |A 0 | = Trans­supp W # |A 0 | = #; thus [A 1 ] # [A 0 ] # = [# # A 1 ] # [A 0 ] # = [# # A 1 # A 0 ] # , as desired. Composition is well­defined: Let [A i ] # = [A # i ] # for i = 0, 1 with both A 1 # A 0 and A # 1 # A # 0 defined. Claim: [A 1 ] # [A 0 ] # = [A # 1 ] # [A # 0 ] # . By hypothesis, there exist bijections # i : |A i | ## |A # i | such that A # i = # i # A i for i = 0, 1. Since |A 1 | # |A 0 | = # and |A # 1 | # |A # 0 | = #, we can define # “ = # 0 # # 1 , a union of bijections with disjoint domains and disjoint codomains. Now, # # (A 1 # A 0 ) = Trans­comp­r # # A 1 # # # A 0 = Trans­res # 1 # A 1 # # 0 # A 0 = A # 1 # A # 0 so [A 1 ] # [A 0 ] # = [A 1 # A 0 ] # = [A # 1 # A # 0 ] # = [A # 1 ] # [A # 0 ] # , as desired. Composition is associative: Follows from the associativity of the underlying composi­ tion in A. Composition respects identities: Follows from the fact that composition respects identities in A. # INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 15 3.6 Construction of F In this final subsection we define a functor F from “ C (the track of A) to C (the support quotient of A). We then verify that F has all the required properties, i.e.: F lifts agents, creates isos, creates compositions, and allows IPO sliding. For the first we verify a stronger property defined below, namely F lifts arrows by their domain. The reason for this choice is that there is no postulated distinguished object in A or C corresponding to the 0 of a functorial reactive system (see Definition 2.5), which is required when defining the property ``F lifts agents''. However, the stronger property ``F lifts arrows by their domain'' is well­defined. Definition 3.12 (support­quotienting functor) Let A be a well­supported precat­ egory and “ C and C be as in Definition 3.3 and Definition 3.10. Then we define a map F : “ C C called the support­quotienting functor : F : (m, U) ## m F : (p 0 A p 1 ) ## F(p 0 ) [A]# F(p 1 ) . # Lemma 3.13 F is a functor. Proof Observe the action on identities: F(id p ) = F(p id m p) = [id m ] # = id m and on compositions: F(p 0 A 0 p 1 A 1 p 2 ) = F(p 0 A 1 #A 0 p 2 ) = [A 1 # A 0 ] # = [A 1 ] # [A 0 ] # = F(p 1 A 1 p 2 ) F(p 0 A 0 p 1 ) # Now we prove all the easy properties of F : Theorem 3.14 Let F : “ C C be the support­quotienting functor constructed from A. Then: ˆ F lifts arrows by their domain: if F(p 0 ) = Dom [A] # then there exists p 0 B p 1 such that F(p 0 B p 1 ) = [A] # . ˆ F creates isos: if F(p 0 A p 1 ) is an iso then p 0 A p 1 is an iso. ˆ F creates compositions: if F(p # 0 B p # 2 ) = [A 1 ] # [A 0 ] # RR n° 4395 16 J.J. Leifer then there exist “ C­arrows p # i B i p # i+1 with F(p # i B i p # i+1 ) = [A i ] # for i = 0, 1 (1) p # 0 B p # 2 = p # 0 B 0 p # 1 B 1 p # 2 (2) Proof F lifts arrows by their domain: Suppose [A] # : (m 0 , n 0 ) (m 1 , n 1 ), thus A : (m 0 , n 0 ) (m 1 , n 1 ) in A. Let W be a fresh set in bijection with |A|, as witnessed by # : |A| ## W . Then p 0 # # A p 1 is an arrow in “ C, where U 1 “ = U 0 # W . Furthermore F(p 0 # # A p 1 ) = [A] # as desired. F creates isos: Suppose F(p 0 A p 1 ) is an iso, i.e. there exists an A­arrow A # : m 1 m 0 such that: [A # ] # [A] # = id m 0 = [id m 0 ] # [A] # [A # ] # = id m 1 = [id m 1 ] # Without loss of generality, assume that |A| # |A # | = #. Then A # # A # id m 0 and A # A # # id m 1 . By Supp­id and Trans­id­r, A # # A = id m 0 and A # A # = id m 1 . By Supp­comp, |A| = |A # | = #. Thus U 1 = U 0 and p 1 A # p 0 is a “ C­arrow. Moreover, p 0 A p 1 A # p 0 = p 0 A # #A p 0 = p 0 id m 0 p 0 = id p 0 and symmetrically. Thus p 0 A p 1 is an iso in “ C as desired. F creates compositions: Without loss of generality, assume that |A 1 | # |A 0 | = #. Then there exist p 0 , p 1 , p 2 such that p i A i p i+1 are arrows in “ C for i = 0, 1. By the definition of F , there exists a bijection # : |A 1 | # |A 0 | ## |B| such that # # (A 1 # A 0 ) = B; moreover m 0 = m # 0 and m 2 = m # 2 . Let B i “ = # # A i for i = 0, 1. Let (m # 1 , U # 1 ) “ = (m 1 , U # 0 # |B 0 |), thus defining p # 1 . We claim that p # i B i p # i+1 are arrows in “ C for i = 0, 1; there are three things that we need to check: U # 0 # U # 0 # |B 0 | # U # 0 # |B| = U # 2 U # 1 \ U # 0 = |B 0 | U # 2 \ U # 1 = (U # 0 # |B|) \ (U # 0 # |B 0 |) = |B| \ |B 0 | = |B 1 | . Now, B 1 # B 0 = B by Trans­comp­r, from which (2) follows. Also, by Trans­res, B i # A i for i = 0, 1, from which (1) follows. # INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 17 An aside on the condition ``F creates compositions'': This looks tantalisingly close to the Conduch’e fibration property [Con72, Joh99, BF00], especially if one says that two decompositions in “ C are equivalent if one is the result of a support translation of the other. Perhaps there is some 2­category version of the Conduch’e property which works exactly if one thinks of “ C as a 2­category with support translations as 2­cells. Let us now return to the main flow of the argument. Finally, we prove the key property, namely that F allows IPO sliding. The proof follows the outline given in Subsection 3.4. We start with two “ C­arrows with the same image under F , namely F(p A 1 p 1 ) = F(p # A # 1 p # 1 ). The first arrow is the left leg of an IPO square in “ C. This square is also an IPO in “ CU,U 2 , the convex subcategory w.r.t. U, U 2 (Definition 3.5), where U # U 2 are the sets in, respectively, the upper­left and lower­right profiles of the square. We isomorphically transform this subcategory by profile translation and then support translation, gaining a new square that has three properties: it has the same image under F as the original; its left leg is p # A # 1 p # 1 ; it is an IPO in a convex subcategory, so is an IPO in “ C. Before looking at the technical details, it is useful to consider a concrete case of sliding. Because we have not formally defined the graph contexts referred to at the beginning of this section, it is impossible to be precise about which commuting squares are IPOs and which are not. Nonetheless, the activity of ``sliding'' is relevant for all commuting squares, whether or not they are IPOs. Let us consider a category of graph contexts formed as the track (Definition 3.3) of the precategory or raw contexts informally defined in Subsection 3.1. The arrows of this category are just like the raw contexts (doughnut­shaped graphs with an inner and outer interface) but with profiles (Definition 3.3) rather than just natural numbers as objects. Consider the square in Figure 7(1). Its left leg has the same F image as the left leg of the square in Figure 7(3): the two graph contexts look essentially the same, the only di#erence being the supports. With a profile translation, we can replace the singleton set {u} in the top­left corner of Figure 7(1) with a fresh 2­element set {u ## 0 , u ## 1 }, as shown in Figure 7(2). The freshness is essential to prevent clashes with the other nodes present in the square, namely v 0 , v 1 . Now, if # is defined as follows: # : v i ## v # i i = 1, 2 # : u ## i ## u # i i = 1, 2 then the support translation by # of Figure 7(2) yields Figure 7(3), as desired. Since the passage from Figure 7(1) to Figure 7(2) and then to Figure 7(3) was e#ected by iso functors, all the universal properties of Figure 7(1) (e.g. being an IPO) hold of Figure 7(3) too. RR n° 4395 18 J.J. Leifer v 1 v 0 v 1 (2, {u}) (2, {v0 , v1 , u}) (0, {v0 , v1 , u}) (4, {v0 , u}) v 0 7(1) A commuting square before sliding v1 v0 v1 (2, {u ## 0 , u ## 1 }) (2, {v0 , v1 , u ## 0 , u ## 1 }) (0, {v0 , v1 , u ## 0 , u ## 1 }) (4, {v0 , u ## 0 , u ## 1 }) v0 7(2) First we apply profile translation . . . v # 0 v # 1 v # 0 v # 1 (4, {v # 0 , u # 0 , u # 1 }) (2, {u # 0 , u # 1 }) (2, {v # 0 , v # 1 , u # 0 , u # 1 }) (0, {v # 0 , v # 1 , u # 0 , u # 1 }) 7(3) . . . and then support translation by # Figure 7: Sliding INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 19 # # # # p p 0 p 1 p 2 A 0 A 1 B 0 B 1 8 Theorem 3.15 (F allows IPO sliding) Let F : “ C C be the support­quotienting functor constructed from A. Then F allows IPO slid­ ing (Definition 2.5). Proof Consider any IPO square in “ C, as in Figure 8, and any arrow p # A # 1 p # 1 with F(p # A # 1 p # 1 ) = F(p A 1 p 1 ); thus A # 1 = # # A 1 for some bijection # : |A 1 | |A # 1 | and U # 1 = U # # #|A 1 |. # # # # H(p) H(p 0 ) H(p 1 ) H(p 2 ) A 0 A 1 B 0 B 1 9 By Proposition 3.6, Figure 8 is an IPO in “ CU,U 2 . Let U ## be a fresh set in bijection with U # , as witnessed by µ : U ## ## U # . Let U ## 2 “ = U ## #(U 2 \U ). Then U 2 \U = U ## 2 \U ## so by Proposition 3.7, there is a profile translation H : “ CU,U 2 “ C U ## ,U ## 2 which is an iso functor and whose action on profiles is: H : (m, U # V ) ## (m, U ## # V ) for V # U 2 \ U and whose action on arrows leaves the underlying A­arrow component unchanged. Since isomorphisms of categories preserve universal constructions, Figure 9 is an IPO in “ C U ## ,U ## 2 and has the same image under F as Figure 8 does. # # # # # # H(p) # # H(p 0 ) # # H(p 1 ) # # H(p 2 ) # # A 0 # # A 1 # # B 0 # # B 1 10 Let W be a fresh set in bijection with |B 1 |, as witnessed by # : |B 1 | ## W . Let # “ = µ # # # #, a union of bijections with mutually disjoint domains and codomains. Also Dom # = U ## # |A 1 | # |B 1 | = U ## 2 . Because # is bijective, Proposition 3.8 im­ plies that there is a support translation # # (·) : “ C U ## ,U ## 2 “ C #U ## ,#U ## 2 which is an iso functor. Iso functors preserve universal constructions, so Figure 10 is a IPO in “ C #U ## ,#U ## 2 and has the same image under F . By Proposition 3.6, this square is an IPO in “ C. Moreover, # # (H(p) A 1 H(p 1 )) = µ # H(p) # # A 1 (µ # #) # H(p 1 ) = p # A # 1 p # 1 as desired. # 3.7 Replacing precategories with bicategories As explained in Section 1, one of the main motivations for presenting the sliding arguments of this section is to advertise them to the (enriched) category theory community. The reason is that precategories are probably not optimal: it would be worthwhile to rework these arguments, replacing precategories with something more ``natural'' from enriched category theory, e.g. bicategories. Such a change might have side­e#ects on the results of Part 1 as well, which are discussed later in this subsection. Recall from Subsection 3.1 that the composition operation # of A is partial, not total, since it requires the supports of the operands to be disjoint: A 1 # A 0 is defined i# |A 1 | # RR n° 4395 20 J.J. Leifer |A 0 | = # and DomA 1 = CodA 0 (Definition 3.2). Composition can be made total by forcing the supports of the operands to be disjoint, i.e. defining a new composition # for which A 1 # A 0 = (# 1 # A 1 ) # (# 0 # A 0 ) where # j : |A j | |A 1 | + |A 0 | is the j­th injection into the coproduct of the supports in Set (the category of sets and functions), for j = 0, 1. This new definition of composition is total. It is not strictly associative, nor does it have strict identities --- which is exactly the kind of situation that bicategories cater for! Let the 2­cells from A : m n to A # : m n be the support translations # : |A| |A # | such that # # A = A # . All of these 2­cells are isos. Moreover, there are 2­cells mediating between the compositions A 2 # (A 1 # A 0 ) and (A 2 # A 1 ) # A 0 as generated from the underlying isos in Set between the coproducts |A 2 | + (|A 1 | + |A 0 |) and (|A 2 | + |A 1 |) + |A 0 |. It remains to be checked that all the bicategory coherence requirements are satisfied, but it seems likely since here they rely on the underlying properties of a coproduct, which is a universal construction. Having indicated how to derive a bicategory from A, it may be possible to go a step further, namely to dispense with A and “ C altogether and to postulate the existence of a bicategory B whose 2­cells are all isos. Since the 2­cells are isos, the property ``the 1­cells A, A # have a 2­cell between them'' is an equivalence relation on the 1­cells of B. We can thereby construct the ``support quotient'' (cf. Definition 3.10) of B by quotienting out the 2­cells, thus obtaining a category E. This quotienting is an enriched functor G : B E. Before looking at the advantages gained by giving this functor a central role, let us consider the price to be paid. First, the congruence results of Part 1 depend on the existence of RPOs in the ``upstairs'' category “ C of a functorial reactive system F : “ C C. The domain of the functor G is instead a bicategory, thus necessitating a bicategorical version of RPOs, which we might call 2­RPOs. One possible definition for 2­RPOs (of which Peter Sewell has made a preliminary study) is to replace in Definition 2.1 each commuting square and triangle by the relevant 2­cell, and their juxtaposition by horizontal and vertical 2­cell compositions. This change would have knock­on e#ects in the proofs of congruence which would have to be rewritten accordingly. Also, the existence proofs of RPOs for concrete systems would have to be redone to provide 2­RPOs. Neither change seems daunting. The potential reward of using bicategories is the ability to simplify the collection of axioms postulated about F in the definition of a functorial reactive system (Definition 2.5). The goal would be to give a neater collection involving G which might be verified for many cases based directly on general categorical reasoning about quotienting bicategories by their 2­cells. Finally, note that the strategy of bringing in enriched categorical machinery is directly opposite to Milner's in [Mil01]. He discards “ C (the track of A) and works directly with a precategory A: he then calculates RPOs in A, slides IPO in A, etc. His approach demands INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 21 that he be vigilant, since he is required to verify that compositions he encounters in A are well­defined. Nonetheless, this extra care seems bearable: for most compositions, a trivial inspection of the operands su#ces. It is therefore a challenge to category theorists to provide a collection of theorems for smoothly manipulating bicategories (for example) in which the e#ort needed to apply these results is less than the e#ort needed to work in the setting of precategories. RR n° 4395 22 J.J. Leifer 4 Action graph contexts 4.1 Introduction As promised in the previous section, the present one gives a substantial example of a precategory A­Ixt of raw contexts based on action calculi. (The ``Ixt'' is for ``insertion context'', a terminology explained in Subsection 4.6.) The need to handle graphs was the original motivation for functorial reactive systems: as we will see in Subsection 4.3, RPOs do not always exist for C­Ixt, the support quotient (Definition 3.10) of A­Ixt, so it is necessary to consider an upstairs category which does possess su#cient RPOs and a functor down to C­Ixt. The precategory A­Ixt has all the extra structure required of A, namely a sup­ port function and a support translation operation, so is a well­supported precategory (Definition 3.2). By direct instantiation of the results of the previous section, we can construct three things: the track of A­Ixt, which we call “ C­Ixt; the support quotient of A­Ixt, which we call C­Ixt; and a functor F : “ C­Ixt C­Ixt. These are related in the following table to their counterparts from the Section 3: well­supported precategory: A A­Ixt track: “ C “ C­Ixt support­quotienting functor: # F # F support quotient: C C­Ixt Thus by Theorem 3.14 and Theorem 3.15, F lifts arrows by their domain, creates isos, creates compositions, and allows IPO sliding. Furthermore A­Ixt has a distinguished ob­ ject 0, hence there are distinguished objects 0 and # of C­Ixt and “ C­Ixt, with F(#) = 0, whence F lifts agents. Thus, any choice of reaction rules Reacts for C­Ixt and reac­ tive context subcategory D of C­Ixt (Definition 2.4) yields a functorial reactive system (Definition 2.5). The main hurdle then in using the congruence results of the section ``Further congru­ ence results'' in Part 1 is proving that F has all redex­RPOs (Definition 2.6). It turns out that this property fails for some choices of reaction rules, but that it does hold for a rich class of them. As promised in Section 3 of Part 1, the category C­Ixt of graph contexts (the codomain of F) does not admit enough RPOs for subtle reasons. Examples are shown in Subsection 4.3. The cause is the lack of su#cient intensional information as to which node in contexts C 0 or C 1 , say, corresponds to a node in the composite C 0 C 1 . It is ex­ actly “ C­Ixt, the domain of F , that contains just enough structure to track how the nodes of two contexts are related to the nodes of their composition. By the definition of ``F INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 23 has all redex­RPOs'', the proof obligation is to show that su#cient RPOs exist in “ C­Ixt (Theorem 4.16). The proof of their existence is not done in the present paper, but is contained in full in [Lei01b]. The development of action calculi presented in this section intersects with that of [CLM00]; however the latter makes no use of functorial reactive systems, a key contribution of the present paper. Note as well that there are some di#erences in naming: in this paper I write “ C­Ixt and C­Ixt; in [CLM00], these are denoted PIns 0 and ACxt 0 respectively. 4.2 Action calculi reviewed I review a restricted class of the action calculi which were presented in [Mil96]. The rest of this section and the next make no specific use of the algebra of action calculi shown here since all of the work is done directly on graphs. Nonetheless, the design decisions taken when defining graphs are guided by the algebraic presentation of action calculi, so the latter provide valuable motivation. A closed, shallow action calculus is a strict monoidal category whose objects are natural numbers k, m, n, o . . ., and whose arrows are called action graphs and written a : (k, o), b : (m, n). (I avoid the usual arrow notation a : k o, reserving it for the context arrows of reactive systems.) The tensor product of these two action graphs is a# b : (k +m, o+n); the composition of a : (k, o) and b : (o, m) is a·b : (k, m); the identity action graph of arity (m, m) is i m . The order of composition is not conventional in category theory: it connotes the orientation of the action graphs we work with. (Note that this composition is the horizontal juxtaposition of action graphs and has nothing to do with contextual composition which we consider later.) A pair of natural numbers (k, o) is an arity ; let #, #, . . . range over arities. I deal only with closed, shallow action calculi and so usually omit these adjectives from now on. An action calculus has a control signature K = {K, L, . . .} consisting of controls, each of which has an arity. There are constants p : (2, 2), c : (1, 2) and # : (1, 0) for permutation, copy and discard. These constants represent only the swapping, sharing and elimination of arcs, not of nodes. They satisfy simple equations, e.g. c·p = c representing the com­ mutativity of copying. There is also an operator called reflexion [Mil94] (similar to the ``trace'' of Joyal et al. [JSV96]) which we need not detail here. Finally, each action calculus has a binary reaction relation , relating action graphs of equal arity. This relation is preserved by all constructions, i.e. by composition, tensor product and reflexion. RR n° 4395 24 J.J. Leifer L M M M K Figure 11: The action graph K·c·(M # L) and the context - 1,1 ·c·(M #M) For examples of action graphs, let K : (0, 1), M : (1, 1) and L : (1, 0) be controls. Then the following are action graphs, with their arities: K #M : (1, 2) K·c·(M # L) : (0, 1) (K·M) # (M ·L) : (1, 1) . Composition · binds tighter than tensor #, so the last can be written K·M #M ·L. A context C is an action graph containing a single hole with arity #, written -# . I omit the arity, writing -, if it is determined by the rest of the context or the surrounding discussion. Thus a context C : # # is an action graph of arity # with a hole of arity #. Here are two contexts along with their domain and codomain arities (the arity of the hole being fully determined in the second case): - 1,1 ·c·(M #M) : (1, 1) (1, 2) K·-·L : (1, 1) (0, 0) . Figure 11 shows an action graph and a context using a graphical notation. It uses nodes (rectangles with two blunt corners) to represent occurrences of controls, and arcs to represent composition. An action graph with arity (m, n) has m source ports on its left side and n target ports on its right side. A control node or hole of arity (m, n) has m target ports at its left side n source ports at its right side. At a source node, branching of arcs represents c and absence of arcs represents #. Two contexts are equal if the algebraic theory equates them, treating the hole as a control distinct from all others. The composition of two contexts C : # # and D : # #, written here DC (note the conventional order of composition), is formed by replacing the hole in D by C and joining the arcs according to the common ports. (This is context composition, not horizontal action graph composition described earlier.) Composition is clearly associative, and there is an identity context id # = - # for each arity. An action graph a : # can be considered as a context a : (0, 0) # whose hole has minimum arity. We shall use lower case letters a, . . . for action graphs. INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 25 We have thus associated with an action calculus a reactive system C­Ixt, whose objects are arities, with distinguished null arity (0, 0), and whose arrows are contexts, including action graphs. 4.3 Examples and a problem In this subsection I give examples of specific RPOs in C­Ixt, illustrating several phenom­ ena. I end with an example showing cases in which RPOs fail to exist; this motivates the strategy of defining a category ``upstairs'' (the domain of a functor with codomain C­Ixt) for which enough RPOs do exist. Remember that C­Ixt is really a family of reactive systems arising from action calculi; each is determined by a control signature and a set of reaction rules. Example 4.1 (arithmetic) I first illustrate how an RPO can determine a labelled transition, using an action calculus for elementary arithmetic having controls 0 : (0, 1), S : (1, 1), and + : (2, 1). The reactive system is shown in Figure 12; it is an example of the sharing graphs of Hasegawa [Has99], which add sharing to the interaction nets of Lafont [Laf90]. Nodes represent subexpressions, and the forking of arcs allows these to be shared. The reaction rules are in the top diagram; the garbage collection rules allow unattached expressions to be incrementally destroyed. The middle diagram shows an action graph a occurring in a larger one b # , which also contains an occurrence of the redex l 1 of the rule for S. The contexts C # and D # correspond to the two occurrences, which overlap. Now what is the ``just large enough'' context C which extends a to contain l 1 ? It is not quite C # , because C # has destroyed the possibility of sharing S which is o#ered by l 1 . In fact it is C as shown in the lower diagram; it may not seem ``smaller'' than C # , but it is indeed a factor of C # , as witnessed by the context E. (C # cannot be a factor of C; no context F surrounding C # can cause its S­node to be shared.) So our synthesised labelled transition system will admit the transition a C Dr 1 . We would expect to add further controls, e.g. for subtraction, before obtaining an interesting behavioural congruence. Example 4.2 (wiring) The preceding example used the forking and deletion of arcs to represent the sharing of components. This non­linearity is a pervasive feature in process calculi. CCS and the #­calculus depend heavily on it; witness the double occurrence of x in its reaction rule for CCS: • x.a | x.b a | b (and similarly for the #­calculus). The redex has no direct representation in the family of action calculi introduced in this subsection because we confine our attention to shallow, closed action graphs, i.e. ones without nesting of graphs (needed for prefixing) and free names. Without such limitations, the redex is exactly modelled by an action graph with a forked arc (representing the sharing of x) connected to two controls representing the output and input prefixes, containing inside a and b respectively. See [Mil96] for many examples. RR n° 4395 26 J.J. Leifer + Arithmetic rules + + S + 0 S S S 0 0 Garbage collection rules r 1 l 0 r 0 l 1 + 0 + S + 0 S b # (0, 0) (1, 1) (1, 1) (2, 2) a l 1 D # C # C # a = D # l 1 = b # S 0 An action graph a overlapping a redex l 1 a l 1 D # 0 S (0, 0) (1, 2) (1, 1) (2, 2) (1, 1) C # D C E Ca = Dl 1 = b S + 0 b An RPO for a and l 1 w.r.t. C # and D # Figure 12: A reactive system for arithmetic (Example 4.1) INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 27 (0, 2) (0, 2) (0, 2) (0, 0) C # C D (0, 0) (0, 2) a t 0 t 1 b t 2 t 3 D # K K K K (t 1 ,t 3 ) (t 1 ,t 2 ) (t 0 ,t 3 ) (t 0 ,t 2 ) E (0, 4) Figure 13: An RPO for copied wiring (Example 4.2) Non­linearity can give rise to RPOs which are more complex than one might expect. Figure 13 shows two identical action graphs a = b = K·c, where K : (0, 1); using the identity contexts C # = D # = - 0,2 they are embedded in K·c. But the RPO C, D,E does not consist of identity contexts! A candidate might choose to identify t 0 in a with either t 2 or t 3 in b, and similarly for t 1 . To be the ``best'' candidate, the C, D,E must handle all these pairings; to indicate this we have indexed its targets by pairs in the diagram. In fact we have Ca = Db = K·c·(c # c) . Example 4.3 (reflexion) A surprising phenomenon is how the presence of reflexion can a#ect the RPO. Let K,N : (1, 1), L : (0, 2) and M : (2, 0), and recall that i 1 is the identity of arity (1, 1) for action graph composition. Figure 14 shows a = L·(i 1 #K) and b = (i 1 #K)·M embedded in C # a = D # b = L·(N #K)·M . The contexts C # and D # do not involve reflexion. In the RPO C, D,E shown we have Ca = Db = (i 1 #L)·(p#K)·(i 1 #M ); this extends a by only one control (M) in order to create an occurrence of b. The contexts C and D do not use reflexion, but E does use it. If reflexion is forbidden then the RPO C + , D + , E + is such that C + a = D + b contains N ; this would yield a more complex synthesised labelled transition relation. These examples do not exhaust the phenomena which arise in finding RPOs in C­Ixt, but they indicate that the general construction will not be trivial. The reader may feel that, having coped informally with a number of phenomena, we are well on the way to finding RPOs in every case. However, they do not always exist in C­Ixt! Here is a counter­example. RR n° 4395 28 J.J. Leifer M N L K (0, 0) L K K L N (0, 0) (0, 0) (0, 0) (1, 1) (0, 2) (2, 0) M M a b D C E N M D # C # L N K Figure 14: An RPO using reflexion (Example 4.3) Example 4.4 (missing RPO) Let K : (0, 1) and L : (1, 0). Let a = b = K and let C # = D # = K·L #- 0,1 ·L with arity (0, 1) (0, 0). Then C # a = D # b = K·L #K·L; this is shown in the upper diagram of Figure 15. The lower diagram shows two candidate RPOs, for which it is easy to verify commutation: C 0 , D 0 , E 0 = -, -, K·L # -·L C 1 , D 1 , E 1 = -#K, K #-, -·(L # L) . But if there were an RPO, then contexts C, D,F 0 , F 1 would exist as shown making the diagram commute, yielding a contradiction as follows: Neither C nor D can contain any control, since F 0 C = F 0 D = -. Hence from CK = DK we deduce C = D, using the criterion for context equality stated above (since the control K appears in neither C nor D). Hence -#K = F 1 C = F 1 D = K #-, a contradiction. This counter­example involves neither copying nor discard of arcs, so is applicable to linear action calculi too [LM02] --- those in which all source ports bear exactly one arc. Thus we cannot attribute the lack of RPOs to c and #, even though they demand careful treatment as shown in Example 4.1 and Example 4.2. The counter­example also illustrates why RPOs do not always exist in C­Ixt. The equations C 0 K = D 0 K = K and C 1 K = D 1 K = K # K hold respectively for the two candidates; but if we ``track'' the two occurrences of a = K and b = K through these equations, we find that they correspond to the same occurrence of K in the first case, and to two di#erent occurrences in the second case. This is a key to solving our problem; we seek a suitable refinement of C­Ixt that possesses the RPOs we need. We expect its INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 29 K K K L L K K K L L L L (0, 0) (0, 0) (0, 0) (0, 1) (0, 1) (0, 0) b a D # C # A context equation C # a = D # b -·(L # L) K·L # -·L (0, 0) - K K K #- K·L # -·L K·L # -·L D -#K F 0 - F 1 (0, 0) (0, 0) (0, 1) (0, 1) impossible! (1, 1) C Figure 15: A missing RPO in C­Ixt (Example 4.4) RR n° 4395 30 J.J. Leifer contexts to track the occurrences of nodes. This is a similar idea to that of ``colouring'', which has been suggested by Sewell to replace his dissection based definitions [Sew]. The strategy is as follows. The next two subsections are devoted to the construc­ tion of A­Ixt, a well­supported precategory of arities and raw contexts. Replaying the constructions of Section 3, we derive two categories from A­Ixt and a functor be­ tween them F : “ C­Ixt C­Ixt. Finally we state the RPO existence theorem for “ C­Ixt (Theorem 4.16), thus showing that F has all redex­RPOs (Theorem 4.17). 4.4 Closed shallow action graphs In this subsection, after introducing some notation, I define a class of action graphs. These graphs are enriched in the next subsection to form raw contexts (graphs with a hole in them), the arrows of the precategory A­Ixt. No attempt is made to verify formally that the action graphs presented here correspond to action calculi terms quotiented by the action calculi axioms (which are not presented here). Such an undertaking represents future work and will be of more value when the tractable graph­theoretic features include free names and nesting. Notation I write [m] for the ordinal number {0, 1, . . . , m-1}. The disjoint sum # i#I X i of a family of sets is taken to be the set # i#I ({i} ×X i ). A particular case is when I = [n]; then the disjoint sum may be written, without parentheses, as X 0 + X 1 + · · · + X n-1 . Examples in this section take the form S = # v#V S v + [m] + [n], a ternary disjoint sum, the first summand of which is itself a disjoint sum; S has elements of the form (0, (v, s)) for each v # V and s # S v , (1, i) for each i # [m], and (2, j) for each j # [n]. If the sets X and Y are disjoint, I often write their union as X #Y . This notation is to be distinguished from a disjoint sum. In particular, (X 1 #X 2 )#X 3 = X 1 #(X 2 #X 3 ) and will often be written without parentheses; on the other hand, the disjoint sums X 1 +X 2 +X 3 , (X 1 + X 2 ) + X 3 and X 1 + (X 2 + X 3 ) are all distinct but in bijective correspondence. If f : X Z and g : Y Z are two functions with X disjoint from Y , then f#g : X#Y Z is their union. I use f : X # Y , f : X # Y and f : X ## Y for respectively injective, surjective and bijective functions, and f : X ## Y for an injection which is an inclusion. Finally, # denotes function composition, Id X the identity function on the set X, and #X the empty function from # to X. Definition 4.5 (control signature) We fix a control signature K, a set of controls, equipped with an arity function called arity : K N 2 and let K, L, . . . range over K. For arity(K) = (m, n) we write K : (m, n); in this case, two functions extract the components of the pair: arin(K) “ = m and arout(K) “ = n. # INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 31 Definition 4.6 (action graphs) A (closed, shallow) action graph G = (m, n, V, contr , src) comprises an arity (m, n), a set V of nodes, called a support, a control map contr : V K assigning a control in K to each node in V , and a source map src : T S assigning a source (port) in S to each target (port) in T , where ˆ the source set S “ = # v#V [arout(contr(v))] + [m] comprises the binding sources for each v # V and the input sources indexed by [m]; ˆ the target set T “ = # v#V [arin(contr(v))] + [n] comprises the argument targets for each v # V and the output targets indexed by [n]. # Nomenclature We may write a graph as G = (V, contr , src) : (m, n), or just G = (V, contr , src) when the arity is understood. We denote the empty graph (#, #K , ## ) : (0, 0) by 0. We shall abbreviate arin(contr(v)) to arin(v) etc., when there is no ambiguity. We denote the injections induced by the disjoint sums S and T as follows: bind(v) : [arout(v)] # S for the binding sources of each v # V ; in : [m] # S for the input sources; arg(v) : [arin(v)] # T for the argument targets of each v # V ; out : [n] # T for the output targets. # We shall write bind(v, i) and arg(v, j) for the ports bind(v)(i) and arg(v)(j). For any injection f into a set A we write A f for the range of f ; thus for example S in is the set of all input sources and T arg(v) the set of argument targets of v. We shall also write for example S bind for # v#V S bind(v) . With this notation we can represent our partitions as S = S in # S bind T = T out # T arg . An example of an action graph with arity (1, 3) is shown in Figure 16, with node names and the control map omitted. The whole graph is in a rectangle, with input sources at the left and output targets at the right. Nodes are drawn as rectangles with two corners blunted to give orientation; we may want to tilt some of them, as here, or even turn them upside down. The three nodes have arities (1, 1), (2, 1) and (1, 2). The arcs represent the source map, with arrows pointing from source to target. Ports could be drawn as blobs, but this is somewhat redundant; a target is always indicated by exactly one incoming arc, and we indicate a source with no outgoing arcs by a little aborted arc. Cycles are allowed. The graphs studied here are for action calculi which are closed, meaning that free names such as x, y, . . . are not used as sources, and shallow, meaning that nodes do not contain action graphs nested inside. I study the closed, shallow action RR n° 4395 32 J.J. Leifer Figure 16: A closed shallow action graph graphs in this paper as a preliminary to future work on a full graphical presentation of action calculi, since notions such as graph contexts are more clearly handled in this simpler setting. Convention Action graphs are almost always denoted by G suitably subscripted. Rather than always explicitly list all their primary components V , contr , and src, or their derived components S, T , bind , in etc., we shall follow a firm convention that the names of these components are standard, decorated as necessary to connote the graph's name. 4.5 The well­supported precategory A­Ixt of arities and raw contexts I proceed now to construct the well­supported precategory A­Ixt of raw contexts with a support function and support translation operation (Definition 3.2). The intuition of ``context'' is well­supplied by Figure 17; the graph G occurs inside the dotted rectangle in G # , and we may think of the context in which G is placed as that part of G # lying outside the dotted rectangle. A context is therefore an action graph, but with a little more structure since it has an internal as well as an external interface. The internal interface is often called a hole. (I do not consider here contexts with more than one hole.) The lower diagram shows the context C which results when G is excised from G # ; in the notation of what follows, G # = CG (C composed with G). Note the new targets and sources on respectively the left and right sides of C's internal interface; in particular, INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 33 G # G The action graph G is a subgraph of G # C The corresponding context Figure 17: The bottom context composed with the middle action graph yields the top action graph RR n° 4395 34 J.J. Leifer the middle internal source lacks any targets and therefore represents the discard of the corresponding output target of G --- or of any other graph --- when placed in the hole. Definition 4.7 (raw context) A (closed, shallow, loose) raw context A = (V, contr , src) of arity (m # , n # ) to (m, n), written A : (m # , n # ) (m, n), comprises a support V , which is a set of nodes, a control map contr : V K assigning a control in K to each node in V , and a source map src : T S assigning a source (port) in S to each target (port) in T , where ˆ the source set S “ = # v#V [arout(v)] + [m] + [n # ] comprises the binding sources for each v # V , the input sources indexed by [m], and the upput sources indexed by [n # ]; ˆ the target set T “ = # v#V [arin(v)] + [n] + [m # ] comprises the argument targets for each v # V , the output targets indexed by [n], and the downput targets indexed by [m # ]. Furthermore, we require that the looseness condition is satisfied (see nomenclature defined below): src(T down ) # S up = # . Loose The looseness condition precludes a ``tight'' loop from the back of the hole to the front, such as is formed by reflexion in action calculi. It does not preclude such a loop proceeding via a control, which indeed occurs in Figure 17; thus the contexts permit only limited reflexion, which simplifies the definition of composition. (See Section 5 for further discussion.) Finally, |A| is the support of A, i.e. V in this case. # Note that an action graph G is just a raw context A as above in which m # = n # = 0. Nomenclature As for action graphs, there are induced injections for raw contexts as follows: bind(v) : [arout(v)] # S for the binding sources of each v # V ; in : [m] # S for the input sources; up : [n # ] # S for the upput sources; arg(v) : [arin(v)] # T for the argument targets of each v # V ; out : [n] # T for the output targets; down : [m # ] # T for the downput targets. With naming similar to that in action graphs for the partitions of S and T , we have S = S bind # S in # S up T = T arg # T out # T down . INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 35 A 0 A 1 T down 0 S in 1 S up 0 T down 1 S in 0 S up 1 T out 1 T out 0 Figure 18: The composition of two raw contexts Raw contexts cannot be composed when the supports of each operand in a composi­ tion intersect non­trivially. Composition is well­defined when the operands have disjoint supports--- one of the required properties of a well­supported precategory (Definition 3.2). Definition 4.8 (identity and composition for raw contexts) The identity raw context id (m,n) = (#, #K , src) : (m, n) (m, n) has S “ = #+ [m] + [n] = S in # S up T “ = #+ [n] + [m] = T out # T down src : # down(i) ## in(i) i # [m] out(j) ## up(j) j # [n] . Let A i = (V i , contr i , src i ) : (m i , n i ) (m i+1 , n i+1 ) be two raw contexts for i = 0, 1, with V 0 # V 1 = #. Their composition, illustrated in Figure 18 by nesting A 0 inside A 1 , is A 1 # A 0 “ = A 2 = (V 2 , contr 2 , src 2 ) : (m 0 , n 0 ) (m 2 , n 2 ) , where V 2 “ = V 1 # V 0 and contr 2 “ = contr 1 # contr 0 (thus determining arin 2 = arin 1 # arin 0 and likewise arout 2 , bind 2 , arg 2 ), and S 2 “ = # v#V 2 [arout 2 (v)] + [m 2 ] + [n 0 ] = (S bind 1 # S bind 0 ) # S in 1 # S up 0 T 2 “ = # v#V 2 [arin 2 (v)] + [n 2 ] + [m 0 ] = (T arg 1 # T arg 0 ) # T out 1 # T down 0 . Note (see Figure 18) that T down 1 is in bijection with S in 0 and [m 1 ], while S up 1 is in bijection with T out 0 and [n 1 ]. It remains to define the source function src 2 ; this is done in terms of two auxiliary functions # i : S i S 2 (i = 0, 1) which describe how sources of A 0 and A 1 RR n° 4395 36 J.J. Leifer ``become'' sources of A 2 : # 0 (s) “ = # s if s # S bind 0 # S up 0 src 1 down 1 (i) if s = in 0 (i) # S in 0 # 1 (s) “ = # s if s # S bind 1 # S in 1 # 0 src 0 out 0 (j) if s = up 1 (j) # S up 1 src 2 (t) “ = # # 1 src 1 (t) if t # T arg 1 # T out 1 # 0 src 0 (t) if t # T arg 0 # T down 0 . # We have adopted the symbol `` # '' for composition of raw contexts as a reminder that it is partial: the supports of the operands are required to be disjoint in order for a composition to be defined. Proposition 4.9 (raw contexts form a precategory) If A 0 and A 1 are raw contexts with |A 1 | # |A 0 | = # then A 1 # A 0 is a raw context too. (In particular, # preserves the Loose condition.) Composition is associative and has identity id (in the way required of a precategory, see Definition 3.1). Proof Follows immediately from Propositions 21 and 22 of [CLM00]. # By definition composition satisfies Supp­comp and Supp­id (Definition 3.2), i.e. |A 1 # A 0 | = |A 1 | # |A 0 | Supp­comp |id m | = # . Supp­id The only task remaining in order to show that A­Ixt is a well­supported precategory is the definition of a support translation operation and the verification of its properties. Definition 4.10 (support translation for raw contexts) Given a raw context A : (m 0 , n 0 ) (m 1 , n 1 ) and an injection # whose domain contains the support of A, i.e. Dom # # |A|, we define the support translation by # of A, written # # A, as follows: # # A “ = A # , where: V # “ = #V contr # (v) “ = contr(# -1 (v)) thus determining arin, arout , bind , arg S # “ = # v#V # [arout # (v)] + [m 1 ] + [n 0 ] T # “ = # v#V # [arin # (v)] + [n 1 ] + [m 0 ] thus determining bijections # S : S ## S # and # T : T # ## T whence we define: src # “ = # S # src # # T . # INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 37 This definition satisfies the appropriate healthiness conditions: Proposition 4.11 (support translation is well­defined) If A satisfies Loose then so does # # A, thus # # (·) is a well­defined operation on raw contexts. Proof Immediate from src # “ = # S # src # # T , since # S and # T are the identity on upput sources and downput targets respectively. (Proposition 24 in [CLM00].) # Furthermore, support translation satisfies the remaining axioms in the definition of a well­supported precategory (Definition 3.2): Proposition 4.12 (support translation properties) All of the following properties hold: # # id m = id m Trans­id­r # # (A 1 # A 0 ) = # # A 1 # # # A 0 Trans­comp­r Id |A| # A = A Trans­id­l (# 1 # # 0 ) # A = # 1 # (# 0 # A) Trans­comp­l # 0 # |A| = # 1 # |A| implies # 0 # A = # 1 # A Trans­res |# # A| = #|A| . Trans­supp Proof All of these except the last follow from Proposition 25 in [CLM00]. Trans­supp follows immediately from Definition 4.10. # Thus: Theorem 4.13 A­Ixt is a well­supported precategory. # 4.6 Constructing a functorial reactive system Having established that A­Ixt is a well­supported precategory, the rest of the results of Section 3 are immediately applicable, as we next see. We let “ C­Ixt be the track of A­Ixt (Definition 3.3), a category of profiles and insertion contexts. The arrows are called ``insertion contexts'' to remind us that they ``insert'' the nodes of the domain profile into the codomain profile. Now let C­Ixt be the support quotient (Definition 3.10) of A­Ixt. Finally let F : “ C­Ixt C­Ixt be the support­quotienting functor (Definition 3.12). Then by Theorem 3.14, F lifts arrows by their domain, creates isos, and creates compositions. By Theorem 3.15, F allows IPO sliding. A­Ixt has a distinguished object (0, 0): as stated immediately after Definition 4.7, a raw context with domain (0, 0) is identical to an action graph. Recall that C­Ixt has the same objects as A­Ixt does, so the distinguished object 0 of C­Ixt (viewed as a reactive system) is just (0, 0). Likewise, let # “ = (0, 0, #), the distinguished object for “ C­Ixt. Since F(#) = 0, we have that F lifts agents, and thus: RR n° 4395 38 J.J. Leifer Theorem 4.14 (F is functorial reactive system) The support­quotienting functor F : “ C­Ixt C­Ixt is a functorial reactive system for any choice of D and Reacts. # Thus all the congruence results of Section 3 in Part 1 are applicable to F (except Theorem 3.34 since we are not dealing with multi­hole contexts) with one proviso: we wish to determine choices of D and Reacts such that F has all redex­RPOs. # # # # # p 0 p 1 p G 0 G 1 A 0 A 1 19 With regard to D, the strongest result obtainable is with D = C­Ixt, i.e. with all contexts in C­Ixt reactive, so let us fix on this. Recall from Definition 2.6, that F has all redex­RPOs if any square in “ C­Ixt, such as in Figure 19, has an RPO provided that there exists r # C­Ixt such that (F(# G 1 p 1 ), r) # Reacts. So the key question is: for which choice of redexes l (first components of the Reacts relation) do there exist RPOs in “ C­Ixt for squares such as Figure 19 where F(# G 1 p 1 ) = l. The answer is that for almost an any choice of redexes, except the most pathological, RPOs exist. In order to make precise which are these pathological cases, we need a definition about action graphs. Definition 4.15 (output­controlled) In any graph, a target is controlled if its source is a bound source. G is output­controlled if all its output targets are controlled; formally: src(T out ) # S bind . (output­controlled) Since Cod src = S in # S bind , an equivalent formulation is: src(T out ) # S in = # . (output­controlled) # Informally, a graph satisfies this definition when it contains no ``floating'' wires con­ necting the left­hand interface ports with the right­hand ones. Recall that in “ C­Ixt a context # G (m, n, U ), whose domain is the empty profile #, is actually a graph G : (m, n) with |G| = U . Thus the definition of output­controlled applies to contexts in “ C­Ixt with domain #. RPOs do exist provided one of the legs is output­controlled: Theorem 4.16 Let C 0 G 0 = C 1 G 1 = G in “ C­Ixt, where G 1 is output­controlled. Then there exists an RPO for G 0 , G 1 w.r.t. C 0 , C 1 . Proof See Corollary 6.28 in [Lei01b]. # Now note that if G is output­controlled then # # G is too for any injection # with Dom # # |G|. Thus it is well­defined to say that a context with domain (0, 0) in C­Ixt (the category formed by quotienting out support translations) is output­controlled. INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 39 Because Theorem 4.16 is asymmetric in the use of the output­controlled hypothesis, it directly implies the following. Theorem 4.17 (F has all redex­RPOs) The functorial reactive system F : “ C­Ixt C­Ixt has all redex­RPOs provided that every redex is output­controlled, i.e. pro­ vided that for all (l, r) # Reacts, l is output­controlled. # Happily, the requirement that redexes be output­controlled is a tolerable one since redexes that are not are pathological (see Chapter 7 in [Lei01b]). Finally, Theorem 4.17 implies that all of the congruence results of Section 3 in Part 1 (except the one for multi­ hole contexts) are immediately applicable to F : “ C­Ixt C­Ixt, as desired. RR n° 4395 40 J.J. Leifer 5 Conclusions and future work Constructing RPOs is di#cult, as witnessed by the daunting complexity in Chapter 6, ``RPOs for action graph contexts'', in [Lei01b] (the proof of Theorem 4.17 in the present paper). It is therefore desirable that it not be done afresh for each new process calculus. This is the impetus for the leading example in this paper, namely action calculi­like con­ texts. Recall that the functorial reactive system F : “ C­Ixt C­Ixt is really a family with varying choices of control signature K and of reaction rules Reacts. The fragment of action calculi considered in Section 4 is thus a framework : if one can express states of a computational model using controls (for atoms) and arcs (for names and sharing) and reactions in terms of redexes that satisfy the condition output­controlled then RPOs exist and hence Section 3 of Part 1 gives labelled transitions and operational congruences. A framework is often deficient for two reasons: (i) it provides insu#cient benefits to compensate for the e#ort of casting a specific example in the framework's form; (ii) it is not rich enough to cover all the phenomena that one wants. Criticism (ii) hits home. The fragment of action calculi presented in this paper is inadequate for most purposes: there is no nesting of action graphs (needed for prefixing), no free names, no binding, limited reflexion, no choice operator, and no multi­hole redexes (needed to represent faithfully metavariables in reaction rules). I describe future work below that addresses these other issues. Criticism (i), however, is unjustified when applied to the action calculi shown here: getting ``for free'' a labelled transition system and a collection of operational congruences is a worthwhile benefit. The reverse situation held for action calculi as originally presented by Milner [Mil96]: criticism (ii) was not such a problem but criticism (i) was: up until now there has been little tangible reward to using action calculi to present specific examples of process calculi. The central goal of future work is to construct a framework with rich enough structure (perhaps like Milner's original action calculi) to dodge criticism (ii) while still providing the rewards of labelled transitions and operational congruences. To this end, it will be important to pursue several research directions: multi­hole redexes: The basic reaction rule of the #­calculus is • x#y#.a | x(z).b a | {y/z}b . (3) There is a problem of adequately representing (3) in a reactive system. Currently I require that the reaction rules Reacts consist of pairs of agents, not agent contexts. As a result, the only way to represent (3) is via an infinite family of rules, one for each possible instantiation of a and b. Thus there might be labelled transitions of the form • x#y# -|x(z).b (4) INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 41 out in in x y Figure 20: Nesting of nodes for all instantiations of b. But these are ungainly labels: the only important part of any label of the form - | x(z).b is the top­level structure, namely x(z); the b is irrelevant. How can we winnow down the family of labels to a single one? The answer lies in using the uniformity present in (3). The a and b there are really metavariables and the rule can be expressed thus: • x#y#.- 1 | x(z).- 2 - 1 | {y/z}- 2 . (5) This rule consists of a pair of 2­hole contexts which capture the uniformity present in it. In Figure 13 of [Mil01], Milner proposes a formalisation of exactly this rule in his bigraphical reactive systems, which cater directly for multi­hole contexts. If we relax the condition on Reacts and allow it to contain pairs of contexts (L, R) for which L, R : m n are arbitrary contexts, then it is easy to generate the reaction relation (forgetting about the details of D) A A # i# (#(L, R) # Reacts, C, D. A = DLC & A # = DRC) . # # # # B A F C L D B # F # C # D # 21 Contrast this to Proposition 2.7 for which the reaction rules are closed­up under context application on the outside, not also on the inside (as shown here). The hard problem is to define labelled transitions A F A # . We cannot rely on IPOs anymore since the domain of A is potentially di#erent from the domain of any redex L. A possible replacement for IPOs might be via hexagon idem pushouts (which are special kinds of hexagon relative pushouts) as suggested by Sewell. Notice how L and A are wrapped up in Figure 21 by arrows RR n° 4395 42 J.J. Leifer composed on either side. The hexagon idem pushout property guarantees that there is no lesser hexagon bounded by B # , C # , F # , D # . It seems plausible that such hexagons can yield the single labelled transition • x#y# - 1 |x(z).- 2 from (5), which is lighter than having the infinite family shown in (4). In [Sew], Sewell already exploited the uniformity present in reaction rules when looking at term algebras with parallel composition. He achieved lightweight labelled transitions, but made use of complex context dissection lemmas. He is now look­ ing at the problem of recasting his results in terms of universal constructions (such as hexagons). In conclusion, there are two important lines of research related to multi­hole redexes which mirror what was done in my paper: (i) defining labelled transitions by universal constructions and proving congruence for a variety of equiv­ alences and preorders; (ii) showing that the relevant universal constructions exist in categories of interest (term algebras, graphs, etc.). nesting: The nesting of agents inside nodes is essential for representing prefixing. For example, in CCS the agent x.y.•x contains three levels of nesting with the name x shared by the outermost and the innermost. In order to represent this with graph­ like constructions, we need that each node packages up the continuation agent, e.g. as in Figure 20 which gives a possible representation of the CCS agent above. At first glance, nesting is a trivial thing: term algebras, for instance, consists of just pure nesting structure with nothing else. It is straightforward to calculate RPOs for them. However the real challenge is the combination of wiring and nesting: Figure 20 has an arc sourced by x that is forked and has targets at multiple levels. In particular, even the notion of context composition is di#cult: when composing contexts that fork an arc at di#erent nesting levels, the forks have to be normalised in some way, either by pushing them in to the innermost level or pulling them out to the outermost. There are many possible representations for nested graphs. One that seems most promising comes out of recent work by Milner [Mil01]: the idea is to treat a nested graph as a flat graph with an added parent function overlaid, a so called topograph structure. RPOs can then be calculated by handling the wiring structure and the nesting structure orthogonally. Even without the full power of nesting, it may be possible to handle the #­calculus (or variants thereof) indirectly. Honda and Yoshida [HY94a] give a translation in terms of ``concurrent combinators''; these encode prefixing in a flat structure by using triggers to point to parts of agents that may execute. A synthesised labelled transition relation for their combinator reaction rules might be too intensional since the labels could detect exactly the combinators present in an agent. It is worth trying this, though, to see what kind of equivalences would transpire. INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 43 free names and binding: It is straightforward to add free names to graphs: the idea is to enrich the set of source ports to include names. It is more subtle though to make precise how a context can bind the names of the thing that goes in its hole. It seems likely that the objects of the category of contexts need to contain name sets to ensure that RPOs exist (analogously to inclusion of node sets in “ C­Ixt), i.e. a context is an arrow of the form (m, n, U, X) (m # , n # , U # , X # ), meaning that its hole is expecting a context with support (nodes) U and names X. (This is similar to Definition 67 in Milner's work on bigraphical reactive systems [Mil01].) It is not clear whether the downstairs category (the analogue of C­Ixt) should include these name sets. For example, in #­calculus we write the binding context (#x)- without saying which names can fit in the hole. Perhaps the functor from upstairs to downstairs (like F : “ C­Ixt C­Ixt in this paper) will allow two kinds of IPO sliding: the first with respect to nodes (as I have shown here) and the second with respect to names. There has been recent work on modelling names and name binding in a categorical way [TFP99, GP99] and it would be exciting to join together those syntactic models with operational semantics, and in particular, the reactive systems shown here. Name binding carries with it the problem of scope extrusion in labelled transitions. In #­calculus, for example, it is a subtle problem to handle the labelled transition of (#x)(•y#x#). There are many ways of handling this when looking at bisimulation, for example, but most involve augmenting the definition with freshness side conditions to cater explicitly for extrusion. An alternate approach [CS00] keeps track of extruded names as annotations of the agents themselves, thus gaining the power of extrusion but keeping the simplicity of bisimulation without added conditions. Adding these annotations seems almost identical to adding name sets in the objects of a context category (as outlined above). sum: As discussed in Subsection 3.5 in Part 1, the proper treatment of summation (such as occurs in CCS and the #­calculus) requires care. It is not good enough for sum to be a free operator (just another control) if we want to describe its reactive behaviour, e.g. (•x.a + b) | (x.a # + b # ) a | a # #.a + b a . Consider the second reaction rule. In order for the sum to be rearranged so that #.a is on the left and the rest is on the right, we require + to be commutative, associative, and have the empty agent as an identity. The same problem surfaces for other operators that change the structural congruence (syntactic equality). In the #­calculus, for example, replication is handled by the RR n° 4395 44 J.J. Leifer axiom ! a # a | ! a . (6) This seems hard to represent in terms of graphs since the RHS has, potentially, more nodes than the LHS. When the problems of finding graph theoretic representation of sum and replication are overcome (see Milner's proposal in Figures 12 and 13 of [Mil01]), it may still be di#cult to construct RPOs. A possible solution, at least for replication, is to disallow the structural equality in (6), and instead confine replication to be input guarded and to have a reaction rule of the form • x#y# | ! x(z).a {y/z}a | ! x(z).a . This is a commonly done in asynchronous variations of #­calculus [HT91]. Another way of handling replication is via an encoding in terms of combinators (already mentioned above) [HY94b]. For input guarded summation, encoding [NP96] is also an option. full reflexion: The contexts considered in Section 4 have only a limited form of reflexion, as enforced by the condition Loose that prevents tight loops linking a hole to itself. This simplifying assumption makes the composition of contexts and the composition of the associated embeddings easy. (Embeddings, which are morphisms between graphs, are not introduced in this paper but play a central role in the construction of RPOs; see Section 6.2 in [Lei01b].) With full reflexion, the composition of contexts can create arcs that are formed from arbitrarily many segments of arcs present in the inner and outer context. Indeed, it is di#cult to prove even that the composition of reflexive embeddings is associative [Lei01a]. Better technology for handling reflexion has been developed in [LM02] for graphs with linear wiring. Proving the existence of RPOs for full reflexion with non­linear wiring represents a future challenge. inductive presentation of labelled transitions: In Part 1, the way of deriving la­ belled transitions from reactions yields a direct characterisation. This is in contrast to the inductive presentation usually found in the process calculus literature. Can the gap be bridged, though? In other words, can an inductive presentation of labelled transitions be synthesised from reaction rules? It seems plausible. For any partic­ ular reactive system whose syntax is generated from some constructors, one could instantiate Lemma 2.17 of Part 1 (recalled here) by substituting each constructor for C: C F # F C # is an IPO a F # a ## C # # D Ca F C # a ## . INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 45 There are several interesting questions that follow: Under what conditions can we synthesise an inductive presentation that generates precisely the same labelled tran­ sition relation as the direct presentation gives? Under what conditions would an inductive presentation satisfy any of the GSOS rule formats [GV92, Blo93]? If some set of the latter is satisfied, it would be enlightening to compare two di#erent proofs of congruence for strong bisimulation, say --- one based on the RPO theory shown in this paper and the other based on GSOS reasoning, particularly as provided by recent categorical treatments of the latter [TP97]. It is not surprising that some of these areas (e.g. free names and multi­hole redexes) require changes to the categorical abstractions of a reactive system, not just cleverer ways of constructing RPOs. This pattern is well­established in this series of papers. I started with reactive systems, then passed to functorial reactive systems when it became clear that RPOs needed to be calculated in a separate category, then considered functorial monoidal reactive system to cater explicitly for RPOs resulting in multi­hole contexts. As argued in Subsection 3.7, it may be advantageous to make an orthogonal extension, replacing categories by bicategories throughout. An intriguing possibility is that this extension is not truly ``orthogonal'', i.e. the power of enriched category theory could be brought to bear on the problems listed above. A test of the future work outlined above is to see what labelled transitions and opera­ tional congruences are generated for applications such as CCS, #­calculus, #­calculus, and ambients. It would be exciting (though not likely) to get congruences that coincide exactly with well­known ones (open bisimulation for #­calculus, say). It should not be a cause for dejection if the derived congruences do not match exactly the historically established ones: #­calculus comes with a zoo of bespoke congruences, no single one of which is good for all applications. The best outcome of this work will be if the mathematical tools that are proposed here ease the path for exploring new primitives and new patterns of behaviour inherent in distributed computing. The development of mathematical techniques for reasoning about hosts and host failure, agent mobility, and cryptography, for example, is critical for guiding infrastructure and language design. Proofs techniques for these models are critical for precise reasoning. Much work needs to be done before the tools of this paper are good enough to address these applications. RR n° 4395 46 J.J. Leifer References Curly braces enclose pointers back to the pages in this paper that cite the work. [BF00] M. Bunge and M. P. Fiore. Unique factorisation lifting functors and categories of linearly­controlled processes. Mathematical Structures in Computer Science, 10(2):137--163, 2000. {17} [Blo93] B. Bloom. Structural operational semantics for weak bisimulations. Techni­ cal Report TR­93­1373, Department of Computer Science, Cornell University, August 1993. {45} [CLM00] G. L. Cattani, J. J. Leifer, and R. Milner. Contexts and embeddings for closed shallow action graphs. Technical Report 496, Computer Laboratory, University of Cambridge, July 2000. Available from http://pauillac.inria.fr/#leifer/. {23, 36, 37} [Con72] F. Conduch’e. Au sujet de l'existence d'adjoints ‘a droite aux foncteurs ``image r’eciproque'' dans la cat’egorie des cat’egories. Comptes rendus de l'Acad’emie des sciences A, pages 891--894, 1972. {17} [CS00] G. L. Cattani and P. Sewell. Models for name­passing processes: interleaving and causal. In 15th Annual IEEE Symposium on Logic in Computer Science, 26--29 June 2000, Santa Barbara, California, USA, pages 322--332. IEEE Press, 2000. {43} [GP99] M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In 14th Annual Symposium on Logic in Computer Science, 2--5 July, 1999, Trento, Italy, pages 214--224. IEEE Press, 1999. {43} [GV92] J. F. Groote and F. W. Vaandrager. Structural operational semantics and bisim­ ulation as a congruence. Information and Computation, 100(2):202--260, 1992. {45} [Has99] M. Hasegawa. Models of sharing graphs: a categorical semantics of let and letrec. BCS Distinguished Dissertation Series. Springer­Verlag, 1999. {25} [Hon00] K. Honda. Elementary structures for process theory (1): sets with renaming. Mathematical Structures in Computer Science, 10(5):617--663, October 2000. {10} [HT91] K. Honda and M. Tokoro. An object calculus for asynchronous communica­ tion. In ECOOP '91: European Conference on Object­Oriented Programming, INRIA Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 47 Geneva, Switzerland, July 15--19, 1991, Proceedings, volume 512, pages 133--147. Springer­Verlag, 1991. {44} [HY94a] K. Honda and N. Yoshida. Combinatory representation of mobile processes. In POPL '94: 21st ACM SIGPLAN­SIGACT Symposium on Principles of Pro­ gramming Languages, Portland, Oregon, January 17--21, 1994, pages 348--360. ACM Press, 1994. {42} [HY94b] K. Honda and N. Yoshida. Replication in concurrent combinators. In Theoreti­ cal Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19--22, 1994, Proceedings, volume 789, pages 786--805. Springer­ Verlag, 1994. {44} [Joh99] P. Johnstone. A note on discrete Conduch’e fibrations. Theory and Application of Categories, 5(1):1--11, 1999. {17} [JSV96] A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119(3):425--446, 1996. {23} [Laf90] Y. Lafont. Interaction nets. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, Cal­ ifornia, January 1990, pages 95--108. ACM Press, 1990. {25} [Lei01a] J. J. Leifer. A category of action graphs and reflexive embeddings. Technical report, Computer Laboratory, University of Cambridge, 2001. To appear. {44} [Lei01b] J. J. Leifer. Operational congruences for reactive systems. PhD thesis, Computer Laboratory, University of Cambridge, 2001. Available in revised form as Tech­ nical Report 521,Computer Laboratory, University of Cambridge, 2001, from http://pauillac.inria.fr/#leifer/. {2, 23, 38, 39, 40, 44} [Lei02] J. J. Leifer. Synthesising labelled transitions and operational congruences in reactive systems, part 1. 2002. Submitted for publication. Available from http://pauillac.inria.fr/#leifer/. {2} [LM02] J. J. Leifer and R. Milner. Shallow linear action graphs and their embeddings. Formal Aspects of Computing, 2002. To appear. Special issue in honour of Rod Burstall. Available from http://pauillac.inria.fr/#leifer/. {28, 44} [Mil94] R. Milner. Action calculi V: reflexive molecular forms. Third draft; with an appendix by O. Jensen. Available from: ftp://ftp.cl.cam.ac.uk/users/rm135/ac5.ps.Z, 1994. {23} [Mil96] R. Milner. Calculi for interaction. Acta Informatica, 33(8):707--737, 1996. {23, 25, 40} RR n° 4395 48 J.J. Leifer [Mil01] R. Milner. Bigraphical reactive systems: basic theory. Technical Report 523, Computer Laboratory, University of Cambridge, 2001. Available from http://www.cl.cam.ac.uk/#rm135/. {20, 41, 42, 43, 44} [MSS00] P. Mateus, A. Sernadas, and C. Sernadas. Precategories for combining proba­ bilistic automata. In M. Hofmann, G. Rosolini, and D. Pavlovic, editors, Proc. CTCS '99, volume 29 of Electronic Notes in Theoretical Computer Science. El­ sevier Science, 2000. {9} [NP96] U. Nestmann and B. C. Pierce. Decoding choice encodings. In CONCUR '96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26--29, 1996, Proceedings, volume 1119 of Lecture Notes in Computer Science. Springer­ Verlag, 1996. {44} [Sew] P. Sewell. From rewrite rules to bisimulation congruences. Theoretical Computer Science. To appear. {30, 42} [TFP99] D. Turi, M. P. Fiore, and G. D. Plotkin. Abstract syntax and variable binding. In 14th Annual Symposium on Logic in Computer Science, 2--5 July, 1999, Trento, Italy, pages 193--202. IEEE Press, 1999. {43} [TP97] D. Turi and G. Plotkin. Towards a mathematical operational semantics. In 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 -- July 2, 1997, pages 280--291. IEEE Press, 1997. {45} INRIA Unité de recherche INRIA Rocquencourt Domaine de Voluceau ­ Rocquencourt ­ BP 105 ­ 78153 Le Chesnay Cedex (France) Unité de recherche INRIA Lorraine : LORIA, Technopôle de Nancy­Brabois ­ Campus scienti£que 615, rue du Jardin Botanique ­ BP 101 ­ 54602 Villers­lès­Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu ­ 35042 Rennes Cedex (France) Unité de recherche INRIA Rhône­Alpes : 655, avenue de l'Europe ­ 38330 Montbonnot­St­Martin (France) Unité de recherche INRIA Sophia Antipolis : 2004, route des Lucioles ­ BP 93 ­ 06902 Sophia Antipolis Cedex (France) Éditeur INRIA ­ Domaine de Voluceau ­ Rocquencourt, BP 105 ­ 78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN 0249­6399