5 - Bigraphical structure

Summary

This chapter refines the structural analysis of concrete bigraphs. In Section 5.1 we establish some properties for concrete bigraphs, including RPOs. In Section 5.2 we enumerate all IPOs for a given span. Finally, in Section 5.3 we show that RPOs do not exist in general for abstract bigraphs.

RPOs for bigraphs

We begin with a characterisation of epimorphisms (epis) and monomorphisms (monos) in bigraphs. These notions are defined in a precategory just as in a category, as follows:

Definition 5.1 (epi, mono) An arrow f in a precategory is epi if g ° f = h ° f implies g = h. It is mono if f ° g = f ° h implies g = h. 〉

Proposition 5.2 (epis and monos in concrete bigraphs)A concrete place graph is epi iff no root is idle; it is mono iff no two sites are siblings. A concrete link graph is epi iff no outer name is idle; it is mono iff no two inner names are siblings.

A concrete bigraph G is an epi (resp. mono) iff its place graph G^Pand its link graph G^Lare so.

EXERCISE 5.1 Prove the above proposition, at least for the case of epi link graphs. Hint: Make the following intuition precise: if G and H differ then, when composed with F, the difference can be hidden if and only if F has an idle name. 〉

The proposition fails for abstract bigraphs, suggesting that concrete bigraphs have more tractable structure. We shall now provide further evidence for this by constructing RPOs for them.