On non-well-founded multisets: Scott Collapse in the Multiworld

Giovanna D’Agostino, Albert Visser

Abstract

We define the class of non well-founded multisets and provide three different descriptions of this class: as collapsed multigraphs, as trees, or as infinitary formulae. Our major tool in this task is Scott-bisimulation, which was originally conceived to give an axiomatization of non well-founded multisets. The natural generalization of Scott-bisimulation from graphs to multigraphs allows us to have a theory of multigraph decorations and a notion of collapse in complete analogy with the theory of graph decorations and collapse given by the non well-founded axiomatization of sets ZF CA. We also show how our approach to multisets fits in the framework developed by Barwise and Moss.

Contents

1 Introduction 2

2 Multisets and multigraph decorations 4 2.1 Multigraphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Multi-decorations . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Multi-bisimulation 7 3.1 The Collapse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 Scott-bisimulation and unravelings 10

5 Multisets and the logic of graded modalities 11

1 Introduction

Multisets are very natural objects: they can model a number of different situations in different contexts, like the store of a shop or the bag of a housewife. A multiset (a bag in Computer Science) is like a set, except that an element can have multiple occurrences in it. For example, a grocery shop with 50 apples, 150 pears, 100 banana, and 0 kiwi in store can be modeled by the multiset

[[apple, apple, ⋯, pear, pear, ⋯, banana, banana, ⋯]] .

In proof theory sequents are often modeled as pairs of multisets (see e.g. [4]).

In general, a multiset of objects from a given domain D can be represented in two ways:

(a) as a partial function from D to Card^{+}, where Card^{+} is the class of all strictly positive cardinals;

(b) as an equivalence class [f] of functions from a cardinal k to D, where [f] is the set of all function g ∈ D^{k} such that there exists a bijection h : k → k with f = g ∘ h.

For example, in the grocery shop above the domain D is given by the set {a, p, b, k}, and the shop is represented by:

(a) a function f with f : D → Card^{+}, f(a) = 50, f(p) = 150, f(b) = 100, f(k) =↑, or

(b) the equivalence class of the function f : 300 → D, where

f(x) = \{ \begin{matrix}a & if x < 50 \\ p & if 50 ≤ x < 150 \\ b & if 150 ≤ x < 300. \end{matrix}

Multiple occurrences of an object d ∈ D in a multiset can be described by the family of relations L_{MS} = {∈_{k}: k ∈ Card^{+}}, interpreted in (a) by d ∈_{k} f ⇔ f(d) ≥ k and in (b) by d ∈_{k} [f] ⇔ |f^{−1}(d)| ≥ k. When possible, we use a notation like [[d, d, c, e, e]] to represent a multiset.

If the domain D is fixed, there is an obvious equivalence between representations (a) and (b): they both describe the multisets based on D, or Dmultisets. In the following, we refer to them as the (a) or (b) representations of D-multisets.

As in the case of ordinary sets we want to represent iterated multisets, where multisets contain (various occurrences) of other multisets. In this case the domain D is made of multisets. By epsilon recursion it is easy to define the class of well-founded multisets, but here we are interested in circular situations, like in set theory: we want to have the possibility for a multiset x to be a member of itself, repeated any number of times, i.e. we want to guarantee the existence of multisets satisfying equations like x = [[x, x]] .

Circular multisets can be modeled using the theory ZF C^{−}A (Zermelo-Fraenkel Theory with choice, with foundation replaced by the anti-foundation axiom AF A, see [1]). One possibility is to use the representation (a) above, and define the operator

Δ(X) = {f is a function : dom(f) ⊆ X ∧ range(f) ⊆ Card^{+}}.

Δ is a monotone operator; its least fixed point gives us the class of well-founded multisets. The same class is obtained by considering the operator Γ defined by using representation (b):

Γ(X) = {[f] : f ∈ X^{k} for some cardinal k}.

Γ is a monotone operator; its least fixed point is isomorphic, as an L_{MS}- structure, to the least fixed point of Δ. We denote it by wfMS. The operators Δ and Γ also have greatest fixed points, which in ZF C^{−}A contain strictly the well-founded multisets. However, we prove that the greatest fixed point Γ^{∗} of Γ is not isomorphic to the greatest fixed point Δ^{∗} of Δ as an L_{MS}-structure: Γ^{∗} has nice AF A-like properties connected with decorations of multigraphs which are not shared by Δ^{∗}. Using these properties we find a correspondence between Γ^{∗} and a certain class of collapsed multigraphs, similar to the correspondence between sets and collapsed graphs given by the anti-foundation axiom AF A ([1]). Defining the multiset-class via Γ^{∗} allows us to propose an alternative (and easier to visualize) definition of multisets. This alternative is lost when we consider multisets defined via Δ.

Our major tool in this task is Scott-bisimulation. In his work [3], Scott proposed a theory of non-well-founded sets, which was later reconsidered by Aczel in [1]. Using the notion of Scott-bisimulation, Aczel compares Scott-theory ZF C^{−}S with ZF C^{−}A. Both can be obtained from ZF C^{−} (Zermelo-Fraenkel with choice, without foundation) by using a strengthening of the extensionality axiom, defined in terms of bisimulation: the maximal bisimulation for ZF C^{−}A, Scott-bisimulation for ZF C^{−}S. In this confrontation, the Scott axiomatization ZF C^{−}S seems to be less natural and manageable than ZF C^{−}A: in ZF C^{−}A any graph has a unique decoration, while in ZF C^{−}S graphs can have more than one decoration; in ZF C^{−}A any set can be represented by a collapsed graph, while a similar notion of collapse is not available in ZF C^{−}S.

In this work we claim that the Scott axiomatization looks like ZF C^{−}A more than it seems, but that this resemblance can be appreciated only by changing from the set to the multiset-context (defined via the Γ operator above). We show that Scott-bisimulation (in its generalization to multigraphs) gives us a way to define multiset-decorations of multigraphs, a criterion for deciding multisets equality, and a notion of collapsed multigraphs corresponding to multisets. In this way we show that the multiset-context is more natural than the set-context for Scott-bisimulation, because in the latter there is no natural notion of collapse or decoration one can work with.

Using Scott bisimulation we prove that the multiset-class admits three different descriptions, beside the greatest fixed point one. These representations are obtained by identifying multisets with rooted collapsed multigraphs, with rooted trees, or with a fragment of the class of infinitary graded modal formulae.

Summarizing, the interest of the work goes two ways. Starting from multisets, rooted collapsed multigraphs, rooted trees, and graded formulas are useful as representations. Conversely, multisets correspond directly to rooted collapsed multigraphs and rooted trees, providing standard representatives of multigraphs modulo Scott-bisimulation and of rooted trees modulo isomorphism, respectively.

This paper is organized as follows. In Section 2 we compare two possible definitions of the multiset-class, working out a theory of multigraph decoration. In Section 3 we give a notion of multi-bisimulation and the corresponding notion of collapse, and we identify multisets and rooted collapsed multigraphs. In Section 4 we compare our notion of multi-bisimulation with Scott-bisimulation, and this gives the second representation of multisets, via rooted trees. Finally, in Section 5 we deal with the identification of multisets with infinitary graded modal formulae.

Due to space limits, we only give examples and no proofs; to understand the paper the reader is supposed to be familiar with the results in [1] and [2].

We would like to thank Marc Bezem, Jelle Gerbrandy, Vincent van Oostrom, and Alberto Policriti for discussions on multisets.

2 Multisets and multigraph decorations

In this section we compare the greatest fixed points of the operators Δ and Γ defined in the introduction. In particular, we study their behavior w.r.t. decorations. We want to develop a theory of decorations which is the multi-analogue of the theory of graph decorations. In non-well-founded set theory, graphs are used as pictures of sets. To model multiplicity, we shall use multigraphs.

2.1 Multigraphs

A multigraph is nothing but a graph in which two nodes can be connected by more than one arrow. A graph can be determined by the set of nodes and a subset of successors Succ(w) for each node w, giving the nodes that are directly accessible from w. Analogously, we specify a multigraph giving a set of nodes O_{G} and an O_{G}-multiset MSucc(w), for each node w.

Definition 2.1 A multigraph G is a pair (O_{G}, MSucc), where O_{G} is a set of objects and MSucc is a function from O_{G} to the O_{G}-multisets.

If we use representation (a) of an O_{G}-multiset, MSucc(w) is a partial function from O_{G} to the strictly positive cardinals, for each node w; if we use representation (b), MSucc(w) is an equivalence class of functions from a cardinal k to O_{G}. By abuse of notation we denote the set of objects O_{G} of a multigraph G by the same symbol G. For each node w, we denote by Succ(w) the set on which MSucc(w) is based, e.g. by using (a)-representation the set Succ(w) is the domain of the partial function MSucc(w). If w, v ∈ G, we denote the multiplicity of v as an element in MSucc(w) by m_{G}(w, v): e.g. under the (a)-representation m_{G}(w, v) is equal to MSucc(w)(v), if v is in the domain of the partial function MSucc(w), 0 otherwise. Notice that the function m_{G} determines the function MSucc, and we could as well define a multigraph as a pair (O_{G}, m_{G}), where m_{G} is a function from G × G to cardinals. In the following, we represent a multigraph by a picture in which two nodes w, v of G are linked by m_{G}(w, v) arrows. A rooted multigraph is a multigraph G with a distinguished object (the root) w ∈ O_{G}, in which every object is accessible from the root: if v ∈ O_{G} then there is a sequence v_{0}, …, v_{n} of elements in O_{G} such that v_{0} = w v_{n} = v and m_{G}(v_{i}, v_{i+1}) ≥ 1, for all i < n.

An isomorphism between two multigraphs G, H is a bijective function ϕ between G and H such that for all w, v ∈ G it holds: m_{G}(w, v) = m_{G′}(ϕ(w), ϕ(v)). An isomorphism of rooted multigraphs (G, w), (H, v) is a isomorphism ϕ between G and H such that ϕ(w) = v.

2.2 Multi-decorations

The following multigraph analogue of a decoration should not come as a surprise, for readers familiar with graph decorations: a multigraph decoration consists of a function from the set of objects of the multigraph to multisets, in such a way that the decoration of a node w is the multiset consisting of all decorations (counting multiplicity) of Succ(w). The definition of multigraph decorations obviously depends on the choice of the class C we use to represent multisets: we speak about C-multi-decorations of multigraphs. For example, in fig.1 the multigraph G has a wfMS-multi-decoration defined by decorating v with ∅ and the root w by [[∅, ∅]] . As another example consider the multigraph H in fig.1. In this case, the leaves v_{1}, v_{2} are both wfMS-multi-decorated by ∅ and the root w′ by [[∅, ∅]] : hence multiple occurrences are not obtained exclusively because of multiple edges.

[figure: v; (G, w); (H, w′); v_{1}; v_{2}; Fig.1]

More formally, consider a class-structure C for the language L_{MS} = {∈_{k}: k ∈ Card^{+}}, and denote by ∈_{k}^{C} the interpretation of ∈_{k} in the structure C.

Definition 2.2 A C-multi-decoration of a multigraph G is a function D from G to multisets, in such a way that for any object w ∈ G it holds:

z ∈_{k}^{C} D(w) ⇔ ∑_{D(v)=z} m_{G}(w, v) ≥ k.

A multi-decoration of a rooted multigraph (G, w) is a multiset D(w), where D is a multi-decoration of the multigraph G.

[figure: [[ [[∅]] , [[∅]] ]]; [[∅]]; ∅; [[ [[∅]] , [[∅]] ]]; [[∅]]; [[∅]]; ∅; Fig.2]

In the previous pictures, each object has been labeled by its wfMS-multi-decoration. Notice that the two rooted multigraphs have the same multidecoration.

Can we find a class-structure C for L_{MS} having the property that any multigraph has a unique C-multi-decoration? Let us consider the two candidates Δ^{∗} and Γ^{∗} defined in the introduction. First we provide a multigraph which does not have any Δ^{∗}-multi-decoration. Counterexample. Consider the following (multi)graph G = ({w, v}, m_{G}), where the function m_{G} is defined as follows: m_{G}(w, w) = m_{G}(w, v) = m_{G}(v, v) = 1, and 0 in all other cases. We first prove that if D is a Δ^{∗}-multi-decoration of G, then D(w) must be different from D(v). Indeed, if D(w) = D(v) then ∑_{D(u)=D(v)} m_{G}(w, u) = 2 and D(v) ∈_{2} D(w); but ∑_{D(u)=D(v)} m_{G}(v, u) = 1 and D(v) ∉_{2} D(v), contradicting D(w) = D(v). On the other hand, a Δ^{∗}-multi-decoration of G with D(w) ≠ D(v) is a solution for the system of equations x_{w} = {⟨x_{w}, 1⟩, ⟨x_{v}, 1⟩}; x_{v} = {⟨x_{v}, 1⟩}, where we denoted by ⟨x, y⟩ the ordered pair {{x}, {x, y}}. But then D(v) = D(w) = {⟨D(v), 1⟩} after all, by uniqueness of solutions.

Hence, the class Δ^{∗} is not well-behaved w.r.t. multigraph decorations. Fortunately, the class Γ^{∗} behaves much better. There is a general reason for this: Γ is monotone and proper (this and the following terminology is from [2]), a multigraph G can be seen as a flat Γ-coalgebra, and a Γ^{∗}-multi-decoration of G is nothing but a solution for this Γ-coalgebra, with value in Γ^{∗}. Then Proposition 16.2 in [2] tells us that any flat Γ-coalgebra has a unique solution in Γ^{∗}, if Γ is monotone and proper. This gives:

Theorem 2.3 Any multigraph has a unique Γ^{∗}-multi-decoration.

Things go wrong with the operator Δ because we cannot see a multigraph as a flat Γ-coalgebra any more, because the operator Δ does not commute with the action of substitutions.

A direct proof of Theorem 2.3 can be given by associating to each multigraph G a system of equations Eq(G) in such a way that a function D with domain G is a Γ^{∗}-multi-decoration of G iff it is a solution for Eq(G). Then existence and uniqueness of Γ^{∗}-multi-decorations follows directly from ZF C^{−}A.

Theorem 2.3 gives us a good reason for choosing Γ^{∗} to represent the class of non well-founded multisets. We acknowledge this by a formal definition:

Definition 2.4 The multiset-class MS is the class Γ^{∗} endowed with the family of binary relations {∈_{k}: k ∈ Card^{+}}, defined by [f] ∈_{k} [g] ⇔ |g^{−1}([f])| ≥ k.

¿From now on, a multiset is an element in Γ^{∗}, and a multi-decoration is a Γ^{∗}-multi-decoration.

3 Multi-bisimulation

We now give a multiset-free criterion for establishing whether two multigraphs G, H have the same multi-decoration. In the set-context this was done via the notion of bisimulation. We generalize this notion in two ways. The first comes from the general theory of monotone operators of [2], while the second is more suited for working with graded modal formulae (see Section 5). Although the first notion is strictly stronger than the second, in the sense that there are relations satisfying the second but not the first definition, we prove that the maximal elements in both classes coincide, being both equal to the class {(w, w′) ∈ G × H : D_{G}(w) = D_{H}(w′)}.

Let us start with the notion of Γ-bisimulation. By the general theory in [2] we know that any smooth operator Σ that preserves covers admits a notion of Σ-bisimulation for which it holds: two points x, y of a Σ-coalgebra are Σbisimilar iff they have the same value under the solution for the coalgebra. It is possible to prove that the operator Γ defining multisets is smooth and cover preserving, and, as we already pointed out in the previous section, a multigraph is nothing but a Γ-coalgebra, with multi-decorations corresponding to solutions. In our case, the notion of Γ-bisimulation amounts to the following:

Definition 3.1 A Γ-bisimulation between two multigraphs G, H is a relation Z ⊆ G × H such that if wZw′ then MSucc(w) and MSucc(w′) are projections of a Z-multiset, i.e. (using representation (b)): there are functions f, g such that MSucc(w) = [f], MSucc(w′) = [g], dom(f) = dom(g), and f(ν)Zg(ν) for all ν ∈ dom(f).

¿From [2] we have:

Proposition 3.2 Two rooted multigraphs have the same decoration iff they are Γ-bisimilar.

We shall now define a weaker notion of bisimulation between multigraphs, the multi-bisimulation.

Definition 3.3 A multi-bisimulation between two multigraphs G, H is a relation Z ⊆ G × H such that if wZw′ then

(a) if X ⊆ Succ(w) and Y = {y ∈ Succ(w′) : ∃x ∈ X xZy}, then

∑_{x∈X} m_{G}(w, x) ≤ ∑_{y∈Y} m_{H}(w′, y);

(b) if Y ⊆ Succ(w′) and X = {x ∈ G : ∃y ∈ Y xZy}, then

∑_{y∈Y} m_{H}(w′, y) ≤ ∑_{x∈X} m_{G}(w, x).

A multi-bisimulation Z between two rooted multigraphs (G, w), (H, w′) is a multi-bisimulation between G and H with wZw′. We write (G, w) ≈_{m} (H, w′) (or simply w ≈_{m} w′, if the multigraphs G, H are uniquely determined from the context) if there is a multi-bisimulation between (G, w) and (H, w′).

In the following, we often consider a multi-bisimulation Z between rooted multigraphs (G, w), (H, w′) which is the restriction to G × H of an equivalence relation ∼ on the class of rooted multigraphs. This is the case of ≈_{m}, or, as we shall see later, of the relation to satisfy the same graded formulae. In this case it make sense to consider, for any node w in a multigraph, the classes of ∼ over w, that is, the sets {z ∈ Succ(w) : z ∼ v}, for any v ∈ Succ(w). The following remark proves that we can consider only this kind of elementary subsets to give an equivalent (and easier to visualize) definition of a multi-bisimulation.

Remark 3.4 If Z ⊆ G ×H is the restriction to G ×H of an equivalence relation ∼ on the class of rooted multigraphs, Definition 3.3 is equivalent to: if wZw′ then

(c) for all v ∈ Succ(w) there exists a v′ ∈ Succ(w′) such that vZv′ and ∑_{z∼v} m_{G}(w, z) = ∑_{z′∼v′} m_{H}(w′, z′);

(d) for all v′ ∈ Succ(w′) there exists a v ∈ Succ(w) such that vZv′.

It is easy to check that a Γ-bisimulation (as in Definition 3.1) is a multibisimulation, but the converse is not true. However, the following lemma says that ≈_{m} is the maximal multi-bisimulation between any pair of multigraphs, and Lemma 3.6 says that ≈_{m} is a Γ-bisimulation as well.

Lemma 3.5 The equivalence relation ≈_{m}, when restricted to multigraphs G, H, is a multi-bisimulation between G and H. In particular, if (G, w) ≈_{m} (H, w′) and u ∈ Succ(w) ∪ Succ(w′) then ∑_{v≈_{m}u} m_{G}(w, v) = ∑_{v′≈_{m}u} m_{H}(w′, v′).

Lemma 3.6 The relation {(w, w′) : (G, w) ≈_{m} (H, w′)} is a Γ-bisimulation between any pair of multigraphs G, H.

From the above lemma and Proposition 3.2 it follows:

Lemma 3.7 (G, w) ≈_{m} (H, w′) ⇔ D_{G}(w) = D_{H}(w′).

3.1 The Collapse

As in the set-context we use the notion of collapse to give canonical representatives for the classes of the equivalence relation to have the same multi-decoration between multigraphs. In other words, given a class of multigraphs with the same multi-decoration (that is, a class of multigraphs that are pictures of the same multiset), we give a way to select a unique representative in the class (modulo isomorphism). This allow us to identify collapsed multigraphs and multisets.

Definition 3.8 The Collapse of a multigraph G is defined as the multigraph G^{⋆} with set of objects equal to {[w] : w ∈ G} where [w] = {v ∈ G : w ≈_{m} v}, and m_{G^{⋆}}([w], [v]) = ∑_{z≈_{m}v} m_{G}(w, z).

The collapse of a multigraph is well-defined by Lemma 3.5. We define the collapse of a rooted multigraph (G, w) as the rooted multigraph (G^{⋆}, [w]).

Notice that it is not possible to define G^{⋆} by simply considering as edges between two classes σ, τ all G-edges between objects in σ and objects in τ. If we were doing so, the collapse of the rooted multigraph (G, w) on the right of picture 2 would be the multigraph K = (O_{K}, m_{K}), with O_{K} = {w_{1}, w_{2}, w_{3}}, root w_{1}, and m_{K}(w_{i}, w_{j}) = 2, if j = i + 1, and 0 otherwise. But the two rooted multigraphs do not have the same decoration (the root of the multigraph on picture 2 is decorated by [[ [[∅]] , [[∅]] ]] , while the root w_{1} of the one described here is decorated by [[ [[∅, ∅]] , [[∅, ∅]] ]] ).

A multigraph and its collapse belong to the same ≈_{m}-class:

Lemma 3.9 The relation Z = {(w, [w]) : w ∈ G} is a multi-bisimulation between G and G^{⋆}.

The following lemma says that a collapsed multigraph is an exact picture of its decoration, in the sense that different multisets correspond to different nodes.

Lemma 3.10 The decoration D_{G^{⋆}} of a collapsed multigraph G^{⋆} is an injective function.

Using the previous lemma we see that for a collapsed multigraph G^{⋆} the multidecoration D_{G^{⋆}} satisfies

z ∈_{k} D_{G^{⋆}}(w) ⇔ ∃v ∈ Succ(w) with D(v) = z and m_{G^{⋆}}(w, v) ≥ k,

and vice versa, any injective function satisfying this equivalence is a multidecoration of G^{⋆}.

A rooted multigraph has the same decoration as its collapse:

Lemma 3.11 D_{G^{⋆}}([w]) = D_{G}(w), for any multigraph G.

and multi-bisimilar rooted multigraphs have the same collapse, modulo isomorphism:

Theorem 3.12 (G, w) ≈_{m} (H, w′) ⇔ (G^{⋆}, [w]) is isomorphic to (H^{⋆}, [w′]).

Theorem 3.12 and Lemma 3.7 allow us to identify multisets and collapsed multigraphs. Given a multiset x, define its multi-transitive closure mTC as the set containing all multisets that are hereditarily members of x (i.e. if x = [f], where f is a function from a cardinal to multisets, then mTC(x) contains the multisets that are in the range of f, as well as the multisets that are in the range of a function representing an element in this range, and so on; mTC(x) can be defined by a simple recursion. Define the canonical rooted multigraph G(x) of a multiset x as the rooted multigraph having set of objects equal to mTC(x) ∪ {x}, as root the multiset x, and as MSucc the identity function. Starting from a multigraph (G, w), we can either perform its collapse (G^{∗}, [w]), or first consider its multi-decoration D_{G}(w) and then its canonical rooted multigraph G(D_{G}(w)), ending with isomorphic rooted multigraphs. The isomorphism is given by sending [v] ∈ G^{∗} to D_{G^{⋆}}([v]) = D_{G}(v). Define a multigraph to be extensional if two different objects are never multi-bisimilar. Every collapsed multigraph is extensional and every extensional rooted multigraph (G, w) is isomorphic to G(D_{G}(w)). So the G(D_{G}(w)) provide standard representatives for the extensional-rooted-multigraph equivalence classes modulo isomorphism.

Finally, notice that the multi-membership relations are represented in the class of collapsed multigraphs by:

(G, w) ∈_{k} (H, v) ⇔ ∃z ∈ H with (H_{|_{z}}, z) ≅ (G, w) and m_{H}(v, z) ≥ k,

where H_{|_{z}} is the restriction of H to the set of nodes that are reachable in H from z.

4 Scott-bisimulation and unravelings

In this section we show that the notion of multi-bisimulation between multigraphs is the natural generalization of the notion of Scott-bisimulation between graphs (see [1]). This allow us to identify multisets and rooted trees. With this aim, we generalize the notion of unraveling, from graphs to multigraphs. First, we summarize the relationship between bisimulation and unraveling in the context of graphs. Here, unravelings can be used to characterize both the maximal bisimulation and the Scott one. The unraveling of a graph produces a rooted tree, in which every node is copied once (in the simple unraveling) or k-times for a cardinal k (in the k-unraveling). It is possible to prove that two graphs are bisimilar if there exists a cardinal k such that the k-unravelings of the graphs are isomorphic, while two graphs are Scott-bisimilar if the simple unravelings are isomorphic.

In the following definition we generalize the notion of simple unraveling to multigraphs.

Definition 4.1 The Unraveling of a rooted multigraph (G, w) is the rooted multigraph (G, w)^{U} defined as follows:

(a) The set of objects is the set of finite sequences of type v_{0}k_{1}v_{1} … k_{n}v_{n}, where v_{0} = w and the k_{i}’s are cardinal numbers satisfying: k_{i+1} < m_{G}(v_{i}, v_{i+1}), for all i ∈ {0, …, n − 1} (in particular, if v_{0}k_{1}v_{1} … k_{n}v_{n} ∈ (G, w)^{U} then m_{G}(v_{i}, v_{i+1}) ≥ 1 and v_{i+1} ∈ Succ(v_{i}), for all i < n).

b) The root of (G, w)^{U} is the sequence w.

c) If σ = v_{0}k_{1}v_{1} … k_{n}v_{n} and τ = σk_{n+1}v_{n+1} ∈ (G, w)^{U} then m_{(G,w)^{U}} (σ, τ) = 1, while in all other cases we have m_{(G,w)^{U}} (σ, τ) = 0.

For example, in fig.1 the unraveling of the multigraph (G, w) is the multigraph (H, w′). Notice that the unraveling of a multigraph G is always a graph (i.e. m_{G}(w, v) ≤ 1, for w, v ∈ G), and if G is a graph then the notion of multigraph unraveling coincides with the notion of graph unraveling. Scottbisimulation (in the equivalent definition given in [1]) relates two rooted graphs (G, w), (H, w′) exactly when their unravelings are isomorphic. Theorem 4.2 below says that two multigraphs are multi-bisimilar if and only if their unravelings are isomorphic, thereby showing that we are working on a generalization of Scott-bisimulation.

Theorem 4.2 If G, H are multigraphs then (G, w) ≈_{m} (H, v) ⇔ (G, w)^{U} is isomorphic to (H, v)^{U}.

Theorem 4.2 and Lemma 3.7 allow us to identify multisets and rooted trees. Define the canonical rooted tree T (x) of a multiset x as (G(x))^{U}, where the rooted multigraph G(x) has been defined at the end of Section 3.1. Staring from a rooted multigraph (G, w), we can either perform its unraveling (G, w)^{U}, or first consider its multi-decoration D_{G}(w) and then its canonical rooted tree T (D_{G}(w)) ending with isomorphic rooted trees. The isomorphism is given by sending a sequence σ = v_{0}k_{1} … k_{n}v_{n} to D_{G}(v_{1})k_{1} … k_{n}D_{G}(v_{n}). Then as in the case of collpased multigraphs we have a way to select standard representatives for the rooted-tree equivalence classes modulo isomorphism.

The multi-membership relations are represented in the rooted-tree class by

(T, t) ∈_{k} (S, s) ⇔ |{u ∈ S : (S_{|_{u}}, u) is isomorphic to (T, t)}| ≥ k,

where (T, t) and (S, s) are rooted trees, and (S_{|_{u}}, u) denotes the subtree of S with root u.

5 Multisets and the logic of graded modalities

In this section we give a characterization of multi-bisimulation via logic. In the set-context, the appropriate logic for describing bisimulation between graphs was proved to be infinitary modal logic ([2]). In the multiset-context we shift to the graded extension of this logic by proving that two rooted multigraphs are multi-bisimilar iff they satisfy the same formulae of infinitary graded modal logic. More than this, we prove that any multigraph can be characterized by a single infinitary graded modal formula, and we isolate a class of formulae that correspond to multisets. In this way we have three alternative ways for modeling multisets: as collapsed multigraphs, as trees, or as infinitary formulae.

Let L_{∞}^{grad} be the infinitary logic of graded modalities, that is, the logic obtained from infinitary modal logic by adding the unary operators ⋄_{h}, for all h ∈ Card^{+}. More formally, we define L_{∞}^{grad} as the smallest class closed under infinitary conjunction (if Φ ⊆ L_{∞}^{grad} is a set then ⋀ Φ ∈ L_{∞}^{grad}), negation (if ϕ ∈ L_{∞}^{grad} then ¬ϕ ∈ L_{∞}^{grad}), and graded diamonds (if h is a strictly positive cardinal and ϕ ∈ L_{∞}^{grad} then ⋄_{h}ϕ ∈ L_{∞}^{grad}).

The truth of a formula ϕ of L_{∞}^{grad} in a rooted multigraph (G, w) is obtained by adding the clause below to the inductive definition of truth in L_{∞}:

(G, w) ⊧ ⋄_{h}ϕ ⇔ ∑_{(G_{|v} ,v)⊧ϕ} m_{G}(w, v) ≥ h.

If we denote ⋄_{1} by ⋄, we see that the logic L_{∞}^{grad} is an extension of infinitary modal logic. We write (G, w) ≡_{g} (H, w′) (or simply w ≡_{g} w′) if (G, w), (H, w′) are two rooted multigraphs that satisfy the same L_{∞}^{grad}-formulae.

The following theorem show that L_{∞}^{grad} is the appropriate language for characterizing multi-bisimulation.

Theorem 5.1 For any rooted multigraph (G, w) there exists a formula ϕ_{(G,w)} ∈ L_{∞}^{grad} which characterizes (G, w) modulo multi-bisimulation, i.e., for any multigraph H it holds: (H, w′) ⊧ ϕ_{(G,w)} ⇔ (G, w) ≈_{m} (H, w′).

This result suggests another representation of the class of multisets, in which the domain of the universe is a fragment of the class of infinitary graded modal formulae. First, we characterize the graded formulae of type ϕ_{(G,w)} for a rooted multigraph (G, w) (for a set-analogue, see [2]).

Definition 5.2 Consider the preorder ≤ defined in L_{∞}^{grad} by ψ ≤ ϕ ⇔⊧ ψ → ϕ, where ⊧ ψ → ϕ stands for: any rooted multigraph that satisfies ψ, satisfies ϕ as well. Define the class MS(L_{∞}^{grad}) as the one containing, modulo equivalence, all satisfiable L_{∞}^{grad}-formulae which are minimal with respect to ≤ on satisfiable formulae, that is:

ϕ ∈ MS(L_{∞}^{grad})
⇕

ϕ is satisfiable and for all satisfiable ψ if ψ ≤ ϕ then ψ is equivalent to ϕ.

Lemma 5.3 ϕ ∈ MS(L_{∞}^{grad}) ⇔ ∃ (G, w) with ⊧ (ϕ_{(G,w)} ↔ ϕ), for all ϕ ∈ L_{∞}^{grad}.

Then, we identify the class MS with the class MS(L_{∞}^{grad}), with ∈_{k} given by the relation {(ϕ, ψ) ∈ MS(L_{∞}^{grad}) × MS(L_{∞}^{grad}) :⊧ ϕ → ⋄_{k}ψ}.

References

[1] P. Aczel. Non-well-founded sets. CSLI, Lecture Notes 14, 1988.

[2] J. Barwise and L. Moss. Vicious Circles., volume 60 of CSLI Lecture Notes, Stanford California, 1996.

[3] D. Scott. A different kind of model for set theory. Unpublished paper, given at the 1960 Stanford Congress of Logic, Methodology and Philosophy of Science.

[4] A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory Cambridge Tracts in Theoretical Computer Science 43, CUP, 1996.