CongruencesforContextualGraph-Rewriting BRICS

BRICS

Basic Research in Computer Science

Congruences for

Contextual Graph-Rewriting

Vladimiro Sassone Paweł Soboci ´nski

BRICS Report Series RS-04-11

ISSN 0909-0878 June 2004

BRICSRS-04-11Sassone&Soboci´nski:CongruencesforContextualGraph-Rewriting

Copyright c2004, Vladimiro Sassone & Paweł Soboci ´nski.

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 subdirectoryRS/04/11/

Congruences for Contextual Graph-Rewriting

Vladimiro Sassone Paweł Soboci´nski

Abstract

We introduce a comprehensive operational semantic theory of graph- rewriting. Graph-rewriting here is meant in a broad sense as we aim to cover and extend previous work based both on Milner’s bigraphs and Ehrig and K ¨onig’s rewriting via borrowed contexts. The central idea is recast- ing rewriting frameworks as Leifer and Milner’s reactive systems. Con- sequently, graph-rewriting systems are associated with canonical labelled transition systems, on which bisimulation equivalence is a congruence with respect to arbitrary graph contexts (cospans of graphs). The central tech- nical contribution of the paper is the construction of groupoidal relative pushouts, introduced and developed by the authors in recent work, in input- linear cospan (bi)categories over arbitrary adhesive categories.

Contents

1 Preliminaries 5

1.1 Adhesive categories . . . 5 1.2 2-categories and cospan bicategories . . . 7 1.3 Reactive systems and GRPOs . . . 8 2 Constructing GRPOs for input linear cospans 10

3 Applications 17

3.1 Double-pushout rewriting and borrowed contexts . . . 18 3.2 Bigraphs as cospans . . . 25

4 Conclusion 27

Introduction

Operational techniques, including coinductive arguments, which originated from research on the semantics of concurrency, have recently begun to be applied in

other areas of (computer) science (cf. e.g. [1, 5]). The main facet of these ap- proaches is the use of labelled transition systems (lts) and the accompanying no- tions of operational preorders and equivalences, bisimulation being chief among these.

Leifer and Milner’s seminal [13] introduced reactive systems and initiated the investigation of their semantics. Reactive systems are a generalisation of ground term-rewriting systems, where a collection of ground rewrite rules is closed under a set of “reactive” contexts to obtain the rewrite relation. Contexts are organised as the arrows of a categoryC. Using a universal categorical construction, the relative pushout (RPO), each reactive system can be equipped with an lts. The labels of the lts are the ‘smallest’ contexts which allow reactions to occur – an idea due to Sewell [18]. Such ltss are very well-behaved; in particular, bisimulation is a congruence with respect to all contexts, provided thatChas enough RPOs.

When applied naively, RPOs have proven inadequate in some reactive sys- tems where contexts have non-trivial algebraic structure. In some cases they do not give the expected labels in the lts (cf. [17]), while in others, they do not ex- ist (cf. [16]). The troublesome contexts often exhibit non-trivial automorphisms, which naturally form a part of a 2-dimensional structure on the underlying cat- egory C. It is important to notice that such situations are the norm, rather than the exception. Context isomorphisms arise naturally already in simple process calculi, where terms are up to structural congruence. In [17], the authors pro- posed an enhanced approach based on a 2-dimensional generalisation of RPOs, the groupoidal relative pushout (GRPO), which has been shown in [16] to en- compass previous approaches addressing these issues.

Several constructions of RPOs have been proposed in the literature for partic- ular categories of models. For example, Leifer [12] constructs RPOs in a category of action graphs, while Jensen and Milner do so in the category of bigraphs [9].

A construction of (G)RPOs in a general setting has so far been missing. In this paper, we construct GRPOs in a general framework of abstract, uninterpreted con- texts. Given a category of interestC, we consider a “category of contexts” where the objects ofCcan be composed with each other through interfaces: the cospan bicategory onC. Such bicategories have the same objects asC, but the arrows are cospans

I ^{ι //}C^{oo o} J,

which can be viewed as an object C enriched with an “input” interfaceιand and

“output” interface o. Roughly,ιis the partial view of C attainable from its “holes,”

while o is the restricted view of C afforded to the “environment.” Composition of cospans is performed by pushing out interfaces, which can be understood as “glue- ing together” an agent and its context along their common interface. Due to the nature of pushouts, composition is only associative up to a unique isomorphism.

$

$

S C C

take money

pour coffee

$

$ C

C Bob

insert money

drink coffee

$

S C Bob

take money

pour coffee insert

money

drink coffee

Figure 1: Example of a contextual system

As an example of these concepts, consider the simple model of a coffee vend- ing machine, illustrated by the leftmost diagram of Figure 1. It has an output interface consisting of two nodes, $ and C, which one can think of as a money slot and the coffee out-tray. These are the parts of the coffee machine accessible to the environment, the internal components, represented by S , are invisible. The middle diagram represents a coffee drinker. He expects to see a money slot and a coffee out-tray, which are his input interfaces. As the output interface of the cof- fee machine and the input interface of the coffee drinker match, one may compose them and obtain the system pictured in the rightmost diagram. (Input and output interfaces of the vending machine and coffee drinker have been omitted.)

The main result of the paper is the construction of GRPOs in a class of cospan bicategories, which in turn allows the derivation of ltss for all reactive systems over such bicategories. Specifically, we require a linearity condition on the input interfaces, namely, that ι is mono. Additionally, our cospans are over adhesive categories [11], which are categories in which pushouts along monomorphisms exist and are suitably well-behaved. As we prove in the paper, adhesive categories have enough structure for the construction of GRPOs in our cospan bicategories.

Although technical in nature, the linearity condition does have an intuitive ac- count. As alluded in the coffee drinker example, one can consider a cospan as a “black box,” with an input interface and an output interface. The environment cannot see the internals of the system and only interacts with it through the out- put interface. The fact that the output interface need not be linear means that the system is free to connect the output interface arbitrarily to its internal representa- tion. For example, the coffee machine could have two extra buttons in its output interface; the “caf´e latte” button and the “cappuccino” button. The machine inter- nals could connect both these buttons to the same internal trigger for coffee with milk; the point is that the system controls its output interface and is able to equate parts of it. On the other hand, the system cannot control what is plugged into one of its holes. Thus, an assumption of input-linearity is essentially saying that the system does not have the right to assume that two components coming in through

the input interface are equal.

In order to prove the relevance and usefulness of the construction, we treat two large examples. Firstly, we apply it to derive lts for double-pushout (DPO) graph-rewriting systems. Graph rewriting is a well-established field of theoreti- cal Computer Science [2], concerned with the extension of rewriting techniques from terms to graph structures. DPO graph rewriting can be generalised nicely to rewriting in arbitrary adhesive categories [11].

As DPO graph-rewriting systems can be seen as reactive systems on the bi- category Cospan(Graph), the bicategory of cospans over the (adhesive) category of graphs, we can derive ltss for graph rewriting directly and systematically. This equips any arbitrary graph rewriting system with a contextual semantics and a corresponding coinduction principle, so as to allow for the transfer of concepts and techniques from the field of process algebra to graph-rewriting. In other words, this yields a behavioural equivalence based uniquely on the interactions of (concurrent) dynamic systems with their environment, while the presence of a well-behaved lts allows the use of bisimulation to prove contextual equivalence.

When restricting cospans to purely linear (mono) maps, the lts we derive agrees, almost on-the-nose, with Ehrig and K¨onig’s recently proposed approach, the so-called rewriting with borrowed contexts [5]. Consequently, Ehrig and K¨onig’s congruence theorem can be understood as a corollary of the congruence theorem for GRPOs [17]. Without the restriction, the application of reactive sys- tems to graph rewriting extends the borrowed-context approach by considering graph contexts where the output interface need not be injective. In this applica- tion, therefore, the paper contributes in two ways. Firstly, it is an extension of the results of Ehrig and K¨onig; secondly, it provides a missing link between their work and the work of Leifer and Milner [13].

Our second application is the construction of GRPOs for a version of Milner’s bigraphs [9]. Bigraphs have been recently proposed as a formalism to model mo- bility of communication channels, or links (as in the π calculus), together with spatial mobility of agents, or places (as in distributed calculi). We introduce the adhesive category of place-link graphs. The cospan bicategories over place-link graphs resemble Milner’s bigraphs, with some differences imposed by the respec- tive linearity conditions. The general construction of GRPOs provides reactive systems over our bigraphs with a labelled transition semantics.

The advantages of a general approach to GRPOs based on abstract “categories of contexts” include, therefore, insights into how these are constructed and apply across a wide range of models. Moreover, given a reactive system within the class treated in this paper, the GRPO construction provides not only a canonical congruent process equivalence (bisimulation on the resulting lts), but also a proof method: the lts itself.

Structure of the paper. In the first of the three preliminary sections, section 1.1, we recall the recently introduced notion of adhesive category due to Lack and the second author [11]. Secondly, in section 1.2, we recall the notions of 2-categories and cospan bicategories. Finally, section 1.3 recalls the definition of a reactive system, which we generalise slightly so that we are able to consider a bicategory as the underlying category of a reactive system. This section relies heavily on technology previously introduced by the authors in [17] and [16]. The main result of the paper, the construction of GRPOs for a class of reactive systems over cospan bicategories, is stated and proved in section 2; sections 3.1 and 3.2 illustrate two applications, respectively the derivation of ltss for DPO graph rewriting and the construction of GRPOs for a variant of bigraphs.

1 Preliminaries

1.1 Adhesive categories

In order to construct GRPOs in cospan bicategories we shall need the notion of ad- hesive categories [11], which we recall below. Adhesive categories have a slogan:

pushouts along monomorphisms exist and are well-behaved. We shall assume that the underlying category of the cospan bicategory is adhesive and use the structure of adhesive categories repeatedly in the proof of our main result, Theorem 2.1.

The definition of adhesive categories uses the notion of van Kampen square.

Definition 1.1 (van Kampen square). A van Kampen (VK) square (i) is a pushout which satisfies the following condition: given a commutative cube (ii) of which (i) forms the bottom face and the back faces are pullbacks, the front faces are pull- backs if and only if the top face is a pushout.

C _f

?

??

m

A

g@@@ B

~~~n

D (i)

C⁰

m⁰

vvmmmmmmm CC!!^f0

c

A⁰

a

g⁰DD!! B⁰

b

n⁰

vvmmmmmmm

D⁰

d

C

lllm

vvlll DDD^f!!

A

gDDD"" B

vvllllnlll

D (ii)

Definition 1.2 (Adhesive category). A categoryCis said to be adhesive if it has pullbacks, pushouts along monos, and these latter are VK-squares.

Given m : C → A and g : A → D, we say that B is a pushout complement of (m,g) when there exist f : C → B and n : B → D such that the resulting diamond (i) is a pushout diagram.

We shall need the following properties of adhesive categories for our construc- tions. The proof of the following lemma can be found in [11].

Lemma 1.3. LetCbe an adhesive category.

1. Monos are stable under pushout inC. In other words, in diagram (i), if m is mono then n is mono.

2. A pushout diagram (i) inCis also a pullback diagram, if m is mono.

3. If it exists, a pushout complement of (m,g), with m mono, is unique up to a compatible isomorphism; more precisely, if f : C → B,n : B → D and f⁰ : C → B⁰,n⁰ : B⁰ → D are pushout complements, then there exists an isomorphismϕ: B→ B⁰such thatϕf = f⁰and n⁰ϕ= n.

The following simple lemma has not been published previously.

Lemma 1.4. Consider the following diagram in an adhesive category C. If the outer region is a pushout, the right square is a pullback, and morphisms k,r,u and w are mono, then the left square is a pushout.

A

l // ^k //B

s// ^r //E

v

C^// _u ^//D^// _w ^//F

Proof. The exterior pushout is stable under pullback along w : D ^{// //}F , as illus- trated below.

A

^k @@@@@

~~~l ~~

C

u

@

@@

@@ A

k

@

@@

@@

~~l

~~

B

@@@@@

C

u@@@@

@ D

@@@@@ B^r_@@

@@

B

 r

~~~~~s

D

w@@@@@ D

w

E

~~~~~v

F

Examples of adhesive categories include Set, the category of sets and func- tions, and Graph, the category of graphs and their morphisms. Toposes, as well as slice and coslice categories over adhesive categories are adhesive. Indeed, several graph structures relevant to computer science form adhesive categories (cf. [11]).

1.2 2-categories and cospan bicategories

In this section we give only a minimal introduction to 2-categories and cospan bi- categories. For an introductory treatment, the reader should refer to [14]. Roughly, a 2-categoryCis a category where homsets (that is the collections of arrows be- tween any pair of objects) are categories and, correspondingly, whose composition maps are functors. Explicitly, a 2-categoryBconsists of the following.

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

• For any X,Y ∈ C, a category C(X,Y). The objects C(X,Y) are called 1- cells, or more often, arrows or morphisms, and denoted by f : X → Y. Its morphisms are called 2-cells, are writtenα: f ⇒ g : X →Y, or sometimes simply α: f ⇒ g. Composition in C(X,Y) is denoted by • and referred to as ‘vertical’ composition. Identity 2-cells are denoted by 1_f: f ⇒ f . Isomorphic 2-cells are occasionally denoted asα: f g;

• For any objects X,Y,Z there is a functor.: C(Y,Z)×C(X,Y) →C(X,Z), the so-called ‘horizontal’ composition, which we shall often denote by mere juxtaposition. On objects, the functor is just the ordinary composition in the underlying “ordinary” category. On arrows, the functor provides a hori- zontal composition of 2-cells; it is associative and admits 1_idX as identities.

A bicategory can be thought of, intuitively, as a 2-category where associativity and identity laws of horizontal composition hold up to isomorphisms. We shall denote all associativity isomorphisms by ζ, as for example,ζ : h(g f ) ⇒ (hg) f . The isomorphisms are required to respect the well-known coherence axioms [15].

Cospan Bicategories. We will assumeCto be a category with chosen pushouts.

That is, for arrows m : C → A and f : C → B, there exists a unique “chosen”

object A+C B and arrows i₁ : A → A+C B and i₂ : B → A+C B such that the resulting square is a pushout. By the universality of pushouts, given any other object D and arrows g : A→ D and n : B→ D which render the resulting square a pushout, there exists a unique isomorphismα: A+C B → D such thatαi₁ = g andαi₂ = n. We shall adopt the convention of always labelling the morphisms into the chosen pushout by i₁and i₂; when considering more than one chosen pushout we shall use the context in order to disambiguate.

The bicategory of cospans Cospan(C) has the same objects asC, but arrows from I₁to I₂are cospans.

I₁ ^{f //}C^{oo g} I₂ We will denote such cospans C^g_f : I₁ → I₂ or C^g:I_{f :I}²

1, and omit f (resp. g) when I₁ (resp. I2) is an initial object. We shall refer to I1and I2as the input and the output

interfaces of C^g_f. Intuitively, we can think of a cospan as a generalised context, where C are the internals, (the image via g of) I2represents the public view of C, and (the image via f of) I₁ the view of C afforded to the ‘holes’ in it.

A 2-cell h : C^g_f ⇒C⁰_f^g₀⁰: I₁ → I₂is an arrow h : C→C⁰inCsatisfying h f = f⁰ and hg =g⁰. The 2-cells that are iso (i.e. invertible) provide a canonical notion of

“structural congruence.” We shall denote the bicategory of cospans which has the 2-cells limited to isomorphisms by CospanC. Given cospans C^g_f : I₁ → I₂ and D^g_f⁰₀ : I₂ → I₃, their composition D^g_f⁰₀ ◦C^g_f : I₁ → I₃ is the cospan (C +I2 D)ⁱ_i^2g0

1f : I₁→ I₃, as illustrated by the pushout diagram below.

C+I2 D I₁ ^{f //}C

i199

I₂

oo g ^f0 //D

i2

ee

I₃

g⁰

oo

Note that in the resulting composition, I₂ is “forgotten.” Composition is associa- tive up to a unique isomorphism. It is easy to check that the associativity isomor- phisms satisfy the coherence axioms, and thus yield a bicategory

In the construction of 2 we shall need certain linearity restrictions. In particu- lar, the notion of input-linear cospan.

Definition 1.5 (Linearity). A cospan C_m^g is said to be input-linear when m is a mono. A cospan Cⁿ_mis said to be linear when both m and n are mono.

When working over an adhesive category, a simple corollary of the first part of Lemma 1.3 is that the composition of two input-linear cospans yields an input- linear cospan. Similarly, composition preserves linearity.

Definition 1.6 (Linear Cospans). Assuming thatCis adhesive, let ILC(C) be the bicategory consisting of input-linear cospans and 2-isomorphisms. Similarly, let LC(C) be the bicategory of linear cospans and 2-isomorphisms.

1.3 Reactive systems and GRPOs

Here we shall briefly recall an extension of Leifer and Milner’s notion of re- active system to two dimensional categories as introduced by the authors previ- ously [17]. In this paper we shall consider cospan bicategories with isomorphic 2-cells, and therefore, we shall be concerned with reactive systems over such bi- categories.

The intuition behind the 2-dimensional structure is that, while arrows of the underlying category are viewed as contexts, the (isomorphic) 2-cells are thought of as “proofs of structural congruence” between contexts (recall that a 2-cellϕ : a⇒ a⁰ : A→ B is an isomorphism when it is an isomorphism in C(A,B), that is,

there exists a 2-cellψ : a⁰ ⇒ a such thatψ•ϕ = 1_a andϕ•ψ = 1_a0). Recall that in the particular case of the bicategory Cospan(Graph), the 2-cells are precisely graph isomorphisms which respect the input and output interfaces.

Definition 1.7 (Reactive System). A reactive system C consists of 1. a bicategoryB;

2. a collectionDof arrows of Bcalled the reactive contexts; it is required to be closed under isomorphic 2-cells and composition-reflecting (see below);

3. a distinguished object 0∈B;

4. a set of reaction rulesR, it consists of pairs of arrowshl,riwith domain 0.

The members l,r of any given pairhl,ri ∈ Rhave the same codomain.

The reactive contexts are those inside which evaluation may occur. To reflect composition means that dd⁰ ∈Dimplies d and d⁰ ∈D, while the closure property means that given d ∈Dand an isomorphismρ: d⇒ d⁰ inBimplies d⁰ ∈D.

The reaction relation Bis defined by taking a Bdr if there ishl,ri ∈ R, d ∈Dandα: dl⇒ a. This represents that, up to structural congruenceα, a is the left-hand side l of a reduction rule in a reaction context d.

Leifer and Milner [13] developed the derivation of a canonical lts associated to any given reactive system. The derivation uses a universal construction, dubbed relative-pushout (RPO), which is a pushout in a slice category. Bisimulation on the resulting lts is a congruence, provided that the underlying category of the reactive system has enough RPOs.

For category theorists, a groupoidal-relative-pushout (GRPO) can be described concisely as a bipushout in a pseudo-slice category. We refer the reader to [17]

for a more accessible definition and fundamental properties. Note that although GRPOs are introduced there in the setting of G-categories (2-categories with iso 2- cells), the development is easily transferred to bicategories with iso 2-cells. Here we give a brief sketch. Given a 2-cellα: ca ⇒ db : I₁ → I₄, as illustrated in (i) below, a candidate is a tuple C =hI₅,e, f,g, β, γ, δi, as illustrated in (ii) below, so that the 2-cells paste together

I₄ I₂ α

c{{{{==

{{

I₃

aa d

CCCCCC

I₁ ^b

=={

{{ {{ {

a

aaCCCCCC

(i)

I₄ I₂ ^{e //}

c{{{{==

{{

I₅

γ δ

β gOO

I₃

oo f

aa d

CCCCCC

I₁ ^b

=={

{{ {{ {

a

aaCCCCCC

(ii)

(taking into account the associativity isomorphisms) to giveα. It is a GRPO if it is the smallest such candidate, in the following sense: given another such candidate

C⁰ there exists a mediating morphism u : I₅ → I⁰₅ and appropriate 2-cells which make the two candidates compatible. Such a mediating morphism is required to be essentially unique, meaning that given any other mediating morphism u⁰ : I₅ → I₅⁰, there exists a unique isomorphic 2-cellξ: u⇒u⁰which makes the two mediating morphisms compatible.

Definition 1.8 (GIPO). Diagram (i) is said to be a G-idem-pushout (GIPO) if hI₄,c,d,id, α,1_c,1_diis its GRPO.

Definition 1.9 (LTS). For C a reactive system and B its underlying bicategory, define GLTS(C) as follows:

• the states GLTS(C) are iso-classes of arrows with domain the chosen object 0 (two arrows a,a⁰ : 0 → I1 are in the same iso-class when there exists an isomorphic 2-cell ϕ : a ⇒ a⁰). We shall denote the iso-class of a as [a] : 0→ I₁;

• there is a transition [a] ^{[ f ]}I [dr] if there exists a 2-cellα, a rulehl,ri ∈ R, and d ∈D, such that the diagram below is a GIPO.

I₄ I2

f @@

α I3

^^ d

>>>

a 0

__???

l

??



(1)

Definition 1.10. A reactive system C is said to have redex-GRPOs when every redex-square (1), with a, f arbitrary, d a reactive context and l a part of a reaction rulehl,ri ∈ R, has a GRPO.

The following is an extension of a theorem for 2-categories which can be found in [17], the proof requires only slight modifications for the extension in generality.

Theorem 1.11. Let C be a reactive system with redex-GRPOs. Then bisimulation on GLTS(C) is a congruence with respect to all the contexts of C.

Theorem 1.11 is quite robust with respect to the equivalence under consider- ation. For example, trace and failures equivalences on GLTS(C) are also congru- ences. Therefore, the derived lts may be considered as very well-behaved.

2 Constructing GRPOs for input linear cospans

In this section we present a general construction of GRPOs for a class of reactive systems over cospan bicategories. We shall conclude with several examples of

GRPOs in the bicategory ILC(Graph), the bicategory of input-linear cospans in the category of directed graphs.

Formally, letCbe an adhesive category. We shall prove that ILC(C) has GR- POs. This implies that any reactive system over ILC(C) has redex-GRPOs and therefore can be given a canonical labelled transition system semantics.

Theorem 2.1. ILC(C) has GRPOs.

We shall first outline an algorithm for the construction of the desired minimal candidate. A redex square in ILC(C), as illustrated in diagram (i) below, amounts to a commutative diagram (ii) in C, withαan isomorphism. We shall adopt the convention of ^{/o /o //} representing the isomorphisms of C which correspond to the 2-cells of ILC(C).

I₄ I₂ α

C @@

I₃

^^ D

>>>

I₁

A

^^>>> _B@@

(i)

C

i2

I₄

oC

oo ^oD //D

i2

I2

:: ^ι

Cuuuu::

uu

oIAIIII$$

I A+I2 C ^{/o /oα/o /o //}B+I3 D I3 oB

zzuuuuuu

dd

ιD

ddIIIIII

A^OO

i1

OO

I₁^// _ι

B

//

ooιA

oo

(ii)

B^OO

i1

OO

Recall that given an object X, a subobject [µ : Y → X] is an equivalence class of monomorphisms into X, where the equivalence relation is generated from the canonical preorder on monomorphisms into X: µ ≤ µ⁰ if there exists k : Y → Y⁰ such that µ⁰k = µ. We shall abuse notation by confusing the subobject (equiva- lence classes of monos) with its representativeµ(one mono).

In the following, we let X = B+I3 D and Y = A∪B, a subobject of X. We obtainµ: Y → X,1 : A→Y and2 : B→Y satisfyingµ1 = αi₁andµ2 =i₁. Algorithm 2.2 (GRPO Construction in ILC(C)). The construction of the com- ponents of the minimal candidate is outlined below. They are illustrated in dia- grams (iii) and (iv). We obtain the components by constructing:

1. G as the pullback ofαi₂: C→X and i₂: D→ X;

2. E as the pullback ofµ: Y → X andαi2 : C→ X;

3. F as the pullback ofµ: Y →X and i2 : D→ X;

4. I₅ as the pullback of ρ2: F → D and π2: G → D; Notice that due to the properties of pullbacks, we obtain a morphism o_E : I₅ →E such that all the faces of (iv) are pullbacks.

Proof. We give an outline of the proof in two parts. Firstly, we show that the components constructed in Algorithm 2.2 are a candidate, secondly, we show that the candidate is universal.

Construction of candidate.

I4

I₂

C{{{{{==

{

E^γ//I₅ ^δ

β GOO

I₃

oo F

aa D

CCCCCC

I₁

A

aaCCCCCC B

=={

{{ {{ {

(iii)

I₅

oE

wwoooooo_o ??^ιG

F

E

σ1

^ρ1?? G

π2

π1

wwnnnnnn

αiC2

σ2 ooF

wwoooo AA^{ρ 2}

Y

µ@@ D

i2

wwnnnnnn

X (iv)

Construct the cube (iv), by taking pullbacks as explained in Algorithm 2.2. The exterior rectangles of diagrams (v) and (vi) are pushouts (dia. (ii)), and therefore, commutative.

I₂ ⁹⁹

ιC

%%// _ιE //

oA

E

σ1 // (†)ρ1 //C

αi2

A^// ₁ ^//Y^// _µ ^//

(v)

X

I₃⁹⁹

ιD

%%// _ιF //

oB

F

σ2 // (‡)ρ2 //D

i2

B^// ₂ ^//Y ^// _µ ^//

(vi)

X

Using the pullback property, we obtainιE : I2 → E satisfying σ1ιE = i1oA and ρ1ιE = ιC. Similarly, we obtainιF : I₃ → F which satisfies analogous equations.

We can now use Lemma 1.4 to conclude that the left hand squares of diagrams (v) and (vi) are pushouts, which in turn implies that (†) and (‡) are pushouts, using ordinary pushout pasting.

Since all the side faces of (iv) are pullbacks and the bottom face is a pushout, we can conclude by adhesiveness that the top face is a pushout. Similarly, the front left face being a pushout implies that the back right face is a pushout. Using the fact that G was defined as a pullback, we obtain a unique morphism o_G : I₄ → G such that π1oG = oC and π2oG = oD. We summarise the parts of the candidate constructed so far in diagram (vii), below.

I₄

oC

^oG

oD

C G^{π1oo π2 //}D

I2//

ιE

//HH

ιC 66

E^OO

ρ1

OO

I5

(vii)

oE

oo oF

//OO^ιGOO

F^OO

ρ2

OO

I3

ooιF

oo VV^ι

ii D

Let E+I5 G denote the chosen pushout of o_E andιG and letγ : C → E+I5 G be the unique induced isomorphism. Similarly, we obtain a unique isomorphism δ : F +I₅ G → D. Referring back to diagrams (iv) and (v), we have A+I2 E

Y B+I3 F. Let β : A+I2 E → B+I3 F denote the unique compatible isomor- phism. The isomorphisms are illustrated in diagram (viii) as arrows ofC, and as 2-cells of ILC(C) in diagram (iii). It is straightforward but tedious to check that δB•Gβ•γA=αin ILC(C).

C ^γ//E+I5 G^oo G ^//F+I5 G ^δ//D I2

ιCOO

oA

ιE //E

OO I5

ιGOO

oE

oo oF //F

OO I3

ιD

OO

oB

ι_R3

oo

A ^//A+I2 E

/o /oβ/o /o //

(viii)

B+I3 F ^oo B

I4

I2 C ??

E^0γ//I₆

0 δ⁰

β⁰ G⁰

OO

I₃

F⁰

oo

__ D

>>>>>

I₁

A

__>>>>> _B??

(ix)

Universality. Suppose that there is another candidate, as illustrated in diagram (ix). Lettingπ⁰₁ = γ⁰⁻¹i₂: G⁰ →C andπ20 = δ⁰i₂ : G⁰ → D and using the fact that G is a pullback object, we get an arrowλ: G⁰ → G such thatπ1λ= π⁰₁ : G⁰ → C andπ2λ = π⁰₂ : G⁰ → C. Consider diagram (x) below, where T denotes B+I3 F⁰. We have an isomorphism (B+I3δ⁰)ζ : T+I6G⁰ → X, Letη: T → X andθ: G⁰ →X denote the corresponding morphisms derived by precomposing with i₁and i₂.

E⁰ β⁰i2

@

@@

@ ⁱ2 F⁰

~~~~~~

I₂^>>

ιE0~~~~>>

oAAAAA T ^``I₃

ι⁰_F

``AAAA

oB

~~}}}}

A^{>> β0i1}

>>

~~

~~

(x)

``B

i1

``@@@@

I6 oT

 ι^G0

A

AA A

T

η??? G⁰

~~||||θ

X (xi)

Letµ⁰ : Y → T be the arrow induced byβ⁰i₁and i₁in diagram (x). One can verify thatηµ⁰ =µ.

In diagram (xii) below, we let ρ⁰₁ denote γ⁰⁻¹i₁, while in diagram (xiii) let ρ⁰₂ = δ⁰i₁. Consider diagram (xii) again, and note that regions (†) and (†)+(‡) are pushouts. Hence, (‡) is a pushout and, using the second part of Lemma 1.3, a pullback. Thus there exists a morphismν1 : E → E⁰ such that ρ⁰₁ν1 = ρ1 and β⁰i₂ν1 = µ⁰σ1. A similar chain of reasoning involving diagram (xiii) allows us to derive the existence ofν2 : F → F⁰which satisfiesρ⁰₂ν2 =ρ2and i₂ν2= µ⁰σ2.

One can now deduce that the leftmost squares in the two diagrams are pull- backs, and therefore, that ν1 and ν2 are both mono, since they are pullbacks of monoµ⁰ along, respectively,β⁰i₂and i₂.

I₆

(†) oE0 // ^ιG0 //G⁰

π⁰₁

σ1E //^ν1//E⁰

β⁰i2 // ⁽_ρ^‡0₁⁾ //C

αi2

Y ^//

µ⁰//T ^// _η ^//X (xii)

I₆

oF0 // ^ιG0 //G⁰

π⁰₂

F

σ2 //^ν2//F⁰

i2 // _ρ⁰₂ //D

i2

Y ^//

µ⁰//T ^// _η ^//X (xiii)

In diagram (xiv), H and morphisms κ1, κ2 andχ are chosen so that the two rear faces are pullbacks. One could do this, e.g., by first taking the pullback ofπ2and ρ⁰₂ and obtainingκ1from the pullback property of the front left face.

κ1 H

vvnnnnnn _χ CC^κ!!²

E⁰

ρ⁰1

β⁰i2

B

B F⁰

ρ⁰2

i2

vvnnnnnn

T

η

π1 nnnG

wwnnn CC^π!!²

C

αi2BB D

i2

vvnnnnnn

X (xiv)

One may consider H as the mediating morphism from I₅ to I₆. Indeed, in dia- grams (xv), (xvi) and we use adhesiveness in order to deduce that the top faces are pushouts.

I₅

oE

wwnnnnnnn @@^ιH

E

^ν1 BB H

χ

κ1

vvnnnnnn

E⁰

ρ⁰₁

I₅

oE nnn

wwnnn ?^ι?^G

E

ρ1BB G

π1

vvnnnnnn

C (xv)

I₅

vvιH

vvnnnnnnn ??^{o F}

H

χ

κ2

!!C

C F

vv

ν2

vvnnnnnn

F⁰

ρ⁰₂

I₅

vvιG nnn

vvnnn

oF

>

>

G

π2CC!! vvF

ρ2

vvnnnnnn

D (xvi)

Because the top face of diagram (xiv) is a pullback, we obtain a unique mor- phism o_H : I₆ → H such thatκ1o_H = o_E0 andκ2o_H =o_F0.

We shall show that diagram

I₆

oH

//^ιG0//G⁰

λ

H^// _χ ^//G

(xvii)

I₆

(∗) oH

// ^ιG0 //G⁰

w

H

κ1

^κ2 C//C!!

v //U u2

!!C

C

u1

F⁰

// //D

E⁰

!!C

C// //C

""

DD D

T ^// _η ^//X (xviii)

κ1 H

vvnnnnnn !!CC^v!!

κ2

E⁰

BB U

u2

u1

vvmmmmmmm

C

F⁰

vvnnn nnn !!CC!!

T _!!

ηBB!! D

vvmmmmmmm

X (xix)

is a pushout. First notice that it is commutative, we have π1χo_H = ρ⁰₁κ1o_H = ρ⁰₁oE⁰ = π⁰₁ιG⁰ = π1λιG⁰ and similarlyπ2χoH = ρ⁰₂κ2oH = ρ⁰₂oF⁰ = π⁰₂ι⁰_G = π2λιG⁰

which implies thatχo_H = λιG⁰, using the fact that the bottom face of diagram (xiv) is a pullback.

We shall now construct diagram (xviii). We start by taking the pushout (∗).

Now since region (†) of diagram (xii) is a pushout, there exists a unique mor- phism u1 : U → C such that u1w = π⁰₁ and u1v = ρ⁰₁κ1. Similarly, using the fact that the corresponding region of diagram (xiii) is a pushout, there exists a unique morphism u₂ : U → D such that u₂w = π⁰₂ and u₂v = ρ⁰₂κ2. Using the stan- dard decomposition property of pushouts, the two newly constructed regions are pushouts. The two lower regions of diagram (xviii) are the pushouts which appear as the two front faces of diagram (xiv). The left face of the cube is the top face of (xiv) which is a pullback. Spinning the cube around into diagram (xix) we use the fact that the bottom and top faces are pushouts, and the back faces pullbacks to deduce that the front right face is a pullback.

Since also the bottom face of diagram (xiv) is a pullback, we obtain a unique isomorphismζ : G → U such that u₁ζ = π1 and u₂ζ = π2. As we have assumed that (∗) is a pushout, to prove that diagram (xvii) is a pushout it remains to show thatζλ=w andζχ=v.

Indeed u₁ζλ = π1λ = π⁰₁ = u₁w and u₂ζλ = π2λ = π⁰₂ = u₂w which implies thatζλ = w. Also u₁ζχ= π1χ= ρ⁰₁κ1 = u₁v and u₂ζχ= π2χ = ρ⁰₂κ2 = u₂v which implies thatζχ=v.

Letϕ : E⁰ → E+I5 H,ψ : F+I5 H → F⁰andτ: H+I6 G⁰ →G be the unique induced isomorphisms. It can be verified thatτE•G⁰ϕ•γ⁰ = γ,δ^{0 •}G⁰ψ•τF = δ andψB•Hβ•ϕA=β⁰in ILC(C).

Essential uniqueness of H : I₅ → I₆ can be shown by using the third part of Lemma 1.3, applied to diagram (xvii), we omit the details here.

Notice that we can give a simplified presentation of the construction of the minimal candidate if we assume that all the cospans are linear.

Algorithm 2.3 (GRPO Construction in LC(C)). When all the morphisms in di- agram (ii) are mono, constructing the pullback amounts to computing the inter- section of subobjects of X. Indeed, we let:

1. G=C∩D;

2. E = Y∩C;

3. F =Y∩D;

4. I₅ = F∩G=F ∩E =E∩G.

In the simple examples below, meant to illustrate the application of Algo- rithm 2.2, we shall consider ILC(Graph) as our category of contexts. In the ac- companying Figures 2–4, we label the nodes of the graphs in order to clarify the