BRICS RS-03-1 Sassone & Sobocinski: Deriving Bisimulation Congruences: 2-Categories vs. Precategories BRICS

Basic Research in Computer Science

Deriving Bisimulation Congruences: 2-Categories vs. Precategories

Vladimiro Sassone Pawe� Sobocinski BRICS Report Series RS-03-1 ISSN 0909-0878 January 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Vladimiro Sassone & Pawe� Sobocinski.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/03/1/

Deriving Bisimulation Congruences: 2-categories vs precategories^{∗}

Vladimiro Sassone Pawe� Sobociński

University of Sussex University of Aarhus

Abstract

G-relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner’s approach to deriving labelled bisimulation congruences from reduction systems. This paper develops the theory of GRPOs further, arguing that they provide a simple and powerful basis towards a comprehensive solution. As an example, we construct GRPOs in a category of ‘bunches and wirings.’ We then examine the approach based on Milner’s precategories and Leifer’s functorial reactive systems, and show that it can be recast in a much simpler way into the 2-categorical theory of GRPOs.

Introduction

It is increasingly common for foundational calculi to be presented as reduction systems. Starting from their common ancestor, the λ calculus, most recent calculi consist of a reduction system together with a contextual equivalence (built out of basic observations, viz. barbs). The strength of such an approach resides in its intuitiveness. In particular, we need not invent labels to describe the interactions between systems and their possible environments, a procedure that has a degree of arbitrariness (cf. early and late semantics of the π calculus) and may prove quite complex (cf. [5, 4, 3, 1]).

∗Research supported by ‘DisCo: Semantic Foundations of Distributed Computation’, EU IHP ‘Marie Curie’ contract HPMT-CT-2001-00290, and BRICS, Basic Research in Computer Science, funded by the Danish National Research Foundation.

By contrast, reduction semantics suffer at times by their lack of compositionality, and have complex semantic theories because of their contextual equivalences. Labelled bisimulation congruences based on labelled transition systems (LTS) may in such cases provide fruitful proof techniques; in particular, bisimulations provide the power and manageability of coinduction, while the closure properties of congruences provide for compositional reasoning.

To associate an LTS with a reduction system involves synthesising a compositional system of labels, so that silent moves (or τ-actions) reflect the original reductions, labels describe potential external interactions, and all together they yield a LTS bisimulation which is a congruence included in the original contextual reduction equivalence. Proving bisimulation is then enough to prove reduction equivalence.

Sewell [19] and Leifer and Milner [13, 11] set out to develop a theory to perform such derivations using general criteria; a meta-theory of deriving bisimulation congruences. The basic idea behind their construction is to use contexts as labels. To exemplify the idea, in a CCS-like calculus one would for instance derive a transition

a.P ▶^{−|ā.Q} P | Q

because term a.P in context − | ā.Q reacts to become P | Q; in other words, the context is a trigger for the reduction.

The first hot spot of the theory is the selection of the right triggers to use as labels. The intuition is to take only the “smallest” contexts which allow a given reaction to occur. As well as reducing the size of the LTS, this often makes the resulting bisimulation equivalence finer. Sewell’s method is based on dissection lemmas which provide a deep analysis of a term’s structure. A generalised, more scalable approach was later developed in [13], where the notion of “smallest” is formalised in categorical terms as a relative-pushout (RPOs). Both theories, however, do not seem to scale up to calculi with non trivial structural congruences. Already in the case of the monoidal rules that govern parallel composition things become rather involved.

The fundamental difficulty brought about by a structural congruence ≡ is that working up to ≡ gives up too much information about terms for the RPO approach to work as expected. RPOs do not usually exist in such cases, because the fundamental indication of exactly which occurrences of a term constructor belong to the redex becomes blurred. A very simple, yet significant example of this is the category Bun of bunch contexts [13], and the same problems arise in structures such as action graphs [14] and bigraphs [15].

In [17] we therefore proposed a framework in which term structure is not explicitly quotiented, but the commutation of diagrams (i.e. equality of terms) is taken up to ≡. Precisely, to give a commuting diagram rp ≡ sq one exhibits a proof α of structural congruence, which we represent as a 2-cell (constructed from the rules generating ≡ and closed under all contexts).

\xymatrix{k \ar[r]^{p} \ar[d]_{q} & l \ar[d]^{r} \\ m \ar[r]^{_{ααα}}_{s} & n}

Since such proofs are naturally isomorphisms, we were led to consider G-categories, i.e., 2-categories where all 2-cells are iso, and initiated the study of G-relative pushouts (GRPOs), as a suitable generalisation of RPOs from categories to G-categories.

The purpose of this paper is to continue the development of the theory of GRPOs. We aim to show that, while replacing RPOs at little further complication (cf. §2 and §3), GRPOs significantly advance the field by providing a convenient solution to simple, yet important problems (cf. §4 and §5). The theory of GRPOs promises indeed to be a natural foundation for a meta-theory of ‘deriving bisimulation congruences.’

This paper presents two main technical results in support of our claims. Firstly, we prove that the case of the already mentioned category Bun of bunch contexts, problematic for RPOs, can be treated in a natural way using GRPOs. Secondly, we show that the notions of precategory and functorial reactive system can be dispensed with in favour of a simpler GRPO-based approach.

The notion of precategory is proposed in [11, 12] to handle the examples of Leifer in [11], Milner in [15] and, most recently, of Jensen and Milner in [7]. It consists of a category appropriately decorated by so-called “support sets” which identifies syntactic elements so as to keep track of them under arrow composition. Alas, such supported structures are no longer categories – arrow composition is partial – which makes the theory laborious, and bring us away from the well-known world of categories and their theory. The intensional information recorded in precategories, however, allows one to generate a category “above” where RPOs exist, as opposed to the category of interest “below”, say ℂ, where they do not. The category “above” is related to ℂ via a well-behaved functor, used to map RPOs diagrams from the category “above” to ℂ, where constructing them would be impossible. These structures take the name of functorial reactive systems, and give rise to a theory to generate a labelled bisimulation congruences developed in [11].

The paper presents a technique for mapping precategories to G-categories so that the LTS generated using GRPOs is the same as the LTS generated using the above mentioned approach. The translation derives from the precategory’s support information a notion of homomorphism, specific to the particular structure in hand, which constitutes the 2-cells of the derived G-category. We claim that this yields an approach mathematically more elegant and considerably simpler than precategories; besides generalising RPOs directly, GRPOs seem to also remove the need for further notions.

Structure of the paper. In §2 we review definitions and results presented in [17]; §3 shows that, analogously to the 1-dimensional case, trace and failures equivalence are congruences provided that enough GRPOs exist. In §4, we show that the category of bunch contexts is naturally a 2category where GRPOs exist; §5 shows how precategories are subsumed by our notion of GRPOs. The exposition ends with a few concluding remarks; §1 recalls basic notions of 2-categories, and can be safely skipped by those readers acquainted with the standard notations.

This paper is a version of [18] extended with proofs.

1 Preliminaries

Throughout the paper we assume a moderate knowledge of category theory and related terminology. In this section we fix notations and recall the basic elements and 2-categories. For a thorough introduction the reader is referred to [9]

We use Ord to denote the category of finite ordinals. We assume that Ord has chosen coproducts, namely the reader’s favourite definition of ordinal addition ⊕. For any finite set x, let ord(x) be the finite ordinal of the same cardinality and t_{x}: x → ord(x) be a chosen isomorphism. There is an equivalence of categories F : Set_{f} → Ord . On objects it sends x to ord(x), on morphisms f: x → y to t_{y}ft_{x}^{−1} : ord(x) → ord(y).

A 2-category ℂ is a category whose homsets are categories and, correspondingly, whose composition maps are functors. Explicitly, a 2category 𝔹 consists of the following.

• A class of objects X,Y,Z,....

• For any X,Y ∈ ℂ, a category ℂ(X,Y). The objects ℂ(X,Y) are called 1-cells, or simply arrows, and denoted by f: Y → X. Its morphisms are called 2-cells, are written α: f ⇒ g: X → Y and drawn as

[figure: X; f; g; α; Y.]

Composition in ℂ(X,Y) is denoted by • and referred to as ‘vertical’ composition. Identity 2-cells are denoted by 1_{f} : f ⇒ f.

• For each X,Y,Z there is a functor .: ℂ(X,Y)×ℂ(Y,Z) → ℂ(X,Z), the so-called ‘horizontal’ composition, which we often denote by mere juxtaposition. Horizontal composition is associative and admits 1_{id_{X}} as identities.

As a notation, we write αf and gα for, respectively, α1_{f} and 1_{g}α. We follow the convention that horizontal composition binds tighter than vertical composition.

In 2-categories, the order of composition of 2-cells is not important. This is a consequence of the horizontal composition being functorial and can be axiomatised with the so called middle-four interchange law: for f,f′,f′′: A → B and g,g′,g′′: B → C and α: f ⇒ f′, α′: f′⇒ f′′, β: g ⇒ g′ and β′: g′⇒ g′′we have β′α′•βα = (β′•β)(α′•α). As a consequence, given a diagram of 2-cells, there is at most one way to compose them and obtain a composite 2-cell. This primitive operation is sometimes referred to as pasting.

Two objects C, D of a 2-category ℂ are equivalent when there are arrows f : C → D, g: D → C and 2-cells α: id_{C}⇒ gf, β: fg ⇒ id_{D}. We refer to f and g as equivalences.

2 Reactive Systems and GRPOs

Lawvere theories [10] provide a canonical way to recast term algebras as categories. For Σ a signature, the (free) Lawvere theory on Σ, say C_{Σ}, has the natural numbers for objects and a morphism t: m → n, for t a n-tuple of m-holed terms. Composition is substitution of terms into holes.

Generalising from term rewriting systems on C_{Σ}, Leifer and Milner formulated a definition of reactive system [13], and defined a technique to extract labelled bisimulation congruences from them.

In order to accommodate calculi with non trivial structural congruences, as explained in the Introduction, we refine their approach as follows.

Definition 2.1. A G-category is a 2-category where all 2-cells are isomorphisms.

A G-category is a thus a category enriched over G, the category of groupoids.

Definition 2.2. A G-reactive system C consists of

1. a G-category ℂ,

2. a subcategory 𝔻 of reactive contexts; it is required to be closed under 2-cells to be and composition-reflecting,

3. a distinguished object I ∈ ℂ,

4. a set of pairs R ⊆ ⋃ _{C∈ℂ}ℂ(I,C)×ℂ(I,C) called the reaction rules.

The reactive contexts are those contexts inside which evaluation may occur. By composition-reflecting we mean that dd′∈ 𝔻 implies d and d′∈ 𝔻, while the closure property means that given d ∈ 𝔻 and ρ: d ⇒ d′ in ℂ implies d′∈ 𝔻. The reaction relation ▷ is defined by taking

a ▷ dr if there exists ⟨l,r⟩, d ∈ 𝔻 and α: dl ⇒ a.

As illustrated by the diagram below, this represents the fact that, up to structural congruence, a is the left-hand side l of a reduction rule in a reaction context d.

\xymatrix{I \ar[d]_{l} \ar[dr]^{a} \\ C \ar[r]^{α}_{d} & C′}

The notion of GRPO formalises the idea of a context being the “smallest” that enables a reaction in a G-reactive system, and is a conservative 2-categorical extension of Leifer and Milner RPOs [13] (cf. [17] for a precise comparison).

For readers acquainted with 2-dimensional category theory, GRPOs are defined in Definition 2.3. This is followed by an elementary presentation in Proposition 2.4 taken from [17].

Definition 2.3 (GRPOs). Let ρ: ca ⇒ db: W → Z be a 2-cell (see diagram below) in a G-category ℂ. A G-relative pushout (GRPO) for ρ is a bipushout [8] of the pair or arrows (a,1) : ca → c and (b,ρ) : ca → d in the pseudo-slice category ℂ/Z.

\xymatrix{ & Z \\ X \ar@{-->}[ur]_{ρ}^{c} &  & Y \ar@{-->}[ul]_{d} \\  & W \ar@{-->}[ur]_{b} \ar@{-->}[ul]^{a}}  (1)

Proposition 2.4. Let ℂ be a G-category. A candidate GRPO for ρ: ca ⇒ db as in diagram (1) is a tuple ⟨R,e,f,g,β,γ,δ⟩such that δb •gβ •γa = ρ – cf. diagram (i).

[figure: Z; X; γ; e; β; c; R; δ; g; Y; f; d; W; b; a; (i); R′; X; φ; e; e′; R; ψ; h; (ii); Y; f; f′; Z; R′; τ; g′; R; g; h; (iii)]

A GRPO for ρ is a candidate which satisfies a universal property. Namely, for any other candidate ⟨R′,e′,f′,g′,β′,γ′,δ′⟩ there exists a quadruple ⟨h,φ,ψ,τ⟩where h: R → R′, φ: e′⇒ he and ψ: hf ⇒ f′– cf. diagram (ii) – and τ: g′h ⇒ g – diagram (iii) – which makes the two candidates compatible in the obvious way, i.e.

τe •g′φ •γ′= γ  δ′•g′ψ •τ^{−1} f = δ  ψb •hβ •φa = β′.

Such a quadruple, which we shall refer to as mediating morphism, must be essentially unique. Namely, for any other mediating morphism ⟨h′,φ′,ψ′,τ′⟩ there must exist a unique two cell ξ: h → h′which makes the two mediating morphisms compatible, i.e.:

ξe •φ = φ′ ψ •ξ^{−1} f = ψ′ τ′•g′ξ = τ

Observe that whereas RPOs are defined up to isomorphism, GRPOs are defined up to equivalence (since they are bicolimits).

The definition below plays an important role in the following development.

Definition 2.5 (GIPO). Diagram (1) of Definition 2.3 is said to be a Gidem-pushout (GIPO) if ⟨Z,c,d,id_{Z},ρ,1_{c},1_{d}⟩is its GRPO.

The next two lemmas explain the relationships between GRPOs and GIPOs.

Lemma 2.6 (GIPOs from GRPOs). If ⟨Z,c,d,u,α,η,μ⟩is a GRPO for

(i) below, as illustrated in (ii), then (iii) is a GIPO.

\xymatrix{ & Z′ &  &  & Z′ &  &  & Z \\ X \ar@{-->}[ur]_{α′}^{c′} &  & Y \ar@{-->}[ul]_{d′} & X \ar@{-->}[ur]^{c′} \ar[r]|{c} & Z \ar[u]^{η}_{μ}|{u} & Y \ar[l]|{d} \ar@{-->}[ul]_{d′} & X \ar@{-->}[ur]_{α}^{c} &  & Y \ar@{-->}[ul]_{d} \\  & W \ar@{-->}[ul]^{a} \ar@{-->}[ur]_{b} &  &  & W \ar@{-->}[ul]_{α}^{a} \ar@{-->}[ur]_{b} &  &  & W \ar@{-->}[ul]^{a} \ar@{-->}[ur]_{b} \\  & (i) &  &  & (ii) &  &  & (iii)}

Lemma 2.7 (GRPOs from GIPOs). If square (iii) above is a GIPO, (i) has a GRPO, and ⟨Z,c,d,u,α,η,μ⟩is a candidate for it as shown in (ii), then ⟨Z,c,d,u,α,η,μ⟩is a GRPO for (i).

The following lemmas from [17] state the basic properties of GRPOs.

Lemma 2.8. Suppose that diagram (ii) below has a GRPO.

[figure: U; a; b; V; d; e; W; g; X; α; c; Y; β; f; Z; (i); U; a; b; V; ge; X; fc; βa•fα; Z; (ii)]

1. If both squares in (i) are GIPOs then the rectangle of (i) is a GIPO;

2. If the left square and the rectangle of (i) are GIPOs then so is the right square.

Lemma 2.9. Suppose that diagram (i) below is a GIPO.

\xymatrix{ & Z &  &  & Z &  &  & Z \\ X \ar@{-->}[ur]_{α}^{c} &  & Y \ar@{-->}[ul]_{d} & X \ar@{-->}[ur]_{α}^{c} &  & Y \ar@{-->}[ul]_{d} & X \ar@{-->}[ur]_{α}^{c} &  & Y \ar@{-->}[ul]^{d} \ar[ul]_{d′} \ar@{-->}[ul]_{ϵ} \\  & W \ar@{-->}[ul]^{a} \ar@{-->}[ur]_{b} &  &  & W \ar@{-->}[ul]_{a} \ar[ul]^{a′} \ar@{-->}[ur]^{ϵ}_{b} &  &  & W \ar@{-->}[ul]^{a} \ar@{-->}[ur]_{b} \\  & (i) &  &  & (ii) &  &  & (iii)}

Then the regions obtained by pasting the 2-cells in (ii) and (iii) are GIPOs.

The previous lemma in particular implies that the following definition of labelled transition system derived from a G-reactive system is well defined.

Definition 2.10 (LTS). For C a G-reactive system whose underlying category ℂ is a G-category, define GTS(C) as follows:

• the states GTS(C) are iso-classes of arrows [a]: I → X in C;

• there is a transition [a] ^{[f]}▶ [a′] if there exists a 2-cell ρ, a rule ⟨l,r⟩∈ R, and d ∈ 𝔻 with a′≅ dr and such that the diagram below is a GIPO.

[figure: Z; X; f; ρ; Y; d; I; a; l]  (2)

Henceforward we shall abuse notation and leave out the square brackets when writing transitions; ie. we shall write simply a ^{f} ▶ a′instead of [a] ^{[f]}▶ [a′].

Categories can be seen as a discrete G-categories (the only 2-cells are identities). Using this observation, each G-concepts introduced above reduces to the corresponding 1-categorical concept. For instance, a GRPO in a category is simply a RPO.

3 Congruence Results for GRPOs

The fundamental property that endows the LTS derived from a reduction system with a bisimulation which is a congruence is the following notion.

Definition 3.1 (Redex GRPOs). A G-reactive system C is said to have redex GRPOs if every square (2) in its underlying G-category ℂ with l the left-hand side of a reaction rule ⟨l,r⟩∈ R, and d ∈ 𝔻 has a GRPO.

In particular, the main theorem of [17] is as follows.

Theorem 3.2 (cf. [17]). Let C be a reactive system whose underlying G-category ℂ has redex GRPOs. The largest bisimulation ∼ on GTS(C) is a congruence.

The next three subsections complement this result by proving the expected corresponding theorems for trace and failure semantics, and by lifting them to the case of weak equivalences. Theorems and proofs in this section follow closely [11], as they are meant to show that GRPOs are as viable a tool as RPOs are.

3.1 Traces Preorder

Trace semantics [16] is a simple notion of equivalence which equates processes if they can engage in the same sequences of actions. Even though it lacks the fine discriminating power of branching time equivalences, viz. bisimulations, it is nevertheless interesting because many safety properties can be expressed as conditions on sets of traces.

We say that a sequence f_{1}··· f_{n} of labels of GTS(C) is a trace of a if

a ^{f_{1}} ▶ ···^{f_{n}} ▶ a_{n+1}

for some a_{1},...,a_{n}. The trace preorder ≲_{tr} is then defined as a ≲_{tr}b if all traces of a are also traces of b.

Theorem 3.3 (Trace Congruence). ≲_{tr}is a congruence.

Proof. Assume a ≲_{tr}b. We prove that ca ≲_{tr}cb for all contexts c ∈ ℂ. Suppose that

ca = ā_{1} ^{f_{1}} ▶ ā_{2}··· ā_{n} ^{f_{n}} ▶ ā_{n+1} .

We first prove that there exist a sequence, for i = 1,...,n,

\xymatrix{· \ar[r]_{α_{i}}^{a_{i}} \ar[d]_{l_{i}} & · \ar[d]^{β_{i}}|{g_{i}} \ar[r]^{c_{i}} & · \ar[d]^{f_{i}} \\ · \ar[r]_{d_{i}} & · \ar[r]_{d′_{i}} & ·}

where a_{1} = a, c_{1} = c, c_{i+1} = d′_{i}, ā_{i} = c_{i}a_{i}, and each square is a GIPO.^{1} The ith induction step proceeds as follows. Since ā_{i} ^{f_{i}} ▶ ā_{i+1} , there exists γ_{i}: f_{i}c_{i}a_{i} ⇒ d̄_{i}l_{i}, for some ⟨l_{i},r_{i}⟩∈ R and d̄_{i} ∈ 𝔻, with ā_{i+1} = d̄_{i}r_{i}. Since C has redex GIPOs (cf. Definition 3.1), this can be split in two GIPOs: α_{i}: g_{i}a_{i} ⇒ d_{i}l_{i} and β_{i}: f_{i}c_{i} ⇒ d′_{i}g_{i} (cf. diagram above). Take a_{i+1} = d_{i}r_{i}, and the induction hypothesis is maintained. In particular, we obtained a trace

a = a_{1} ^{g_{1}} ▶ a_{2}··· a_{n} ^{g_{n}} ▶ a_{n+1}

that, in force of the hypothesis a ≲_{tr} b must be matched by a corresponding trace of b. This means that, for i = 1,..,n, there exist GIPOs α′_{i}: g_{i}b_{i} ⇒ e_{i}l′_{i}, for some ⟨l′_{i},r′_{i}⟩∈ R and e_{i} ∈ 𝔻, once we take b_{i+1} to be e_{i}r′_{i}. We can then paste each of such GIPOs together with β_{i}: f_{i}c_{i} ⇒ d′_{i}g_{i} obtained above and, using Lemma 2.8, conclude that there exist GIPOs f_{i}c_{i}b_{i} ⇒ d′_{i}e_{i}l′_{i}, as in the diagram below.

\xymatrix{· \ar[r]_{α′_{i}}^{b_{i}} \ar[d]_{l′_{i}} & · \ar[d]^{β_{i}}|{g_{i}} \ar[r]^{c_{i}} & · \ar[d]^{f_{i}} \\ · \ar[r]_{e_{1}} & · \ar[r]_{d′_{i}} & ·} which means c_{i}b_{i} ^{f_{i}} ▶ d′_{i}e_{i}r′_{i}.

1Since the fact is not likely to cause confusion, we make no notational distinction between the arrows of C (e.g. in GRPOs diagrams) and the states and labels of GTS(C), where the latter are iso-classes of the former.

As cb = c_{1}b_{1}, in order to construct a trace cb = b̄_{1} ^{f_{1}} ▶ ···^{f_{n}} ▶ b̄_{n+1} and complete the proof, we only need to verify that for i = 1,...,n, we have that d′_{i}e_{i}r′_{i}= c_{i+1} b_{i+1} . This follows at once, as c_{i+1} = d′_{i}and b_{i+1} = e_{i}r′_{i}.

3.2 Failures Preorder

Failure semantics [6] enhances trace semantics with limited branch-inspecting power. More precisely, failure sets allow the testing of when processes renounce the capability of engaging in certain actions.

Formally, for a a state of GTS(C), a failure of a is a pair (f_{1}··· f_{n},X), where f_{1}··· f_{n} and X are respectively a nonempty sequence and a set of labels, such that:

• f_{1}··· f_{n} is a trace of a, a ^{f_{1}} ▶ ···^{f_{n}} ▶ a_{n+1} ;

• a_{n+1} , the final state of the trace, is stable, i.e. a_{n+1} ▷̸;

• a_{n+1} refuses X, i.e. a_{n+1} ^{x̸} ▶ for all x ∈ X.

The failure preorder ≲_{f} is defined as a ≲_{f} b if all failures of a are also failures of b.

Theorem 3.4 (Failures Congruence). ≲_{f} is a congruence.

Proof. Assume a ≲_{f} b to prove that ca ≲_{f} cb for all contexts c ∈ ℂ. The proof extends the previous one of Theorem 3.3.

Let (f_{1}··· f_{n},X), n > 0, be a failure of ca. We proceed exactly as above to determine a matching trace cb = b̄_{1} ^{f_{1}} ▶ ···^{f_{n}} ▶ b̄_{n+1}. In addition, we contextually need to prove that b̄_{n+1} is stable and refuses X, exploiting the corresponding hypothesis on ā_{n+1} . First, we claim that a_{n+1} is stable. In fact, were it not, it would follow from c_{n+1} (= d′_{n}) ∈ 𝔻 that also ā_{n+1} = c_{n+1} a_{n+1} ▷, which is impossible, since ā_{n+1} is stable. Secondly, a_{n+1} refuses both

Y ={g | there exists a GIPO δ_{g}: xc_{n+1} ⇒ dg, for x ∈ X} and
Z = {g | there exists a 2-cell ϵ_{g}: dg ⇒ c_{n+1} , for d ∈ 𝔻},

which can be seen as follows. If a_{n+1} ^{g} ▶ for g ∈ Y, then there exists a GIPO α: ga_{n+1} ⇒ d′l, for some rule ⟨l,r⟩, which could be pasted together with δ_{g} to yield a GIPO xc_{n+1} a_{n+1} ⇒ dd′l, which is impossible since it means that ā_{n+1} ^{x} ▶, for x ∈ X. Similarly, if a_{n+1} ^{g} ▶ for g ∈ Z, pasting the corresponding GIPO with ϵ_{g}, we see that ā_{n+1} ▷, contradicting the hypothesis that ā_{n+1} is stable. If follows then from the hypothesis a ≲_{f} b that b_{n+1} is stable and refuses Y ∪ Z. It is then easy to complete the proof by transferring stability and X-refusal to b̄_{n+1}. First, suppose that b̄_{n+1} ▷. This means that there exists a 2-cell dl ⇒ b̄_{n+1}. Since C has redex-GRPOs, we can factor c_{n+1} out and obtain from this a GRPOs α: gb_{n+1} ⇒ d′l together with a 2-cell d′′g ⇒ c_{n+1} . But this would mean that b_{n+1} ^{g} ▶, for g ∈ Z, which is a contradiction. Suppose finally that b̄_{n+1} ^{x} ▶, for x ∈ X. Again, by definition of the transition relation, and exploiting the existence of redex-GRPOs, we find GRPOs xc_{n+1} ⇒ d′′g and gb_{n+1} ⇒ d′l, which mean that b_{n+1} ^{g} ▶, for g ∈ Y.

3.3 Weak Equivalences

Theorems 3.2, 3.3, and 3.4 can be extended to weak equivalences, as outlined below.

For f a label of GTS(C) define a weak transition a ▶^{f} b to be a mixed sequence of transitions and reductions a ▷^{∗} ^{f} ▶ ▷^{∗} b. Observe that this definition essentially identifies silent transitions in the LTS with reductions. As a consequence, care has to be taken to avoid interference with transitions ^{equi}▶ synthesised from GRPOs and labelled by an equivalence. These transitions have essentially the same meaning as silent transitions (i.e. no context involved in the reduction), and must therefore be omitted in weak observations. This lead to consider the following definitions.

Definition 3.5 (Weak Traces and Failures). A sequence f_{1}··· f_{n} of nonequivalence labels of GTS(C) is a weak trace of a if

a ▶^{f_{1}} a_{1}··· a_{n−1} ▶^{f_{n}} a_{n}

for some a_{1},...,a_{n}. The weak trace preorder is then defined accordingly.

A weak failure of a is a pair (f_{1}··· f_{n},X), where f_{1}··· f_{n} and X are respectively a sequence and a set of non-equivalence labels, such that f_{1}··· f_{n} is a weak trace of a reaching a final state which is stable and refuses X. The weak trace preorder is defined accordingly.

Definition 3.6 (Weak Bisimulation). A symmetric relation S on GTS(C) is a weak bisimulation if for all a S b

a ^{f} ▶ a′ f not an equivalence, implies b ▶^{f} b′with a′S b′;
a ▷ a′ implies b ▷^{∗} b′with a′S b′.

Using the definitions above Theorems 3.2, 3.3, and 3.4 can be lifted, respectively, to weak traces, failures and bisimulation.

It is worth remarking that the congruence results, however, only hold for contexts c ∈ 𝔻, as it is well known that non reactive contexts (i.e. those c where ca ▷ cb does not follow from a ▷ b, as e.g. the CSS context c = c_{0}+−) do not preserve weak equivalences. Alternative definitions of weak bisimulations are investigated in [11], and they are applicable mutatis mutandis to GRPOs.

4 Bunches and Wires

The category of “bunches and wires” was introduced in [13] as a skeletal algebra of shared wirings, abstracting over the notion of names in, e.g., the π calculus. Although elementary, its structure is complex enough to lack RPOs.

A bunch context of type m_{0} → m_{1} consists of an ordered set of m_{1} trees of depth 1 containing exactly m_{0} holes. Leaves are labelled from an alphabet K.

Definition 4.1. The category of bunch contexts Bun_{0} has

• objects the finite ordinals, denoted m_{0},m_{1},...

• arrows are bunch contexts c = (X,char,root): m_{0} → m_{1}, where X is a finite carrier, root: m_{0}+X → m_{1} is a surjective function linking leaves (X) and holes (m_{0}) to their roots (m_{1}), and char: X → K is a leaf labelling function.

Composing c_{0}: m_{0} → m_{1} and c_{1}: m_{1} → m_{2} means filling the m_{1} holes of c_{1} with the m_{1} trees of c_{0}. Formally, c_{1}c_{0} is (X,root,char) where

X = X_{0}+ X_{1},  root= root_{1}(root_{0}+id_{X_{1}}),  char= [char_{0},char_{1}],

where + and [ , ] are, resp., coproduct and copairing. Identities are (∅,!,id) : m_{0} → m_{0}.

A homomorphism of bunch contexts ρ: c ⇒ c′: m_{0} → m_{1} is a function ρ: X → X′ which respects root and char, i.e. root′ρ = root and char′ρ = char. An isomorphism is a bijective homomorphism. Isomorphic bunch contexts are equated, making composition associative and Bun_{0} a category.

A bunch context c: m_{0} → m_{1} can be depicted as a string of m_{1} nonempty multisets on K + m_{0}, with the proviso that elements m_{0} must appear exactly once in the string. In the examples, we represent elements of m_{0} as numbered holes −_{i}.

As we mentioned before, RPOs do not exist in Bun_{0}. Indeed, consider (i) below together with the two candidates (ii) and (iii). It is easy to show that these have no common “lower bound” candidate.

[figure: 1; 1; {K,−_{1}}; 1; {K,−_{1}}; 0; {K}; {K}; (i); 1; 1; {K,−_{1}}; {−_{1}}; 1; {K,−_{1}}; 1; {−_{1}}; {K,−_{1}}; 0; {K}; {K}; (ii); 1; 1; {K,−_{1}}; {−_{1}}{K}; 2; {−_{1},−_{2}}; 1; {K}{−_{1}}; {K,−_{1}}; 0; {K}; {K}; (iii)]

The point here is that by taking the arrows of Bun_{0} up to isomorphism we lose information about how bunch contexts equal each other. Diagram (i), for instance, can be commutative in two different ways: the K in the bottom left part may corresponds either to the one in the bottom right or to the one in the top right, according to whether we read {K,−_{1}} or {−_{1},K} for the top rightmost arrow. In order to track this information we endow Bun_{0} with its natural 2-categorical structure.

Definition 4.2. The 2-category of bunch contexts Bun has:

• objects the finite ordinals (cf. §1), denoted m_{0},m_{1},...

• arrows c = (x,char,root): m_{0} → m_{1} consist of a finite ordinal x, a surjective function root: m_{0} ⊕ x → m_{1} and a labelling function char: x → K.

• 2-cells ρ are isomorphisms between bunches’ carriers.

Composition of arrows and 2-cells is defined in the obvious way. Notice that since ⊕ is associative, composition in Bun is associative. Therefore Bun is a G-category.

Replacing the carrier set X with a finite ordinal x allows us to avoid the unnecessary burden of working in a bicategory, which would arise because sum on sets is only associative up to isomorphism. Observe that this simplification is harmless since the set theoretical identity of the elements of the carrier is irrelevant. We remark, however, that GRPOs are naturally a bicategorical notion and would pose no particular challenge in bicategories.

Theorem 4.3. Bun has GRPOs.

Proof. In the following, we use only the fact that Bun is an extensive [2] category with pushouts.

Suppose that we have an isomorphic 2-cell ρ: ca ⇒ dl as illustrated below:

\xymatrix{ & m_{3} \\ m_{1} \ar@{-->}[ur]_{ρ}^{c} &  & m_{2} \ar@{-->}[ul]_{d} \\  & m_{0}. \ar@{-->}[ur]_{l} \ar@{-->}[ul]^{a}}

Using ρ and the injections into the chosen coproduct in Ord (which are unlabelled below), we take four pullbacks obtaining the following diagram. Due to the extensivity of Ord , all the outside arrows are coproduct injections.

\xymatrix{x_{c_{1}} \ar[d]_{c_{1}} \ar[rr]^{l_{1}} &  & x_{l} \ar[d] &  & x_{a_{1}} \ar[ll]_{l_{2}} \ar[d]^{a_{1}} \\ x_{c} \ar[r] & x_{a}⊕ x_{c} \ar[r]^{ρ} & x_{l} ⊕ x_{d} & x_{c}⊕ x_{a} \ar[l]_{ρ} & x_{a} \ar[l] \\ x_{c_{2}} \ar[u]^{c_{2}} \ar[rr]_{d_{1}} &  & x_{d} \ar[u] &  & x_{a_{2}} \ar[ll]^{d_{2}} \ar[u]_{a_{2}}}

Using the morphisms from the diagram above as building blocks, we can construct bijections γ: x_{c} → x_{c_{1}} ⊕ x_{c_{2}}, δ: x_{a_{2}} ⊕ x_{c_{2}} → x_{d} and β: x_{a}⊕ x_{c_{1}} → x_{l} ⊕ x_{a_{2}} such that

x_{l} ⊕ δ.β ⊕ x_{c_{2}}.x_{a}⊕ γ = ρ.  (3)

Let root_{c_{1}} and root_{a_{2}} be the morphisms making (i) below

[figure: m_{0}⊕ x_{a}⊕ x_{c_{1}}; root_{a}⊕x_{c_{1}}; m_{0}⊕β; m_{0}⊕ x_{l} ⊕ x_{a_{2}}; root_{l} ⊕x_{a_{2}}; m_{2}⊕ x_{a_{2}}; root_{a_{2}}; m_{1}⊕ x_{c_{1}}; root_{c_{1}}; m_{4}; (i); m_{3}; m_{1}; γ; c_{1}; β; c; m_{4}; δ; c_{2}; m_{2}; a_{2}; d; m_{0}; l; a; (ii)]

into a pushout diagram. We can define char_{c_{1}}, char_{a_{2}} and char_{c_{2}} in the obvious way.

Now consider the diagram below:

\xymatrix{m_{0}⊕ x_{a}⊕ x_{c_{1}} \ar[dd]_{root_{a}⊕x_{c1}} \ar[dr]_{m_{0}⊕x_{a}⊕c_{1}} \ar[r]^{m_{0}⊕β} & m_{0}⊕ x_{l} ⊕ x_{a_{2}} \ar@{-->}[dr]_{(†)}^{m_{0}⊕x_{l}⊕d_{2}} \ar[rr]^{root_{l} ⊕x_{a2}} &  & m_{2}⊕ x_{a_{2}} \ar[d]^{m_{2}⊕d_{2}} \\  & m_{0}⊕ x_{a}⊕ x_{c} \ar[d]^{(‡)}_{root_{a}⊕x_{c}} \ar[r]_{m_{0}⊕ρ} & m_{0}⊕ x_{l} ⊕ x_{d} \ar[r]_{root_{l} ⊕x_{d}} & m_{2}⊕ x_{d} \ar[d]^{root_{d}} \\ m_{1}⊕ x_{c_{1}} \ar[r]_{m_{1}⊕c_{1}} & m_{1}⊕ x_{c} \ar[rr]_{root_{c}} &  & m_{3}.}

Region (†) can be verified to be commutative using (3) while region (‡) commutes since ρ is a homomorphism. Using the pushout property, we get a unique function h: m_{4} → m_{3}. Thus we define root_{c_{2}} = [h,root_{c}i]: m_{4}⊕x_{c_{2}} → m_{3}. It is easy to verify that this function is surjective, indeed, using root_{c_{1}}: m_{1}⊕x_{c_{1}} → m_{4} we get a function [root_{c_{1}},x_{c_{2}}]: m_{1}⊕ x_{c} → m_{4}⊕ x_{c_{2}} such that

\xymatrix{m_{1}⊕ x_{c} \ar[d]_{[root_{c1},x_{c2}]} \ar[dr]^{root_{c}} \\ m_{4}⊕ x_{c_{2}} \ar[r]_{root_{c2}} & m_{3}}

is commutative. Thus surjectivity follows from the surjectivity of root_{c}.

We shall verify that β: c_{1}a → a_{2}l, γ: c → c_{2}c_{1} and δ: c_{2}a_{2} → d are homomorphisms. Because of the definition of char_{c_{1}}, char_{c_{2}} and char_{a_{2}} it is clear that each of the functions preserves the character. Notice that diagram (i) implies that β preserves the roots. The commutativity of the diagrams below can be checked by examining the injections of m_{1}, x_{c_{1}}, x_{c_{2}} and m_{2}, x_{a_{2}}, x_{c_{2}} respectively.

\xymatrix{m_{1}⊕ x_{c} \ar[d]_{root_{c}} \ar[r]^{m_{1}⊕γ} & m_{1}⊕ x_{c_{1}} ⊕ x_{c_{2}} \ar[d]^{root_{c_{1}} ⊕x_{c_{2}}} & m_{2}⊕ x_{a_{2}} ⊕ x_{c_{2}} \ar[r]^{m_{2}⊕δ} \ar[d]_{root_{a_{2}} ⊕x_{c_{2}}} & m_{1}⊕ x_{d} \ar[d]^{root_{d}} \\ m_{3} & m_{4}⊕ x_{c_{2}} \ar[l]^{root_{c_{2}}} & m_{4}⊕ x_{c_{2}} \ar[r]_{root_{c_{2}}} & m_{3}}

Thus (ii) is a a candidate for the region.

Suppose that ⟨m_{5},r,s,t,β′,γ′,δ′⟩ is another candidate. A diagram chase shows that

\xymatrix{x_{t} \ar[d]_{i_{2}} \ar[r]^{i_{2}} & x_{s}⊕ x_{t} \ar[r]^{δ′} & x_{d} \ar[dd]^{i_{2}} \\ x_{r}⊕ x_{t} \ar[d]_{γ^{′−1}} \\ x_{c} \ar[r]_{i_{2}} & x_{a}⊕ x_{c} \ar[r]_{ρ} & x_{l} ⊕ x_{d}}

Thus there is an injective function k: x_{t} → x_{c_{2}} satisfying γ^{′−1}i_{2} = c_{2}k and δ′i_{2} = d_{1}k.

Take the pullback

\xymatrix{x_{u} \ar[r] \ar[dd]_{j} & x_{r} \ar[d] \\  & x_{r}⊕ x_{t} \ar[d]^{γ^{′−1}} \\ x_{c_{2}} \ar[r]_{c_{2}} & x_{c}.}

It is easy to verify that x_{u} −→^{j} x_{c_{2}} ⟵^{k} x_{t} is a coproduct diagram. Let

τ = [j,k]: x_{u}⊕ x_{t} → x_{c_{2}}.

By the definition of τ,

\xymatrix{x_{r} \ar[d] \ar[rrr]^{φ} &  &  & x_{c_{1}} ⊕ x_{u} \ar[d] \\ x_{r}⊕ x_{t} \ar[r]^{γ^{′−1}} & x_{c} \ar[r]^{γ} & x_{c_{1}} ⊕ x_{c_{2}} \ar[r]^{x_{c_{1}}⊕τ^{−1}} & x_{c_{1}} ⊕ x_{u}⊕ x_{t} \\ x_{a_{2}} ⊕ x_{u} \ar[d] \ar[rrr]^{ψ} &  &  & x_{s} \ar[d] \\ x_{a_{2}} ⊕ x_{u}⊕ x_{t} \ar[r]^{x_{a_{2}}⊕τ} & x_{a_{2}} ⊕ x_{c_{2}} \ar[r]^{δ} & x_{d} \ar[r]^{δ^{′−1}} & x_{s}⊕ x_{t}}

the composites at the bottom of the two rectangles above are the identity on the second injection (x_{t}). Therefore, one can find functions φ and ψ such that the regions are pullbacks. They are iso, being the pullbacks of isos. The commutativity of these pullback diagrams implies that x_{c_{1}} ⊕ τ.φ⊕x_{t}.γ′= γ (ℵ), δ′.ψ⊕x_{t}.x_{a_{2}}⊕τ^{−1} = δ. These two equations together with the equations which define ρ in terms of β, γ, δ and β′, γ′,δ′ give x_{l} ⊕ ψ.β ⊕ x_{u}.x_{a}⊕ φ = β′(✠).

The following diagram is commutative,

\xymatrix{m_{0}⊕ x_{a}⊕ x_{c_{1}} \ar@{-->}[dr] \ar[ddd]_{root_{a}⊕x_{c1}} \ar[r]^{m_{0}⊕β} & m_{0}⊕ x_{l} ⊕ x_{a_{2}} \ar[rrr]^{root_{l} ⊕x_{a2}} &  &  & m_{2}⊕ x_{a_{2}} \ar[d] \\  & m_{0}⊕ x_{a}⊕ x_{c_{1}} ⊕ x_{u} \ar[r]^{m_{0}⊕β⊕x_{u}} \ar[dd]_{root_{a}⊕x_{c1}⊕x_{u}} \ar@{-->}[dr]_{m_{0}⊕x_{a}⊕φ^{−1}} & m_{0}⊕ x_{l} ⊕ x_{a_{2}} ⊕ x_{u} \ar@{-->}[dr]_{(✠)}^{m_{0}⊕x_{l}⊕ψ} \ar[rr]^{root_{l} ⊕x_{a2}⊕x_{u}} &  & m_{2}⊕ x_{a_{2}} ⊕ x_{u} \ar[d]^{m_{2}⊕ψ} \\  &  & m_{0}⊕ x_{a}⊕ x_{r} \ar[r]_{m_{0}⊕β′} \ar[d]_{root_{a}⊕x_{r}} & m_{0}⊕ x_{l} ⊕ x_{s} \ar[r]_{(‡)}_{root_{l} ⊕x_{s}} & m_{2}⊕ x_{s} \ar[d]^{root_{s}} \\ m_{1}⊕ x_{c_{1}} \ar[r] & m_{1}⊕ x_{c_{1}} ⊕ x_{u} \ar[r]_{m_{1}⊕φ^{−1}} & m_{1}⊕ x_{r} \ar[rr]_{root_{r}} &  & m_{5}}

region (‡) since β′ is a homomorphism. We obtain h′: m_{4} → m_{5}. Let root_{u} = [h′,f]: m_{4}⊕ u → m_{5} where f is the composite

x_{u} → m_{1}⊕ x_{c_{1}} ⊕ x_{u} −→^{m_{1}⊕φ^{−1}} m_{1}⊕ x_{r} −→^{root_{r}} m_{5}

or equivalently (using the previous diagram)

x_{u} → m_{2}⊕ x_{a_{2}} ⊕ x_{u} −→^{m_{2}⊕ψ} x_{2}⊕ x_{s} −→^{root_{s}} m_{5}.

The diagrams below are commutative, and either implies that root_{u} is surjective.

\xymatrix{m_{1}⊕ x_{c_{1}} ⊕ x_{u} \ar[d]_{m_{1}⊕φ^{−1}} \ar[r]^{root_{c_{1}} ⊕x_{u}} & m_{4}⊕ x_{u} \ar[d]^{root_{u}} & m_{2}⊕ x_{a_{2}} ⊕ x_{u} \ar[d]_{m_{2}⊕ψ} \ar[r]^{root_{a_{2}} ⊕x_{u}} & m_{4}⊕ x_{u} \ar[d]^{root_{u}} \\ m_{1}⊕ x_{r} \ar[r]_{root_{r}} & m_{5} & m_{2}⊕ x_{s} \ar[r]_{root_{s}} & m_{5}}

Define char_{u} in the obvious way. Then u: m_{4} → m_{5} is a bunch context. The above diagrams imply that φ: r → uc_{1} and ψ: ua_{2} → s are homomorphisms. To see that τ: tu → c_{2} is a homomorphism, notice that the region below is commutative

\xymatrix{m_{1}⊕ x_{c} \ar[d]_{root_{c}} \ar[r]^{m_{1}⊕γ′} & m_{1}⊕ x_{r}⊕ x_{t} \ar[d]_{root_{r}⊕x_{t}} \ar[r]^{m_{1}⊕φ⊕x_{t}} & m_{1}⊕ x_{c_{1}} ⊕ x_{u}⊕ x_{t} \ar@{->>}[d]_{root_{c_{1}} ⊕x_{u}⊕x_{t}} \ar[r]^{m_{1}⊕x_{c_{1}}⊕τ} & m_{1}⊕ x_{c_{1}} ⊕ x_{c_{2}} \ar[d]^{root_{c_{1}} ⊕x_{c_{2}}} \\ m_{3} & m_{5}⊕ x_{t} \ar[l]^{root_{t}} & m_{4}⊕ x_{u}⊕ x_{t} \ar[l]^{root_{u}⊕x_{t}} \ar[r]_{m_{4}⊕τ} & m_{4}⊕ x_{c_{2}}}

with the two left rectangles commutative since γ′ and φ are homomorphisms. Using (ℵ), the top row is equal to m_{1} ⊕ γ. Using the fact that γ is a homomorphism, and the surjectivity of the marked arrow in the above diagram, we conclude that root_{c_{2}}.m_{4}⊕ τ = root_{t}.root_{u}⊕x_{t}. Thus ⟨u,φ,ψ,τ⟩is a mediating morphism.

Now for any other mediating morphism ⟨u′,τ′,φ′,ψ′⟩ notice that φ′ and ψ′are uniquely determined by τ′. It can be checked that τ^{′−1}τ: x_{u}⊕ x_{t} ≅ x_{u′}⊕ x_{t} is the identity on the second projection; using a property of extensive categories [2] we get a unique homomorphism ξ: x_{u} → x_{u′} such that τ′.ξ ⊕ x_{t} = τ.

Example 4.4. Let γ: 2 → 2 be the function taking 1 ↦ 2 and 2 ↦ 1. We give below on the right the GRPOs for the squares on the left.

\xymatrix{ & 1 &  &  & 1 \\ 1 \ar[ur]_{γ}^{\{K,−_{1}\}} &  & 1 \ar[ul]_{\{K,−_{1}\}} & 1 \ar[ur]^{\{K,−_{1}\}} \ar[r]^{\{−_{1}\}\{K\}} & 2 \ar[u]|{\{−_{1},−_{2}\}} & 1 \ar[l]_{\{K\}\{−_{1}\}} \ar[ul]_{\{K,−_{1}\}} \\  & 0 \ar[ur]_{\{K\}} \ar[ul]^{\{K\}} &  &  & 0 \ar[ur]^{γ}_{\{K\}} \ar[ul]^{\{K\}}}

\xymatrix{ & 1 &  &  & 1 \\ 1 \ar[ur]^{\{K,−_{1}\}} &  & 1 \ar[ul]_{\{K,−_{1}\}} & 1 \ar[ur]^{\{K,−_{1}\}} \ar[r]^{\{−_{1}\}} & 1 \ar[u]|{\{K,−_{1}\}} & 1 \ar[l]_{\{−_{1}\}} \ar[ul]_{\{K,−_{1}\}} \\  & 0 \ar[ur]_{\{K\}} \ar[ul]^{\{K\}} &  &  & 0 \ar[ur]_{\{K\}} \ar[ul]^{\{K\}}}

5 2-categories vs precategories

Other categories which, besides Bun_{0}, lack RPOs include the closed shallow action contexts [11, 12] and bigraph contexts [15, 7]. The solution adopted by Leifer [12] and later by Milner [15] is to introduce a notion of a well-supported precategory, where the algebraic structures at hand are decorated by finite “support sets.” The result is no longer a category – since composition of arrows is defined only if their supports are disjoint – but from any such precategory one can generate two categories which jointly allow the derivation of a bisimulation congruence via a functorial reactive system. These categories are the so-called track category, where support information is built into the objects, and the support quotient category, where arrows are quotiented by the support structure. The track category has enough RPOs and is mapped to the support quotient category via a well-behaved functor, so as to transport RPOs adequately.

In this section we present a translation from precategories to G-categories. The main result shows that the LTS derived using precategories and functorial reactive systems is identical to the LTS derived using GRPOs. We begin with a brief recapitulation of the definitions from [12].

Definition 5.1. A precategory 𝔸 consists of the same data as a category. The composition operator ∘ is, however, a partial function which satisfies

1. for any arrow f : A → B, id_{B}∘f and f ∘id_{A}are defined and id_{B}∘f = f = f ∘ id_{A};

2. for any f : A → B, g: B → C, h: C → D, (h ∘ g) ∘ f is defined iff h ∘ (g ∘ f) is defined and then (h ∘ g) ∘ f = h ∘ (g ∘ f).

Definition 5.2. Let Set_{f} be the category of finite sets. A well supported precategory is a pair ⟨𝔸,| − | ⟩, where 𝔸 is a precategory and | − |: Arr𝔸 → Set_{f} is the so-called support function, satisfying:

1. g∘f is defined iff |g|∩|f| = ∅, and if g∘f is defined then |g∘f| = |g| ∪ |f|;

2. |id_{A}| = ∅.

For any f : A → B and any injective function ρ in Set_{f} the domain of which contains |f| there exists an arrow ρ · f : A → B called the support translation of f by ρ. The following axioms are to be satisfied.

1. ρ · id_{A}= id_{A};  4. ρ · (g ∘ f) = ρ · g ∘ ρ · f;
2. id_{|f|} ·f = f;  5. (ρ_{1}∘ ρ_{0}) · f = ρ_{1}· (ρ_{0}· f);
3. ρ_{0}|f| = ρ_{1}|f| implies ρ_{0}· f = ρ_{1}· f;  6. |ρ · f| = ρ|f|.

We illustrate these definitions giving a precategorical definition of bunches and wiring (viz. §4).

Example 5.3 (Bunches). The precategory of bunch contexts A-Bun has objects and arrows as in Bun_{0}. However, differently from Bun_{0}, they are not taken up to isomorphism here. The support of c = (X,char,root) is X. Composition c_{1}c_{0} = (X,char,root): m_{0} → m_{2} of c_{0}: m_{0} → m_{1} and c_{1}: m_{1} → m_{2} is defined if X_{0}∩ X_{1} = ∅ and, if so, we have X = X_{0}∪ X_{1}. Functions char and root are defined in the obvious way. The identity arrows are the same as in Bun_{0}. Given an injective function ρ: X → Y, the support translation ρ · c is (ρX,charρ^{−1} ,root(id_{m_{0}}+ρ^{−1} )). It is easy to verify that this satisfies the axioms of precategories.

The definitions below recall the construction of the track and the support quotient categories from a well-supported precategory.

Definition 5.4. The track of 𝔸 is a category ℂ̂ with

• objects: pairs ⟨A,M⟩where A ∈ 𝔸 and M ∈ Set_{f};

• arrows: ⟨A,M⟩ −→^{f} ⟨B,N⟩ where f: A → B is in 𝔸, M ⊆ N and

|f| = N\M.

Composition of arrows is as in 𝔸. Observe that the definition of |f| ensures that composition is total. We leave it to the reader to check that the data defines a category (cf. [12]).

Definition 5.5. The support quotient of 𝔸 is a category ℂ with

• objects: as in 𝔸;

• arrows: equivalence classes of arrows of 𝔸, where f and g are equated if there exist a bijective ρ such that ρ · f = g.

The support quotient is the category of interest, and it is the underlying category of the reactive system under scrutiny.

Example 5.6 (Bunches). The support quotient of A-Bun is Bun_{0}.

There is an obvious functor F : ℂ̂ → ℂ, the support-quotienting functor. Henceforward we suppose that the precategory 𝔸 has a distinguished object I. In the following we use the typewriter font for objects and arrows of ℂ̂. We make the notational convention that any A and f in ℂ̂ are such that F (A) = A and F (f) = f.

Definition 5.7 (The LTS). The LTS FLTS^{c}(ℂ) has

• States: arrows a: 0 → n in ℂ;

• Transitions: a ^{c} ▶ dr if and only if there exist a,l,c,d in ℂ̂ with ⟨F (l),r⟩∈ R, F (d) ∈ 𝔻, and such that

                    \xymatrix{ & Z \\ X \ar@{-->}[ur]^{c} &  & Y \ar@{-->}[ul]_{d} \\  & I \ar@{-->}[ul]^{a} \ar@{-->}[ur]_{l}}  is an IPO.

It is proved in [12] that the support-quotienting functor F satisfies the properties required for the theory of functorial reactive systems [11, 12]. Thus, for instance, if the category ℂ̂ has enough RPOs, then the bisimulation on FLTS^{c}(ℂ) is a congruence.

All the theory presented so far can be elegantly assimilated into the theory of GRPOs. In [12], Leifer predicted instead of precategories, one could consider a bicategorical notion of RPO in a bicategory of supports. This is indeed the case, with GRPOs being the bicategorical notion of RPO. However, working with ordinals for support sets we can avoid the extra complications bicategories as in the case of Bun. It is worth noticing, however, that a bicategory of supports as above and the G-category define below would be biequivalent [20]. In the following, we make use of a chosen isomorphism t_{x}: x → ord(x), as defined in §1.

Definition 5.8 (G-category of Supports). Given a well-supported precategory 𝔸, the G-category of supports 𝔹 has

• objects: as in 𝔸;

• arrows: f: A → B where f: A → B is an arrow of 𝔸 and |f| is an ordinal;

• 2-cells: ρ: f ⇒ g for ρ a “structure preserving” support bijection, i.e. ρ · f = g in 𝔸.

Composition is defined as follows. Given f : A → B and g: B → C,

g ∘_{𝔹}f = i_{2}· g ∘_{𝔸}i_{1}· f

where |f| −→^{i_{1}} |f| ⊕ |g| ⟵^{i_{2}} |g| is the chosen coproduct diagram in Ord . Given an arrow f in 𝔸, we use f̃= t_{f} · f in 𝔹.

The following theorem guarantees that the LTS generated is the same as the one generated with the more involved theory of functorial reactive systems.

Theorem 5.9. FLTS^{c}(𝔸) = GTS(𝔹).

Proof. It is enough to present translations between GIPOs in 𝔹 and IPOs in ℂ̂ which preserve the resulting label in the derived LTS. Suppose that (i) below

[figure: Z; X; c; ρ; Y; d; I; a; l; (i); ⟨Z,N⟩; _{⟨X,ρi_{1}|a|⟩}; ρi_{2}·c; _{⟨Y,i_{1}|l|⟩}; i_{2}·d; _{⟨I,∅⟩}; ρi_{1}·a; i_{1}·l; (ii)]

is a GIPO. Then we claim that (ii) above is an IPO (in the following let N = |l| ⊕ |d|). Note that (ii) is commutative since ρ is a structurepreserving support bijection and therefore ρ(i_{2}· c ∘ i_{1}· a) = i_{2}· d ∘ i_{1}· l.

Indeed, suppose that ⟨⟨R,M⟩,e,f,g⟩is a candidate for (ii). Then we show that ⟨R,ẽ,f̃,g̃,β,γ,δ⟩. is a candidate for (i), that is, we need to define γ, β and δ so that their pasting composite yields ρ and that each of them is a structure-preserving bijection.

Let β represent the following composite

|a| ⊕ |ẽ| −→^{ρi_{1}⊕t_{e}^{−1}} |ρi_{1}· a| ∪ |e||i_{1}· l| ∪ |f| −→^{i_{1}^{−1} ∪t_{f}} |l| ⊕ ||f̃|,

and similarly let γ and δ be respectively

|c| −→^{ρi_{2}} |ρi_{2}· c| = |g ∘ e| = |e| ∪ |g| −→^{i_{1}t_{e}∪i_{2}t_{g}}|ẽ| ⊕ |g̃|

and

|f̃| ⊕ |g̃| −→^{t_{f}^{−1} ⊕t_{g}^{−1}} |f| ∪ |g| = |g ∘ f| = |i_{2}∘ d| −→^{i_{2}^{−1}} |d|

It is easy to check that the pasting of γ, β and δ yields ρ. We show that γ is a structure-preserving bijection, the argument for the other morphisms is similarly trivial. Since ρi_{2}·c = g∘e we have (i_{1}t_{e}∪i_{2}t_{g})ρi_{2}·c = (i_{1}t_{e}∪ i_{2}t_{g}) · g ∘ e and so γ · c = g̃∘ ẽ.

Indeed, ⟨R,ẽ,f̃,g̃,β,γ,δ⟩ is a candidate for (i). Thus there exists h: Z → R and 2-cells (structure-preserving support bijections) φ: ê ⇒ hc, ψ: hd ⇒ f̂ and τ: ĝh ⇒ id_{Z}

From the existence of τ we can deduce that |g̃| = |g| = ∅ and |h| = ∅. Note that τ = id since there is only one endofunction on ∅. We can therefore also derive M = N and g̃ = g.

[figure: ⟨R,N⟩; _{⟨X,i_{1}|a|⟩}; e; ρi_{2}·c; _{⟨Z,N⟩}; h; _{⟨Y,i_{1}|l|⟩}; i_{2}·d; f; (i); ⟨Z,N⟩; _{⟨R,N⟩}; g; _{⟨Z,N⟩}; h; id; (ii)]

We also get immediately that (ii) above commutes. We show that the left triangle of (i) commutes, the proof for the right one is similar. From the definition of GRPO, we have that id_{c} = τc • g̃φ •γ = gφ •γ which then implies that φ = γ^{−1} . Using the definition of γ, ρi_{2} •φ •t_{e} = id which is the same as saying that the triangle is commutative.

Uniqueness in ℂ̂ easily follows from essential uniqueness in 𝔹 (which is in this case the same as uniqueness since there is only one endofunction on the ∅).

Going the other way, suppose that (i) below

[figure: ⟨Z,N⟩; _{⟨X,L⟩}; c; _{⟨Y,M⟩}; d; _{⟨I,K⟩}; l; a; (i); Z; X; ρ; c̃; Y; d̃; I; ã; l̃; (ii)]

is a RPO. Then (ii) is a GRPO where ρ is

|ã| ⊕ |c̃| −→^{t_{a}^{−1} ⊕t_{c}^{−1}} |a| ∪ |c| = |l| ∪ |d| −→^{t_{l}∪t_{d}} |l̃| ⊕ |d̃|

It is trivial to show that that ρ is structure-preserving (ρ · (c̃∘ ã) = d̃∘ l̃). Now consider a candidate ⟨R,e,f,g,β,γ,δ⟩for (ii) above. Since the pasting composite of γ, β and δ yields ρ, we have that t_{c}^{−1} γ^{−1} i_{2} · g = t_{d}^{−1} δi_{2}· g = g′. Let V = N\|g′|. Let e′= t_{c}^{−1} γ^{−1} i_{1}· e and f′= t_{d}^{−1} δi_{1}· f. Then it is easy but tedious to check that ⟨⟨R,V⟩,e′,f′,g′⟩is a candidate for (i). By assumption, there exists an arrow h: ⟨Z,N⟩→ ⟨R,V⟩which satisfies hc = e′, hd = f′and g′h = f′. This can be translated in the now standard way into a mediating morphism ⟨h,φ,ψ,τ⟩where τ is again the unique endofunction on the ∅. Uniqueness again follows.

Example 5.10 (Bunches). The 2-category of supports of the precategory A-Bun is Bun. Note that a “structure preserving” support bijection is a bunch homomorphism. Indeed, ρ: (X,char,root) → (X′,char′,root′) if X′= ρX, char′= charρ^{−1} and root′= root(id⊕ρ^{−1} ) which is the same as saying char= char′ρ and root= root′(id⊕ρ).

6 Conclusion

We have extended our theory of GRPOs initiated in previous work in order to strengthen existing techniques for deriving operational congruences for reduction systems in the presence of non trivial structural congruences. In particular, this paper has shown that previous theories can be recast using G-reactive systems and GRPOs at no substantial additional complexity. Also, we proved that the theory is powerful enough to handle the examples considered so far in the literature. Therefore, we believe that it constitutes a natural starting point for future investigations towards a fully comprehensive theory.

It follows from Theorem 5.9 that G-categories are at least as expressive as well-supported precategories. A natural consideration is whether a reverse translation may exist. We believe that this is not the case, as general G-categories appear to carry more information than precategories.

Acknowledgement. The authors are indebted to the referees for their helpful comments and suggestions.

References

[1] M. Bugliesi, S. Crafa, M. Merro, and V. Sassone. Communication interference in mobile boxed ambients. In Foundations of Software Technology and Theoretical Computer Science, FST&TCS 02, volume 2556 of Lecture Notes in Computer Science, pages 71–84. Springer, 2002.

[2] A. Carboni, S. Lack, and R. F. C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84(2):145– 158, February 1993.

[3] G. Castagna and F. Zappa Nardelli. The seal calculus revised. In Foundations of Software Technology and Theoretical Computer Science, FST&TCS 02, volume 2556 of Lecture Notes in Computer Science, pages 85–96. Springer, 2002.

[4] J. C. Godskesen, T. Hildebrandt, and V. Sassone. A calculus of mobile resources. In Int. Conf. on Concurrency Theory, CONCUR 02, volume 2421 of Lecture Notes in Computer Science, pages 272–287. Springer, 2002.

[5] M. Hennessy and M. Merro. Bisimulation congruences in safe ambients. In Principles of Programming Languages, POPL 02, pages 71–80. ACM Press, 2002.

[6] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

[7] O. H. Jensen and R. Milner. Bigraphs and transitions. In Principles of Programming Languages, POPL 03. ACM Press, 2003.

[8] G. M. Kelly. Elementary observations on 2-categorical limits. Bull. Austral. Math. Soc., 39:301–317, 1989.

[9] G. M. Kelly and R. H. Street. Review of the elements of 2-categories. Lecture Notes in Mathematics, 420:75–103, 1974.

[10] F. W. Lawvere. Functorial semantics of algebraic theories. Proceedings, National Academy of Sciences, 50:869–873, 1963.

[11] J. Leifer. Operational congruences for reactive systems. Phd thesis, University of Cambridge, 2001.

[12] J. Leifer. Synthesising labelled transitions and operational congruences in reactive systems, parts 1 and 2. Technical Report RR-4394 and RR-4395, INRIA Rocquencourt, 2002.

[13] J. Leifer and R. Milner. Deriving bisimulation congruences for reactive systems. In Int. Conf. on Concurrency Theory, CONCUR 00, Lecture Notes in Computer Science, pages 243–258. Springer, 2000.

[14] R. Milner. Calculi for interaction. Acta Informatica, 33(8):707–737, 1996.

[15] R. Milner. Bigraphical reactive systems: Basic theory. Technical Report 523, Computer Laboratory, University of Cambridge, 2001.

[16] A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1997.

[17] V. Sassone and P. Sobociński. Deriving bisimulation congruences: A 2categorical approach. Electronic Notes in Theoretical Computer Science, 68(2), 2002.

[18] V. Sassone and P. Sobociński. Deriving bisimulation congruences: 2categories vs. precategories. In Proceedings of FOSSACS 03, lncs. sv, 2003.

[19] P. Sewell. From rewrite rules to bisimulation congruences. Lecture Notes in Computer Science, 1466:269–284, 1998.

[20] R. H. Street. Fibrations in bicategories. Cahiers de topologie et géométrie différentielle, XXI-2:111–159, 1980.

Recent BRICS Report Series Publications

RS-03-1 Vladimiro Sassone and Pawe� Sobocinski. Deriving Bisimulation Congruences: 2-Categories vs. Precategories. January 2003. 28 pp. Appears in Gordon, editor, Foundations of Software Science and Computation Structures, FoSSaCS ’03 Proceedings, LNCS 2620, 2003, pages 409–424.

RS-02-52 Olivier Danvy. A New One-Pass Transformation into Monadic Normal Form. December 2002. 16 pp. To appear in Hedin, editor, Compiler Construction, 12th International Conference, CC ’03 Proceedings, LNCS, 2003.

RS-02-51 Gerth Stølting Brodal, Rolf Fagerberg, Anna Östlin, Christian N. S. Pedersen, and S. Srinivasa Rao. Computing Refined Buneman Trees in Cubic Time. December 2002. 14 pp.

RS-02-49 Mikkel Nygaard and Glynn Winskel. HOPLA—A Higher-Order Process Language. December 2002. 18 pp. Appears in Brim, Jančar, Křetínský and Antonín, editors, Concurrency Theory: 13th International Conference, CONCUR ’02 Proceedings, LNCS 2421, 2002, pages 434–448.

RS-02-48 Mikkel Nygaard and Glynn Winskel. Linearity in Process Languages. December 2002. 27 pp. Appears in Plotkin, editor, Seventeenth Annual IEEE Symposium on Logic in Computer Science, Lics ’02 Proceedings, 2002, pages 433–446.

RS-02-47 Zoltán Ésik. Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators. December 2002. 16 pp. To appear in 6th International Conference, Developments in Language Theory, DLT ’02 Revised Papers, LNCS, 2002.

RS-02-46 Zoltán Ésik and Hans Leiß. Greibach Normal Form in Algebraically Complete Semirings. December 2002. 43 pp. An extended abstract appears in Bradfield, editor, European Association for Computer Science Logic: 16th International Workshop, CSL ’02 Proceedings, LNCS 2471, 2002, pages 135–150.

RS-02-45 Jesper Makholm Byskov. Chromatic Number in Time O(2.4023^{n}) Using Maximal Independent Sets. December 2002. 6 pp.