The Main Question

The purpose of this book is to use the tools of mathematical logic to study certain problems in foundations of mathematics. We are especially interested in the question of which set existence axioms are needed to prove the known theorems of mathematics.

The scope of this initial question is very broad, but we can narrow it down somewhat by dividing mathematics into two parts. On the one hand there is set-theoretic mathematics, and on the other hand there is what we call “non-set-theoretic” or “ordinary” mathematics. By set-theoretic mathematics we mean those branches of mathematics that were created by the set-theoretic revolution which took place approximately a century ago. We have in mind such branches as general topology, abstract functional analysis, the study of uncountable discrete algebraic structures, and of course abstract set theory itself.

We identify as ordinary or non-set-theoretic that body of mathematics which is prior to or independent of the introduction of abstract set-theoretic concepts. We have in mind such branches as geometry, number theory, calculus, differential equations, real and complex analysis, countable algebra, the topology of complete separable metric spaces, mathematical logic, and computability theory.

The distinction between settheoretic and ordinary mathematics corresponds roughly to the distinction between “uncountable mathematics” and “countable mathematics”. This formulation is valid if we stipulate that “countable mathematics” includes the study of possibly uncountable complete separable metric spaces.

In this chapter we study dynamics at the general level of s-categories. It is based upon Section 2.2 and Chapter 4, and is independent of the intervening work on bigraphs.

Recall from Chapter 2 the distinction between concrete and abstract bigraphs; the former have their nodes and edges as support, while the latter have no support. In s-categories, this distinction is less sharp; an spm category is just an s-category with empty supports. Much of the work of this chapter therefore applies to both. However, when we introduce behavioural equivalence in Section 7.2, we first make sure it is robust (i.e. that the equivalence is preserved by context) in the case where the s-category possesses RPOs; we are then able to retain this robust quality when the s-category is quotiented, or abstracted, in a certain way – even if RPOs are thereby lost.

We begin in Section 7.1 with a notion of a basic reactive system, based upon an s-category equipped with reaction rules. This determines a basic reaction relation which describes how agents may reconfigure themselves. We refine this definition to a wide reactive system, with a notion of locality based on the width of objects in a wide s-category, introduced in Definition 2.14. We are then able to describe where each reaction occurs in an agent, and thus to define a wide reaction relation that permits reactions to occur only in certain places.

In Section 7.2 we introduce labelled transition systems, which refine reactive systems by describing the reactions that an agent may perform, possibly with assistance from its environment.

In Section 2.1 we define bigraphs formally, together with fundamental ways to build with them.

In Section 2.2, using some elementary category theory, we introduce a broader mathematical framework in which bigraphs and their operations can be expressed. The reader can often ignore this generality, but it will yield results which do not depend on the specific details of bigraphs.

In Section 2.3 we explain how the concrete place graphs, link graphs and bigraphs over a basic signature each form a category of a certain kind. We then use the tools of the mathematical framework to introduce abstract bigraphs; they are obtained from the concrete ones of Section 2.1 by forgetting the identity of nodes and edges.

Throughout this chapter, when dealing with bigraphs we presume an arbitrary basic signature Κ.

Bigraphs and their assembly

Notation and terminology We frequently treat a natural number as a finite ordinal, the set of all preceding ordinals: m = {0, 1, …, m − 1}. We write S # T to mean that two sets S and T are disjoint, i.e. S ∩ T = ∅.

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 GPand its link graph GLare 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.

In this chapter we shall see how our dynamic theory for a nice BRS can be applied to recover the standard dynamic theory of CCS.

Section 10.1 deals mainly with the translation of finite CCS into bigraphs, covering both syntactic structure and the basic features of reaction. It begins with a summary of all work done on CCS in previous chapters, in order to gather the whole application of bigraphs to CCS in one chapter. It then presents the translation into bigraphs, which encodes each structural congruence class of CCS into a single bigraph. It ends with the simple result that reaction as defined in CCS terms correponds exactly to reaction as defined by bigraphical rules.

Based upon this summary, Section 10.2 lays out the contextual transition system derived for finite CCS by the method of Chapter 8, recalling that its bisimilarity is guaranteed to be a congruence. This congruence is finer than the original bisimilarity of CCS. This is because the original is not preserved by substitution; on the other hand, our derived contextual TS contains transitions that observe the effect of substitution on an agent, and this yields a finer bisimilarity that is indeed a congruence. By omitting the substitutional transitions from the contextual TS, we then obtain a bisimilarity that coincides with the original.

This contextual TS is more complex than the original raw one, since its labels are parametric. But we are able to reduce it to a smaller faithful contextual TS whose labels are no longer parametric, and this corresponds almost exactly with the original raw TS for CCS.

In this chapter we show how bigraphs can be built from smaller ones by composition, product and identities. In this we follow process algebra, where the idea is first to determine how distributed systems are assembled structurally, and then on this basis to develop their dynamic theory, deriving the behaviour of an assembly from the behaviours of its components.

This contrasts with our definition of a bigraph as the pair of a place graph and a link graph. This pairing is important for bigraphical theory, as we shall see later; but it may not reflect how a system designer thinks about a system. The algebra of this chapter, allowing bigraphs to be built from elementary bigraphs, is a basis for the synthetic approach of the system-builder.

Our algebraic structure pertains naturally to the abstract bigraphs Bg(Κ). Much of it pertains equally to concrete bigraphs. Properties enjoyed exclusively by concrete bigraphs are postponed until Chapter 5.

Elementary bigraphs and normal forms

Notation and convention The places of G: 〈m, X〉 → 〈n, Y〉 are its sites m, its nodes and its roots n. The points of G are its ports and inner names X. The links of G are its edges and outer names Y; the edges are closed links, and the outer names are open links. A point is said to be open if its link is open, otherwise it is closed. G is said to be open if all its links are open (i.e. it has no edges).