Technical Report
Number 570
UCAMCLTR570 ISSN 14762986
Computer Laboratory
Bigraphs and mobile processes
Ole H?gh Jensen, Robin Milner
July 2003
15 JJ Thomson Avenue Cambridge CB3 0FD United Kingdom phone +44 1223 763500 http://www.cl.cam.ac.uk/
c 2003 Ole H?gh Jensen, Robin Milner Technical reports published by the University of Cambridge Computer Laboratory are freely available via the Internet: http://www.cl.cam.ac.uk/TechReports/ Series editor: Markus Kuhn ISSN 14762986
Bigraphs and mobile processes
Ole H?gh Jensen ? BRICS, Alborg University Department of Computer Science July 2003 Robin Milner University of Cambridge Computer Laboratory
Abstract: A bigraphical reactive system (BRS) involves bigraphs, in which the nesting of nodes represents locality, independently of the edges connecting them; it also allows bigraphs to recon?gure themselves. BRSs aim to provide a uniform way to model spatially distributed systems that both compute and communicate. In this memorandum we develop their static and dynamic theory. In Part I we illustrate bigraphs in action, and show how they correspond to to process calculi. We then develop the abstract (nongraphical) notion of wide reactive system (WRS), of which BRSs are an instance. Starting from reaction rules —often called rewriting rules— we use the RPO theory of Leifer and Milner to derive (labelled) transition systems for WRSs, in a way that leads automatically to behavioural congruences. In Part II we develop bigraphs and BRSs formally. The theory is based directly on graphs, not on syntax. Key results in the static theory are that suf?cient RPOs exist (enabling the results of Part I to be applied), that parallel combinators familiar from process calculi may be de?ned, and that a complete algebraic theory exists at least for pure bigraphs (those without binding). Key aspects in the dynamic theory —the BRSs— are the de?nition of parametric reaction rules that may replicate or discard parameters, and the full application of the behavioural theory of Part I. In Part III we introduce a special class: the simple BRSs. These admit encodings of many process calculi, including the π calculus and the ambient calculus. A still narrower class, the basic BRSs, admits an easy characterisation of our derived transition systems. We exploit this in a case study for an asynchronous π calculus. We show that structural congruence of process terms corresponds to equality of the representing bigraphs, and that classical strong bisimilarity corresponds to bisimilarity of bigraphs. At the end, we explore several directions for further work.
3
CONTENTS
PAGE
Part I : Illustrations and Mathematical Framework 1 2 3 4 5 Introduction Bigraphs in action Precategories and relative pushouts Wide reactive systems Transition systems and bisimilarity
5 6 12 21 26 30 37 38 40 48 54 64 68 77 81 82 89 95 104 108 111
Part II : Bigraphical Reactive Systems 6 7 8 9 10 11 12 Pure bigraphs: de?nition Place graphs Link graphs Pure bigraphs: development Algebra of pure bigraphs Binding bigraphs Reactions and transitions
Part III : Specialisation and Application 13 14 15 16 Simple BRSs and adequacy Characterising basic BRSs Asynchronous pi calculus Further research directions
References Appendix
4
Part I
Illustrations and Mathematical Framework
The introduction to Part I provides a rationale for bigraphs, an account of the work that leads up to bigraphs, and a synopsis of the whole memorandum. We continue with illustrations of bigraphs themselves, how they may recon?gure, and how they correspond to process calculi. We then present the categorical framework in which the theory of bigraphs will be developed; this includes the notion of a wellsupported precategory and the properties of relative pushouts (RPOs). We introduce an abstract notion of dynamic system called a wide reactive system (WRS); it is not graphical, but gives prominence to spatial extension, or width as we shall call it. This allows us to develop important aspects of structure and behaviour, which we shall apply to BRSs in Part II. In particular a WRS has parametric reaction (rewriting) rules; in terms of these, we de?ne labelled transition systems for a wide range of WRSs and prove behavioural congruence theorems for them. Thus Part I provides a mathematical frame within which both BRSs (in Part II) and their applications (in Part III) can be developed.
5
x
y
K L
L K L
Figure 1: An example of a bigraph
1 Introduction
Bigraphical reactive systems (BRSs) [27, 28, 29, 20] are a graphical model of computation in which both locality and connectivity are prominent. Recognising the increasingly topographical quality of global computing, they take up the challenge to base all distributed computation on graphical structure. A typical bigraph is shown in Figure 1. Such a graph is recon?gurable, and its nodes (the ovals and circles) may represent a great variety of computational objects: a physical location, an administrative region, a data constructor, a π calculus input guard, an ambient, a cryptographic key, a message, a replicator, and so on. Bigraphs are a development of action calculi [25], but simpler. They use ideas from many sources: the Chemical Abstract machine (Cham) of Berry and Boudol [2], the π calculus of Milner, Parrow and Walker [30], the interaction nets of Lafont [21], the mobile ambients of Cardelli and Gordon [7], the explicit fusions of Gardner and Wischik [16] developed from the fusion calculus of Parrow and Victor [32], Nomadic Pict by Wojciechowski and Sewell [40], and the uniform approach to a behavioural theory for reactive systems of Leifer and Milner [23]. This memorandum is selfcontained; it builds on preliminary de?nitions and results put forward by Milner [28], but the approach here is a lot simpler and developed more fully. The theory of BRSs responds to twin challenges: from application, and from existing process theory. The former demands greater breadth of concepts, while the latter demands continuity of ideas. We now discuss these challenges separately.
6
The challenge from applications
The longterm aim of this work is to provide a model of computation on a global scale, as represented by the Internet and the Worldwide Web. The aim is not just to build a mathematical model in which we can analyse systems that already exist. Beyond that, we seek a theory to guide the speci?cation, design and programming of these systems, to guide future adaptations of them, and not to deteriorate when these adaptations are implemented. There is much talk of the vanishing ubiquitous computer of the future, which will obtrude less and less visibly in our lives, but will pervade them more and more. Technology will enable us to create this. To speak crudely, we must make sure that we understand it before it vanishes. This will only be achieved if we can reverse the typical order of events, in which design and implementation come ?rst, modelling later (or never). For example, a programming language is rarely based thoroughly upon a theoretical model. This has inevitably meant that our initial understanding of designed systems is brittle, and deteriorates seriously as they are adapted. We believe that the only acceptable solution, in the long run, is for system designs to be expressed with the concepts and notations of a theory rich enough to admit all that the designers wish. The arrival of ubiquitous mobile computing provides an opportunity for this, simply because it is new enough for its languages and implementation techniques not to be entrenched. Another reason is that concurrency theorists have anticipated mobility and have some structures to offer for new languages. Thus designers and analysts may come to speak the same tongue. For example the π calculus model is beginning to be adopted by business process management to provide languages and analytical tools for business processes with mobile structure [39]. Whatever our optimism, we cannot expect to arrive immediately at the right model. Initially we have to strike a compromise between incremental development of existing ideas on the one hand, and making too large a leap on the other hand. For if a model is to be seriously used in design, then it must be somewhat complex; it must grasp enough of the complexity of real systems to allow us to assess whether we are on the right track. If we tackle each aspect of global computation in isolation from the others we may develop an elegant theory, but it may not survive when other aspects are taken into account. Yet to tackle all aspects at once will defeat us. So our strategy here is to tackle just two aspects —mobile connectivity and mobile locality— simultaneously. In fact this combination contains a novel challenge: to what extent in a model should connectivity and locality be interdependent? In plain words, does where you are affect whom you can talk to? To a user of the Internet there is total independence, and we want to model the Internet at a high level, in the way it appears to users. But to the engineer these remote communications are not atomic, but represented by chains of interactions between neighbours, and we should also provide a lowlevel model which re?ects this reality. So we want to have it both ways; furthermore, we want to be able to describe rigorously how the highlevel model is realised by the lowlevel one. Of these two models, the lowlevel is the less novel. Indeed, von Neumann’s cellular automata are the original paradigm for it; his agents were arranged on a ?xed rectangular grid and interaction could only occur between neighbours. But in such a 7
model we can realise a higherlevel one in which a single agent is represented by different cells at different moments, and may send messages to other distant agents. So the challenge we address here is to provide the means to make locality and connectivity as dependent —or independent— as you wish. This seems to require new mathematical structures, and bigraphs represent our attempt to provide them. In de?ning the bigraph model we are concerned not to ignore familiar calculi of mobile processes, which deal with interaction and mobility in a variety of different ways. Instead, we want a theory that can be specialised to each of these calculi, and therefore uni?es them. This leads naturally to the second of our twin challenges.
The challenge from process theory
Existing process calculi have made great progress with interconnected concurrent processes [4, 1, 18, 26], with processes having mobile connectivity [30, 13] and with processes having notions of spatial location and mobility [2, 7]. There is some agreement among all these approaches, both in their basic notions and in their theories; perhaps the strongest feature is a good understanding of behavioural speci?cation and equivalence. At the same time the space of possible calculi is large, we lack a uniform development of their theories, and there is no settled way to combine their various kinds of mobility. In particular, as shown by Castellani’s [8] comprehensive survey, widely varying notions of locality have been explored. The bigraphical model aims at further generality both in the treatment of mobility and in behavioural theory. As far as mobility is concerned, its notion of spatial region is akin to the ambients of Cardelli and Gordon [7]; we ?nd that it supports both mobility in physical space (or in analogous organisational spaces, which may be virtual), and the dynamical control structures found in more traditional process calculi. The way this works is explained at some length, with examples, in Section 2. Here, we turn to the quest for a uniform behavioural theory. It is common to present the dynamics of processes by means of reactions (typia , where a and a are agents. In cally known as rewriting rules) of the form a the context of process calculi this treatment is typically re?ned somehow into labelled a , where the label is drawn from some vocabulary extransitions of the form a pressing the possible interactions between an agent and its environment. These transitions have the great advantage that they support the de?nition of behavioural preorders and equivalences, such as traces, failures and bisimilarity. But the extension to labelled transitions is tailored for each calculus. We therefore ask whether these labels can be derived uniformly from any given set of reaction rules of the form r r , where r is an agent that may change its state to r . A natural approach is to take the labels to be a certain class of (environmental) contexts; if L is such a context, the transition a L a implies that a reaction can occur in L ? a leading to a new state a . (As we shall see, bigraphical agents and contexts live in a category, or more generally a precategory, where the composition L ? a represents the insertion of agent a in context L.) Moreover, we would like to be sure that the behavioural relations —such as bisimilarity— that are determined by the transitions are indeed congruential, i.e. preserved by insertion into any surrounding environment.
8
But we don’t want all contexts as labels; as Sewell [37] points out, the behavioural equivalences that result from this choice are unsatisfactory. How to ?nd a satisfactory —and suitably minimal— set of labels, and to do it uniformly, remained an open problem for many years. As a ?rst step, Sewell [37] was able uniformly to derive satisfactory contextlabelled transitions for parametric termrewriting systems with parallel composition and blocking, and showed bisimilarity to be a congruence. It remained a problem to do it for reactive systems dealing with connectivity, which presents extra dif?culty. Recently Leifer and Milner [23] were able to de?ne minimal labels in terms of the categorical notion of relative pushout (RPO), and moreover to ensure that behavioural equivalence is a congruence for a wide class of reactive systems. These results were extended and re?ned in Leifer’s PhD Dissertation [22], and Cattani et al [9] applied this theory to action graphs with rich connectivity. Meanwhile, Milner developed the bigraph model from action graphs, with inspiration from the mobile ambients of Cardelli and Gordon. The development was driven by the simplicity that comes from treating locality and connectivity independently, and was also inspired by Gardner’s development [15] of symmetric action graphs (i.e. undirected edges). In this memorandum, the technical thrust is towards a theory of bigraphs in which behaviour is uniformly represented by RPObased transitions. The reader will soon see that, with this purpose in mind, several different paths could have been taken. We could therefore have proceeded more slowly, analysing each different option and its implications. Instead, we chose to follow one path far enough to provide evidence that a bigraphical approach will work; we have aimed at a point at which we can, within the new theory, recover some of the successes of existing theories such as the π calculus. At the same time, we have tried to make it easier to explore different paths by dividing the theory —wherever possible— into independent topics. For example, bigraphs themselves are de?ned in terms of two independent structures, place graphs and link graphs, and each of these can be varied. Also, bigraphical reactive systems (BRSs) are de?ned as merely one instance of a general concept, wide reactive systems (WRSs), whose abstract theory we ?rst develop; many other instances are possible. Thus, making reasonable choices (which can be reexamined), we have taken the theory far enough to be able to set up within it a version of the π calculus. Our main example is a ?nite asynchronous π calculus, for which —as one member of a broad class— we are able to derive a transition system that corresponds closely to that de?ned in the classical approach; indeed, structural congruence in this π calculus turns out to be represented by equality of bigraphs, and exactly the same bisimilarity congruence is achieved. In deriving this system we de?ne general tools for the re?nement of contextual transition systems, and comment on how we may tackle richer calculi, including ambient calculi, with the same approach.
Related work
We now turn to related work by other researchers, apart from those already mentioned. The longest tradition in graph recon?guration —often called graphrewriting— is based upon the double pushout (DPO) construction originated by Ehrig [11]. Our use of (relative) pushouts to derive transitions is quite distinct from the DPO construction, whose purpose is to explain the anatomy of graphrewriting rules (not labelled 9
transitions) working in a category of graph embeddings with graphs as objects and embeddings as arrows. This contrasts with our contextual (pre)categories, where objects are interfaces and arrows are bigraphs. But there are links between these formulations, both via cospans [14] and via a categorical isomorphism between graph embeddings and a coslice over our contextual (pre)categories [9]. Ehrig [12] has recently investigated these links further, after discussion with the second author, and we believe that useful crossfertilisation is possible. In the paper just cited, Gadducci, Heckel and Llabr? es Segura [14] represent graphrewriting by 2categories, whose 2cells correspond to our reactions. Another use of 2categories is by Sassone and Sobocinski [36]; they present an alternative way of deriving congruential bisimilarities in which 2categories replace our precategories. This correspondence is under ongoing discussion; it appears to be very close. Thus the 2categories will link our theory more closely to categorytheoretic standards, while the corresponding precategories may continue to provide ease of manipulation. Several other formulations of graph recon?guration employ hypergraphs, for example Hirsch and Montanari [17]. In their model the hypergraphs are not nested, as bigraphs are; rewriting rules may replace a hyperedge by an arbitrary graph. Drewes, Hoffmann and Plump [10] deal with hierarchical graphs, but their links do not join graphs at different levels.
Synopsis
Part I In Section 2, as an illustration of bigraphs in action, it is shown how the dynamics of the π calculus and (in less detail) the ambient calculus can be modelled in bigraphs. Then Section 3 sets up our categorytheoretic framework, including the notion of relative pushout (RPO); in particular it introduces supported precategories, building upon work in Leifer’s PhD thesis. Roughly speaking, in a precategory whose arrows are graphs or syntactic entities, support is a way of identifying each occurrence of a node or a subterm. Supported precategories are then enriched to wide precategories, suitable for representing systems with distributed regions. On this basis, Section 4 de?nes the notion of wide reactive systems (WRS), equipped with parametric reaction rules; these are well illustrated by the examples of Section 2, even though we do not formulate bigraphs explicitly in Part I. Section 5 shows how a (labelled) transition system (TS) can be uniformly derived in any WRS, using RPOs and their closely associated idem pushouts (IPOs), which are a kind of weak pushout. It also adapts the work of Leifer and Milner [23] to show that bisimilarity in such a TS with suf?cient RPOs must be congruential. Using WRS functors (de?ned in Section 4), it is seen that these TSs and their congruential bisimilarities can be transmitted from one WRS to another, along a functor that is suf?ciently wellbehaved. One wellbehaved functor is the support quotient, which forgets the identity of nodes and subterms. The ?nal topic in Part I is the notion of an adequate subTS; it allows a TS to be reduced while leaving bisimilarity unchanged. This will be important in Part III, to make certain applications tractable.
10
Part II In Section 6 the notion of a pure bigraph is formally de?ned in terms of its two constituents: a place graph and a link graph. These two notions, dealing respectively with locality and connectivity, are developed in Sections 7 and 8. In each of these two sections the crucial results are the theorem that RPOs always exist, and the characterisation of all the IPOs for a given pair of arrows. In Section 9 the static theory of bigraphs is developed. A pure bigraph is an arrow in a supported precategory whose objects are interfaces; each interface consists of places for the place graphs and points for the link graphs. Several structural properties are introduced, especially RPOs and IPOs — whose characterisation is already provided by that for place graphs and link graphs respectively. The section provides a taxonomy of bigraphs, including the notions of ion, atom and molecule which are based upon a single control node. It also de?nes forms of parallel product close to the parallel composition operators of familiar process calculi. The algebra of pure bigraphs is axiomatised and proved complete in Section 10. (This section is not required for any subsequent section.) In Section 11 pure bigraphs are enriched to binding bigraphs by adding binding names, along lines already set out in [28]. This relaxes the independency between placing and linking, by allowing certain names to have scope. The precategory of binding bigraphs has enriched interfaces, and its arrows are de?ned in terms of underlying pure bigraphs. Thus there is a forgetful functor from binding to pure bigraphs; the RPO theory for binding bigraphs is derived via this functor. Finally in Section 11, with the addition of reaction rules, the central notion of a bigraphical reactive system (BRS) is de?ned. A BRS is seen to be a special case of WRS, as de?ned in Part I. Furthermore, because bigraphs have RPOs, the congruence results from Part I immediately apply. The work of Part I also tranfers these results to abstract BRSs, which are those most closely related to process calculi. It is shown that RPOs do not exist in abstract BRSs; that is why concrete BRSs —and indeed concrete WRSs and supported precategories— were introduced. Part III In Section 13 the class of simple BRSs is introduced. These BRSs include models of both the π calculus and the mobile ambient calculus. Their structural properties also ensure adequacy of a certain subTS, namely the engaged transitions; this eases the task of modelling the calculi mentioned. Section 14 narrows the class of BRSs still further, to the basic ones. The purpose of this is to obtain a nice characterisation of the labels involved in modelling the asynchronous π calculus; moreover we believe that a slight widening of the class of basic BRSs will embrace both the full π calculus and mobile ambients. In Section 15 this characterisation is specialised to a ?nite asynchronous π calculus. It is then proved that the bisimilarity induced by this representation coincides with two standard congruences, strong bisimilarity and strong barbed bisimilarity. This provides the technical detail for work already presented by the authors at a conference [20]. It justi?es the claim that bigraphical systems are consistent with previous work in process calculi, which has been one of the main purposes of the work reported here. Finally, Section 16 explores several lines for further research.
11
2 Bigraphs in action
We introduce bigraphs informally, with examples showing the kinds of system that they represent, and the kind of mobility that they model. We also illustrate a simple term language for describing bigraphs. The examples allow us to explain how locality and connectivity cooperate; they also help to understand how bigraphs are naturally treated as arrows in a (pre)category whose objects are a simple kind of interface. Figure 1 shows an uninterpreted example of a bigraph. It has nodes that support two kinds of structure; hence the term ‘bigraph’. First, nodes may occur inside other nodes, so a bigraph has depth; since a node represents locality we call this nesting structure of a bigraph its place graph. Second, nodes have ports that may be connected by links, represented here by thin lines which may fork; we call this linked structure of a bigraph, which is independent of locality, its link graph. To each node is assigned a control, such as K or L, which tells us what kind of node it is. Each control has an arity, a ?nite ordinal; for example, L has arity three, so each Lnode has an ordered set of three ports, at each of which a link may impinge. It may impinge either from inside or from outside the node. The diagram also shows the use of names x and y ; such names allow a bigraph to be linked into larger bigraph. The place graph and the link graph share a node set, but are otherwise independent structures. The dynamics of bigraphs, i.e. the recon?gurations that may occur, depend upon both structural components; they are determined by one or more reaction rules. Each such rule has a redex and a reactum. The redex is a precondition for a reaction, represented by a pattern of nesting and linkage; the reactum is a postcondition indicating how the reaction will change that pattern. The places at which reactions may occur are determined by the controls. A control K may be speci?ed as atomic, meaning that nothing may be nested within a Knode; if nonatomic it may also be speci?ed as active, meaning that reactions may occur within a Knode. On the other hand if K is nonatomic but passive, then a Knode must be destroyed before its inhabitant nodes can react. We now give some typical reaction rules. A reaction consists of the replacement of a redex occurring in a bigraph by the corresponding reactum; we shall see later how the notion of ‘occurrence’ is represented in a precategory of bigraphs. Example 1 (reaction in the π calculus) Our ?rst example (Figure 2) represents the familiar reaction rule of the asynchronous π calculus (without summation) xy  x(z ).P {y /z }P .
To present this reaction rule in terms of bigraphs we need two controls send and get, both with arity two. Recall that in the asynchronous π calculus there are no output guards xy.(?) and reaction is forbidden inside the input guard x(z ).(?); to match this we declare send atomic, and get nonatomic but inactive. The redex R of Figure 2 illustrates a feature of bigraphs that is absent in Figure 1; the notion of a hole — the grey box. This is a place where another bigraph may be inserted. Arcs may impinge at points upon the hole, which we call inner names of R; when another bigraph is inserted, its (outer) names are fused with these inner names. The inner names and ports in a bigraph are collectively called its points. A link may 12
y
x
y
x
R send get send xy  get x(z ) z
R
x y
Figure 2: Reaction rule for the asynchronous π calculus connect an arbitrary number of points, and may also (but need not) be given an outer name. Here, the hole in R represents the parameter P of the π calculus rule; the port on the hole represents the name z bound in P . In fact, every bigraph is parametric in general; it has both an inner interface I with its parameter(s), and an outer interface J indicating the kind of hole(s) in which it, in turn, may be placed. We shall call I and J respectively the inner face and outer face of R. The precategory of bigraphs will have interfaces as objects and parametric bigraphs such as R : I → J as arrows. Interfaces will be triples of the form I = m, k, X , where m is a width (i.e. the number of sites represented by I ), k is a vector of length m indicating how many local names are associated with each site, and X is a set of global names. In the present case R has an inner face I = 1, (1), ? ; the width 1 tells us that there is only one hole in R, the singleton vector (1) tells us that this hole has one local name (corresponding to z in the π calculus rule) associated with it, and the third component tells us that there are no global names involved at the inner face. Note that if I is an inner face of a bigraph R, as here, then its names (local or global) are the inner names of R. The outer face of R is J = 1, (0), {xy } ; again, the width is 1, telling us that R will occupy just one hole in some outer bigraph. The third component indicates that J has two global names x and y , also called global (outer) names of R. In a bigraph, both (outer) names and ports can be binding. Here R has only free names; if it had a binding name then this would be a local name of the outer face J . Dually, a local inner name of the inner face I corresponds to a binding name of any parameter. (The parameter in this example really corresponds to the π calculus abstraction (z ).P .) We represent a binding occurrence of a point by a small circle; note that a port —such as the second port of get— may be binding, which means that it may only be connected to ports inside the node. The reactum R : I → J has the same inner face I as R, because the parameter persists through the reaction; it also has the same outer face J so that it may replace R in some outer context. The substitution {y /z } in the π calculus rule is represented just by an arc. The name x is unattached in R , because the two nodes have been discarded. 13
y
x
y
x
R send !get send xy  !get x(z ) z
R
!get y  !get x(z ) z
Figure 3: Reaction rule for input replication in the asynchronous π calculus Turning to the term language, note how a local name (here z ) is written in parentheses. Local names may be changed by alphaconversion. Holes are squares. Note especially that the operation of juxtaposing two bigraphs, linking any edges with a name in common, is represented in a term by parallel composition ‘  ’. The occurrence of x in the reactum R = x  y means that x, though unused, is part of the outer face of R . Thus the correspondence between terms and bigraphs is quite accurate. Example 2 (a π calculus reaction rule for replication) In the previous rule, the parameter P of the π calculus redex appears exactly once in the reactum; this is re?ected in the bigraphical rule by the single occurrence of a hole in the reactum R , and by the fact that R and R have the same inner face. But there is also a π calculus rule called replicated input: {y /z }P  !x(z ).P . xy  !x(z ).P
Here the parameter P is replicated; we can think of the input of y along x as triggering the creation of a copy of P to handle it. Figure 3 represents the rule bigraphically; note that it uses a different control !get, which is preserved in the reactum. Thus the reactum in this case has a different inner face of width two, namely R : I → J with I = 2, (1, 1), ? .
Example 3 (a π calculus reaction rule for summation) Figure 4 shows the communication rule for a π calculus with summation, (M + xy.P )  (N + x(z ).Q) → P  {y /z }Q , in which two of the parameters, M and N , are discarded. The controls send, get and sum are passive; this means that no reaction may occur inside nodes with these controls. Note that sum has arity 0; it serves to group together alternatives, only one of which will be enacted.
14
y
x y x
send
0
get
2
R
R
0 2
1
3
sum sum(send xy
0
sum 
1 )  sum(get x(z ) 2z

3)
x
0

2z
Figure 4: A reaction rule for the π calculus with summation
z
w
z
w
in
0
R
R
0 1
amb amb
1
amb amb
amb z (in w 
0)
 amb w
1
amb w(amb z
0

1)
Figure 5: Reaction rule for the ambient calculus
15
y
x
y
x
get send
R
R
send xy get x(z ) z
1 x
y
Figure 6: Global reaction rule for the π calculus Example 4 (reaction in the ambient calculus) In the ambient calculus of Cardelli and Gordon [7], one of the primitive forms of reaction is the movement of one ambient into another. Figure 5 shows how bigraphs may represent such a rule. We use two controls, each with arity one: amb for an ambient, and in for a ‘command’ to move its parent ambient somewhere else. We declare in to be atomic; on the other hand we declare amb to be nonatomic and active, since ambients are intended only to localize activity, not to inhibit it. The redex and reactum again have two global names z, w in their outer face, which has width 1; so this interface is J = 1, (0), {zw} . The inner face now has two sites, so has width 2, and no names (local or global) associated with either site; so it is I = 2, (0, 0), ? . The two parameters of this rule are, literally, passengers; their linkage (if any) plays no part in the reaction. However, as we shall see later, this does not prevent the two passengers —like passengers with mobile phones on a train— being linked to elsewhere, or even to each other. One can imagine interactions occurring between them independently of the occurrence of this ambient reaction. Our next example provides a possible instance of this. In the preceding examples the reactions permitted are all local. For example, the ambient reaction rule will permit the ambient named x to enter the ambient named y only if these two ambients are neighbours — i.e. not separated by any control boundaries. Similarly, the ?rst π calculus rule requires the send and get nodes to be neighbours. But we may want to have in a more permissive rule which will allow action at a distance; in the case of the π calculus this will mean that we can model the passing of a message in one step across arbitrarily many control boundaries. For this purpose the sender and receiver must be linked across region boundaries, as shown in the next example. Example 5 (global reaction in the π calculus) In the π calculus reaction rule of Example 3 the redex has width 1; this means that the rule applies only when the send and get molecules are colocated. To allow a context to place them apart, we need only 16
1: → I : I →I (xy ) xy : J → J
x
x y x y w y z
(x/x, y/y) : X → X (/x, w/y, w/z ) : {xyz } →{w} /z ? (z /x, z /y) : X →
x
y
( Interfaces: I = 1, (0), ? , J = 1, (2), ? , X = {xy } ) Figure 7: Some simple bigraphs change the outer width of the redex and reactum to 2, shown in Figure 6; thus in this case we have R, R : 1, (1), ? → 2, (0, 0), {xy } . Note that, in the term language, we have used ‘ ’ rather that ‘  ’ for parallel composition; this combinator keeps regions separate but still merges links with a common global name. Such ‘wide’ reaction rules are interesting in the presence of one or more active controls, because they can be used to separate the components of a distributed redex but still allow it to react. We have already introduced amb as an example of an active control. Indeed, our categorical representation will allow us to insert a bigraph with arbitrarily many global names in the doublewidth hole of the ambient rule’s redex. In particular, we might insert an instance of the redex of our remote π calculus rule; by this means we would create two interwoven but independent redexes, such that neither reaction precludes the other. This is not an unlikely occurrence in the Internet, modelled at a suitable level of abstraction. In our illustrations of reaction rules we chose to stay close to familiar calculi. Beyond these, the possibilities range widely. For example, using a combination of active and passive controls, various forms of failure management can be modelled. This may include the inactivation of processes due to failure, the reporting of failures, recovery procedures, and the subsequent reactivation of inactivated processes. Our illustrations so far have emphasised dynamics. We should also realise that some bigraphs have no dynamic behaviour but are useful building blocks. Figure 7 shows six simple examples, together with the terms that denote them. On the left side, the ?rst is just a region containing nothing. Its inner face is the socalled origin , the simplest possible interface where everything is null, while its outer face is the simplest interface I of width 1. The second is the categorical identity at I . The third is again an identity at an interface J of width 1, but here the site has two local names. The three bigraphs on the right side of the ?gure will be called wirings; they have both interfaces of width 0, i.e. of the form 0, (), X , which we abbreviate to X (a set of names). Their function is to link global inner and outer names in various patterns. The ?rst wiring is just the identity on an interface {xy }; think of it as the identity 17
substitution on these two names. The next involves a substitution of the name w for both the inner names y and z . This wiring also closes the inner name x; that is, when composed with another bigraph with name x, such as R in Example 3, it will remove x from the outer face. The last is an example of what Gardner and Wischik [16] call a fusion. It is like a substitution of z for x and y , but it also closes z . This concludes our illustration of bigraphs. Our main purpose was to show how they can represent the dynamics of process calculi; we have also seen that even simple things like name closure and substitution are bigraphs. We wrote each bigraph as a term in a language that we shall not formalise here (this will be done in future work). These terms are a mildly sugared form of mathematical constructions that we shall introduce in later parts of the paper; we have shown them here to indicate that bigraphs are not far from a programming language — in which a programmer can de?ne a wide variety of specialised reaction rules.
Discussion
By means of several examples we have informally introduced what we shall call, in Part II, a bigraphical reactive system (BRS). Each BRS is based upon a precategory of agents and contexts built according to a signature that de?nes controls and their static properties, and a set of reaction rules that de?nes dynamics. The bigraphical theory of Part II will begin with a direct formulation of bigraphs, in the classical tradition of graph theory. As we have said, bigraphs will be the arrows of a precategory whose objects are interfaces. The reader may ask why we go to the trouble of a graphical formulation, when —as we have illustrated in our examples— there is a rather pleasant algebraic formulation of them. Can we not develop this algebraic theory, and then consider bigraphs as just an alternative presentation of its elements? There are two reasons for taking the graphs as primary. The ?rst is that the space of mobile computing that we want to model has a strong topographical character — whether the topography is real or virtual— and it is reasonable to seek to model this directly. The second reason is theoretically deeper. One of our main goals is to build a theory of dynamic systems embracing as much as possible of the behavioural theory embodied in process calculi. This is often based upon a (labelled) transition system, and we wish to apply the theory originated by Leifer and Milner [23], which de?nes such transition systems in terms of socalled relative pushouts (a weak form of pushout); this ensures that the resulting behavioural equivalences are congruential — provided that suf?cient relative pushouts (RPOs) exist in the appropriate precategory of agents and contexts. But it turns out that neither the algebraic theory of bigraphs, nor their straightforward presentation as a category, possesses RPOs. This is because they do not cater for the notion of occurrence of one bigraph in another; they represent only abstract bigraphs, where the identity of nodes is absent. By moving to concrete bigraphs —formulated as a precategory rather than a category— we regain enough structure for the RPO theory to work, and can thereby gain a congruential behavioural theory. Fortunately, when we quotient this theory to recover a category of abstract bigraphs, the quotiented behavioural theory is still congruential, and we thereby derive a uniform 18
bigraph G : 3, X → 2, Y
y0 r0 v0 v1 y1 v2 r1
X = {x0 , x1 , . . .} Y = {y0 , y1 , . . .} y2
s2 s0 s1 v3
x0
x1
place graph GP : 3 → 2
roots . . . . . . v0 v2 v1 sites . . . s0 v3 r0 r1
names . . . y0
link graph GL : X → Y
y1 v2 v3 v1 y2
v0 inner names . . . . . . x0
s1
s2
x1
Figure 8: Resolving a pure bigraph into a place graph and a link graph approach to behaviour that can be instantiated for different process calculi. We shall formalise bigraphs directly in Part II. To manage their complexity we shall ?rst consider pure bigraphs, those that have no local names; then in a later section we introduce local names and binding and de?ne binding bigraphs. We represent a pure bigraph as a combination of two independent mathematical structures — a place graph and a link graph. Note that this combination is quite distinct from the categorical composition used to insert one bigraph into another (e.g. an agent into a context). But it is simply related to them; to compose two bigraphs categorically, we ?rst resolve them into their respective place graphs and link graphs, then compose these, and ?nally combine the results into a new bigraph. It is helpful to see an example in Figure 8 of how a pure bigraph G can be resolved into a place graph GP representing locality, and a link graph GL representing connectivity. (Controls are not shown in the diagram.) The nodes v0 , . . . , v3 are common to the two structures, which are otherwise independent. Note the bigraph’s double inter
19
faces 3, X → 2, Y ; there is no third component k here, because a pure bigraph has no local names. This interface combines the place graph interface 3 → 2 with the link graph interface X → Y ; nothing determines that the names y0 , y1 , y2 ‘belong’ to any particular region of the bigraph (= root of the place graph), nor that the inner names x0 , x1 ‘belong’ to any particular site. Let us repeat: in a pure bigraph G : m, X → n, Y we admit no association between the names Y and the roots (regions) n, nor between the inner names X and the sites m. It is this dissociation that enables us to treat locality and connectivity independently, yielding a tractable theory. This theory can then be extended rather easily to binding bigraphs. Part II ends with a section introducing the dynamic theory of bigraphs, and Part III goes on to specialise and apply this theory. But the foundation of this theory is laid in the abstract setting of wide reactive systems (WRSs), where the topographical element is reduced to a very simple categorical notion of width. The remainder of Part I is devoted entirely to these abstract dynamic systems.
20
3 Precategories and relative pushouts
In this section and the following one we develop a mathematical framework for the static and dynamic properties of bigraphs. There are several varieties of bigraph, and we wish to derive in an abstract setting as many de?nitions and properties as we can that will apply to all varieties. Sections 3 and 4 are an adaptation and extension of work started by Leifer and Milner [23], then further developed by Leifer in his PhD Dissertation [22] and by Milner [28]. These two sections closely follows Section 3 in the latter paper. The reader can perfectly well study Part II and beyond, independently of Sections 3 and 4, provided he or she is willing to take their main results on trust and to refer back to important de?nitions from time to time. The present section is concerned with the categorical framework and the important concepts, especially relative pushouts, that will underlie the treatment of dynamics in Section 4. Notation We shall always accent the name of a precategory, as in ?C. We use ‘ ? ’, ‘id’ and ‘?’ for composition, identity and tensor product. We denote the domain I and codomain J of an arrow f : I → J by dom(f ) and cod(f ); the set of arrows from I to J , called a homset, is denoted by ?C(I, J ). IdS will denote the identity function on a set S , and ?S the empty function from ? to S . We shall use S ∪ · T for union of sets S and T known or assumed to be disjoint, and f ∪ · g for union of functions whose domains are known or assumed to be disjoint. This use of ∪ · on sets should not be confused with the disjoint sum ‘+’, which disjoins sets before taking their union. We assume a ?xed representation of disjoint sums; for example, X + P + Y means ({0} × X ) ∪ ({1} × P ) ∪ ({2} × Y ), and v∈V Pv means v ∈V ({v } × Pv ). We write f S or R S for the restriction of a function f or relation R to the set S . A natural number m is often interpreted as a ?nite ordinal m = {0, 1, . . . , m ? 1}. We often use i to range over m; when m = 2 we use ? for the complement 1 ? i of i. We use x to denote a ?nite sequence {xi  i ∈ m}; when m = 2 this is an ordered pair. De?nition 3.1 (precategory, functor) A precategory ?C is de?ned exactly as a category, except that the composition of arrows is not always de?ned. Composition with the identities is always de?ned, and id ? f = f = f ? id. In the equation h ? (g ? f ) = (h ? g ) ? f , the two sides are either equal or both unde?ned. A subprecategory ?D of ?C is de?ned like a subcategory, with g ? f de?ned in ?D exactly when de?ned in ?C. A functor F : ?D → ?C between precategories is a total function on objects and on arrows that preserves identities and composition, in the sense that if g ? f is de?ned in ?D, then F (g ) ? F (f ) = F (g ? f ) in ?C. In general we shall use I, J, K, . . . to stand for objects and f, g, h, . . . for arrows. We shall extend categorytheoretic concepts to precategories without comment when they are unambiguous. One concept which we now extend explicitly is that of a monoidal category:
21
De?nition 3.2 (tensor product, monoidal precategory) A (strict, symmetric) monoidal precategory has a partial tensor product ? both on objects and on arrows. It has a unit object , called the origin, such that I ? = ? I = I for all I . Given I ? J and J ? I it also has a symmetry isomorphism γI,J : I ? J → J ? I . The tensor and symmetries satisfy the following equations when both sides exist: (1) (2) (3) (4) (5) f ? (g ? h) = (f ? g ) ? h (f1 ? g1 ) ? (f0 ? g0 ) = (f1 ? f0 ) ? (g1 ? g0 ) γI, = idI γJ,I ? γI,J = idI ?J γI,K ? (f ? g ) = (g ? f ) ? γH,J (for f : H → I, g : J → K ) .
‘Strict’ means that equation (1) holds exactly, as stated, not merely up to isomorphism; ‘symmetric’ refers to the symmetry isomorphisms satisfying equations (3)–(5). We shall omit ‘strict’ and ‘symmetric’ from now on, as we shall always assume these properties. Why do we wish to work in precategories? In the Introduction we pointed out that the dynamic theory of bigraphs will require the existence of relative pushouts (RPOs). This means that we need to develop the theory ?rst for concrete bigraphs, those in which nodes have identity; then we can transfer the results to abstract graphs by the quotient functor that forgets this identity. Precategories allow a direct presentation of concrete bigraphs; for we can stipulate that two bigraphs F and G may be composed to form H = G ? F only if their node sets are disjoint. We can think of this composition as as keeping track of nodes1 ; we can recover from H exactly which nodes come from F and which from G. More generally, we are interested in monoidal precategories where the de?nedness of composition and of tensor product depends upon a support set associated with each arrow. In bigraphs the support of an arrow will be its node set. In general we assume support to be drawn from some unspeci?ed in?nite set. We now give a general de?nition of precategories ?C with support; we continue to use this accented notation for them, dropping the accent only when we have a category. De?nition 3.3 (supported (monoidal) precategory) A precategory ?C is supported if it has: ? for each arrow f , a ?nite set f  called its support, such that idI  = ?. The composition g ? f is de?ned iff g ∩f  = ? and dom(g ) = cod(f ); then g ? f  = g  ∪ · f . ? for any arrow f : I → J and any injective map ρ whose domain includes f , an
1 Leifer’s development [22] (see Chapter 7) made use of a special category Track(?C) to keep track of nodes in a precategory ?C. This allowed the theory of RPOs to be developed for categories rather than for precategories. However, it can be developed more succinctly if we stay with the latter.
22
arrow ρ f : I → J called a support translation of f such that (1) (2) (3) (4) (5) (6) ρ idI = idI ρ (g ? f ) = ρ g ? ρ f Idf  f = f (ρ1 ? ρ0 ) f = ρ1 (ρ0 f ) ρ f = (ρ f ) f ρ f  = ρ(f ) .
If ?C is monoidal as a precategory, it is monoidal as a supported precategory if it also satis?es (7) ρ (f ? g ) = ρ f ? ρ g . Each of these seven equations is required to hold only when both sides are de?ned. Exercise Deduce condition (1) from conditions (5) and (3). We now consider functors between supported precategories. De?nition 3.4 (support equivalence, supported functor) Let ?A be a supported precategory. Two arrows f, g : I → J in ?A are supportequivalent, written f g , if ρ f = g for some support translation ρ. By De?nition 3.3(5) and (6) this is an equivalence relation. If ?B is another supported precategory, then a functor F : ?A → ?B is called supported if it preserves support equivalence, i.e. f g ? F (f ) F (g ). When we no longer need to keep track of support we may use a quotient category (not just precategory). To de?ne such quotients, we need the following notion:2 De?nition 3.5 (static congruence) Let ≡ be an equivalence de?ned on every homset of a supported precategory ?C. We say that ≡ is preserved by an operator ? if f ≡ f and g ≡ g imply f ? g ≡ f ? g whenever the latter are de?ned. Then ≡ is a static (monoidal) congruence on ?C whenever it is preserved by (tensor product and) composition. As an example of a simple static congruence on bigraphs, we may de?ne f ≡ f to mean that f and f are identical when all K nodes are discarded, for some particular control K . The most important example of a static congruence will be support equivalence ( ). But the following de?nition shows that any static congruence at least as coarse as support equivalence will yield a wellde?ned quotient category: De?nition 3.6 (quotient categories) Let ?C be a supported precategory, and let ≡ be a static congruence on ?C that includes support equivalence, i.e. ? ≡. Then the def quotient of ?C by ≡ is a category C = ?C/≡, whose objects are the objects of ?C and whose arrows are equivalence classes of arrows in ?C: C(I, J ) = { [f ]≡  f ∈ ?C(I, J ) } .
def
2 We use the term static congruence to emphasize that these congruences depend only on static structure, in contrast with behavioural congruences —like bisimilarity— that depend upon the dynamics of a system.
23
In C, identities and composition (and tensor product when ?C has it) are given by idm [f ]≡ ? [g ]≡ [f ]≡ ? [g ]≡ = def = def =
def
[idm ]≡ [f ? g ]≡ [f ? g ]≡ .
By assigning empty support to every arrow we may also regard C as a supported precategory, so that [·]≡ : ?C → C is a special supported functor called the ≡quotient functor for ?C. Note that the quotient does not affect objects; thus any tensor product on C may still be partial on objects. But composition is always wellde?ned in C because f ≡ g implies f g , and so also is tensor product provided it is de?ned on the domains and codomains. We often abbreviate [·] to [·]; we call it the support quotient functor. From the de?nition, clearly a coarser quotient [·]≡ exists whenever ≡ is the least equivalence that includes an arbitrary static congruence ≡ as well as support equivalence. In Parts II and III we shall de?ne two coarser quotient functors on bigraphs by this means. We now turn to the notion of relative pushout (RPO), which is of crucial importance in de?ning labelled transitions in the following section. Notation In what follows we shall frequently use f to denote a pair f0 , f1 of arrows in a precategory. If, for example, the two arrows share a domain H and have codomains I0 , I1 we write f : H → I . De?nition 3.7 (bound, consistent) If two arrows f : H → I share domain H , the pair g : I → K share codomain K and g0 ? f0 = g1 ? f1 , then we say that g is a bound for f . If f has any bound, then it is said to be consistent. De?nition 3.8 (relative pushout) In a precategory, let g : I → K be a bound for f : H → I . A bound for f relative to g is a triple (h, h) of arrows such that h is a bound for f and h ? hi = gi (i = 0, 1). We may call the triple a relative bound when g is understood. A relative pushout (RPO) for f relative to g is a relative bound (h, h) such that for any other relative bound (k, k ) there is a unique arrow j for which j ? hi = ki (i = 0, 1) and k ? j = h.
g0 h g1
g0 k0
h j h0
k
g1
h0 f0
h1 f1
k1 h1 f1
f0
24
We shall often omit the word ‘relative’; for example we may call (h, h) a bound (or RPO) for f to g . The more familiar notion, a pushout, is a bound h for f such that for any bound g there exists an h which makes the lefthand diagram commute. Thus a pushout is a least bound, while an RPO provides a minimal bound relative to a given bound g . In bigraphs we shall ?nd that RPOs exist in cases where there is no pushout; see the discussions following Constructions 7.11 and 8.12. Now suppose that we can create an RPO (h, h) for f to g ; what happens if we try to iterate the construction? More precisely, is there an RPO for f to h? The answer lies in the following important concept: De?nition 3.9 (idem pushout) In a precategory, if f : H → I is a pair of arrows with common domain, then a pair h : I → J is an idem pushout (IPO) for f if (h, idJ ) is an RPO for f to h. Then it turns out that the attempt to iterate the RPO construction will yield the same bound (up to isomorphism); intuitively, the minimal bound for f to any bound g is reached in just one step. This is a consequence of the ?rst two parts of the following proposition, which summarises the essential properties of RPOs and IPOs on which our work relies. They are proved for categories in Leifer’s Dissertation [22] (see also Leifer and Milner [23]), and the proofs can be routinely adapted for precategories. 3 Proposition 3.10 (properties of RPOs) In any precategory ?A: (1) If an RPO for f to g exists, then it is unique up to isomorphism. (2) If (h, h) is an RPO for f to g , then h is an IPO for f . (3) If h is an IPO for f , and an RPO exists for f to h ? h0 , h ? h1 , then the triple (h, h) is such an RPO. (4) (IPO pasting) Suppose that the diagram below commutes, and that f0 , g0 has an RPO to the pair h1 ? h0 , f2 ? g1 . Then – if the two squares are IPOs, so is the big rectangle; – if the big rectangle and the left square are IPOs, so is the right square.
h0 f0 g0 f1 g1 h1 f2
(5) (IPO sliding) If ?A is supported then IPOs are preserved by support translation; that is, if g is an IPO for f and ρ is any injective map whose domain includes the supports of f and g , then ρ g is an IPO for ρ f .
3 This adaptation works for the de?nition of precategory in De?nition 3.1, which is satis?ed by our supported precategories.
25
4 Wide reactive systems
We now introduce a kind of dynamical system, of which bigraphs will be an instance. This section adapts and extends the work of Section 3.3 in [28]. In previous work [23, 22] a notion of reactive system was de?ned. In our present terms, this consisted of a supported precategory whose arrows are called contexts, including agents whose domain is the origin , together with a set of agentpairs (r, r ) called reaction rules, and a subprecategory of socalled active contexts. The reaction between agents was taken to be the smallest such that D ? r D?r relation for every active context D and reaction rule (r, r ). For such systems we uniformly derived labelled transitions based upon IPOs. Several behavioural preorders and equivalences based upon these transitions —including bisimilarity— were shown to be congruences, subject to two conditions: ?rst, that suf?cient RPOs exist in the precategory; second, that decomposition preserves activity — i.e. D ? C active implies both C and D active. In subsequent work, suf?cient RPOs were found in interesting cases (Leifer [22], Cattani et al [9]). In each of these cases the condition that decomposition preserves activity is also met, if we limit attention to contexts with a single hole. However, certain derived transition systems are unsatisfactory under this limitation, as Sewell [37] has pointed out with examples. Also, as we saw in Section 1, we wish to consider multihole bigraphical contexts — not only to represent parametric reaction rules but also to accommodate multiple or ‘wide’ agents, as in the remote π calculus reaction rule in Example 5. There are other reasons for treating wide agents; for example, we would like to understand reactions that may occur between agents located arbitrarily far apart. This gives rise to the possibility of contexts in which some sites may be active, i.e. may permit reaction to occur, but not others. The following de?nitions allow this. They lead to wide reactive systems, which re?ne the above notion of reactive system as little as necessary for that purpose. We shall also see that, if we specialise this new treatment to narrow contexts (those with unit width), we recover the original notion of reactive system. In what follows we shall use Nat, the strict symmetric monoidal category whose objects are ?nite ordinals, and whose arrows are functions between them. De?nition 4.1 (wide precategory, wide functor) A wide precategory ?A is a supported precategory equipped with a functor width : ?A → Nat invariant under support translation, and a distinguished object called the origin such that width( ) = 0. Moreover, for each permutation π on the ordinal width(I ) there is an isomorphism πI : I → I in ?A with width(πI ) = π . If ?A —as a precategory— is monoidal with unit , and width preserves tensor product, then ?A equipped with and width is a wide monoidal precategory. The objects I, J, . . . of ?A are called interfaces, and its arrows A, B, . . . are called contexts. The set of contexts from I to J , called as usual the homset of the pair (I, J ), will be denoted by ?A(I, J ) or I → J . We call I and J the inner and outer faces of this def homset. Arrows in a homset Gr(I ) = → I are called ground arrows; we let lower case letters a, b, . . . range over these, and abbreviate a : → I to a : I .
26
A supported functor F : ?A → ?B is called wide if it preserves origin and width, i.e. (distinguishing elements of ?B by a prime) = F ( ) and width ? F = width. We shall de?ne bigraphs as a wide precategory in the next section. Meanwhile, from our discussion in Section 1 it is easy to see that, in bigraphs, ‘width’ is concerned only with locality, not with connectivity; the width of a bigraphical interface I = m, k, X is just its multiplicity m, and the width of a bigraph G : m, k, X → n, , Y is the function mapping each site s ∈ m to the unique region r ∈ n that contains s. We here de?ne width at the abstract level of wide precategories, but when specialised to bigraphs it will allow us to de?ne exactly which sites of a bigraph permit reaction. The notion of location will help us to formulate this: De?nition 4.2 (location) A location of an interface I with width m is a subset λ ? m. We denote by loc(I ) the set of locations of I , i.e. the powerset of width(I ). def The width function of a context C : I → J is extended to loc(I ) by width(C )(λ) = def {width(C )(i)  i ∈ λ}. The offset of λ by n is given by n λ = {n + i  i ∈ λ}. We are now ready to consider how to add dynamics to wide precategories. We shall de?ne a reaction relation over ground arrows. At the start of this section we spoke of reaction rules of the form (r, r ), a pair of agents (redex and reactum) in the same homset. This does not re?ect our examples of reaction rules in the introduction, which were all parametric; they were pairs of the form (R : I → J, R : I → J )
with, in general, different inner faces I and I . The parameter for such a rule will be a ground arrow in Gr(I ). In general the reactum R will be composed with a transform of this parameter, in Gr(I ). This is illustrated by Example 2, the replication rule which duplicates its parameter, and by Example 3 which discards parts of a parameter (which may of course have arbitrary width). So the following de?nition allows rules that arbitrarily transform their parameters. It also allows for the possibility that parameters are constrained to lie in some subset of Gr(I ). Remarkably, the congruence theorem of this section holds without any constraint upon either the parameter set or the nature of parameter transformations. Finally, since reactions are supposed to occur only in contexts that are active, the following de?nition introduces an activity map to determine the sites at which each context is active, and how this activity is treated by composition; this map is further explained in the discussion that follows the de?nition. De?nition 4.3 (wide reactive system) A wide reactive system (WRS) is a wide precategory ?A equipped with a triple (Par, Reacts, act), where ? For each I , the set Par(I ) ? Gr(I ) represents the parameters of reaction rules.
? Reacts is a set of reaction rules of the form (R, R , trans), with redex R : I → J , reactum R : I → J and transform map trans : Par(I ) → Gr(I ).
27
? For each I, J the activity map act : ?A(I, J ) → loc(I ) satis?es two properties: (1) (2) act(idI ) = width(I ) ?1 act(D ? C ) = act(C ) ∩ width(C ) (act(D)) .
We require that Par(I ) and Reacts are closed under support translation, that each trans preserves it, and that act respects it. We say C is active at i if i ∈ act(C ); similarly C is active at λ if λ ? act(C ), and C is active if act(C ) = width(dom(C )). over ground arrows is de?ned as follows: g g The reaction relation iff there exist a reaction rule (R, R , trans), an active4 context D and a parameter d ∈ Par(I ) such that g = D ? R ? d and g = D ? R ? d , where D D and d trans(d). For a monoidal WRS we require a third condition on act: (3) act(C ? D) = act(C ) ∪ · (width(dom(C )) act(D)) .
We shall usually denote this WRS just by ?A. Let us explain the activity conditions more fully. Condition (2) asserts that D ? C is active at i iff C is active at i and D is active at width(C )(i). If width(dom(C )) = m then condition (3) asserts that C ? D is active at i iff either i < m and C is active at i or i ≥ m and D is active at i ? m. We leave it to the reader to check that these conditions make sense — i.e. that they are consistent with the equations governing composition and tensor product. In passing, suppose that we are only concerned with reaction in contexts D that have interfaces of unit width 1 = {0}, so that width(D)(0) = 0. Then D is active iff it is active at 0. Conditions (1) and (2) then amount to requiring that the active contexts form a subprecategory closed under decomposition. Thus, as promised, we have a proper generalisation of the conditions under which the original congruence theorems [22, 23] were proved. De?nition 4.3 ensures that all its ingredients are closed under support equivalence, allowing us in De?nition 4.7 to divide ?A by , forming a quotient WRS. The following is immediate: Proposition 4.4 (support translation of reactions) Reaction in a WRS is closed ung then h h. der support equivalence, i.e. if g h, g h and g A natural notion of functor F : ?A → ?B between WRSs is one that preserves reaction. What this means is that all the ingredients that constitute a reaction in ?B must be at least as generous as in ?A. The de?nition is as follows: De?nition 4.5 (WRS functor, subWRS) Let ?A and ?B be wide reactive systems. A wide functor F : ?A → ?B of wide precategories is a WRS functor from ?A to ?B if it
4 Our de?nition requires D to be active at the whole width n of the codomain of the redex R. An alternative, more re?ned, approach is to equip a reaction rule with a fourth component λ, a location in n; then we can require only that D be active at λ, not at the whole of n. One can imagine reaction rules, like the one in Example 5 of width two, where we might wish only one part of the redex to lie at an active site. Everything that follows can be adapted to this re?nement; we avoid it here only for the sake of simplicity.
28
preserves the extra components of a WRS, i.e. (distinguishing the components of ?B by a prime): d ∈ Par(I ) ? F (d) ∈ Par (F (I )) (R, R , trans) ∈ Reacts ? (F (R), F (R ), trans ) ∈ Reacts where F ? trans = trans ? F act(C ) ? act (F (C )) . Call F monoidal if both ?A and ?B are monoidal and F preserves tensor product. If F is a (monoidal) inclusion functor then we call ?A a (monoidal) subWRS of ?B. Proposition 4.6 (WRS functors preserve reaction) A WRS functor F : ?A → ?B preg in ?A then F (g ) F (g ) in ?B. serves reaction, i.e. if g Clearly WRSs and their functors form a category. An important example of a functor is the support quotient functor, extended to WRSs as follows: De?nition 4.7 (quotient WRS) Let ?A be a wide reactive system. Then its support quotient wide reactive system is based upon the support quotient A = ?A/ , with other ingredients de?ned as follows: ? the parameters are [d], for each parameter d in ?A ? the reaction rules are ([R], [R ], trans), for each rule (R, R , trans) in ?A, where def in A we de?ne trans([d]) = [trans(d)] ? the active sites are given by act([D]) = act(D). Proposition 4.8 (quotient re?ects reaction) The support quotient functor [·] : ?A → A both preserves and re?ects reaction, i.e. [g ] [g ] in A iff g g in ?A. The quotient functor takes a concrete WRS, based on a precategory, to an abstract WRS based upon a category. In the next section we show how to obtain a behavioural congruence for an arbitrary concrete WRS ?A with suf?cient RPOs. The support quotient A of ?A may not possess RPOs, but nevertheless the quotient functor allows us to derive a behavioural congruence for A also. This use of a concrete WRS with RPOs to supply a behavioural congruence for the corresponding abstract WRS was ?rst represented by the functorial reactive systems of Leifer’s thesis [22].
def
29
5 Wide transition systems
We now consider how to equip a WRS with a labelled transition system. This will comprise a subset of the ground arrows, called agents, together with a set of transitions of a form such as a L a , where a, a are agents and L is a context with L ? a de?ned. Then bisimilarity is de?ned in the usual way, and we are interested in general conditions under which it will be a congruence. The de?nition of labelled transitions of Leifer and Milner [23] was as follows: a L a if there is a reaction rule (r, r ) and an active context D for which (L, D) is an idem pushout (IPO) for (a, r) and a = D ? r . We shall do something close to this, but with two re?nements. The ?rst re?nement is to equip a transition with information about locality. For an agent a : I , a transition of the form a L a tells us the extra context L : I → J needed by a to create a redex, but does not specify where this completed redex occurs within L ? a, i.e. at which location in J the reaction takes place. This makes a difference if J has more than unit width. It turns out that, to achieve congruence of bisimilarity, we must index each Ltransition by a location in the outer face of L. Let us illustrate this with a simple example involving bigraphs. We need only the super?cial understanding of bigraphs supplied by the introduction. Example 6 (noncongruence) This example shows that bisimilarity based upon unlo. cated transitions, which we denote by ?, is not in general a congruence for bigraphical systems. Take the signature K = {K, L, M}, each with arity zero; let K, L be atomic and M nonatomic but passive. Ports, names and links are irrelevant in this example, so we take interfaces to be just ?nite ordinals (widths). Now write K, L : 0 → 1 for agents with a single atomic node, and M : 1 → 1 for the elementary passive context consisting of a single Mnode. Let there be a single L in any active context. reaction rule (K, L); it allows the reaction K Consider the two agents a, b : 0 → 2 illustrated below, where a = K ? L and b = L ? K. They can each do a transition that turns K into L, i.e. we have a
id2
L ? L and b
id2
L?L.
Because these two transitions do not record the different places at which the reaction . occurs, it turns out that a ? b.
M
K
L
? L
.
K
M K
def
L
?
.
.
M L
K
a?b
.
C = M  id1
def
C ?a ? C ?b
.
Now put a and b in the context C = M  id1 : 2 → 1, as shown; then we ?nd C ? a ? C ? b. In C ? b the Knode is active, so there is a transition C ? b id1 ; but C ? a has no such transition since its Knode is passive. 30
Our second re?nement is concerned with the parametric nature of reaction. Each reaction is based on a redex R together with a parameter d. To re?ect this in transitions, we adopt pairlabels of the form L = (Lred , Lpar ), where Lred arises from the redex and Lpar from its parameter. In a pairlabel L we require the composition Lred ? Lpar to be de?ned, and indeed it represents the previous single label. Thus each transition will have an underlying pair of IPOs, not just a single IPO. For a pairlabel L, in expressions we shall usually write L to mean Lred ? Lpar . Also, for any equivalence ≡, we shall take L ≡ M to mean Lred ≡ M red and Lpar ≡ M par . None of the results in Part I and II appears to depend on the use of pairlabels; we adopt them mainly in anticipation of future work that may depend on them.5 For example it provides a starting point for relating our present work more closely to that of Sewell [37], in which labels themselves are parametric. With these two re?nements, we now de?ne transition systems. We allow for a broad class of transitions, within which we distinguish those based upon IPOs. Lpar a d R Lred D
De?nition 5.1 (transition) A transition consists of a quadruple written a L λ a , where a and a are ground, L is a pairlabel and there exist a reaction rule (R, R , trans), an active context D and a parameter d such that the above diagram commutes, and λ = width(D)(m) a = D ?R ?d where m = width(cod(R)) where D D and d trans(d) .
We say that the reaction rule and the diagram underlie the transition. A transition is minimal if the underlying diagram is an IPOpair. De?nition 5.2 (transition system) Given a WRS ?A, a (labelled) transition system L for ?A is a pair (Agi, Trans), where ? Agi is a set of interfaces called the agent interfaces; for I ∈ Agi, the members of Gr(I ) are called agents of L. ? Trans is a set of transitions whose sources and targets are agents of L. The full (resp. standard) transition system for a WRS consists of all interfaces, together with all (resp. all minimal) transitions. When the WRS concerned is understood we shall denote these two transition systems respectively by FT and ST. Let ≡ be a static congruence (De?nition 3.5) in a WRS equipped with L. Suppose that, for every transition a L λ a in L, if a ≡ b and L ≡ M —where M is another label of L with M ? b de?ned— then there exist an agent b and a transition b M λ b in L such that a ≡ b . Then ≡ and L are said to respect one another. We abbreviate ‘(labelled) transition system’ to TS. A TS M is a subTS of L, written M ? L, if its interfaces and transitions are included among those of L.
5 Indeed,
examples exist where the bisimilarity for single labels is strictly coarser than for pairlabels.
31
From now on we shall use ‘label’ to mean a pairlabel. Note that ‘respect’ is mutual between an equivalence and a TS, so that ‘L respects ≡ ’ means the same as ‘≡ respects L’; we shall use them interchangeably. Note that our de?nition of transition presupposes a set of reaction rules, i.e. an unlabelled transition relation. Sometimes —for example in CCS— labelled transition systems have been the primary means of providing process dynamics, and unlabelled transitions corresponded to transitions with a ‘null’ label (τ in CCS). But in this work we are committed to taking reaction rules as primary, because they can be described generally without any presupposition about the interaction discipline of each calculus. Returning brie?y to Example 6 we now see that the location component in transitions allows us to distinguish between the two agents a and b. In fact their only transitions take the respective forms a L {0} and b L {1} , where L = (id, id). We shall meet various different equivalences when we deal with bigraphical WRSs. For support equivalence ( ) we now deduce from Propositions 3.10(5) and 4.4 that: Proposition 5.3 (support translation of transitions) In any wide reactive system ?A, the full and standard transition systems respect support equivalence. The standard transition system ST is only useful when RPOs exist. Later we shall show how to derive from it a TS for the quotient WRS, which may not possess RPOs. But however transitions are de?ned or derived, we may de?ne behavioural equivalences and preorders in the usual way. Here we shall limit attention to strong bisimilarity. (Throughout this paper we shall omit ‘strong’ since we do not de?ne or use weak bisimilarity.) De?nition 5.4 (wide bisimilarity) Let ?A be a wide reactive system equipped with a TS L. A simulation (on L) is a binary relation S between agents with equal interface such that if aS b and a L λ a in L, then whenever L ? b is de?ned there exists b such that b L λ b in L and a S b . A bisimulation is a symmetric simulation. Then bisimilarity (on L), denoted by ?L , is the largest bisimulation (on L). We shall often omit ‘on L’, and write ? for ?L , when L is understood from the context. This will usually be when L is ST. Note the slight departure from the usual de?nition of bisimulation of Park [31]; here we must require L ? b to be de?ned. This is merely a technical detail, provided that the TS respects support translation; for then, whenever L ? a is de?ned there will always exist L L for which both L ? a and L ? b are de?ned. Moreover if the WRS is based on a category —in particular if it is a support quotient— then the sidecondition holds automatically; in this case the de?nition of bisimilarity reduces to the standard. We may now prove our main congruence theorem for WRSs. Its main point is that ST ensures bisimulation congruence. The reader can deduce the (perhaps more obvious!) result that FT ensures the same; simply replace the word ‘IPO’ by‘commuting square’ in the proof. Theorem 5.5 (congruence of wide bisimilarity) In a wide reactive system with RPOs, equipped with the standard transition system, wide bisimilarity of agents is a congruence; that is, if a0 ? a1 then C ? a0 ? C ? a1 . 32
M par
M red E E0 Lred D0 R0
J0
(a)
M
par
(b)
M
red
C
Lpar
C ? a0 d0
E0 R0
J0
a0 d0
M par
M red E E1
red
(c)
L a1 d1 R1
par
L
red
(d) C
L
par
L
D1
J1
a1 d1
D1 R1
J1
Proof The proof is along the lines of Theorem 3.9 in Leifer [22]. We establish the bisimulation def S = {(C ? a0 , C ? a1 )  a0 ? a1 , C any context} . Suppose that a0 ? a1 , and that C ? a0 M ? b0 , for some label M such that M ? C ? a1 is de?ned. It is enough to ?nd b1 such that C ? a1 M ? b1 and (b0 , b1 ) ∈ S . There exist a reaction rule (R0 , R0 , trans0 ) with outer face J0 , an active context E0 and a parameter d0 such that diagram (a) is an IPOpair; moreover if width(J0 ) = m0 then width(E0 )(m0 ) = ? and b0 = E0 ? R0 ? trans0 (d0 ). Then because consistent pairs have RPOs, there exists an RPO for (a0 , d0 ) relative to the given bound, and using Proposition 3.10(5) we can complete diagram (b) so that every square is an IPO. D0 is active at m0 by De?nition 4.3, so the lower squares represent a transition a0 L λ a0 , where λ = width(D0 )(m0 ) and a0 = D0 ? R0 ? trans0 (d0 ). Also E is active at λ. Since a0 ? a1 there is a transition a1 L λ a1 with a0 ? a1 . (Note that L ? a1 is de?ned, since M ? C ? a1 is de?ned and M ? C = E ? L.) So there exist a reaction rule (R1 , R1 , trans1 ) with outer face J1 , an active context D1 and a parameter d1 such that diagram (c) is an IPO pair; moreover width(D1 )(m0 ) = λ and a1 = D1 ? R1 ? trans1 (d1 ). Now replace the lower two squares of (b) by diagram (c), obtaining diagram (d) in def which, by Proposition 3.10(5), the large square is an IPO. Moreover E1 = E ? D1 is def active, since E is active at λ. Hence C ? a1 M ? b1 where b1 = E1 ? R1 ? trans1 (d1 ). Finally (b0 , b1 ) ∈ S as required, because b0 = E ? a0 and b1 = E ? a1 with a0 ? a1 . We shall henceforth often omit the adjective ‘wide’ when discussing bisimilarity. We should remark that we are taking (strong) bisimilarity as a representative of many preorders and equivalences; Leifer [22] has proved congruence theorems for several others, and we expect that those results can be transferred to the present setting. Now, if a WRS is equipped with a TS we can de?ne transitions for various quotient WRSs as follows:
33
De?nition 5.6 (transitions for quotient WRSs) Let ?A be a WRS equipped with a TS L, and let F : ?A → ?B be a WRS functor. We say that F respects L if the static congruence it induces on ?A respects L. The TS F (L) induced by F on ?B has the agent interface F (I ) whenever I is an agent interface of L, and whenever L has a transition a L λ a then F (L) has the transition F (a)
F (L) λ
F (a ) .
This de?nition always makes sense, but it will not always make bisimilarity a congruence in ?B, even if it is so in ?A. However, the next theorem tells us when this will be ensured. Recall that a full functor is surjective for each homset. Theorem 5.7 (transitions induced by functors) Let ?A be equipped with a TS L. Let F : ?A → ?B be a full WRS functor that is the identity on objects and respects L. Then the following hold for F (L): (1) a ? b in ?A iff F (a) ? F (b) in ?B. (2) If bisimilarity is a congruence in ?A then it is a congruence in ?B. (3) Both (1) and (2) hold when F = [·] : ?A → A, the support quotient functor. Proof (1) (?) We establish in ?B the bisimulation R = {(F (a), F (b))  a ? b} . Let a ? b in ?A, and let p = F (a), q = F (b) and p M λ p in ?B. Then by de?nition of the induced TS we can ?nd L and a such that M = F (L) and p = F (a ), and a L λ a in ?A with L ? b de?ned. So for some b we have b L λ b with a ? b . It follows that q M λ q in ?B, where q = F (b ) and (p , q ) ∈ R, so we are done. (1) (?) We establish in ?A the bisimulation S = {(a, b)  F (a) ? F (b)} . Let F (a) ? F (b) in ?B, and let p = F (a), q = F (b) where a L λ a in ?A with L ? b de?ned. Then p M λ p in ?B, where M = F (L) and p = F (a ). So for some q we have q M λ q with p ? q . This transition must arise from a transition b1 L1 λ b1 in ?A, where q = F (b1 ), M = F (L1 ) and q = F (b1 ). But then b1 ≡ b and L1 ≡ L, where ≡ is the equivalence induced by F ; we also have L ? b de?ned, and L respects ≡, so we can ?nd b for which b L λ b and b1 ≡ b . But also (a , b ) ∈ S so we are done. (2) Assume that bisimilarity in ?A is a congruence. In ?B, let p ? q and let G be a context with G ? p and G ? q de?ned. Then there exist a, b, C in ?A with p = F (a), q = F (b) and G = F (C ), and with C ? a and C ? b de?ned. From (1)(?) we have a ? b, hence by assumption C ? a ? C ? b. Applying the functor F we have from (1)(?) that G ? p ? G ? q in ?B, as required. (3) The result follows immediately from Proposition 5.3. 34
In a later section we shall set up bigraphical reactive systems as WRSs. Then, using the theorems we have just proved —or close analogues of them— we shall derive TS and deduce behavioural congruences for them. We now turn to a question that arises strongly in applications. Our standard TS, containing only the minimal transitions, is of course much smaller than the full TS. But it turns out that in particular cases we can reduce the standard TS still further, without affecting bisimilarity. We introduce here the basic concepts to make this idea precise, since they do not depend at all on the notion of bigraph. De?nition 5.8 (relative bisimulation, adequacy) Assume given a TS L, with a subTS M. A relative bisimulation for M (on L) is a symmetric relation S such that whenever aS b, then for every transition a L λ a in M, with L ? b de?ned, there exists b such that b L λ b in L and a S b . De?ne relative bisimilarity for M (on L), denoted by ?M L , to be the largest relative bisimulation for M (on L). We call M adequate (for L) if ?M L coincides with ?L on the agents of M; if M has interfaces I , we write this as ?M L = ?L I . When L is understood we may omit ‘on L’; equally we may write ?M for ?M L . Note that, for a ?M b , we require b only to match the transitions of a that lie in M , L and b’s matching transition need not lie in M. This means that relative bisimilarity is in general not transitive, so it is not in itself a behavioural equivalence. The value of relative bisimilarity lies in the case when M is adequate for L, for then the proof technique of relative bisimulation can relieve us of the task of checking a large class of transitions. Indeed it may be the case that fewer labels are employed in Mtransitions than in Ltransitions; then we only have to consider transitions involving this smaller set of labels. Even at this abstract level of WRSs, we can draw attention to possibilities for a transition system M adequate for L, in particular when L is ST. A simple example depends on the fact that ST is closed under isomorphism, i.e. if a L λ a is a transition of ST then so is ιa κLι λ κa for any isos ι and κ. (We are omitting ‘ ? ’ when composing with an iso.) Then when checking for bisimilarity with a given a, intuitively it should suf?ce to consider not every transition of a, but only one in every iso class. This holds more generally: Proposition 5.9 (representative transitions) Let L be a transition system closed under isomorphism, and let M ? L be a subTS. Suppose that, for every transition a L λ a in L, there is a transition a κL λ κa in M for some iso κ. Then M is adequate for L.
?1
M Proof We show that R = {(ιa, ιb)  a ?M L b} is an Lbisimulation. Let a ?L b, and let ιa L λ a in L. We must ?nd a matching Ltransition for ιb. Since isomorphism preserves transitions in L, there is an Ltransition a Lι λ a . def So by assumption there is an Mtransition a κLι λ a = κa . Since a ?M b there is an Ltransition b κLι λ b with a ?M b . Applying L L def L ?1 ?1 two isos, there is an Ltransition ιb b . But a = κ a , so (a , b ) ∈ R λb =κ and we are done.
35
We shall exploit this result in Section 15. A deeper example of adequacy arises from the intuition that the transitions that really matter are those where the agent ‘contributes’ to the underlying reaction, i.e. a supplies a ‘part’ of the redex R, leaving the label L to supply the rest. We can make this precise in terms of support: we are interested in transitions a whose underlying redex R is such that a ∩ R = ?. We call such transitions engaged. Intuitively, we may conjecture that the engaged transitions are adequate, for the standard TS. We shall later prove this for a particular class of bigraphical reactive systems, broad enough to include the π calculus and the ambient calculus. It is very nice when the conjecture holds, for it means that the only signi?cant labels L are those whose leading part Lred is strictly contained in some redex R. We now look at a rather wellbehaved kind of subTS. For arbitrary M ? L and any given pair (L, λ), it is possible that M contains some but not all of the (L, λ)transitions in L. But if this is not the case —i.e. if such pairs determine which transitions are in M— then the situation is somewhat simpler: De?nition 5.10 (de?nite subTS) Let M ? L. Call M de?nite for L if, for all pairs (L, λ) and all transitions of L a
L λ
a ∈ M iff b
L
λ
b ∈M.
Then immediately we deduce that a relative bisimilarity is an absolute one: Proposition 5.11 (de?nite subTS) If M is de?nite for L then ?M = ?M L . If M is de?nite and adequate for L, we can deduce an important corollary for later use. To illustrate it, suppose that L is the standard TS. If we are interested only in agents at I , and are able to establish that M with interfaces I is de?nite and adequate for L, then we can deduce congruence for bisimilarity on M. More generally: Corollary 5.12 (adequate congruence) Let M, with interfaces I , be de?nite and adequate for L. Then (1) The bisimilarities on M and L coincide at I , i.e. ?M = ?L I . (2) If ?L is a congruence, then ?M is a congruence; that is, for any C : I → J where I, J ∈ I , if a ?M b then C ? a ?M C ? b.
36
Part II
Bigraphical Reactive Systems
In Part II we begin by de?ning the notion of a pure bigraph formally, in terms of its two constituents: a place graph representing locality and a link graph representing connectivity. We continue by de?ning these two notions in turn, ensuring that they enjoy the categorical properties that we shall need. We then combine them, yielding a theory of pure bigraphs where locality and connectivity are totally independent. A short section is devoted to the algebraic theory of pure bigraphs, showing that they possess a simple complete axiomatisation. We proceed to relax the independence of locality and connectivity, in a controlled manner, in de?ning binding bigraphs; these allow certain local names to have a scope consisting of a particular bigraphical region. Properties of binding bigraphs are derived from those of the underlying pure ones. Finally we introduce dynamics, in the form of reaction rules, yielding bigraphical reactive systems (BRSs). These are shown to be a special case of WRSs. We therefore apply Part I to yield labelled transition systems and behavioural congruences, for both pure and binding BRSs.
37
6 Pure bigraphs: de?nition
In this section we de?ne the notion of pure bigraph formally, in terms of the constituent notions of place graph and link graph, which are dealt with in the following two sections. Then in Section 9 we resume the study of pure bigraphs, combining the properties of its constituents. In Section 10 we develop their algebraic theory. In Section 11 we de?ne a binding bigraphs as an enrichment of the pure ones; we ensure that they enjoy the properties that allow us to apply the theory developed in Part I. Finally, in Section 12 we give the central de?nition of a bigraphical reactive system (BRS) and study its dynamic behaviour; then we apply the results of Part I to derive labelled transitions and congruences for both pure and binding BRSs. De?nition 6.1 (pure signature) A (pure) signature K is a set whose elements are called controls. For each control K it provides a ?nite ordinal ar (K ), an arity; it also determines which controls are atomic, and which of the nonatomic controls are active. Controls which are not active (including the atomic controls) are called passive. Note that a signature need not be ?nite, or even denumerable. Thus a bigraph, though itself ?nite, may denote an element of a continuous state space. We shall not here exploit this possibility, but we comment further on it in Section 16. As we saw in Section 1 of Part I, a nonatomic node —one with a nonatomic control— may contain other nodes. A node’s control determines its ports, and if the control is active then reactions are permitted inside the node. A passive node —such as a getnode in the π calculus— can be thought of as a script, or program, awaiting activation; this must take the form of a reaction that destroys the node boundary. In re?nements of the theory a signature may carry further information, such as a sign and/or a type for each port. The sign may be used, for example, to enforce the restriction that each negative port is connected to exactly one positive port, as in action calculi [9, 25]. Another possible re?nement is a kind assigned to each node, determining the controls of the nodes it may contain. (Our atomic nodes already represent the most restrictive kind.) In Part III we shall de?ne an important re?nement that allows names to have scope, and controls to bind names. The theory of pure bigraphs, where names have no scope, is prerequisite to understanding all these re?nements. We begin by de?ning concrete bigraphs. The de?nition is ‘topdown’; here we de?ne a bigraph as the combination of two parts, and in the following sections we de?ne those parts themselves. De?nition 6.2 (concrete pure bigraph) A (concrete) pure bigraph over the signature K takes the form G = (V, E, ctrl , GP , GL ) : I → J where I = m, X and J = n, Y are its inner and outer faces, each combining a width (a ?nite ordinal) with a ?nite name set. Its ?rst two components V and E are ?nite sets of nodes and edges respectively. The third component ctrl : V → K, a control map, assigns a control to each node. The remaining two are: GP = (V, ctrl , prnt ) : m → n GL = (V, E, ctrl , link ) : X → Y a place graph a link graph .
Place graphs and link graphs are de?ned in De?nitions 7.1 and 8.1 respectively. 38
We refer to these as concrete bigraphs because their nodes and edges have identity. Thus we shall work with a supported precategory of bigraphs, because there we shall be able to ?nd RPOs. The support of a concrete bigraph consists of its nodes and edges; in terms of the de?nition, G = V + E . In Section 9 we shall take the quotient by support equivalence to obtain abstract bigraphs. As is usual in graph theory, we shall omit the adjectives ‘concrete’ and ‘abstract’ when they are unimportant or implied by the context. We shall normally work with a ?xed but unspeci?ed signature. We refer to G as the combination of its constituents GP and GL ; we write it as G = GP , GL . A place graph can be combined with a link graph iff they have the same node set and control map. In Section 9 we revisit bigraphs, developing their structure by combining attributes from their constituent place graphs and link graphs.
39
7 Place graphs
De?nition 7.1 (place graph) A place graph A = (V, ctrl , prnt ) : m → n has an inner width m and an outer width n, both ?nite ordinals; a ?nite set V of nodes with a control map ctrl : V → K; and a parent map prnt : m ∪ · V →V ∪ · n. The parent map is acyclic, i.e. prnt k (v ) = v for all k > 0 and v ∈ V . An atomic node —i.e. one whose control is atomic— may not be a parent. We write w >A w , or just w > w , to mean w = prnt k (w ) for some k > 0. The widths m and n index the sites and roots of A respectively. The sites and nodes —i.e. the domain of prnt — are called places. The acyclicity condition makes the parent map prnt represent a forest of n unordered trees. The sites and roots provide the means of composing the forests of two place graphs; each root of the ?rst is planted in a distinct site of the second. Figure 9 shows two simple examples of composition, B0 ? A0 and B1 ? A1 . Formally: De?nition 7.2 (precategory of place graphs) The precategory ?P LG has ?nite ordinals as objects and place graphs as arrows. The composition A1 ? A0 : m0 → m2 of two place graphs Ai = (Vi , ctrl i , prnt i ) : mi → mi+1 (i = 0, 1) is de?ned when def the two node sets are disjoint; then A1 ? A0 = (V, ctrl , prnt ) where V = V0 ∪ · V1 , · prnt 1 ) ? (prnt 0 ∪ · IdV1 ). The identity place ctrl = ctrl 0 ∪ · ctrl 1 , and prnt = (IdV0 ∪ def graph at m is idm = (?, ?K , Idm ) : m → m. It is easy to check that A ? id = A = id ? A, and that composition is associative. Note that ?P LG is supported, with node sets V as support. Here are some basic properties:
De?nition 7.3 (barren, sibling, active, passive) A node or root is barren if it has no children. Two places are siblings if they have the same parent. A site s of A is active if ctrl (v ) is active whenever v > s; otherwise s is passive. If s is active (resp. passive) in A, we also say that A is active (resp. passive) at s. When dealing with many place graphs A, B , . . . , instead of indexing their parent maps as prnt A , prnt B etc. we shall ?nd it more convenient to abuse notation and denote the parent map of a place graph A again by A. The context will prevent ambiguity; for example in B ? A we are talking of place graphs, while in B (A(v )) we are talking of their parent maps. Thus (B ? A)(v ) means the parent map of the composite place graph B ? A applied to the node v . Note especially that (B ? A)(v ) differs from B (A(v )); in fact if v ∈ VA then (B ? A)(v ) is equal to A(v ) if this is a node, otherwise equal to B (A(v )). Proposition 7.4 (isomorphisms in place graphs) An arrow ι : m → m in ?P LG is an isomorphism iff it has no nodes, and its parent map is a bijection. What is a suitable tensor product for ?P LG ? We do not want A ? B to have the effect of merging nodes from A and B . So we adopt a partial tensor product, with A ? B de?ned exactly when the node sets are disjoint, in which case its node set is VA ∪ · VB . Intuitively, the tensor product of two place graphs consists in placing them sidebyside. 40
De?nition 7.5 (tensor product) The tensor product ? in ?P LG is de?ned as follows: def On objects, we take m ? n = m + n. For two place graphs Ai : mi → ni (i = 0, 1) we take A0 ? A1 : m0 + m1 → n0 + n1 to be de?ned when A0 and A1 have disjoint node sets; for the parent map, we ?rst adjust the sites and roots of A1 by adding them to m0 and n0 respectively, then take the union of the two parent maps. Epimorphisms (epis) will play a central role, both for place graphs and for link graphs. Monomorphisms (monos) will also be used. Recall that in the category of sets with functions the epis and monos are the surjective and injective functions respectively. Here we ?nd something analogous: Proposition 7.6 (epis and monos in place graphs) In ?P LG , a place graph is an epi iff no root is barren; it is mono iff no two sites are siblings. We shall now prove that RPOs always exist in place graphs, and we show how to construct them. We ?rst give a simple intuition. Let D be a bound for A; we wish to build an RPO (B, B ) as shown in the diagram below. To form B , we ?rst truncate D by removing the roots, and all nodes not present in A. Then for the upper interface of B , we create a new parent (a root) for each place orphaned by the truncation, equating these new roots only when required so that B0 ? A0 = B1 ? A1 . Notation When considering a pair A : h → m of place graphs with common sites h, we shall adopt a convention for naming their nodes. We denote the node set of A i (i = 0, 1) by Vi , and denote V0 ∩ V1 by V2 . Recall that ? means 1 ? i for i ∈ 2. We shall use vi , vi , . . . to range over Vi (i = 0, 1, 2), and ri , ri to range over the roots mi (i = 0, 1). We shall also use w2 , w2 , . . . to range over h ∪ · V2 ; this is useful because shared sites behave just like shared nodes in our construction of pushouts. We shall now give a construction for RPOs in ?P LG . Construction 7.7 (RPOs in place graphs) An RPO (B : m → m, ? B: m ? → p), for a pair A : h → m of place graphs relative to a bound D : m → p, will be built in three stages. We use the notational conventions introduced above. p D0 B0 A0 B m ? B1 A1 D1
m0
m1
nodes: If Vi are the nodes of Ai (i = 0, 1) then the nodes of Di are V? \ V2 ∪ · V3 for some V3 . De?ne the nodes of Bi and B to be V? \ V2 (i = 0, 1) and V3 respectively. 41
interface: Construct the shared codomain m ? of B as follows. First, de?ne the roots in each mi that must be mapped into m ?: Next, on the disjoint sum m0 + m1 , de?ne ? = to be the smallest equivalence for which · V2 . Then (0, r0 ) ? = (1, r1 ) whenever A0 (w) = r0 and A1 (w) = r1 for some w ∈ h ∪ de?ne the codomain up to isomorphism: m ? = (m0 + m1 )/? =.
def
mi = {r ∈ mi  Di (r) ∈ V3 ∪ · p} .
def
parents: De?ne B0 to simulate D0 as far as possible (B1 is similar): For r ∈ m0 : For v ∈ V1 \ V2 : B0 (r) = B0 (v ) =
def def
For each r ∈ mi we denote the ? =equivalence class of (i, r) by i, r.
Finally de?ne B , to simulate both D0 and D1 :
def
0, r if r ∈ m0 D0 (r) if r ∈ / m0 1, r if A1 (v ) = r ∈ m1 D0 (v ) if A1 (v ) ∈ / m1 .
For r ?∈ m ? : B (? r) = Di (r) where i, r = r ? def For v ∈ V3 : B (v ) = Di (v ) . Several checks are necessary to ensure that this de?nition is sound; that is, that the righthand sides in the clauses de?ning the parent maps B0 and B are wellde?ned places in B0 and B respectively. These points are checked in Appendix A.1, which gives the proof of the following: Theorem 7.8 (RPOs in place graphs) In ?P LG , whenever a pair A of place graphs has a bound D, there exists an RPO (B, B ) for B to D, and Construction 7.7 yields such an RPO. For the behavioural theory of bigraphs we need to know not only how to construct each RPO (which we do for place graphs and link graphs separately), but also how to characterise the set of IPOs for a pair A with common domain. For then, when A1 is a redex, we shall know all the labelled transitions of A0 . For place graphs, an immediate question is: how does our RPO (B, B ) vary, when we keep A ?xed but vary the given bound D? One corollary of our next theorem will be that, if A are both epi, then B remains ?xed, and only B varies; thus A is this case has a unique IPO — which is in fact a pushout. But in general B will vary, so there will be many IPOs. This phenomenon will be important for our transition systems, and also occurs in link graphs, so it is worth seeing a simple example. The diagram shows a pair A in which A0 consists only of a barren root r0 , while A1 has two nodes u, v . There is a bound D with shared root r and an extra node w. Keeping D1 ?xed, we can vary D0 by choosing D0 (r0 ) to be any of {w, u, v, r} while keeping D0 ? A0 ?xed (since r0 is barren in A0 ). The diagram also indicates how the pair B of the RPO varies; for D0 (r0 ) ∈ {u, v } we take B0 (r0 ) = D0 (r0 ), while for D0 (r0 ) ∈ {w, r} we take B0 (r0 ) to be an extra root (shown in parentheses), which also appears (barren) in B 1 . 42
D0
r w u v r0 w
r
D1
B
()
r w
r1 r1 u v
B0 A1
r0
A 0 r0
()
u v
()
B1
r1
This example illustrates all the possible IPOs B for a given pair A; each barren root ri of Ai may be mapped in Bi either to a special root or to any node. In the former case the composite Bi ? Ai has a special root as a trace of ri , but in the latter case it retains no such trace; so we shall call the latter case an elision. Before constructing IPO families formally, we must answer the question: Under what conditions does a pair A have a bound at all? If a bound exists we call A consistent, and our next step is to de?ne certain conditions on A that are necessary and suf?cient for consistency. Roughly speaking, these conditions ensure that A 0 and A1 treat their shared members (all the sites and some of the nodes) compatibly; then a bound B can exist, since B0 can extend A0 to include ‘the part of A1 not shared with A0 ’. Such a bound will also be an IPO if, roughly, it adds no more than necessary for this. De?nition 7.9 (consistency conditions for place graphs) We de?ne three consistency conditions on a pair A : h → m of place graphs. We let i range over {0, 1}; also recall that w2 , w2 range over h ∪ · V2 , the shared places.
CP 0 CP 1
CP 2
ctrl 0 (v2 ) = ctrl 1 (v2 ) If Ai (w) ∈ V2 then w ∈ h ∪ · V2 and A? (w) = Ai (w) If Ai (w2 ) ∈ Vi \ V2 then A? (w2 ) ∈ m? , and if also A? (w) = A? (w2 ) then w ∈ h ∪ · V2 and Ai (w) = Ai (w2 ) .
It may be helpful to express CP 1 and CP 2 in words; they are both to do with children of nodes in Ai . If i = 0, CP 1 says that if the parent of any place w in A0 is a node shared with A1 , then w is also shared and has the same parent in A1 . CP 2 says, on the other hand, that if the parent of a shared place w2 in A0 is an unshared node, then its parent in A1 must be a root, and further that any sibling of w2 in A1 must also be its sibling in A0 . Necessity of these conditions is easy, and we omit the proof: Proposition 7.10 (consistency in place graphs) If the pair A has a bound, then the consistency conditions hold. Before going further, it may be helpful to see a simple example.
43
B0
r v1 v1
B1
v0 r1
r
r0
r0 r0 v2
r1 r1 v2 v2 v1 v1
A0
v0 v2
r0
A1
v2 r v2
r1
B0 ? A 0 = B 1 ? A 1
v0 v2
v2 v2
v1 v1
Figure 9: A consistent pair A of place graphs, with bound B Example 7 (consistent place graphs) Consider the pair A in Figure 9, each with two roots and no sites; nodes with subscript 2 are shared. (Controls are not shown). It is worth checking that the consistency conditions hold. What happens if an extra node u is added to A1 as a sibling of v2 ? If u is unshared then CP 2 is violated, so no bound can exist. If u is shared, then to preserve the consistency conditions —in particular CP 2— u must also become a sibling of v2 in A0 ; then B remains a bound. Now, assuming the consistency conditions of De?nition 7.9, we shall prove that there exist one or more IPOs for A. (Thus, since any IPO is a bound, we shall also have shown that the consistency conditions are suf?cient for a bound to exist.) The idea behind the following construction is that if A are both epis then there is a unique IPO; but every barren root r of A allows a variation, as we saw earlier. Construction 7.11 (IPOs in place graphs) Assume the consistency conditions for the pair of place graphs A : h → m. We de?ne a family of IPOs C : m → n for A as follows. nodes: Take the nodes of Ci to be V? \ V2 . interface: For i = 0, 1 choose any subset i of the barren roots in mi . Set ki = mi\ i . De?ne ki ? ki , the roots to be mapped to the codomain n, by ki = {r ∈ ki  ?v ∈ V2 . Ai (v ) = r ? A? (v ) ∈ m? } . 44
def
Next, on the disjoint sum k0 + k1 , de?ne to be the smallest equivalence such that (0, r0 ) (1, r1 ) whenever A0 (w) = r0 and A1 (w) = r1 for some w ∈ h ∪ · V2 . Then de?ne the codomain up to isomorphism by n = (k0 + k1 )/ For each r ∈ ki we denote the
def
.
equivalence class of (i, r) by i, r.
parents: Choose two functions ηi : i → V?\V2 (i = 0, 1), arbitrary except that ηi (r) is a nonatomic node for all r ∈ i . Then de?ne the parent map C0 : m0 → n as follows (C1 is similar): For r ∈ m0 : C0 (r) = For v ∈ V1 \ V2 : C0 (v ) =
def def
? ? 0, r if r ∈ k0 A1 (v ) if r ∈ k0 \ k0 , for v ∈ h ∪ · V2 with A0 (v ) = r ? η0 (r) if r ∈ 0 1, r A1 (v ) if A1 (v ) = r ∈ m1 if A1 (v ) ∈ / m1 .
The maps ηi are called elisions; this refers to the fact that the barren roots i in Ai are not exported in the IPO interface n, but instead mapped into the body of C i . There is a distinct IPO for each choice of i and ηi . However the IPO will be unique if i = ? is forced (i = 0, 1). This can happen for one of two reasons: either Ai has no barren roots; or V? \ V2 is empty (i.e. all nodes of A? are shared), so no elision can exist. We have to show that the de?nition of C0 is sound. Thus in the ?rst clause for C0 (r) we must ensure that v ∈ V2 exists such that A0 (v ) = r, and that each such v yields the same value A1 (v ) in V1 \ V2 ; in the second clause for C0 (v ) we must ensure that r ∈ k1 . The consistency conditions do ensure this, and also that C0 ? A0 = C1 ? A1 . We can now validate Construction 7.11: Theorem 7.12 (characterising IPOs for place graphs) A pair C : m → n is an IPO for A : h → m iff it is generated (up to isomorphism) by Construction 7.11. Proof (outline) We work up to isomorphism. (?) Recall that a bound B for A is an IPO iff it is the legs of an RPO for A w.r.t. some bound D. So assume such a B : m → m built by Construction 7.7, and recall the subsets mi ? mi and the equivalence ? = over m0 + m1 de?ned there. Now apply Construction 7.11 to create a pair C : m → n, by choosing sets and elisions η as follows: def = {r ∈ mi  r barren in Ai , Di (r) ∈ V? } i def η i : i → V? = D i i . Then indeed C coincides with B . To prove this, ?rst show that k0 , k1 and in the IPO construction coincide with m0 , m1 , ? = in the RPO construction; hence the codomain n of C coincides with the codomain m of B . Then show that the parent maps Ci coincide with Bi . Thus every IPO is a bound built by Construction 7.11. 45
(?) To prove the converse, consider any bound C : m → n built by Construction 7.11, for some sets and elisions η . Now apply Construction 7.7 to yield an RPO (B, B ) for A to C . Then indeed B coincides with C . To prove this, ?rst show that m0 , m1 and ? = in the RPO construction coincide with k0 , k1 , in the IPO construction; hence the codomain of B coincides with the codomain n of C . Then show that the parent maps Bi coincide with Ci . Thus every bound built by Construction 7.11 is an IPO. We shall ?nish this section by introducing an important subprecategory of place graphs, motivated by development to be studied in Section 12. De?nition 7.13 (hard place graphs) A hard place graph is one in which no root or nonatomic node is barren. They form a subprecategory denoted by P LG h . The condition on roots ensures that hard place graphs are epi. This means, as we have seen, that a consistent pair always has a unique IPO, i.e. a pushout. The extra condition, that a nonatomic node must not be barren, makes some of the mathematics simpler; for example, if B ? A is hard then so are both A and B . Moreover, no change to the IPO (or pushout) construction is needed, as we now see: Proposition 7.14 (pushouts for hard place graphs) If A is a consistent pair of hard place graphs, then the pushout B built in ?P LG by Construction 7.11 is also hard, and is indeed a pushout in P LG h . There is another connection between ?P LG and ?P LG h . Let K be any signature, and choose a new atomic control with zero arity; adjoin to K to form K . We can make any arrow G of ?P LG (K) into a hard place graph in ?P LG h (K ) by adding a node as a child of any barren root or node. We shall call nodes place nodes. Now let us say that two bigraphs F and G in ?P LG h (K ) are placeequivalent, F ≡ G, if they differ only in occurrences of place nodes. Then place equivalence is a static congruence (De?nition 3.5). Also there exists a quotient precategory ?P LG h (K )/≡ , whose arrows are placeequivalence classes of hard place graphs, and where the support of each equivalence class is just the support of each member less its place nodes. Furthermore this quotient precategory is isomorphic with ?P LG (K). The reader may safely omit the rest of this section until reading Section 14. Until then we shall work with hard place graphs because their IPOs are pushouts, which helps to avoid elisions. But at that point we need to invoke place equivalence in order to forget place nodes. For this purpose, in order to transfer our results to an abstract setting, we need to know certain properties of ≡ . We prepare for this now by showing that the operation which generates ≡ —i.e. the addition or removal of a single place node u — does not affect the pushout property, under certain conditions. In the following two propositions, for ease of notation, we shall use to mean a fresh place node u distinct from all others present. The proofs appear in the Appendix. Proposition 7.15 (?rst pushout variation) Let B be a bound for A in ?P LGh (K ). Add a new place node to both A0 and B1 , yielding A0 and B1 such that B0 ? A0 = B1 ? A1 . Then B is a pushout for A iff (B0 , B1 ) is a pushout for (A0 , A1 ). 46
(a) C0 C B0 A0 C1 B1 A1
(b) C0 C C1
B0 A0
B1 A1
There are other ways of adding a single place node to a square consisting of a bound B for A, and preserving the bound. Which of these ways will preserve the pushout property in both directions, as in the last proposition? If we add to both B 0 and B1 then we lose the pushout; for we violate the IPO property that the nodes of an IPO for A must be among the nodes of A. What about adding to both A0 and A1 ? In this case we may gain a pushout where only a bound previously existed. This is best seen in reverse; if B is a pushout for the augmented pair A , then by deleting from the latter we may remove the only shared node, thus leaving a merging of roots that should not occur in a pushout. However, by adding a constraint we obtain the following: Proposition 7.16 (second pushout variation) Let B be a bound for A in ?P LGh (K ). Let a fresh place node be added to both members of A, yielding A such that B is also a bound for A , and with A0 ( ) a node (not a root). Then (1) If B is a pushout for A, it is also a pushout for A . (2) Let have a sibling w in both A0 and A1 . Then if B is a pushout for An , it is also a pushout for A. (a) C0 C B0 A0 C1 B1 A1 (b) C0 C C1
B0 A0
B1 A1
47
8 Link graphs
Link graphs capture the connectivity of bigraphs, ignoring their nesting. The treatment here is signi?cantly simpler than the previous treatment [28], though compatible with it.6 There is a close formal analogy in the treatment of place graphs and link graphs. As with place graphs, we assume a signature K assigning to each control K an arity ar (K ). We also assume an in?nite set X of names.
De?nition 8.1 (link graph) A link graph A = (V, E, ctrl , link ) : X → Y has ?nite sets X of inner names, Y of (outer) names, V of nodes and E of edges. It also has a function ctrl : V → K called the control map, and a function link : X ∪ · P →E ∪ · Y def called the link map, where P = v∈V ar (ctrl (v )) is the set of ports of A. We shall call the inner names X and ports P the points of A, and the edges E and outer names Y its links. The outer and inner names are for interfacing, and will be important in de?ning composition. When we talk of a ‘name’ without adjective, we mean an outer name. Here are some basic properties: De?nition 8.2 (idle, open, closed, peer, lean) A link is idle if it has no preimage under the link map. An (outer) name is an open link, an edge is a closed link. A point (i.e. an inner name or port) is open if its link is open, otherwise closed. Two distinct points are peers if they are in the same link. A link graph is lean if it has no idle edges. An idle name is sometimes needed; for example we may want to consider two bigraphs as members of the same homset, even if one of them uses a name x and the other does not. On the other hand an idle edge serves no useful purpose, but may be created by composition. Sometimes we shall need to ensure that the property of leanness (no idle edges) is preserved by certain constructions. De?nition 8.3 (precategory of link graphs) The precategory ?L IG has name sets as objects and link graphs as arrows. The composition A1 ? A0 : X0 → X2 of two link graphs Ai = (VI , ctrl i , Ei , link i ) : Xi → Xi+1 (i = 0, 1) is de?ned when their node def · V1 , sets and edge sets are disjoint; then A1 ? A0 = (V, ctrl , E, link ) where V = V0 ∪ · link 1 ) ? (link 0 ∪ · IdE1 ). The ctrl = ctrl 0 ∪ · ctrl 1 , E = E0 ∪ · E1 and link = (IdE0 ∪ def identity link graph at X is idm = (?, ?K , ?, IdX ) : X → X . Note that ?L IG is supported, with nodeedge sets V + E as support sets. We can describe the composite link map link of A1 ? A0 as follows, considering all possible arguments p ∈ X0 ∪ · P0 ∪ · P1 : ? · P0 and link 0 (p) ∈ E0 ? link 0 (p) if p ∈ X0 ∪ link 1 (x) if p ∈ X0 ∪ · P0 and link 0 (p) = x ∈ X1 link (p) = ? link 1 (p) if p ∈ P1 .
6 The main difference is that we here give identity not only to the nodes, but also to the links, in a link graph. Using our present terminology, we previously de?ned links in terms an equivalence over points and names, each link being an equivalence class. This avoided introducing an explicit link set, but the manipulation of equivalences required to exhibit and characterise RPOs and IPOs was much harder than with the present treatment.
48
By analogy with place graphs, we often denote the link map of A simply by A. Proposition 8.4 (isomorphisms in link graphs) An arrow ι : X → Y in ?L IG is an isomorphism iff it has no nodes or edges and its link map is a bijection from X to Y . Note that the names in an interface are identi?ed alphabetically, not positionally. This difference is mathematically unimportant. Alphabetical names are convenient for link graphs just as they are convenient in the λcalculus, and they also lead naturally to forms of parallel product that are familiar from process calculi. But in de?ning tensor product we have to require disjoint interfaces: De?nition 8.5 (tensor product) The tensor product ? in ?L IG is de?ned as follows: On objects, X ? Y is simply the union of sets required to be disjoint. For two link graphs Ai : Xi → Yi (i = 0, 1) we take A0 ? A1 : X0 ? X1 → Y0 ? Y1 to be de?ned when the interface products are de?ned and when A0 and A1 have disjoint node sets and edge sets; then we take the union of the link maps. There is an important variant of tensor product that merges outer names, i.e. does not require them to be disjoint. This has fewer algebraic properties than the tensor (categorically, it is not a bifunctor), but will be important in modelling process calculi: De?nition 8.6 (parallel product) The parallel product  in ?L IG is de?ned as foldef lows: On objects, X  Y = X ∪ Y . On link graphs Ai : Xi → Yi (i = 0, 1) we de?ne A0  A1 : X0 ? X1 → Y0  Y1 whenever X0 and X1 are disjoint, by taking the union of link maps. Again we shall need epis and monos, and we have the following: Proposition 8.7 (epis and monos in link graphs) A link graph is epi iff no name is idle; it is mono iff no two inner names are peers. Notation When considering a pair A : W → X of link graphs with common domain W , we shall adopt a convention for naming their nodes, ports and edges. We denote the node set of Ai (i = 0, 1) by Vi , and denote V0 ∩ V1 by V2 . We shall use vi , vi , . . . to range over Vi (i = 0, 1, 2). Similarly we use pi ∈ Pi and ei ∈ Ei for ports and edges (i = 0, 1, 2). However, we shall sometimes use pi also for points, i.e. pi ∈ W ∪ · Pi ; the context will resolve any ambiguity. One of the reasons for equipping link graphs with explicit edge sets, as well as node sets, is that we get a simple RPO theory. Also, as the reader will have noticed, there is a striking formal analogy between link graphs and place graphs. On closer inspection, the analogy appears to break down. For a parent map is prnt : h ∪ · V →V ∪ · m where both the domain and codomain include the nodes V , while a link map is link : W ∪ · P →E ∪ · X where the sets P and E are disjoint; so unlike a parent map, a link map cannot be iterated, i.e. a link graph has no notion of nesting. Nonetheleless, The RPO theories are almost identical, and we present them as similarly as possible. We ?rst give the same intuition as for place graphs. Suppose D is a bound for A, and we wish to construct the RPO (B, B ). To form B , we ?rst truncate D by removing 49
the names, and all points and edges not present in A. Then for the outer face of B , we create a new link (a name) for each point unlinked by the truncation, equating these new names only when required so that B0 ? A0 = B1 ? A1 . Formally: ? B: X ? → Z ), for a Construction 8.8 (RPOs in link graphs) An RPO (B : X → X, pair A : W → X of link graphs relative to a bound D : X → Z , will be built in three stages. Since RPOs are preserved by isomorphism, we assume X0 , X1 disjoint. We use the notational conventions introduced above. nodes and edges: If Vi are the nodes of Ai (i = 0, 1) then the nodes of Di are V? \ V2 ∪ · V3 for some V3 . De?ne the nodes of Bi and B to be V? \ V2 (i = 0, 1) and V3 respectively. Edges Ei are treated exactly analogously, and ports Pi inherit the analogous treatment from nodes. ? of B as follows. First, de?ne the names interface: Construct the shared codomain X ? in each Xi that must be mapped into X : Xi = {x ∈ Xi  Di (x) ∈ P3 ∪ · Z} . Next, on the disjoint sum X0 + X1 , de?ne ? = to be the smallest equivalence for which · P2 . (0, x0 ) ? = (1, x1 ) whenever A0 (p) = x0 and A1 (p) = x1 for some point p ∈ W ∪ Then de?ne the codomain up to isomorphism:
def ?= X (X0 + X1 )/? =. def
For each x ∈ Xi we denote the ? =equivalence class of (i, x) by i, x. links: De?ne B0 to simulate D0 as far as possible (B1 is similar): For x ∈ X0 : For p ∈ P1 \ P2 : B0 (x) = B0 (p) =
def def
0, x if x ∈ X0 D0 (x) if x ∈ / X0 1, x if A1 (p) = x ∈ X1 D0 (p) if A1 (p) ∈ / X1 .
Finally de?ne B , to simulate both D0 and D1 : ?: For x ?∈X For p ∈ P3 : B (? x) = Di (x) where x ∈ Xi and i, x = x ? def B (p) = Di (p) .
def
This de?nition can be proved sound; for it can be shown that the righthand sides in the clauses de?ning link maps Bi and B are wellde?ned links in Bi and B respectively. Then we can prove the following (the proof appears in Appendix A.2): Theorem 8.9 (RPOs in link graphs) In ?L IG , Whenever a pair A of link graphs has a bound D, there exists an RPO (B, B ) for B to D, and Construction 8.8 yields such an RPO.
50
We now proceed to characterise all the IPOs for a given pair A : W → X of link graphs, just as we did for place graphs. Fortunately, the formal analogy between the two allows us to omit proofs, but we shall exhibit the construction in full. Again we ask: how does our link graph RPO (B, B ) vary, when we keep A ?xed but vary the given bound D? The answer is the same: if A are both epi, then B remains ?xed and only B varies, so that in this case there is a pushout. But, as with place graphs, we need to treat the general case. The ?rst step is to establish consistency conditions. De?nition 8.10 (consistency conditions for link graphs) We de?ne three consistency conditions on a pair A : W → X of place graphs. We use p to range over arbitrary points, pi , pi , . . . to range over Pi , and p2 , p2 , . . . to range over W ∪ · P2 , the shared points.
CL 0 CL 1
CL 2
ctrl 0 (v2 ) = ctrl 1 (v2 ) If Ai (p) ∈ E2 then p ∈ W ∪ · P2 and A? (p) = Ai (p) . If Ai (p2 ) ∈ Ei \ E2 then A? (p2 ) ∈ X? , and if also A? (p) = A? (p2 ) then p ∈ W ∪ · P2 and Ai (p) = Ai (p2 ) .
Again, let us express CL 1 and CL 2 in words. If i = 0, CL 1 says that if the link of any point p in A0 is closed and shared with A1 , then p is also shared and has the same link in A1 . CL 2 says, on the other hand, that if the link of a shared point p2 in A0 is closed and unshared, then its link in A1 must be open, and further that any peer of p2 in A1 must also be its peer in A0 . Proposition 8.11 (consistency in link graphs) If the pair A has a bound, then the consistency conditions hold. Before going further, it may be helpful to see a simple example. Example 8 (consistent link graphs) Consider the pair A : ? → X of link graphs in Figure 10, where X0 = {x0 , y0 , z0 } and X1 = {x1 , y1 }. Nodes with subscript 2 are shared. (Controls are not shown). The pair is consistent, with bound B as shown. It is worth checking the consistency conditions. Now, assuming the consistency conditions of De?nition 8.10, we shall construct a nonoempty family of IPOs for A; the construction exactly follows the analogy with place graphs. As before, it is clear that when A are both epi there are no elisions, and hence the IPO is unique and hence pushout. Construction 8.12 (IPOs in link graphs) Assume the consistency conditions for the pair of link graphs A : W → X . We de?ne a family of IPOs C : X → Y for A as follows. nodes and edges: Take the nodes and edges of Ci to be V? \ V2 and E? \ E2 . interface: For i = 0, 1 choose any subset Li of the names Xi such that all members of Li are idle. Set Ki = Xi \ Li . De?ne Ki ? Ki , the names to be mapped to the codomain Y , by Ki = {xi ∈ Ki  ?p ∈ P2 . Ai (p) = xi ? A? (p) ∈ X? } . 51
def
B0
v1
e1
w v1
B1
e0
w v0
x0
y0 y0
z0 z0
x1
y1 y1
A0
e0
v0
x0
A1
x1 v1 v1 v2
e2 e1
v2
e2
v2
v2 w v0 v1 v 1
e0
v2
v2
B0 ? A 0 = B 1 ? A 1
v2
v2 v2
v2
e2 e1
Figure 10: A consistent pair A of link graphs, with bound B Next, on the disjoint sum K0 + K1 , de?ne to be the smallest equivalence such that (0, x0 ) (1, x1 ) whenever A0 (p) = x0 and A1 (p) = x1 for some p ∈ W ∪ · P2 . Then de?ne the codomain up to isomorphism: Y = (K0 + K1 )/ For each x ∈ Ki we denote the
def
.
equivalence class of (i, x) by i, x.
links: Choose two arbitrary functions ηi : Li → E? \ E2 (i = 0, 1). Then de?ne the link maps Ci : Xi → Y as follows (we give C0 ; C1 is similar): For x ∈ X0 : C0 (x) = For p ∈ P1 \ P2 : C0 (p) =
def def
? ? 0, x A (p) ? 1 η0 (x) 1, x A1 (p)
if x ∈ K0 if x ∈ K0 \ K0 , for p ∈ W ∪ · P2 with A0 (p) = x if x ∈ L0 if A1 (p) = x ∈ X1 if A1 (p) ∈ / X1 .
The maps ηi are called elisions; this refers to the fact that the idle names Li in Ai are not exported in the IPO interface Y , but instead mapped into the body of C i . There is a distinct IPO for each choice of Li and ηi . However the IPO will be unique if 52
Li = ? is forced. This can happen for one of two reasons: either Ai has no idle names; or E? \ E2 is empty (i.e. all edges of A? are shared), so no elision can exist. The soundness of the above de?nition, and the fact that C is a bound, are both established by analogy with the corresponding results for place graphs. Similarly the following characterisation theorem, stating that our construction creates all and only IPOs for A, is proved analogously to Theorem 7.12 for place graphs: Theorem 8.13 (characterising IPOs for link graphs) A pair C : X → Y is an IPO for A : W → X iff it is generated (up to isomorphism) by Construction 8.12.
53
9 Pure bigraphs: development
We now develop the theory of pure bigraphs, based upon De?nition 6.2. First we introduce the obvious precategory by combining ?P LG and ?L IG : De?nition 9.1 (precategory of pure concrete bigraphs) The precategory ?B IG (K) of pure concrete bigraphs over a signature K has pairs I = m, X as objects (interfaces) and bigraphs G = (V, E, ctrl G , GP , GL ) : I → J as arrows (contexts). We call I the inner face of G, and J the outer face. If H : J → K is another bigraph with node set disjoint from V , then their composition is de?ned directly in terms of the composition of the components as follows: H ? G = H P ? GP , H L ? GL : I → K . The identities are idm , idX : I → I , where I = m, X . The subprecategory ?B IG h consists of hard bigraphs, those with place graphs in ?P LG h . Throughout this section, unless otherwise stated the de?nitions and results apply equally to ?B IG and ?B IG h . The whole section is about pure bigraphs, in contrast to the binding bigraphs to be studied in Section 11, so we shall omit the adjective ‘pure’ here. We shall also omit ‘concrete’ for the time being; but in De?nition 9.12 we shall introduce abstract bigraphs, via a forgetful functor. We shall continue to omit the signature K except when it is important. We now combine some familiar place graph and link graph structures to yield bigraph structures. Proposition 9.2 (isomorphisms in bigraphs) The isomorphisms in ?B IG are all combinations ι = ιP , ιL of a place graph isomorphism and a link graph isomorphism. De?nition 9.3 (tensor product) The tensor product of two bigraph interfaces is dedef ?ned by m, X ? n, Y = m + n, X ∪ · Y when X and Y are disjoint. The tensor product of two bigraphs Gi : Ii → Ji (i = 0, 1) is de?ned by
L L P G0 ? G 1 = G P 0 ? G 1 , G 0 ? G 1 : I 0 ? I 1 → J0 ? J 1
def def
when the interfaces exist and the node sets are disjoint. This combination is wellformed, since its constituents share the same node set. It is routine to verify the axioms for a partial tensor product. In fact bigraphs are an instance of a mathematical structure that we introduced in Section 4: Theorem 9.4 (bigraphs are wide monoidal) For any signature K, the precategories ?B IG (K) and ?B IG h (K) are wide monoidal; the origin is = 0, ? , and the interface n, X has width n. Proof We leave the details for the reader to check. Note ?rst that ?B IG and ?B IG h are supported, with support sets of the form V + E — a disjoint sum of a node set and an edge set. The width functor on arrows (bigraphs) is given as follows: for G :
54
m, X → n, Y , its width is the function sending each site s ∈ m to the unique root r ∈ n such that r >G s. Following Section 4 we use lower case latters a, b, . . . for ground bigraphs, those with inner face , and we write a : → I as a : I . These will represent the agents of our BRSs in Section 12, and will be used to model the agents in a conventional process calculus in Section 15. Several properties of bigraphs are inherited from place graphs and link graphs. For example: Proposition 9.5 (epis and monos in bigraphs) A bigraph G in ?B IG (or ?B IG h ) is epi (resp. mono) iff its components GP and GL are epi (resp. mono) in ?P LG (or ?P LG h ) and ?L IG . It follows from Theorem 9.4 that when we later equip bigraphs with reaction rules we shall have a WRS, and then we can apply the main congruence theorem, Theorem 5.5, provided that we have enough RPOs. So now we draw together our RPO results for place graphs and link graphs. We deduce from Theorem 7.8 and 8.9 the following: Corollary 9.6 (RPOs for bigraphs) In both ?B IG and ?B IG h an RPO for A to D is provided by the triple
L P L P , BP, BL ) , B1 , B1 , B0 ( B0
where (B P , B P ) is a place graph RPO for AP to DP and (B L , B L ) is a link graph RPO for AL to DL . Proof We can check from Constructions 7.7 and 8.8 that each combination in the triple is well formed, since its two constituents have the same node set. Once this is established, the RPO property is easily veri?ed by diagram chasing. Now we shall consider IPOs for bigraphs. We can use Theorems 7.12 and 8.13 to prove that: Corollary 9.7 (IPOs for bigraphs) A pair B is an IPO for A in ?B IG or ?B IG h iff B P is a place graph IPO for AP and B L is a link graph IPO for AL . Proof It is enough to prove it just for ?B IG .
(?) Assume the IPO in ?B IG . Then in ?P LG , by de?nition B P is a bound for AP . We need to show that (B P , id) is an RPO for AP to B P . So, for any other candidate RPO (C P , C P ), we must ?nd a unique mediating arrow between the intended RPO and this candidate. It can be shown that the members of (C P , C P ) have the same support as the members of (B P , id). So we may form the triple of combinations
P L P L ( C0 , B0 , C1 , B1 , C P , id )
55
w v1 v0 v1
w
B0
B1
x0
y 0 z0 x0 v2
x1 y0 z0 x1
y1 y1 v1 v1
A0
v0
A1
v2 v2 v2 w v2
v2
B0 ? A 0 = B 1 ? A 1
v0
v2 v2
v1 v1 v2
Figure 11: A consistent pair A of bigraphs, with IPO B (with suitable interfaces), and also prove it to be a candidate RPO in ?B IG for A to B . Hence there is a unique mediating arrow between the given RPO (B, id) and this candidate. The place graph constituent of this mediator then provides the required unique mediator in ?P LG , and we are done. A similar argument applies also to ?L IG . (?) Assuming IPOs in ?P LG and ?L IG , by routine diagram chasing we can verify the IPO property in ?B IG . Example 9 (Bigraph IPOs) To illustrate IPOs in ?B IG , we can combine Example 7 for place graphs and Example 8 for link graphs, since they have the same node sets. In both cases the bounds B are IPOs, and indeed pushouts because the graphs A are epi. The combination is shown in Figure 11. Again, both of the bigraphs A are epi, so our results show that the bound B is again an IPO and a pushout. We now give a few special cases of IPOs. First, some pushouts (hence also IPOs) that are easy to verify for any precategory: Proposition 9.8 (containment pushout) Let A be epi. Then the pair (A, F ? A) has the pair (F, id) as a pushout. In particular, by taking A = id and F = id respectively: (1) any pair (id, F ) has (F, id) as a pushout, and (2) if A is epi then (A, A) has (id, id) as a pushout. 56
Next, tensor product preserves IPOs with disjoint support: Proposition 9.9 (tensor IPO) In any of ?P LG , ?P LG h , L IG , ?B IG or ?B IG h , Let C be an IPO for A and D be an IPO for B , where the supports of the two IPOs are disjoint. Then, provided the tensor products exist, C ? D is an IPO for A ? B . An important corollary, with the help of Proposition 9.8, is when the two given IPOs contain identities:
(a)
I ?J
idI ? B idI ? B
(b)
I ?J I
idI ? b b
I ?J
A ? idJ
A ? idJ
I ?J
a
J
a ? idJ
Corollary 9.10 (tensor IPOs with identities) Let A : I → I and B : J → J share no nodes, and let the free names of I , I be disjoint from those of J , J . Then the pair (A ? idJ , idI ? B ) has an IPO (idI ? B, A ? idJ ). See diagram (a). In particular if I = J = then A = a and B = b are ground bigraphs, and the IPO is as in diagram (b). We shall call a bigraph lean if its link graph is lean, i.e. has no idle edges. In Section 12 we shall need to transform IPOs by the addition or subtraction of idle edges. Let us write AE for the result of adding a set E of fresh idle edges to A. The following is easy to prove from the IPO construction for link graphs: Proposition 9.11 (IPOs, idle edges and leanness) For any two pairs A and B : (1) If B is an IPO for A, and A1 is lean, then B0 is lean.
E (2) For any fresh set E of edges, B is an IPO for A iff (B0 , B1 ) is an IPO for (AE , A ) . 1 0
We now turn to abstract bigraphs. To get them from concrete bigraphs, we wish to factor out the identity of nodes and edges; we also wish to forget any idle edges. So we de?ne an equivalence that is a little coarser than support equivalence ( ): De?nition 9.12 (Abstract pure bigraphs and their category) Two concrete bigraphs A and B are leansupport equivalent, written A B , if after discarding any idle edges they are support equivalent. The category B IG (K) of abstract pure bigraphs has the same objects as ?B IG (K), and its arrows are leansupport equivalence classes of concrete bigraphs. Leansupport equivalence is clearly a static congruence (De?nition 3.5). The associated quotient functor, assured by De?nition 3.6, is [[ · ]] : ?B IG (K) → B IG (K) . The de?nition of B IG h is analogous, with the restriction of [[ · ]] to ?B IG h as quotient functor. 57
G
L K x L
C D (= G)
L L
G
L K L
y
z y K z
x
D0
(= id)
y z K x x
D1 (= id)
C0 B0 A
D
C B1
x K
x
C1
?
K
A
Figure 12: Two abstract bigraphs may lack an RPO Note that there are natural abstract versions of place graphs and link graphs. But we have little use for them, for we cannot combine an abstract place graph with an abstract link graph to form an abstract bigraph! (The combination only makes sense when nodes have identity.) The deeper reason for studying concrete bigraphs is that they possess RPOs. This will allow us Section 12 to derive a behavioural congruence for ?B IG , and then to show how to transfer it, under certain assumptions, to B IG . To see why we cannot work directly in B IG , let us see how it lacks some of the structure present in ?B IG . A simple example of this is that the functor [[ · ]] loses epis; for example, the abstract bigraph A in Figure 12 is not epi, though (since it has no idle names) all its [[ · ]]preimages are epi. More seriously, B IG lacks RPOs in general; this we shall now show. Example 10 (abstract bigraphs lack RPOs) Let the controls K and L be atomic with arity 1. Figure 12 shows two candidate RPOs for the pair (A, A) of abstract bigraphs w.r.t. the pair (G, G). The candidates are (C, C ) and (D, D), where Di = id (i = 0, 1) and D = G. Speaking informally, the ?rst candidate keeps the two K nodes in (A, A) distinct, whereas the second candidate coalesces them. These two treatments of nodeoccurrences cannot be properly distinguished in abstract bigraphs; that is why an RPO fails to exist in this example. To see this, suppose an RPO (B, B ) exists. Then there must be mediators C , D to the two candidates, as shown, making the diagram commute. But this leads to a contradiction, as follows. First, B0 and B1 must have empty support, since for example 58
D ? B0 = D0 = id. From B0 ? A = B1 ? A it can then be deduced that B0 = B1 .7 It follows that C0 = C ? B0 = C ? B1 = C1 , a contradiction. We shall ?nish this section by introducing some terminology and operations that will be needed in following sections. Notations and terminology We often abbreviate an interface 0, X to X , and {x} to x; similarly we abbreviate m, ? to m. Thus the interfaces ? and 0 are identical with the origin , and indeed the identity id may be written variously as , ? or 0. A bigraph with interfaces of zero width (and hence having no nodes) is called a wiring. The wirings ω are generated by composition and tensor product from two basic forms: /x : x → , called closure; and a function σ : X → Y , not necessarily surjective, called a substitution. For X = {x1 , . . . , xn } we write /X for /x1 ? · · · ? /xn , a multiple closure. For vectors x and y of equal length, with the xi distinct, we write y /x or (y0 /x0 , y1 /x1 , . . .) for the surjective substitution xi → yi . The unique substitution with empty domain and codomain Z is written Z : → Z . Every substitution σ can be expressed uniquely as σ = τ ? Z , with τ surjective. We let α range over renamings, the bijective substitutions. An interface is prime if it has width 1. We shall often write a prime interface I = 1, X as X ; note in particular that 1 = ? . A prime bigraph P : m → X has no inner names and a prime outer face. An important prime is merge : m → 1; it has no nodes, and simply maps m sites to a single root. A bigraph G : m → n, X with no inner names is converted by merge into a prime (merge ? idX ) ? G. A bigraph is discrete if it has no edges, and its link map is bijective. This means that every point is open, no two points are peers, and no name is idle. For any nonatomic control K with arity k and sequence x of k distinct names we de?ne the discrete ion Kv,x : 1 → x to have a single K node v , whose ports are severally linked to x. We omit the subscript v when it can be understood. For a discrete prime P with names Y the composite (Kx ? idY ) ? P is a discrete molecule. If K is atomic it has no ion, but we de?ne the discrete atom Kx : → x ; it resembles an ion but possesses no site. An arbitrary (nondiscrete) ion, molecule or atom is gained by composing ω ? id1 with a discrete one. We often omit . . . ? idI in compositions, when there is no ambiguity; examples from above are merge ? G for (merge ? idX ) ? G and Kx ? P for (Kx ? idY ) ? P . Given a wiring ω : Y → Z we may restrict its link map to any subset X ? Y , yielding the restricted wiring ω X : X → Z . Then, if the outer face of G is m, X we may write simply ωG for (ω X ? idm ) ? G. Note that every atom and every molecule is prime, but whereas an atom is ground, a molecule need not be (it can have sites). The reader may wonder why primes do not have inner names. This is what allows us to prove a prime factorisation property in Proposition 9.17(2). We now look at variants of the tensor product, which re?ect more closely the notion of ‘parallel composition’ familiar in process calculi. Although these operations apply
7 This would be immediate if A were epi, but it is not! (Even though its representatives in ?B IG are epi.) However, a speci?c argument can be given in this case.
59
to arbitrary bigraphs, they are especially signi?cant when applied to ground bigraphs, because these will model processes. Process calculi often have a parallel product p q or p  q , in which the processes p and q may share names. We therefore extend the parallel product ‘  ’ of link graphs (De?nition 8.6) as follows: De?nition 9.13 (parallel product) The parallel product of two bigraphs is de?ned def on interfaces by m, X n, Y = m + n, X ∪ Y , and on bigraphs by
L L P G0 G 1 = G P 0 ? G 1 , G 0  G 1 : I 0 ? I 1 → J0 J 1
def
when the interfaces exist and the node sets are disjoint. It is easy to verify that is associative, with unit . We insist that G0 and G1 have disjoint inner names, this ensures that their parallel product is wellformed. Note that it keeps the regions of G0 and G1 separate; this was its purpose in the remote reaction rule for the π calculus shown in Figure 6. Another way of constructing G0 G1 , which we shall use later in extending the product to binding bigraphs, is to disjoin the names of G0 and G1 , then take the tensor product and merge the names again: Proposition 9.14 (parallel product) Let G0 G1 be de?ned. Then G0 G1 = σ (G0 ? τ G1 ) , where the substitutions σ and τ are de?ned as follows: If zi (i ∈ n) are the names shared between G0 and G1 , and wi are fresh names in bijection with the zi , then τ (zi ) = wi and σ (wi ) = σ (zi ) = zi (i ∈ n). We shall continue to use  to combine two wirings; in fact ω0  ω1 (as de?ned for link graphs) means the same as ω0 ω1 . We shall also abuse notation by extending  to primes: De?nition 9.15 (prime product) The prime product of prime interfaces is given by 1, X  1, Y = 1, X ∪ Y . For two prime bigraphs P : I → J , with I0 ? I1 de?ned, we de?ne their prime product by def P0  P1 = merge ? (P0 P1 ) : I0 ? I1 → J0  J1 . Again  is associative, with unit 1 when applied to primes. We have chosen the symbol that is used in CCS and the π calculus, since the correspondence will turn out to be exact. We shall ?nd it useful to abuse notation even further, and write ω  P instead of ω P when joining a wiring to a prime. To summarise: G0  G1 is de?ned whenever G1 have width ≤ 1, and it has the maximum of their widths. Let us now consider discrete bigraphs. In a precise sense they fully complement wiring: 60
def
Proposition 9.16 (underlying discrete bigraph) Every bigraph G in ?B IG or ?B IG h can be expressed uniquely (up to iso) as G = (ω ? idn ) ? D, where ω is a wiring and D is discrete. We shall call this unique factorisation of G a discrete normal form (DNF). It applies equally to abstract bigraphs, and indeed it will play an important part in the complete axiomatisation of B IG which is the subject of a later section. Discreteness is very wellbehaved. It is clear that both composition and tensor product preserve it, and more: Proposition 9.17 (synthesis and analysis of discrete bigraphs) In ?B IG or ?B IG h the discrete pure bigraphs form a monoidal subprecategory. Moreover (1) Every discrete D : m, X → n, Y may be factored uniquely, up to isomorphism on the domain of each factor Di , as D = α ? ((D0 ? · · · ? Dn?1 ) ? π ) with α a renaming, each Di prime and discrete, and π a permutation. (2) If (D , G ) is an IPO for (G, D) and D is discrete, then D is discrete. (3) If D
?G
= ωD with D and D discrete, then (D , ω ) is an IPO for (G, D).
Note that a renaming is discrete but not prime (since it has zero width); this is why (1) has such a factor. This unique factorisation depends on the fact that primes have no inner names. In the special case that D is ground, the factorisation in (1) is just D = d0 ? · · · ? dn?1 , a product of prime discrete ground bigraphs. We have to make one more preparation for Section 12 on dynamics. When we de?ne parametric reaction rules we must allow them to replicate some of their parameters and discard others. We shall call this operation on parameters instantiation. The following de?nition ensures that names are shared between all copies of a parameter, and uses support translation to ensure that the several copies are given disjoint supports. De?nition 9.18 (instantiation) An instantiation from (width) m to (width) n, which we write :: m → n, is determined by a function : n → m. For any X this function de?nes the map : Gr m, X → Gr n, X as follows. Decompose g : m, X into g = ω (d0 ? · · · ? dm?1 ), with ω : Y → X and each di prime and discrete. Then de?ne (g ) = ω (e0
def
···
en?1 ) ,
where ei d (i) for i ∈ n. This map is wellde?ned (up to support translation), by Propositions 9.16 and 9.17. Note that the names of e0 · · · en?1 may be fewer than Y , because may not be surjective. But by our convention the outer names of (g ) are determined by the outer names of ω , i.e. X . We deduce two important properties of wirings: 61
Proposition 9.19 (wiring an instance) Wiring commutes with instantiation; that is, ω (a) (ωa) .
Proof Let a : m, X , with :: m → m . Take the DNF a = ω d. Then (a) = ω a , where a = d0 · · · dm ?1 with each di d (i) . So (ωa) = = = (ω (ω d)) ((ω ? ω )d) (ω ? ω )a ω (ω a ) ω (a) .
Proposition 9.20 (wiring a product) Wiring commutes with parallel and prime product; that is, ω (F G) = ωF ωG and ω (F  G) = ωF  ωG . Proof Routine.
We can now deduce how to apply instantiation to a product of primes: Proposition 9.21 (instantiating a product) Let ai : Yi be prime and ground (i ∈ m), and let Y = i Yi . Let :: m → n be an instantiation. Then (a0 where bj a
(j )
···
am?1 ) = Y
b0
···
bn?1
for j ∈ n.
Proof First express each ai in DNF, using discrete di with disjoint name sets. Then apply Propositions 9.19 and 9.20. Thus, although instantiation breaks up a ground bigraph in general, it does not break up a prime; in fact, applied to a product of primes, it simply reassembles copies of the prime factors. Also, if we instantiate G ? a where a is prime, then a will not be broken up but the result may contain several copies of a. This fact, which will be important for Section 12, means that (G ? a) can be transformed into (G ? b) by replacing a ?nite number of occurrences of a by b. Formally: Proposition 9.22 (instantiating with prime component) Let G : X → m, Y be arbitrary with prime inner face, and :: m → n be an instantiation. Then for some k ≥ 0, if we choose disjoint renamings αi : X → Xi (i ∈ k ), there exists a context C : k, i Xi → n, Y such that (G ? a) C ? (a0 ? · · · ? ak?1 ) whenever G ? a is de?ned, where ai αi a. Moreover for any pair a, b : X we have ( (G ? a), (G ? b)) ∈ S ? , where S = {(H ? a, H ? b)  H any context } . 62
Proof For the ?rst part, apply Propositions 9.16 and 9.17 to express G in terms of a product of prime discrete factors. Then use the fact that all but one of these factors is ground (since G has prime inner face) to obtain the equation G ? a = (ω ? π ) ? ((F ? a) ? d1 ? · · · ? dm?1 ) where π is a permutation, F has prime outer face and all of the righthand side (except a) is independent of a. Finally we use Proposition 9.21 to obtain an expression for (G ? a) involving several supportdisjoint copies of a, as required. For the second part, de?ne for each i ∈ k ci = C ? (b0 ? · · · ? bi?1 ? ai ? · · · ? ak?1 ) , so that ci differs from ci+1 by the replacement of a single copy of a by b. For the required result we only need to observe that (ci , ci+1 ) is in S , by choosing the context Ei = C ? (b0 ? · · · ? bi?1 ? αi ? ai+1 · · · ? ak?1 ) . We have now taken the theory of pure bigraphs as far as required for the dynamics of bigraphs, which we introduce in Section 12.
63
10 Algebra of pure bigraphs
In this section we diverge from our main theme, the behavioural theory of bigraphs, to sharpen our understanding of their algebraic structure. The reader may safely study later sections without reading this one. Ths algebra we develop here is just for abstract bigraphs B IG . These are our primary model; we introduced concrete bigraphs ?B IG mainly to obtain – in Part III – a behavioural theory, which can then be transferred to B IG . However, it is likely that the algebraic theory for B IG will, with minor modi?cations, be valid also for ?B IG . We shall ?nd that there is a simple complete axiomatisation of pure bigraphs. There are also two useful kinds of normal form. One of them is in terms of discrete bigraphs, and is useful for proving the completeness of our axioms; the other uses the parallel products and  , and is better ?tted for practical applications. We begin by de?ning our algebraic signature (not to be confused with the control signature K), consisting of elementary bigraphs suf?cient to generate all bigraphs. Elementary bigraphs We de?ne six elementary forms of pure bigraph: x→ X →Y →1 2→1 m+n → n+m 1 → 1, x closure substitution (f : X → Y ) a barren root map two sites to one root swap m with n places a discrete ion (x distinct).
/x : [f ] : 1 : merge : γm,n : Kx :
We shall show that they generate all bigraphs by composition and tensor product. The ?rst two elements generate all wirings, i.e. the nodefree link graphs, as explained in Section 9. The notation [f ] is introduced here for clarity, distinguishing a bigraphical substitution from its underlying functional substitution f . Recall that σ ranges over bigraphical substitutions, and α over renamings. The next three elements generate all placings, i.e. the nodefree place graphs. For example merge m : m → 1, which merges m sites, can be de?ned for all m ≥ 0 by merge 0 merge m+1 = def =
def
1 merge ? (id1 ? merge m ) .
Note that merge 1 = id, and hence merge 2 = merge . Note also that the unit 1 is absent in hard bigraphs B IG h . We use π : m → m to range over permutations, those placings generated by the γm,n . Every isomorphism ι is the product π ? α of a renaming and a permutation. The usual symmetries of a strict symmetric monoidal category are de?ned by extending the place symmetries γm,n as follows: γI,J = γm,n ? idX ?Y , where I = m, X and J = n, Y . Finally, given all these nodefree elements, we require only the discrete ions K x to express everything in B IG . In particular, we can express a discrete atom as Kx ? 1. 64
def
Discrete normal forms The following proposition shows the expressive power of the elementary bigraphs. Further, it shows that every bigraph in B IG can be expressed in a kind of normal form, called discrete normal form (DNF). We shall consistently use D, Q and N to stand for discrete, discrete prime and discrete molecular bigraphs. Proposition 10.1 (discrete normal form) In B IG each bigraph G, discrete D, discrete prime Q and discrete molecule N can be expressed in discrete parts by an equation of the respective following form (recall that α is a renaming, π a permutation): G D Q N = = = = (ω ? idn ) ? D α ? ((Q0 ? · · · ? Qn?1 ) ? π ) (merge n+p ? idY ) ? (idn ? N0 ? · · · ? Np?1 ) ? π (Kx ? idY ) ? Q .
Moreover, the expression is unique up to certain isomorphisms on the parts. By applying the equations to any bigraph expression G, we transform it into DNF; after applying the ?rst two equations once, we apply the last two repeatedly. Note that the unit 1 occurs as a special case of Q when n = p = 0. Axiomatisation We now address the question: What set of axioms is complete in the sense that every valid equation in terms of the elementary bigraphs is provable? The answer turns out to be rather simple; the axioms are shown in the table below. C ATEGORICAL AXIOMS : A ? id = A A ? (B ? C ) = A ? id = A A ? (B ? C ) = (A1 ? B1 ) ? (A0 ? B0 ) = γI, = γJ,I ? γI,J = γI,K ? (A ? B ) = L INK AXIOMS : [f ] ? [g ] = [f ? g ] [f ] ? [g ] = [f ∪ · g] /y ? [f ] = /X [f ] ? (x ? idX ) = [f X ] P LACE AXIOMS : merge ? (1 ? id1 ) = id1 merge ? (merge ? id1 ) = merge ? (id1 ? merge ) merge ? γ1,1 = merge = id ? A (A ? B ) ? C = id ? A (A ? B ) ? C (A1 ? A0 ) ? (B1 ? B0 ) idI idI ?J (B ? A) ? γH,J
(A : H → I, B : J → K )
(f : X → y ) (f : x ? X → Y ) (unit) (associative) (commutative) .
The categorical axioms are standard for a strict symmetric monoidal category. But note that the tensor product is de?ned only when interfaces have disjoint name sets; thus the 65
equations are required to hold only when both sides are de?ned. What is remarkable is that no axioms at all are required on ions, which are the only nonempty elements. Thus bigraphs are a rather free structure. Theorem 10.2 (Complete axiomatisation) Two expressions, constructed from the elements by composition and tensor product, denote the same bigraph in B IG if and only if they are in the congruence generated by the axioms. Proof The proof of the theorem is quite detailed, and we only give a brief outline here. The ‘if’ direction, soundness, just requires an easy proof that each of the axioms is valid. The ‘only if’ direction, completeness, requires two steps. First we show, by induction on the structure of expressions, that the equality between an arbitrary expression and its DNF is provable from the axioms. Second, since DNFs are only unique up to certain isomorphisms, we show that the equality between isomorphic DNFs is also provable from the axioms. Connected normal forms The discrete normal form (DNF) was important for our proof of completeness of the axioms. Moreover, the tensor product is heavily used in our axiomatisation; in particular its bifunctoriality (A1 ? B1 ) ? (A0 ? B0 ) = (A1 ? A0 ) ? (B1 ? B0 ) plays a very important part. On the other hand parallel products like and  , which allow the sharing of names (so do not preserve discreteness) are found very natural in process calculi and in programming; the main purpose of a combinator such as  in the π calculus is to combine expressions that use the same channel, and which may therefore communicate via that channel, as in the reaction rule xy  x(z ).P → {y /z }P . See all the examples in Section 2, where these combinators are used; see also the discussion of parametric reaction rules in Section 12 to follow. In fact we can ?nd a normal form that is in a sense opposite to DNF. Whereas in DNF we pull all wiring to the outermost, we can adopt instead the strategy of pushing it inwards as far as we can. This is achieved by using and  in place of ?, and by pushing closures /Z inwards wherever possible. We call the result connected normal form (CNF); it is embodied in the following proposition, analogous to Proposition 10.1. We use P and M for primes and molecules (not necessarily discrete): Proposition 10.3 (connected normal form) In B IG each bigraph G, prime P and molecule M can be expressed by an equation of the respective following form (recall that σ is a substitution and π a permutation): G P M = (/Z ? idn ) ? (σ ((P0 · · · Pn?1 ) ? π ) = (/Z ? idm+n ) ? (idm  M0  · · ·  Mn?1 ) ? π = (/Z ? id1 ) ? (Kx  idY ) ? P
where, in each case, any member z ∈ Z is a name of at least two members of the ensuing product ( or  ). The names x need not be distinct. Moreover, in each case the expression is unique up to a renaming of Z and certain isomorphisms on the parts. 66
We regard CNF as important for practical use. For example, although we shall not do so, it is not hard to derive the CNF for F ? G, F G or F  G from the CNFs for F and G. We shall also leave open whether there exists a pleasant axiomatisation that uses these parallel products in place of the tensor product.
67
11 Binding bigraphs
The reader who is interested in dynamics rather than in adding binding to bigraphs can safely skip this section and proceed to the dynamic theory in Section 12. He or she will also be able to read Sections 13 and 14 of Part III, interpreting them in pure bigraphs. However, binding is needed for Section 15 on the asynchronous π calculus. In Section 9 we studied a pure form of bigraph in which placing and linking are completely independent structures over a set of nodes. In doing so we found several roles played by a place: it may de?ne a neighborhood within which reactions can be con?ned (e.g. in the ambient calculus); in contrast it may prevent reaction until its boundary is removed (e.g. in the π calculus); it may de?ne the site for a parameter of a reaction rule, thereby determining what may be replicated or discarded. In this section we shall relax the independence of placing and linking by de?ning yet another role for a place: it may de?ne the scope of a bound link. This will allow us to represent, among other things, the input pre?x of the π calculus (which binds a name). The ?rst step we take is to enrich signatures. De?nition 11.1 (binding signature) A binding signature K is like a pure signature (De?nition 6.1), except that the arity of a control K : h → k now consists of a pair of ?nite ordinals: the binding arity h and the free arity k , determining the number of binding and nonbinding ports of any K node. If K is atomic then h = 0. For example, for the π calculus controls, we have get : 1 → 1 and send : 0 → 2 (see Examples 2, 3, 4 and 6). We wish to de?ne a binding bigraph G in terms of an underlying pure one, in which all points linked to a binding port of a node u lie inside u. These points may be inner names as well as ports; to ensure that these inner names transmit the scope discipline to any other bigraph composed at the inner face of G, we enrich interfaces as follows: De?nition 11.2 (binding interface) A binding interface takes the form I = m, k, X , where the width m and the global names X are as before, and the new component k = k0 , . . . , km?1 is a sequence of ?nite ordinals, indexing for each r ∈ m a set {(r, j )  j ∈ kr } of local names; we say these are located at r. Denote the local names of I by X and set X u = X ∪ · X . Then we call I u = u m, X the pure interface underlying I . We call an interface global if all its names are global. Note that we represent local names positionally, but continue to represent global names alphabetically. We are now ready for the main de?nition: De?nition 11.3 (binding bigraphs) A (concrete) binding bigraph G : I → J consists of an (underlying) pure bigraph Gu : I u → J u with extra structure as follows. Declare its binders to be the binding ports of its nodes together with the local names of its outer face J . Then G must satisfy the following: S COPE RULE: If p is a binder located at a node or root w, then every peer p of p must be located at a place w (a site or a node) such that w <Gu w. 68
In the precategory ?B BG (K) of (concrete) binding bigraphs over K, composition and identities are de?ned as for the underlying pure bigraphs; they are easily found to respect the scope rule. The forgetful functor U : ?B BG (K) → ?B IG (K) forgets binding; it sends each I to I u and each G to Gu . The analogous de?nition holds also for hard binding bigraphs ?B BG h (K). As for pure bigraphs, a link is open if it is a name, otherwise closed. In binding bigraphs we have a further distinction: a link is bound if it contains a binder, otherwise free. These terms also extend to the points in the link. The scope rule ensures that every bound link in G : I → J has exactly one binder and that all global inner names are free; local inner names (i.e. local names of I ) can be free or bound. Note that, in considering names, the global/local distinction is with reference to interfaces, while the free/bound distinction is with reference to bigraphs. For example, for G : I → J , an inner name of G may be a local name in I but free in G. We shall say that a bigraph G : I → J is free if its outer face J is global, i.e. every outer name of G is free. To avoid confusion, note that G itself may still not be a pure bigraph, i.e. it may have closed links that are bound. Free bigraphs will be important in what follows; their characteristic is that no bound point of G can become free in F ? G, for any F . We shall now embark on recording or verifying several properties of binding bigraphs, and how each relates to the corresponding property in Section 9 for pure bigraphs. Where the correspondence is easy we do not give a new de?nition, proposition etc; we merely cite the corresponding one for pure bigraphs. In many cases the correspondence is illuminated by an attribute of the forgetful functor U . Let us recall the relevant attributes. First, U is faithful but not full; that is, restricted to each particular homset ?B BG (I, J ) or ?B BG h (I, J ) it is injective, but not surjective. A functor can be characterised by the properties that it preserves or re?ects. Letting ? range over arbitrary commuting diagrams, a functor F is said to preserve a property Φ of diagrams if Φ(?) ? Φ(F (?)), and to re?ect Φ if Φ(F (?)) ? Φ(?). An interesting example will be that U preserves the RPO property but does not re?ect it. This means that to ?nd an RPO in binding bigraphs we cannot take any U preimage of an RPO in pure bigraphs; but we shall ?nd that one particular preimage, unique up to iso, is indeed an RPO. For the remainder of this section we shall extend to binding bigraphs several properties of pure bigraphs, in the order in which they were treated in Section 9. Binding bigraphs: Elementary notions isomorphisms (Proposition 9.2) An iso ι : m, k, X → m, , Y of binding bigraphs combines a permutation π : m → m of places with a bijection X → Y of global names and, for each place r ∈ m, a bijection kr → π(r) between the local names at corresponding places. U both preserves and re?ects isos. 69
tensor product (De?nition 9.3) The tensor product of interfaces I = m, k, X and J = n, , Y , where X and Y are disjoint, is I ? J = m + n, k , X ∪ · Y . The tensor product of two binding bigraphs Gi : Ii → Ji (i = 0, 1), where I0 ? I1 u and J0 ? J1 are de?ned, is just Gu 0 ? G1 , but after disjoining the local inner and outer names names of G1 from those of G0 . U neither preserves nor re?ects tensor product. This is essentially because of the partial nature of the tensor; a more standard categorical tensor product would be total, because it would disjoin name sets before taking their product. This would complicate our application of bigraphs to process calculi. However the following shows that the tensor is wellbehaved for binding bigraphs: wide monoidal (Theorem 9.4) ?B BG (K) and ?B BG h (K) are wide monoidal precategories. epis and monos (Proposition 9.5) A binding bigraph is epi (resp. mono) iff its underlying pure bigraph is epi (resp. mono). U both preserves and re?ects epis and monos. This concludes the elementary notions for binding bigraphs. We now move on to the central properties of relative and idem pushouts. To ensure that RPOs and IPOs exist we have to take a little more care, but can still rely mostly on the corresponding results for pure bigraphs. In what follows we shall use the terms binding and pure RPO to mean RPOs in binding and in pure bigraphs respectively; the results apply to ?B BG h and ?B IGh and well as to ?B BG and ?B IG . We shall also talk of binding IPOs and pure IPOs. Construction 11.4 (building a binding RPO) Let D : I → K be a bound for A : H → I in binding bigraphs. We wish to build in a binding RPO (B : I → I, B : I → K ) . We ?rst build a pure RPO (B , B ) for Au to Du , using the separate constructions for place graphs and link graphs (Constructions 7.7 and 8.8). Let I = m, X be the interface of the RPO, i.e. the inner face of B . We shall build the required (B, B ) with interface I = m, k, X so that for some link isomorphism ι : I → I u in ?B IG (see the diagram) B u = ι ? B and B u ? ι = B . In general, several such triples exist as bounds for A relative to D; they vary with the chosen isomorphism ι, because for a given name x ∈ X we may choose ι(x) either to be a global name in X or to be a local name located at some place r ∈ m. They will not all be binding RPOs; this amounts to saying that U does not re?ect the RPO property from pure to binding bigraphs.
70
BINDING BIGRAPHS
PURE BIGRAPHS
D0 B0
I0
B
I
D1 B1
I1
u I0
u D0 u B0
B ι
I
Bu
Iu
u B1
u D1
B0 Au 0
B1 Au 1
u I1
A0
A1
In fact we shall choose I and ι so that B and B obey the scope rule, and also — subject to that constraint— so that I contains as many local names as possible. By Construction 8.8 (and using its notation), each x ∈ X is linked in Bi to one or more u u names xi ∈ Xi (i = 0, 1), where Xi is the name set of Au . If any such name xi is a global name of Ai then we choose ι(x) to be global in I u — i.e. a member of X . Otherwise every such xi is a local name of Ai , so we choose one of them, located at some site s in Ii ; we then choose ι(x) to be located at the unique r ∈ m such that s < r in Bi . This determines both (B, B ) and I up to isomorphism. Note that the scope rule on A ensures that the de?nition of r is independent of the choice of local name xi linked to x. The construction is therefore well de?ned. Proposition 11.5 (binding RPOs) A binding RPO for A to D is provided by Construction 11.4, via Corollary 9.6. Proof Let (B, B ) be as in the construction. Note that (B, B ) is a pure RPO for Au to Du . Let (C, C ), with interface J , be any bound for A relative to D. We must ?nd a unique mediating arrow C : I → J .
u D0 u C0
u I0
u
Bu
u B0
Cu
Ju
u D1 u C1 u B1
u I1
C
Iu
Au 0
u
Au 1
Now (C, C ) , with interface J u , is a bound for Au relative to Du . Hence there is a unique mediating arrow C as shown in the diagram. We now claim that C obeys the scope rule. This can be shown by a case analysis for the bound points in C , and depends on three facts: ?rst, that B u and C u obey the scope rule; second, that each u u name x ∈ I u is linked in Bi (i = 0 or 1) to some name xi ∈ Ii ; third, that by construction x is local iff all u such xi are local. It follows that C = C for some mediating arrow C : I → J ; also that this is unique, since C : I u → J u is a unique mediating arrow and U is a faithful functor. This completes the proof. 71
Corollary 11.6 (preserving RPOs) The forgetful functor U preserves RPOs; that is, u if (C, C ) is a binding RPO for A to D then (C, C ) is a pure RPO for Au to Du . Proof Assume the binding RPO (C, C ) with interface J . Let (B, B ), with interface I , be the binding RPO built for A to D by Construction 11.4. Then, since RPOs are unique up to isomorphism, there is a mediating iso ι : I → J between these two RPOs. u Also from the construction we know that (B, B ) is a pure RPO for Au to Du , and we u have a mediating iso ιu : I u → J u between this RPO and the relative bound (C, C ) . u But isomorphism preserves the RPO property, so (C, C ) is also a pure IPO. Let us now turn to binding IPOs. Their construction —unlike RPOs— depends upon a set of consistency conditions, and we ?nd that one extra condition is needed in binding bigraphs. Then we show how to construct a family of binding IPOs for any consistent pair A : H → I , based upon the corresponding construction of pure IPOs. Finally we check that this indeed yields all binding IPOs for A, up to isomorphism. De?nition 11.7 (consistency conditions) Let A be a pair of binding bigraphs with common inner face. We de?ne three conditions for A to be consistent:
CP CL CB
Conditions CP 0 – CP 2 for the underlying place graphs (De?nition 7.9); Conditions CL 0 – CL 2 for the underlying link graphs (De?nition 8.10); If p is a shared point, bound and closed in Ai but open in A? , then A? (p) is a local name.
To see the need for CB, suppose that B is a bound for A; let A0 (p) = e be bound and closed, and A1 (p) = x, a name. Then (B0 ? A0 )(p) = e, hence also (B1 ? A1 )(p2 ) = e; thus B1 (x) = e, and the scope rule for B1 requires x to be local. As we did for place graphs and link graphs, we ?nd that these conditions are necessary and suf?cient for the existence of both bounds and IPOs in binding bigraphs. We can also characterise the binding IPOs in terms the pure ones. We deal with these in a single theorem as follows (note that the suf?ciency of the consistency conditions follows from clause (2) of the theorem): Theorem 11.8 (binding IPOs) (1) The consistency conditions CP, bounds in binding bigraphs.
CL
and
CB
are necessary for the existence of
(2) Let A satisfy the consistency conditions and Au have a pure IPO B . Then A has a binding IPO B , with B u isomorphic to B . (3) If A has a binding IPO B , then Au has a pure IPO B u . Proof (1) Suppose B bounds A in binding bigraphs. Then B u bounds Au in pure bigraphs; so immediately CP and CL hold, since they are necessary for a bound in place graphs and link graphs respectively. The condition CB can be established by an argument based on the preceding discussion.
72
(2) Suppose that A satis?es the consistency conditions, and Au has a pure IPO B . (Note that conditions CP and CL ensure at least one such IPO.) We construct a binding bigraph B and a pure isomorphism ι such that B u = ι ? B ; the construction proceeds as in Construction 11.4 but uses condition CB on A. Then B u is also a pure IPO, hence u (B, id) is an RPO for Au to B u . Therefore, using the construction and corollary in this special case, we conclude that B is a binding IPO for A. (3) Finally, the third result is a special case of Corollary 11.6. Thus, when the pair A of binding bigraphs is consistent, there is a precise correspondence between its binding IPOs and the pure IPOs of Au . We now lift further static properties to binding bigraphs, especially IPO properties. Note especially that pure bigraphs are a subprecategory of binding bigraphs: those without binders. Although we shall not labour the point, our theory for binding bigraphs is a conservative extension of that for pure bigraphs; that is, every property of binding bigraphs, when restricted to pure ones, coincides with the corresponding property of the latter as previously de?ned. Binding bigraphs: Further properties special IPOs (Propositions 9.8 and 9.9, Corollary 9.10 and Proposition 9.11) The containment pushout, and the tensoring of two IPOs with disjoint supports, hold unchanged in binding bigraphs. Also, the notion of a lean bigraph —one with no idle edges— is unchanged, because of course an idle edge cannot be bound, so properties relating IPOs to idle edges and leanness are unchanged. It follows that leansupport equivalence ( ), which extends support equivalence ( ) by discarding idle edges, also unchanged. This leads to the following: abstract bigraphs (De?nition 9.12) An abstract binding bigraph is a leansupport equivalence class of concrete ones. For any signature K this leads to the category B BG (K), and the quotient functor [[ · ]] : ?B IG (K) → B IG (K). Similarly for hard binding bigraphs we have [[ · ]] : ?B IG h (K) → B IGh (K).
ground bigraphs As before, a ground bigraph is one with inner face .
interfaces The general form of interface is I = m, k, X . If it is global we may write it as m, X ; if it has no places (so m = 0) we may write it as X ; if it has no names we may write it as m. I is prime if it has width m = 1, i.e. I = 1, (k ), X ; then we may write it as (k ), X , or as (k ) if X = ?, or as X if k = 0. Note that X , with unit width, differs from X with zero width. wirings As before, a wiring is a bigraph whose faces have zero width. Thus it has no nodes, and takes the form ω : X → Y . We retain our notations /X and y /x for closure and substitution of global names. prime bigraphs A bigraph G is prime if its outer face is prime and its inner face has no global names; thus G : m, k, ? → ( ), X . Note particularly that it may have local inner names. An important prime is the datum x : (k ) → x , which links k local inner names one by one to k free names x = x1 , . . . , xk . 73
abstraction Dual to the datum is a the new operation of abstraction on primes P . For P : I → (k ), x ∪ · X we may form the abstraction (x) P : I → (1+k ), X , which turns a free name of P into a local name. (This cannot violate the scope rule, because P has no global inner names.) If x = x1 , . . . , xk is a vector of distinct names we write (x) P for (x1 ) · · · (xk ) P ; then we have the dual properties ( x ? idX ) ? (x) P = P and (x) x = id(k) . discreteness The notion of discreteness becomes more subtle for binding bigraphs. Recall that a link is free if it is not bound by a binder — a local name or a binding port; also that a point is a port or an inner name. A binding bigraph is discrete if every free link is an (outer) name and has exactly one point. This is a conservative extension of discreteness for pure bigraphs; it imposes no constraint on bound links. ions, atoms, molecules The de?nition of an ion must now allow for binding. For any nonatomic control K : h → k and sequence x of k distinct names we de?ne the free discrete ion Kx : (h) → x whose h local inner names are bound by a single K node. Then for any prime discrete P with outer face (h), Y , where Y is disjoint from the names x, we call (Kx ? Y ) ? P a free discrete molecule. For atomic K a free discrete atom is just Kx : → x as before. An arbitrary ion, molecule or atom is got by imposing wiring and abstracting free names. This concludes our second list of properties for binding bigraphs, including a taxonomy which is a conservative extension of the taxonomy of pure ones. Finally we (conservatively) extend the important operations and decompositions from pure to binding bigraphs, and add some new ones. Binding bigraphs: Operations and decompositions parallel product (De?nition 9.13, Proposition 9.14) Extending the previous de?nition, the parallel product of two interfaces Ji = ni , ki , Yi (i = 0, 1) keeps their local names disjoint but may share their global names: J 0 J 1 = n 0 + n 1 , k0 k1 , Y 0 ∪ Y 1 . We de?ne parallel product on binding bigraphs by the equation in Proposition 9.14. prime product (De?nition 9.15) Extending the previous de?nition, the prime product of two prime interfaces is k, X  , Y = k , X ∪ Y . The expression of the prime product of two prime binding bigraphs in terms of their parallel product is just as before.
def def
74
underlying discrete bigraph (Proposition 9.16) The previous unique decomposition of any bigraph G in terms of its underlying discrete one is extended almost exactly: G = (ω ? idI ) ? D ,
where ω is a wiring, D is discrete and I has no free names. As before, this is called the discrete normal form (DNF) of G.
synthesis and analysis of discrete bigraphs (Proposition 9.17) Again the discrete binding bigraphs form a monoidal subprecategory. The factorisation of a discrete D : m, k, X → n, , Y into a tensor product of prime discrete factors is as before (where of course k and were essentially zerovectors), and the IPO properties of discrete bigraphs are as before — but replacing the wiring component ω ? idn by ω ? idI where I has no free names. instantiation (De?nition 9.18) We replace instantations :: m → n for pure bigraphs by instantations :: I → J for binding bigraphs, where the interfaces I = m, k and J = n, have no free names. The instantiation is again determined by the underlying function : n → m, which must also satisfy j = k (j ) for all j ∈ n. For any X , this condition allows the map : Gr(X ? I ) → Gr(X ? J ) to be de?ned just as before in terms of DNF, but with wiring component ω ? id n replaced by ω ? idI where I has no free names. wiring an instance (Proposition 9.19) The proof that (ωa) = ω (a) for all instantiations and wirings ω proceeds as before. wiring a product (Proposition 9.20) The proofs that ω (F G) = ωF ωG and that ω (F  G) = ωF  ωG proceed as before. instantiating a product (Proposition 9.21) The proof proceeds as before that if the ai are prime, with total name set Y , then (a0 where bj a
(j )
···
am?1 ) = Y
b0
···
bn?1
for j ∈ n.
instantiating with prime component (Proposition 9.22) This proposition asserts that if G has prime inner face I and a, b : I are two prime agents, then the two instances (G ? a) and (G ? b) are similar, in the sense that one can be transformed into the other by replacing several occurrences of a by b. This property is vital for proofs of bisimilarity, and its proof proceeds as for pure bigraphs. This concludes our extension of operations and decompositions to binding bigraphs. We shall not re?ne the algebraic theory of Section 10 for binding bigraphs. We conjecture that the de?nitions and results need only minor adjustments, chie?y concerning data and abstractions, but we do not need them for this paper. 75
To conclude: We have established the static theory of binding bigraphs as a conservative extension of that for pure bigraphs. The re?nements were mostly minor; only with RPOs and IPOs was a nontrivial extra argument needed. In later sections, where we develop the dynamics of binding bigraphs, we shall often appeal to a de?nition or result about pure bigraphs that has been extended or re?ned here to binding bigraphs; then we shall add a superscript ‘b’ to the reference, for example ‘De?nition 9.18 b ’.
76
12 Reactions and transitions
In Section 11 we ensured the existence of RPOs in binding bigraphs, and de?ned some useful structural properties such as discreteness. We are now ready to specialise the de?nitions and theory for wide reactive systems (WRSs) in Section 4, to obtain bigraphical reactive systems (BRSs). We do it here for binding bigraphs. The binding BRSs form the objects of a category whose arrows are WRS functors; the pure BRSs constitute a subcategory. Readers who have omitted reading Section 11 on binding bigraphs may interpret this whole section in terms of pure bigraphs; to do this, simply read ?B IG and B IG for ?B BG and B BG , and ignore the superscript ‘b’ on references to de?nitions and results. To de?ne the notion of BRS, the main remaining step is to de?ne parametric reaction rules over (binding) bigraphs, and the main result we obtain is a congruence theorem —both for ?B BG and for ?B BG h — which we are then able to transfer to abstract bigraphs in B BG and B BG h . Let us consider reaction rules for a BRS, recalling both the abstract De?nition 4.3 for WRSs and the examples in Section 2. What should the parameters Par(I ) be, and what should the transform maps trans : Par(I ) → Gr(I ) be? Parameters will be discrete; recall from Section 11 that a binding bigraph is discrete if every free link is open (i.e. a free name) and has exactly one point. This does not limit the applicability of the reaction rules, because from Proposition 9.16b we can obtain everything by combining discreteness with wiring; moreover, the technical development is smoother with discrete parameters. For the transforms, we must allow for both replication and discard of parameters, so we use the instantiations of De?nition 9.18b . De?nition 12.1 (reaction rules for bigraphs) A ground (reaction) rule is a pair (r, r ), where r and r are ground with the same outer face. Given a set of ground over agents is the least such that D ? r D ? r for rules, the reaction relation each active D and each ground rule (r, r ). A parametric (reaction) rule has a redex R and reactum R , and takes the form ( R : I → J, R : I → J, )
where the inner faces I and I have widths m and m but no free names.8 The third component :: I → I is an instantiation (De?nition 9.18b ). For every X and discrete d : X ? I the parametric rule generates the ground reaction rule ( (idX ? R) ? d, (idX ? R ) ? (d) ) . Note that as d = d0 ? · · · ? dm?1 is discrete (where each di is prime) the instance (d) takes the form (d) = X d (0) · · · d (m ?1) : X ? I .
Thus, if some di occurs more than once in the instance, the bound names of each copy may be treated differently by the reactum R . On the other hand, the free names of d are exported to the context that surrounds the reaction.
8 For
pure bigraphs we shall have I = m and I = m ; then the instantiation is
:: m → m .
77
It follows from this remark that requiring d to be discrete does not limit reaction, because the outer context can impose any wiring present in a nondiscrete parameter. However, it does limit transitions, essentially because the parameter part Lpar of a label L re?ects the discreteness of d. Without the limitation, the parameter underlying a transition a L λ a might impose an arbitrary substitution on the part of a shared with it, exceeding the role a parameter should play. The function underlying an instantiation need not be injective, so it allows for replication of parameters in the reactum. Similarly it need not be surjective, so it allows for the discard of parameters. De?nition 12.2 (bigraphical reactive system) A bigraphical reactive system (BRS) over a signature K consists of ?B BG (K) equipped with a set ?Reacts of reaction rules closed under support equivalence ( ). We denote it —and similarly for ?B BG h (K)— by ?B BG (K, ?Reacts) . Proposition 12.3 (a BRS is a WRS) Every bigraphical reactive system is a wide reactive system. Proof First, it is easy to see that ?B BG (K) and ?B BG h (K) are wide precategories, for any signature K. The support of a bigraph is the disjoint sum V + E of its node set and edge set, the width of an interface m, k, X is m, and we have already discussed the width of a bigraph. The other details are easy to check. For the reaction rules, their parameters Par(I ) at any interface are just the discrete agents d : I . The activity map act is given by act(C ) = {s ∈ m  ?v. v >C s ? v active} . Lastly the transform of each reaction rule is provided by its instantiation . This result ensures that BRSs inherit from WRSs the de?nition of transitions a L λ a based upon IPO pairs, and the standard transition system ST induced from its reaction rules. They also inherit the de?nition of bisimilarity, and so we have the following immediate corollary of Theorem 5.5: Corollary 12.4 (congruence of wide bisimilarity) In any concrete BRS equipped with the standard transition system ST, wide bisimilarity of agents is a congruence. We would now like to transfer ST, together with its congruence property, to the abstract BRS B BG (K,Reacts), where B BG (K) is de?ned by the quotient functor [[ · ]] of De?nition 9.12b , and Reacts is obtained from ?Reacts also by [[ · ]]. (Similarly for B BGh .) Now recall that this functor, the quotient by leansupport equivalence ( ), is a little coarser than the quotient by support equivalence ( ), because it discards idle edges. To transfer the congruence result we must prove that respects ST. For this purpose, we have to impose a slight constraint upon the reaction rules ?Reacts, namely that every redex is lean — i.e., recalling Section 9, it has no idle edges. We then deduce the crucial property of leansupport equivalence: 78
def
Proposition 12.5 (transitions respect equivalence) In a concrete BRS with all redexes lean, equipped with ST: (1) In every transition label L, both components are lean. (2) Transitions respect leansupport equivalence ( ) in the sense of De?nition 5.2. That is, for every transition a L λ a , if a b and L M where M is another label with M ? b de?ned, then there exists a transition b M λ b for some b such that a b. Proof For the ?rst part, use Proposition 9.11b (1) and the fact that every discrete agent is lean. For the second part, use Proposition 9.11b (2); the assumption that each redex is lean ensures that it cannot share an idle edge with the agent a. We are now ready to transfer the congruence result of Corollary 12.4 from concrete to abstract BRSs. The following is immediate by invoking Theorem 5.7: Corollary 12.6 (behavioural congruence in abstract BRSs) Let ?A be a concrete BRS with all redexes lean, equipped with ST. Let [[·]] : ?A → A be the quotient functor by leansupport equivalence. Then (1) a ? b in ?A iff [[a]] ? [[b]] in A. (2) Bisimilarity is a congruence in A. This concludes the elementary theory of bigraphical reactive systems. In Part III we shall re?ne these results for two important classes of BRS, thereby obtaining more tractable transition systems. Part III ends by applying the results to a bigraphical presentation of an asynchronous π calculus, exactly recovering its standard behavioural theory.
79
80
Part III
Specialisation and Application
The class of simple BRSs is introduced; they include models of both the π calculus and the mobile ambient calculus. Their structural properties allow us to simplify the transition systems that were derived more generally in Part II. In particular, we prove an important adequacy theorem; it asserts that in the derived transition system for a simple BRS it is enough to con?ne attention to those transitions a L λ a in which the agent a contributes nontrivially to the underlying reaction. We then narrow the simple BRSs still further, to the basic BRSs. The purpose is to obtain a nice characterisation of the labels involved in the derived transition systems; this result is veri?ed using the techniques of relative pushouts. We proceed to encode a ?nite asynchronous π calculus as a basic BRS. The ?rst result —independently of dynamics— is that two processes are structurally congruent if and only if their representing bigraphs coincide. Then it turns out that the labels of the derived transition system correspond well with the standard labels. Finally, we prove that the bisimilarity induced by the bigraph representation of this calculus coincides with two standard congruences, strong bisimilarity and strong barbed bisimilarity. This supports the claim that bigraphical systems are consistent with previous work in process calculi. The ?nal section explores several lines for further research, including suggestions both for varying the technical presentation of bigraphs and for enriching their domain of application.
81
13 Simple BRSs and adequacy
We shall now specialise our theory by de?ning the simple BRSs, whose redexes have certain structural properties. As predicted in Section 5, working in ?B BG h we are then able to show that engaged transitions on free prime agents are adequate for the standard transition system ST. This yields a tractable transition system, which we can then transfer to abstract BRSs over B BG h , yielding a bisimilarity that is a congruence. The class of simple BRSs admits both the π calculus and the ambient calculus. Recall from Section 8 that a link is open if it belongs to the outer face, otherwise closed, and that these properties are inherited by the points of the link. Recall also from Section 11 that a bigraph is free if every open link is free. De?nition 13.1 (simple BRSs) Call a bigraph open if every free link is open. Call it guarding if no inner name is open, and no site has a root as parent. Call it simple if it has no idle names and no barren regions; no two inner names are peers, and no two sites are siblings; it is free, prime, open and guarding.
A BRS is simple if all its redexes are simple. The ?rst two conditions are easy to accept; indeed, we see no purpose for a redex which fails them. In a concrete BRS they equate respectively to the epi and mono properties. However, we de?ne simpleness as above because we would like it to be preserved by the quotient functor [[ · ]] (which preserves neither epis nor monos). Again, guarding is an easy condition to accept. So the main simpleness constraints are freeness, primeness and openness. It remains to be seen how far we can relax these three constraints without weakening our results. We give without proof three easy properties of openness: Proposition 13.2 (openness properties) (1) A composition F ? G is open iff both F and G are open. (2) Every open bigraph is also lean (i.e. has no idle edges). (3) If B is an IPO for A and A1 is open, then B0 is open. For the rest of this section we are concerned only with hard BRSs, i.e. over ?B BG h (K) or B BGh (K) for some signature K. To see where simpleness is used in our adequacy proof we shall underline each use of a simpleness condition. The ?rst consequence of simpleness in a hard concrete BRS is that, if we limit consideration to free agents, we can often avoid the elisions that arise in IPOs and RPOs: Proposition 13.3 (transition pushouts) In a hard concrete BRS, if the IPO pair underlying a standard transition of a free agent has a simple redex then its main rectangle and righthand square are pushouts.9
9 It is easy to show that the lefthand square need not be a pushout; in fact it may be an elisive IPO. This arises because d, though discrete, may have idle bound names. This cannot happen in pure bigraphs, so in that case the lefthand square is indeed a pushout.
82
Proof The typical IPO pair underlying a transition a L λ a is shown in the diagram below. Let r = (idW ? R) ? d be the ground redex. It will be enough to show that in the two IPOs, (L, D) for (a, r) and (Lred , D) for (D par , idW ? R), there can be no elisions. There can be no place elisions because we are working with hard place graphs, so we need only consider link elisions. In the ?rst case, since R is open and every parameter d (being discrete) is open, then so are r and L by Proposition 13.2. So any elision of a name x of a would be to a bound closed link in L, violating the scope rule for L because x is free. On the other hand no names of r can be elided, since it has no idle names because R —and hence r— is epi. The argument in the second case is similar except that, unlike a, D par may have bound names. But since a is free, and the left square is an IPO, any outer name in D par can only be bound if it is linked by D par to a bound name of d; therefore it is a busy name and cannot be elided. The rest of the argument for the second case is as for the ?rst case, so we are done. Lpar a d Lred Dpar idW ? R D
We shall also need a speci?c property of transitions with simple redexes: Lemma 13.4 In a hard concrete BRS, let the IPO pair underlying a standard transition (as shown) have a simple redex R. Suppose that D par ∩R = ?. Then D par = D ?idI for some D , up to isomorphism, where I is the inner face of R. Proof We ?rst prove that, for each name y (necessarily local) in I , there is a local outer name z of D par such that D par (y ) = z and y has no peers in D par . Since R is guarding and open, R(y ) = p for some binding port p, so by commutativity (Lred ? Dpar )(y ) = p. But p is not a port in D par by assumption, so for some outer name z we have D par (y ) = z and Lred (z ) = p. Also p is binding, so z is local by the scope rule for Lpar . Now suppose y has a peer, i.e. D par (q ) = z for some point q = y . Then we have red (L ? Dpar )(q ) = p, whence also R(q ) = p. If q is an inner name this contradicts R mono; if q is a node port then q is also in R, contradicting D par  ∩ R = ?. Hence no such q can exist. The result follows by a similar argument showing that each site s of I has a root as parent and has no siblings. We now turn to engaged transitions, especially those involving free prime agents. De?nition 13.5 (engaged transitions) A standard transition of a is said to be engaged if it can be based on a reaction with redex R such that a ∩ R = ?. We denote by FPE the transition system of free prime interfaces and engaged transitions. We write ?FPE for ?FPE , bisimilarity for FPE relative to ST. ST 83
Now we would like to prove that ?FPE is adequate for standard bisimilarity (De?nition 5.8), i.e. ?FPE = ? restricted to free prime interfaces; for then, when a and b are free prime agents, to establish a ? b we need only prove a ? FPE b. For this purpose, we need only match each engaged transition of a (resp. b) by an arbitrary transition of b (resp. a). This is a lighter task than matching all transitions. In proving that a ?FPE b implies a ? b for free prime a and b, we have to show how b can match the nonengaged transitions of a, and the antecedent only tells us how to match the engaged ones. However, it turns out that a nonengaged transition of a can be suitably matched by any b (whether or not a ? FPE b). This is intuitively not surprising, because a contributes nothing to such a transition, so replacing it by b should not prevent the transition occurring. We begin with a lemma that justi?es this intuition, even in the case that a may contribute to the parameter of the reaction. Lpar a d Lred Dpar idW ? R D
Lemma 13.6 In a hard concrete BRS let a be free and prime, with a standard transition a L λ a based upon the reaction rule (R, R , ), with underlying IPO pair as shown in the above diagram. Let R be simple, and assume that a∩R = ? but that a∩d = ?. Then a ? d, and moreover Lred and a can be expressed to within isomorphism in the form Lred = idW ? R and a = (idW ? R ) ? (Lpar ? a) .
Proof From Lemma 13.4 we ?nd that D par takes the form D par = D ? idI up to isomorphism, where D has domain W (with zero width). We now claim that D has no nodes. Fo