BRICS RS-95-30 F. van Breugel: From Branching to Linear Metric Domains (and back)

BRICS

Basic Research in Computer Science

From Branching to Linear Metric Domains (and back)

Franck van Breugel

BRICS Report Series RS-95-30 ISSN 0909-0878 June 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

From Branching to Linear Metric Domains

(and back)

Franck van Breugel^{∗}

McGill University School of Computer Science 3480 University Street, Montreal H3A 2A7, Canada

Abstract A branching and a linear metric domain—both turned into a category—

are related by means of a reflection and a coreflection.

Introduction

Besides partial orders, also metric spaces have turned out to be very useful to give semantics to programming languages (see, e.g., the collection of papers of the Amsterdam Concurrency Group [BR92]). In the literature, one encounters two main classes of metric domains: linear domains and branching domains. Linear domains were already studied by topologists in the early twenties. Branching domains have been introduced by, e.g., De Bakker and Zucker [BZ82, BZ83], Golson and Rounds [GR83, Gol84], and the author [Bre93]. The elements of these linear and branching domains are convenient to model—one might even say that they represent—trace equivalence classes and bisimulation equivalence classes, respectively. The former is a simple observation. The latter has been proved by Van Glabbeek and Rutten [GR89].

Linear domains are more abstract than branching domains. Our aim is to show that linear domains can be embedded in branching domains. We focus on the branching domain B introduced by De Bakker and Zucker in [BZ83] and the linear domain L the elements of which can be viewed as nonempty and compact sets of sequences. The elements of the branching domain B can be viewed as labelled trees.

There is an obvious way to abstract from the branching structure of the branching domain B arriving at the linear domain L. This abstraction operator— called linearize operator in the sequel—can be viewed as assigning to a labelled tree the set of label sequences corresponding to the paths from the root of the tree to any of its leaves. For example, to the labelled tree

∗Supported by the Netherlands Organization for Scientific Research.

[figure: ·; a; a; ·; b; ·; b; ·; ·; a; b; ·; ·]

the linearize operator assigns the set of sequences

{ab, aba, abb}.

The linearize operator can be defined conveniently in terms of a metric labelled transition system. The theory of metric labelled transition systems has been outlined in the author’s [Bre94a] and has been developed further in his thesis [Bre94b]. The branching domain B can be seen as a labelled transition system as De Bakker, Bergstra, Klop, and Meyer noted in [BBKM84]. It can even be viewed as a compactly branching—being a generalization of finitely branching— metric labelled transition system. The additional metric structure of a metric labelled transition system (with respect to a labelled transition systems) is essential in the definition of the linearize operator lin. Similarly, we can linearize other branching domains like the more involved branching domains—used to model object-oriented and higher-order features—introduced by Rutten [Rut90] and De Bakker and the author [BB93].

There are various ways to add branching structure to the linear domain L arriving at the branching domain B. Some of the branch operators have the property being a right inverse for the linearize operator. We will focus on two of these branch operators: branch_{0} and branch_{1}.

[figure: L; ^{branch^{0}}; _{branch_{1}}; B; lin]

These two branch operators are canonical. The operator branch_{0} can be characterized as “branch as late as possible” whereas the operator branch_{1} “branches as soon as possible (i.e. at the root)”. For example, to the set of sequences

{ab, ac}

the branch operator branch_{0} assigns the labelled tree

[figure: ·; a; ·; b; c; ·; ·]

and to the set the branch operator branch_{1} assigns the labelled tree

[figure: ·; a; a; ·; b; ·; c; ·; ·]

We detail the relationship between the linearize and branch operators. We follow the work of Nielsen and Winskel et al. [Win84, SNW93, WN94] using category theory—in particular functors—to classify domains. The linear and branching domain are both turned into a generalized metric space. Generalized metric spaces were already studied by Lawvere [Law73]. Lately, there is a growing interest in generalized metric spaces (see, e.g., Wagner’s thesis [Wag94], Flagg and Kopperman’s [FK94] and Rutten’s [Rut95]). The generalized metrics are obtained from the metrics the domains are endowed with by dropping one half of the Hausdorff metric [Hau14]. Generalized metric spaces induce very simple categories, namely preorders. The morphisms of the branching domain can be seen as simulations and the morphisms of the linear domain can simply be viewed as inclusion functions. The linearize operator and both the branch operators are functors. The functors branch_{0} and branch_{1} are a right and a left adjoint for the functor lin. The adjunctions form a reflection and a coreflection^{1}.

[figure: L; B]

Among the branch operators which are a right inverse for the linearize operator lin, the operator branch_{0} is final and the operator branch_{1} is initial.

By means of this reflection and coreflection we have expressed that the linear domain L can be embedded in the branching domain B in two canonical ways. For a detailed discussion of the merits of relating domains by means of reflections and coreflections we refer the reader to the introduction of [WN94].

1We use the term reflection to mean an adjunction the right adjoint of which is full and faithful. Similarly, the term coreflection is used here to mean an adjunction the left adjoint of which is full and faithful. Although the same uses can be found in the literature, they are not entirely standard.

The linear domain L and the branching domain B are introduced in Section 1 and 2. In the next two sections, the linearize operator lin and the branch operators branch_{0} and branch_{1} are defined. The main results—including the facts that lin and branch_{0} form a reflection and that lin and branch_{1} form a coreflection—are presented in Section 5. In the concluding section, some related work and future work is discussed. Appendix A contains some notions from metric topology and Banach’s fixed point theorem. Banach’s theorem [Ban22] plays a central role. It is used to define the linear domain L, the branching domain B, the linearize operator lin, the branching operators branch_{0} and branch_{1}, and the generalized metric the branching domain B is endowed with. Furthermore, branch_{0} and branch_{1} being a right inverse for lin and the reflection and coreflection results are proved by means of Banach’s theorem. In Appendix B, some of the theory on (metric) labelled transition systems is developed. We assume that the reader is familiar with the basics of category theory. For further reading we refer the reader to Mac Lane’s standard work [ML71]. Some proofs have been sent to Appendix C.

Acknowledgements

Part of this work has been carried out during a visit of BRICS. The author would like to thank BRICS for the financial support making this visit possible. The author has benefitted from discussions with Jaco de Bakker, Michael Barr, Claudio Hermida, Bart Jacobs, Mogens Nielsen, Jaap van Oosten, Prakash Panangaden, Jan Rutten, Vladimiro Sassone, and Glynn Winskel, and from presenting this material at a seminar of the Centre de Recherche en Theorie des Categories.

1 A linear domain

Both the linear and the branching domain are defined in terms of a set (a, b, c ∈)^{2} A of actions. This set is turned into a complete metric space (see Definition A.1 and A.5) by endowing it with the discrete metric (see Definition A.2).

The linear domain is defined in two steps. In the first step, the complete metric space A^{∞} is defined in terms of the complete metric space A, the singleton metric space 1 containing 0 as single element, and the operations \frac{1}{2}·, ×, and + (see Definition A.3).

Definition 1.1 The complete metric space (σ ∈) A^{∞} is the unique complete metric space satisfying

A^{∞} ≅ A × \frac{1}{2} · (1 + A^{∞}).

2We use the notation (x ∈) X for the introduction of a set or metric space X with typical elements x, x′, x_{0}, …

The fact that there exists a unique (up to isometry) complete metric space A^{∞} being isometric^{3} (see Definition A.11) to the complete metric space A× \frac{1}{2} ·(1+A^{∞}) follows from Theorem 4.4 of America and Rutten’s [AR89]. The proof of this theorem relies on Banach’s theorem.

The elements of the complete metric space A^{∞} can be viewed as nonempty and finite or infinite sequences over the action set A. For example, the element

⟨a, ⟨b, 0⟩⟩

corresponds to the finite sequence ab and the infinite sequence a^{ω} corresponds to the element

⟨a, ⟨a, ⋯⟩⟩.

The metric m_{A^{∞}} is a Baire-like metric [Bai09]. For example,

m_{A^{∞}} (⟨a, ⟨b, 0⟩⟩, ⟨a, ⟨a, ⋯⟩⟩)

= (m_{A} × \frac{1}{2} · (m_{1} + m_{A^{∞}})) (⟨a, ⟨b, 0⟩⟩, ⟨a, ⟨a, ⋯⟩⟩)
= max \{m_{A} (a, a), \frac{1}{2} · m_{A^{∞}} (⟨b, 0⟩, ⟨a, ⋯⟩)\}
= max \{0, \frac{1}{2} · (m_{A} × \frac{1}{2} · (m_{1} + m_{A^{∞}})) (⟨b, 0⟩, ⟨a, ⋯⟩)\}
= max \{0, \frac{1}{2} · max \{m_{A} (b, a), \frac{1}{2} · m_{A^{∞}} (0, ⋯)\}\}
= max \{0, \frac{1}{2} · max \{1, \frac{1}{2} · 1\}\}
= \frac{1}{2}.

In the second step, the linear domain L is defined in terms of the singleton metric space 1, the complete metric space A^{∞}, and the operations + and P_{nk} (see Definition A.7).

Definition 1.2 The complete metric space (L ∈) L is defined by

L = 1 + P_{nk} (A^{∞}).

The elements of the linear domain, the linear processes, can be viewed as sets of sequences. The element 0 of the singleton metric space 1 can be seen as the singleton set consisting of the empty sequence. All other elements of the linear domain can be viewed as nonempty and compact (see Definition A.6) sets of nonempty sequences.

In Section 5, we will discuss (half of) the metric m_{L} in some detail (see Property 5.3).

The elements of the linear domain L represent (infinitary completed) trace equivalence classes (see, e.g., Section 2.7 of Van Glabbeek’s [Gla90]). Let (C, A, →) be a finitely branching labelled transition system (see Definition B.1 and B.2).

3We shall treat the isometry as an identity and thus elide its use. It can be put in without any difficulties, but will clutter up the presentation.

According to Property B.3, the labelled transition system induces a contractive (see Definition A.12) function Φ_{(C,A,→)} from the nonempty complete metric space C → L to itself. From Banach’s theorem we can deduce that the function has a unique fixed point

fix (Φ_{(C,A,→)}) : C → L.

One can easily verify that, for all c_{0}, c_{1} ∈ C, c_{0} and c_{1} are trace equivalent if and only if

fix (Φ_{(C,A,→)})(c_{0}) = fix (Φ_{(C,A,→)})(c_{1}).

That is, there is a one-to-one correspondence between the trace equivalence classes (of the labelled transition system (C, A, →)) and the linear processes (in the image of fix (Φ_{(C,A,→)})).

2 A branching domain

The branching domain B is defined in terms of the complete metric space A, the singleton metric space 1, and the operations \frac{1}{2}·, ×, +, and P_{nk}.

Definition 2.1 The complete metric space (B ∈) B is the unique complete metric space satisfying

B ≅ 1 + P_{nk} (A × \frac{1}{2} · B).

Again we conclude from Theorem 4.4 of [AR89] that such a complete metric space exists.

The elements of the branching domain, the branching processes, can be viewed as labelled trees with the following three properties. First of all, the labelled trees are commutative, i.e. for all nodes of a tree, its subtrees are not ordered. For example, the labelled trees

[figure: ·; a; b; ·; a; b; ·; ·; ·; and; ·; b; a; ·; ·; b; a; ·; ·]

are identified by commutativity, and both correspond to the branching process

{⟨a, {⟨a, 0⟩, ⟨b, 0⟩}⟩, ⟨b, 0⟩}.

Second, the labelled trees are absorptive, i.e. for all nodes of a tree, the collection of its subtrees contains no duplicates. For example, the labelled tree

[figure: ·; a; a; a; ·; b; b; b; ·; ·; ·; ·; ·]

is not absorptive. By absorption we obtain the tree

[figure: ·; a; a; ·; b; ·; ·]

This labelled tree corresponds to the branching process

{⟨a, {⟨b, 0⟩}⟩, ⟨a, 0⟩}.

From the first and the second property we can conclude that, for all nodes of a labelled tree, the collection of its subtrees is a set. Third, the trees are compactly branching, i.e. for all nodes of a tree, the set of its subtrees—corresponding to branching processes—is compact (with respect to the metric m_{B}). For example,

the labelled tree [figure: ·; a; a; ⋯; a; a; ·; ·; a; ·; a; ·; a; ·; ·; a; ·; a; ·; ·; ⋮]

including the infinite branch is compactly branching. It corresponds to the branching process

{⟨a, 0⟩, ⟨a, {⟨a, 0⟩}⟩, ⟨a, {⟨a, {⟨a, 0⟩}⟩}⟩, …, ⟨a, {⟨a, {⟨a, ⋯⟩}⟩}⟩}.

If we would leave out the infinite branch, the labelled tree would not be compactly branching any more.

The branching domain B has been introduced by De Bakker and Zucker (see Theorem 3.2 of [BZ83]). In Section 5 we will discuss (half of) the metric m_{B} (see Property 5.3).

Van Glabbeek and Rutten [GR89] have shown that the elements of the branching domain B represent bisimulation equivalence classes—bisimulation is a notion due to Milner and Park [Mil80, Par81, Mil94]. Let (C, A, →) be a finitely branching labelled transition system. According to Property B.4, the labelled transition system induces a contractive function Ψ_{(C,A,→)} from the nonempty complete metric space C → B to itself. As a consequence of Banach’s theorem the function has a unique fixed point

fix (Ψ_{(C,A,→)}) : C → B.

Van Glabbeek and Rutten have proved in Theorem 1 of [GR89] that, for all c_{0}, c_{1} ∈ C, c_{0} and c_{1} are bisimilar if and only if

fix (Ψ_{(C,A,→)}) (c_{0}) = fix (Ψ_{(C,A,→)}) (c_{1}),

i.e. there is a one-to-one correspondence between the bisimulation equivalence classes (of the labelled transition system (C, A, →)) and the branching processes (in the image of fix (Ψ_{(C,A,→)})).

3 A linearize operator

The linearize operator is defined by means of the theory of (metric) labelled transition systems. As De Bakker, Bergstra, Klop, and Meyer noted in Remark 4.3 of [BBKM84], the branching domain B can be viewed as a labelled transition system. The configurations of the labelled transition systems are the branching processes. As action set we take the set A. The transition relation is presented in

Definition 3.1 The transition relation → ⊆ B × A × B is defined by

B ⟶^{a} B′ if and only if ⟨a, B′⟩ ∈ B.

There exists a function

fix (Φ_{(B,A,→)}) : B → L

according to Property B.3 and Banach’s theorem, provided that the labelled transition system is finitely branching (see Definition B.2). However, the labelled transition system is not finitely branching. For example,

[figure: {⟨a, 0⟩, ⟨a, {⟨a, 0⟩}⟩, ⟨a, {⟨a, {⟨a, 0⟩}⟩}⟩, …, ⟨a, {⟨a, {⟨a, ⋯⟩}⟩}⟩}; a; a; a; a; 0; {⟨a, 0⟩}; a; {⟨a, {⟨a, 0⟩}⟩}; a; ⋯; {⟨a, {⟨a, {⟨a, ⋯⟩}⟩}⟩}; a]

By endowing the branching processes with their metric m_{B} and the actions with the discrete metric we obtain a metric labelled transition system (see Definition B.5). This metric labelled transition system is compactly branching (see Definition B.6).

Property 3.2 The metric labelled transition system (B, A, →) is compactly branching. Proof We have that, for all B ∈ B,

T (B) = \{ \begin{matrix}∅ & if B = 0 \\ B & otherwise \end{matrix}

Obviously, the metric labelled transition system is compactly branching. □

According to Property B.7 and Banach’s theorem, there exists a function

fix (Υ_{(B,A,→)}) : B →^{1} L. This is the aimed for linearize operator. Definition 3.3 The function lin : B →^{1} L is defined by

lin = fix (Υ_{(B,A,→)}). The function lin is the unique function lin : B →^{1} L satisfying

lin (B) = \{ \begin{matrix}0 & if B = 0 \\ \{ ⟨a, σ⟩ | ⟨a, B′⟩ ∈ B ∧ σ ∈ lin (B′) \}∪ \\ \{ ⟨a, 0⟩ | ⟨a, 0⟩ ∈ B \} & otherwise \end{matrix}

For example, to the branching process

{⟨a, {⟨b, 0⟩}⟩, ⟨a, {⟨b, {⟨a, 0⟩, ⟨b, 0⟩}⟩}⟩} corresponding to the labelled tree

[figure: ·; a; a; ·; b; ·; b; ·; ·; a; b; ·; ·]

the linearize operator assigns the linear process

{⟨a, ⟨b, 0⟩⟩, ⟨a, ⟨b, ⟨a, 0⟩⟩⟩, ⟨a, ⟨b, ⟨b, 0⟩⟩⟩} corresponding to the set of sequences

{ab, aba, abb}.

The technique of viewing the branching domain as a compactly branching metric labelled transition system and deriving from it a linearize operator as described above can also be applied to more involved branching domains.

In Definition 7.1 of [Rut90], Rutten has introduced the linearize operator abstr to abstract from the branching structure of a branching domain (introduced in Definition 5.1 of [Rut90]).The well-definedness proof of abstr is far from trivial (cf. Appendix II of [Rut90]). The branching domain can be viewed as a compactly branching metric labelled transition system and the linearize operator abstr can be defined as fix (Υ).

The branching domain introduced by De Bakker and the author in Definition 4.5 of [BB93] can also be linearized in this way. For details we refer the reader to Chapter 10 of [Bre94b] (see Definition 10.4.14 and Proposition 10.4.15).

4 Two branch operators

The two branch operators branch_{0} and branch_{1} are both defined by means of the theory of (metric) labelled transition systems. As in the previous section, we view the linear domain as a labelled transition system. This time, the linear processes are the configurations of the labelled transition system. Again we take the set A as the action set. Two transition relations are presented in

Definition 4.1

• The transition relation →_{0} ⊆ L × A × L is defined by

L ⟶^{a}_{0} L′ if and only if L′ = a\L, or ⟨a, 0⟩ ∈ L and L′ = 0,

where

a\L = { σ | ⟨a, σ⟩ ∈ L }.

• The transition relation →_{1} ⊆ L × A × L is defined by

L ⟶^{a}_{1} L′ if and only if ⟨a, σ⟩ ∈ L and L′ = {σ}, or ⟨a, 0⟩ ∈ L and L′ = 0.

The first transition relation “branches as late as possible” and the second one “branches as soon as possible”. For example, the transition relation →_{0} gives rise

to [figure: {⟨a, ⟨b, 0⟩⟩, ⟨a, ⟨b, ⟨a, 0⟩⟩⟩, ⟨a, ⟨b, ⟨b, 0⟩⟩⟩}; a; {⟨b, 0⟩, ⟨b, ⟨a, 0⟩⟩, ⟨b, ⟨b, 0⟩⟩}; b; b; {⟨a, 0⟩, ⟨b, 0⟩}; a; b; 0]

whereas the transition relation →_{1} gives rise to

[figure: {⟨a, ⟨b, 0⟩⟩, ⟨a, ⟨b, ⟨a, 0⟩⟩⟩, ⟨a, ⟨b, ⟨b, 0⟩⟩⟩}; a; a; a; {⟨b, ⟨b, 0⟩⟩}; b; {⟨b, ⟨a, 0⟩⟩}; b; {⟨b, 0⟩}; b; {⟨a, 0⟩}; a; 0]

The transition relation →_{0} gives rise to a finitely branching labelled transition system. Property 4.2 The labelled transition system (L, A, →_{0}) is finitely branching.

Proof We have that, for all L ∈ L,

T (L) = \{ \begin{matrix}∅ & if L = 0 \\ \{ ⟨a, a\L⟩ | a\L ≠ ∅ \} ∪ \{ ⟨a, 0⟩ | ⟨a, 0⟩ ∈ L \} & otherwise \end{matrix}

Since the set A is endowed with the discrete metric and the set L, with L ≠ 0, is compact, the set T (L) is finite. □

Property B.4 and Banach’s theorem give us the branch operator branch_{0}. Definition 4.3 The function branch_{0} : L → B is defined by

branch_{0} = fix (Ψ_{(L,A,→_{0})}).

The function branch_{0} is the unique function branch_{0} : L → B satisfying

branch_{0} (L) = \{ \begin{matrix}0 & if L = 0 \\ \{ ⟨a, branch_{0} (a\L)⟩ | a\L ≠ ∅ \}∪ \\ \{ ⟨a, 0⟩ | ⟨a, 0⟩ ∈ L \} & otherwise \end{matrix}

The transition relation →_{1} does not give rise to a finitely branching labelled transition system. For example,

[figure: {⟨a, 0⟩, ⟨a, ⟨a, 0⟩⟩, ⟨a, ⟨a, ⟨a, 0⟩⟩⟩, …, ⟨a, ⟨a, ⟨a, ⋯⟩⟩⟩}; a; a; a; a; 0; {⟨a, 0⟩}; a; {⟨a, ⟨a, 0⟩⟩}; a; ⋯; {⟨a, ⟨a, ⟨a, ⋯⟩⟩⟩}; a]

We endow the linear processes with m_{L} and the actions with the discrete metric. The obtained metric labelled transition system is compactly branching. Property 4.4 The metric labelled transition system (L, A, →_{1}) is compactly branching. Proof We have that, for all L ∈ L,

T (L) = \{ \begin{matrix}∅ & if L = 0 \\ \{ ⟨a, \{σ\}⟩ | ⟨a, σ⟩ ∈ L \} ∪ \{ ⟨a, 0⟩ | ⟨a, 0⟩ ∈ L \} & otherwise \end{matrix}

Clearly, the metric labelled transition system is compactly branching. □

From Property B.8 and Banach’s theorem we obtain the branching operator branch_{1} as follows. Definition 4.5 The function branch_{1} : L →^{1} B is defined by

branch_{1} = fix (Θ_{(L,A,→_{1})}). The function branch_{1} is the unique function branch_{1} : L →^{1} B satisfying

branch_{1} (L) = \{ \begin{matrix}0 & if L = 0 \\ \{ ⟨a, branch_{1} (\{σ\})⟩ | ⟨a, σ⟩ ∈ L \}∪ \\ \{ ⟨a, 0⟩ | ⟨a, 0⟩ ∈ L \} & otherwise \end{matrix}

For example, to the linear process

{⟨a, ⟨b, 0⟩⟩, ⟨a, ⟨c, 0⟩⟩} corresponding to the set of sequences

{ab, ac} the branch operator branch_{0} assigns the branching process

{⟨a, {⟨b, 0⟩, ⟨c, 0⟩}⟩}

corresponding to the labelled tree

[figure: ·; a; ·; b; c; ·; ·]

The branch operator branch_{1} assigns to the above linear process the branching process

{⟨a, {⟨b, 0⟩}⟩, ⟨a, {⟨c, 0⟩}⟩}

corresponding to the labelled tree

[figure: ·; a; a; ·; b; ·; c; ·; ·]

Both branch_{0} and branch_{1} are a right inverse for lin.

Property 4.6 lin ∘ branch_{0} = id_{L} and lin ∘ branch_{1} = id_{L}.

Proof We only prove the first equality. One can easily verify that

Φ_{(L,A,→_{0})} (lin ∘ branch_{0}) = lin ∘ branch_{0}

and

Φ_{(L,A,→_{0})} (id_{L}) = id_{L}.

Since Φ_{(L,A,→_{0})} is a contractive function from a nonempty complete metric space to itself, it has a unique fixed point according to Banach’s theorem. Consequently, lin ∘ branch_{0} and id_{L} are equal. □

5 A reflection and a coreflection

The linear and the branching domain are systematically turned into a category. We drop one half of the Hausdorff metric (see Definition A.7) in the definition of the metrics m_{L} and m_{B}. Lawvere studied this half of the Hausdorff metric in some detail (see the introduction of [Law73]). By dropping half of the Hausdorff metric we do not obtain a metric but a generalized metric.

Definition 5.1 A (1-bounded) generalized metric space is a pair (X, g_{X}) consisting of

• a set X and

• a function g_{X} : X × X → [0, 1], called generalized metric, satisfying, for all x, y, z ∈ X,

∗ g_{X} (x, x) = 0 and

∗ g_{X} (x, z) ≤ g_{X} (x, y) + g_{X} (y, z).

In contrast with a metric, a generalized metric might assign to a pair (x, y), with x ≠ y, the value 0. (Furthermore, a generalized metric need not be symmetric.) One can easily verify that, given a generalized metric space (X, g_{X}),

x ≤ y if g_{X} (x, y) = 0

defines a preorder on X (and hence a category with the elements of X as objects). The generalized metrics on L and B are presented in

Definition 5.2

• The function g_{L} : L × L → [0, 1] is defined by

g_{L} (L_{0}, L_{1}) = \{ \begin{matrix}0 & if L_{0}, L_{1} = 0 \\ sup \{ inf \{ m_{A^{∞}} (σ_{0}, σ_{1}) | σ_{1} ∈ L_{1} \} | σ_{0} ∈ L_{0} \} & if L_{0}, L_{1} ≠ 0 \\ 1 & otherwise \end{matrix}

• The function g_{B} : B × B → [0, 1] is the unique function satisfying

g_{B} (B_{0}, B_{1}) = \{ \begin{matrix}0 & if B_{0}, B_{1} = 0 \\ sup \{ inf \{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} \\ | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \} | ⟨a_{0}, B′_{0}⟩ ∈ B_{0} \} & if B_{0}, B_{1} ≠ 0 \\ 1 & otherwise \end{matrix}

Note that the definition of g_{B} is recursive. This definition is justified in Appendix C.

The generalized metrics g_{L} and g_{B} are characterized in Property 5.3

1. For all L_{0}, L_{1} ∈ L, with L_{0}, L_{1} ≠ 0, and ϵ, with 0 ≤ ϵ < 1, g_{L} (L_{0}, L_{1}) ≤ ϵ if and only if for all σ_{0} ∈ L_{0} there exists a σ_{1} ∈ L_{1} such that m_{A^{∞}} (σ_{0}, σ_{1}) ≤ ϵ.

2. For all B_{0}, B_{1} ∈ B, with B_{0}, B_{1} ≠ 0, and ϵ, with 0 ≤ ϵ < 1, g_{B} (B_{0}, B_{1}) ≤ ϵ if and only if for all ⟨a, B′_{0}⟩ ∈ B_{0} there exists a ⟨a, B′_{1}⟩ ∈ B_{1} such that g_{B} (B′_{0}, B′_{1}) ≤ 2 · ϵ.

Proof See Appendix C. □

From the above property we can conclude that the morphisms of the linear domain are inclusion functions. The morphisms of the branching domain can be seen as simulations (see, e.g., Section 2.8 of [Gla90]) which preserve configurations with no outgoing transitions—recall that the branching domain can be viewed as a labelled transition system.

Having turned the linear and the branching domain into a category, we are ready to prove the main results of this paper. In Property 5.4, we prove that

1. lin is a functor,

2. branch_{0} is a functor,

3. branch_{1} is a functor,

4. branch_{0} is a right adjoint for lin,

5. branch_{1} is a left adjoint for lin,

6. branch_{0} is full, and

7. branch_{1} is full. Since functors on preorders are faithful, we can conclude from 4. and 6. that lin and branch_{0} form a reflection and from 5. and 7. that lin and branch_{1} form a coreflection. Property 5.4 For all L, L_{0}, L_{1} ∈ L and B, B_{0}, B_{1} ∈ B,

1. if g_{B} (B_{0}, B_{1}) = 0 then g_{L} (lin (B_{0}), lin (B_{1})) = 0,

2. if g_{L} (L_{0}, L_{1}) = 0 then g_{B} (branch_{0} (L_{0}), branch_{0} (L_{1})) = 0,

3. if g_{L} (L_{0}, L_{1}) = 0 then g_{B} (branch_{1} (L_{0}), branch_{1} (L_{1})) = 0,

4. g_{L} (lin (B), L) = 0 if and only if g_{B} (B, branch_{0} (L)) = 0,

5. g_{L} (L, lin (B)) = 0 if and only if g_{B} (branch_{1} (L), B) = 0, 6. if g_{B} (branch_{0} (L_{0}), branch_{0} (L_{1})) = 0 then g_{L} (L_{0}, L_{1}) = 0, and

7. if g_{B} (branch_{1} (L_{0}), branch_{1} (L_{1})) = 0 then g_{L} (L_{0}, L_{1}) = 0. Proof We only treat the fifth case. All other cases can be dealt with similarly. The proof is divided into two parts. We first prove that, for all L ∈ L and B ∈ B,

if g_{L} (L, lin (B)) = 0 then g_{B} (branch_{1} (L), B) = 0. We define, for all n ∈ IN, the function υ_{n} : L →^{1} B by

υ_{n} (L) = \{ \begin{matrix}0 & if n = 0 \\ Υ_{(L,A,→_{1})} (υ_{n−1})(L) & otherwise \end{matrix}

We prove that, for all n ∈ IN, L ∈ L, and B ∈ B,

if g_{L} (L, lin (B)) = 0 then g_{B} (υ_{n} (L), B) ≤ 2^{−n} by induction on n. The above is vacuously true if n = 0. Let n > 0. By definition,

υ_{n} (L) = { ⟨a, υ_{n−1} ({σ})⟩ | ⟨a, σ⟩ ∈ L } ∪ { ⟨a, 0⟩ | ⟨a, 0⟩ ∈ L }. According Property 5.3.2, it suffices to prove

1. if ⟨a, σ⟩ ∈ L then there exists a ⟨a, B′⟩ ∈ B such that g_{B} (υ_{n−1} ({σ}), B′) ≤ 2^{−(n−1)} and

2. if ⟨a, 0⟩ ∈ L then ⟨a, 0⟩ ∈ B. We start with 1.

⟨a, σ⟩ ∈ L

⇒ ⟨a, σ⟩ ∈ lin (B) [g_{L} (L, lin (B)) = 0, Property 5.3.1]
⇒ ∃⟨a, B′⟩ ∈ B : σ ∈ lin (B′)
⇒ ∃⟨a, B′⟩ ∈ B : g_{L} ({σ}, lin (B′)) [Property 5.3.1]
⇒ ∃⟨a, B′⟩ ∈ B : g_{B} (υ_{n−1} ({σ}), B′) ≤ 2^{−(n−1)} [induction]

We continue with 2.

⟨a, 0⟩ ∈ L

⇒ ⟨a, 0⟩ ∈ lin (B) [g_{L} (L, lin (B)) = 0, Property 5.3.1]
⇒ ⟨a, 0⟩ ∈ B.

We can conclude that, for all L ∈ L and B ∈ B, if g_{L} (L, lin (B)) = 0 then

∀n ∈ IN : g_{B} (υ_{n} (L), B) ≤ 2^{−n}
⇒ lim_{n} g_{B} (υ_{n} (L), B) = 0
⇒ g_{B} (lim_{n} υ_{n} (L), B) = 0 [Property C.4]
⇒ g_{B} ((lim_{n} υ_{n}) (L), B) = 0
⇒ g_{B} (branch_{1} (L), B) = 0 [Banach’s theorem]

Second, for all L ∈ L and B ∈ B,

g_{B} (branch_{1} (L), B) = 0

⇒ g_{L} (lin (branch_{1} (L)), lin (B)) = 0 [Property 5.4.1]
⇒ g_{L} (L, lin (B)) = 0 [Property 4.6]
□

Of the functor category L → B we consider the full subcategory of right inverses for lin. In this subcategory,

1. branch_{0} is final and

2. branch_{1} is initial

as is shown in

Property 5.5 For all branch : L → B, with lin ∘ branch = id_{L},

1. g_{L→B} (branch, branch_{0}) = 0 and

2. g_{L→B} (branch_{1}, branch) = 0.

Proof We only consider the second case. Let L ∈ L. Since g_{L} (L, L) = 0 and lin ∘ branch = id_{L}, we have that g_{L} (L, lin (branch (L))) = 0. According to Property 5.4.5, g_{B} (branch_{1} (L), branch (L)) = 0. Consequently, we can conclude that g_{L→B} (branch_{1}, branch) = 0. □

Related and future work

We briefly discuss some related work.

In Section 4 and 5 of [WN94], Winskel and Nielsen have presented a category of synchronization trees S and a category of languages L. The morphisms of the fibred categories S_{A} and L_{A} are simulations and inclusion functions, respectively. The category L_{A} has been reflectively (but not coreflectively) embedded in S_{A}.

[figure: L_{A}; S_{A}]

The categories S_{A} and L_{A} have been related to various other categories in [WN94] (see also [SNW93]).

In Section 8 of [Rut95], Rutten has introduced the notion of a pair of (nonexpansive) functions between two generalized metric spaces being a metric adjoint pair. Neither lin and branch_{0} nor lin and branch_{1} form a metric adjoint pair.

From Corollary 4.9 of Rutten and Turi’s [RT92] we can conclude that B forms an initial algebra and a final coalgebra. By providing L with algebraic and coalgebraic structures we can define the linearize and branch operators as the unique morphisms from the initial algebra and to the final coalgebra.

Property 5.4 can also be proved by means of the ϵ ≤ \frac{1}{2} · ϵ (coinductive) proof principle (see, e.g., page 174 of [ABKR89]).

We conclude with some topics for future research.

Besides dropping one half of the Hausdorff metric in the definitions of the generalized metrics g_{L} and g_{B}, we can also drop one half of the disjoint union (see Definition A.3):

(g_{X} ; g_{Y}) (v, w) = \{ \begin{matrix}g_{X} (v, w) & if v, w ∈ X \\ g_{Y} (v, w) & if v, w ∈ Y \\ 0 & if v ∈ X and w ∈ Y \\ 1 & otherwise \end{matrix}

The above can be viewed as one half of the disjoint union as we have that

m_{X} + m_{Y} = max {m_{X} ; m_{Y} , m_{Y} ; m_{X}}.

The preorder corresponding to g_{X} ; g_{Y} (see page 14) is the concatenation (as defined, e.g., in Section 2.4 of [Pra86]) of the preorders corresponding to g_{X} and g_{Y}. We conjecture that in this setting Property 5.4 and 5.5 are still valid.

We are interested to see whether constructions like the sequential composition of branching processes (as defined in, e.g., Definition 2.14 of [KR90]) are universal.

References

[ABKR89] P. America, J.W. de Bakker, J.N. Kok, and J.J.M.M. Rutten. Denotational Semantics of a Parallel Object-Oriented Language. Information and Computation, 83(2):152–205, November 1989.

[Ale27] P. Alexandroff. Über stetige Abbildungen kompakter Räume. Mathematische Annalen, 96:555–571, 1927.

[AR89] P. America and J.J.M.M. Rutten. Solving Reflexive Domain Equations in a Category of Complete Metric Spaces. Journal of Computer and System Sciences, 39(3):343–375, December 1989.

[Bai09] R. Baire. Sur la Représentation des Fonctions Discontinues. Acta Mathematica, 32(1):97–176, 1909.

[Ban22] S. Banach. Sur les Opérations dans les Ensembles Abstraits et leurs Applications aux Equations Intégrales. Fundamenta Mathematicae, 3:133–181, 1922.

[BB93] J.W. de Bakker and F. van Breugel. Topological Models for Higher Order Control Flow. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, volume 802 of Lecture Notes in Computer Science, pages 122–142, New Orleans, April 1993. Springer-Verlag.

[BBKM84] J.W. de Bakker, J.A. Bergstra, J.W. Klop, and J.-J.Ch. Meyer. Linear Time and Branching Time Semantics for Recursion with Merge. Theoretical Computer Science, 34(1/2):135–156, November 1984.

[BR92] J.W. de Bakker and J.J.M.M. Rutten, editors. Ten Years of Concurrency Semantics, selected papers of the Amsterdam Concurrency Group. World Scientific, Singapore, 1992.

[Bre93] F. van Breugel. Three Metric Domains of Processes for Bisimulation. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, volume 802 of Lecture Notes in Computer Science, pages 103–121, New Orleans, April 1993. Springer-Verlag.

[Bre94a] F. van Breugel. Generalizing Finiteness Conditions of Labelled Transition Systems. In S. Abiteboul and E. Shamir, editors, Proceedings of the 21th International Colloquium on Automata, Languages, and Programming, volume 820 of Lecture Notes in Computer Science, pages 376–387, Jerusalem, July 1994. Springer-Verlag.

[Bre94b] F. van Breugel. Topological Models in Comparative Semantics. PhD thesis, Vrije Universiteit, Amsterdam, September 1994.

[BZ82] J.W. de Bakker and J.I. Zucker. Processes and the Denotational Semantics of Concurrency. Information and Control, 54(1/2):70–120, July/August 1982.

[BZ83] J.W. de Bakker and J.I. Zucker. Compactness in Semantics for Merge and Fair Merge. In E. Clarke and D. Kozen, editors, Proceedings of 4th Workshop on Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 18–33, Pittsburgh, June 1983. Springer-Verlag.

[Eng89] R. Engelking. General Topology, volume 6 of Sigma Series in Pure Mathematics. Heldermann Verlag, Berlin, revised and completed edition, 1989.

[FK94] B. Flagg and R. Kopperman. Continuity Spaces: reconciling domains and metric spaces - part I. Draft, May 1994.

[Gla90] R.J. van Glabbeek. The Linear Time - Branching Time Spectrum. In J.C.M. Baeten and J.W. Klop, editors, Proceedings of CONCUR’90, volume 458 of Lecture Notes in Computer Science, pages 278–297, Amsterdam, August 1990. Springer-Verlag.

[Gol84] W.G. Golson. Denotational Models based on Synchronous Communicating Processes. PhD thesis, University of Michigan, Ann Arbor, 1984.

[GR83] W.G. Golson and W.C. Rounds. Connections between Two Theories of Concurrency: Metric Spaces and Synchronization Trees. Information and Control, 57(2/3):102–124, May/June 1983.

[GR89] R.J. van Glabbeek and J.J.M.M. Rutten. The Processes of De Bakker and Zucker represent Bisimulation Equivalence Classes. In J.W. de Bakker, 25 jaar semantiek, pages 243–246. CWI, Amsterdam, 1989.

[Hau14] F. Hausdorff. Grundzüge der Mengenlehre. Leipzig, 1914.

[KR90] J.N. Kok and J.J.M.M. Rutten. Contractions in Comparing Concurrency Semantics. Theoretical Computer Science, 76(2/3):179–222, November 1990.

[Kur56] K. Kuratowski. Sur une Méthode de Métrisation Complète des Certains Espaces d’Ensembles Compacts. Fundamenta Mathematicae, 43(1):114–138, 1956.

[Law73] F.W. Lawvere. Metric Spaces, Generalized Logic, and Closed Categories. Rendiconti del Seminario Matematico e Fisico di Milano, 43:135–166, 1973.

[Mil80] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1980.

[Mil94] R. Milner. David Michael Ritchie Park (1935–1990) in memoriam. Theoretical Computer Science, 133(2):187–200, October 1994.

[ML71] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1971.

[Par81] D. Park. Concurrency and Automata on Infinite Sequences. In P. Deussen, editor, Proceedings of 5th GI-Conference on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167–183, Karlsruhe, March 1981. Springer-Verlag.

[Pra86] V.R. Pratt. Modelling Concurrency with Partial Orders. International Journal of Parallel Programming, 15(1):33–71, February 1986.

[RT92] J.J.M.M. Rutten and D. Turi. On the Foundations of Final Semantics: non-standard sets, metric spaces, partial orders. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop on Semantics: Foundations and Applications, volume 666 of Lecture Notes in Computer Science, pages 477–530, Beekbergen, June 1992. Springer-Verlag.

[Rut90] J.J.M.M. Rutten. Semantic Correctness for a Parallel Object-Oriented Language. SIAM Journal of Computation, 19(2):341–383, April 1990.

[Rut95] J.J.M.M. Rutten. Elements of Generalized Ultrametric Domain Theory. Report CS-R9507, CWI, Amsterdam, January 1995.

[SNW93] V. Sassone, M. Nielsen, and G. Winskel. A Classification of Models for Concurrency. In E. Best, editor, Proceedings of the 4th International Conference on Concurrency Theory, volume 715 of Lecture Notes in Computer Science, pages 82–96, Hildesheim, August 1993. Springer-Verlag.

[Wag94] K.R. Wagner. Solving Recursive Domain Equations with Enriched Categories. PhD thesis, Carnegie Mellon University, Pittsburgh, July 1994.

[Win84] G. Winskel. Synchronization Trees. Theoretical Computer Science, 34(1/2):33–82, November 1984.

[WN94] G. Winskel and M. Nielsen. Models for Concurrency. Number 12 in BRICS Notes Series. University of Aarhus, Aarhus, May 1994. To appear in S. Abramsky, Dov M. Gabbay and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, Oxford University Press, Oxford.

A Metric spaces

We present some notions from metric topology and Banach’s fixed point theorem. For further details on (metric) topology we refer the reader to Engelking’s standard work [Eng89]. We start with the definition of a basic notion: a 1-bounded metric space.

Definition A.1 A (1-bounded) metric space is a pair (X, m_{X}) consisting of

• a set X and

• a function m_{X} : X ×X → [0, 1], called metric, satisfying, for all x, y, z ∈ X,

∗ m_{X} (x, y) = 0 if and only if x = y,

∗ m_{X} (x, y) = m_{X} (y, x), and

∗ m_{X} (x, z) ≤ m_{X} (x, y) + m_{X} (y, z).

To simplify notations, we shall usually write X instead of (X, m_{X}) and denote the metric of a metric space X by m_{X}.

Two examples of a metric are presented in

Definition A.2

• Let X be a set. The discrete metric m_{X} : X × X → [0, 1] is defined by

m_{X} (x, y) = \{ \begin{matrix}0 & if x = y \\ 1 & if x ≠ y \end{matrix}

• The Euclidean metric m_{[0,1]} : [0, 1] × [0, 1] → [0, 1] is defined by

m_{[0,1]} (x, y) = |x − y|.

From metric spaces one can build new metric spaces by extending operations on sets like the Cartesian product × and the disjoint union + to metrics.

Definition A.3 Let X and Y be metric spaces.

• For all ϵ, with 0 < ϵ ≤ 1, the metric ϵ · m_{X} : X × X → [0, 1] is defined by

(ϵ · m_{X}) (x, y) = ϵ · m_{X} (x, y).

• The metric m_{X} × m_{Y} : (X × Y) × (X × Y) → [0, 1] is defined by

(m_{X} × m_{Y}) (⟨v, w⟩, ⟨x, y⟩) = max { m_{X} (v, x), m_{Y} (w, y) }.

• The metric m_{X} + m_{Y} : (X + Y) × (X + Y) → [0, 1] is defined by

(m_{X} + m_{Y}) (v, w) = \{ \begin{matrix}m_{X} (v, w) & if v, w ∈ X \\ m_{Y} (v, w) & if v, w ∈ Y \\ 1 & otherwise \end{matrix}

Below we will encounter some other operations on metrics.

The completeness of a metric space is essential in Banach’s theorem. Before we introduce this notion, we first present the definitions of converging and Cauchy sequence.

Definition A.4 Let X be a metric space. Let (x_{n})_{n} be a sequence in X and x an element of X.

• The sequence (x_{n})_{n} is said to converge to the element x, which is denoted by lim_{n} x_{n} = x, if

∀ϵ > 0 : ∃N ∈ IN : ∀n ≥ N : m_{X} (x_{n}, x) ≤ ϵ.

• The sequence (x_{n})_{n} is called Cauchy if

∀ϵ > 0 : ∃N ∈ IN : ∀m, n ≥ N : m_{X} (x_{m}, x_{n}) ≤ ϵ.

As can be easily seen, every convergent sequence is Cauchy.

Definition A.5 A metric space is called complete if every Cauchy sequences in the metric space is convergent.

As one can easily verify, the operations ϵ·, ×, and + preserve completeness. Compactness, a generalization of finiteness, is introduced in

Definition A.6 A subset of a metric space is called compact if every sequences in the set has a converging subsequence.

The set P_{nk} (X) of nonempty and compact subsets of the metric space X is turned into a metric space by endowing it with the Hausdorff metric (see Chapter VIII, § 6 of [Hau14]) introduced in

Definition A.7 Let X be a metric space. The Hausdorff metric

P_{nk} (m_{X}) : P_{nk} (X) × P_{nk} (X) → [0, 1]

is defined by

P_{nk} (m_{X}) (A, B) = max { sup { inf { m_{X} (a, b) | b ∈ B } | a ∈ A },
sup { inf { m_{X} (b, a) | a ∈ A } | b ∈ B } }.

The operation P_{nk} preserves completeness (Lemma 3 of [Kur56]). The metric space P_{k} (X) of compact subsets of the metric space X is defined by

P_{k} (X) = {∅} + P_{nk} (X).

The set X → Y of functions from the metric space X to the metric space Y is turned into a metric space by endowing it with the metric introduced in

Definition A.8 Let X and Y be metric spaces. The metric

m_{X} → m_{Y} : (X → Y) × (X → Y) → [0, 1]

is defined by

(m_{X} → m_{Y}) (f, g) = sup {m_{Y} (f (x), g (x)) | x ∈ X}.

Frequently we restrict ourselves to the subspace of nonexpansive functions.

Definition A.9 Let X and Y be metric spaces. A function f : X → Y is called nonexpansive if, for all x, y ∈ X,

m_{Y} (f (x), f (y)) ≤ m_{X} (x, y).

We denote the metric space of nonexpansive functions from the metric space X to the metric space Y by X →^{1} Y. The operations → and →^{1} preserve completeness as can easily be verified.

Next we will introduce an equivalence notion of metric spaces.

Definition A.10 Let X and Y be metric spaces. A function f : X → Y is called isometric if, for all x, y ∈ X,

m_{Y} (f (x), f (y)) = m_{X} (x, y).

Note that an isometric function is injective.

Definition A.11 The metric spaces X and Y are called isometric, denoted by X ≅ Y, if there exists an isometric function from X to Y which is surjective.

Besides the completeness of the metric space, the contractiveness of the function is another essential ingredient of Banach’s theorem.

Definition A.12 Let X and Y be metric spaces. A function f : X → Y is called contractive if there exists an ϵ, with 0 < ϵ < 1, such that

f ∈ (ϵ · X) →^{1} Y.

Instead of (ϵ·X) →^{1} Y we usually write X →^{ϵ} Y. We conclude with Banach’s fixed point theorem.

Theorem A.13 (Banach) Let X be a nonempty complete metric space. If the function f : X → X is contractive then it has a unique fixed point fix (f) and, for all x ∈ X,

fix (f) = lim_{n} x_{n}

where

x_{n} = \{ \begin{matrix}x & if n = 0 \\ f (x_{n−1}) & otherwise \end{matrix}

Proof See Theorem II.6 of [Ban22]. □

B Metric labelled transition systems

We introduce some of the theory on (metric) labelled transition systems developed in the author’s thesis [Bre94b].

Definition B.1 A labelled transition system is a triple (C, A, →) consisting of

• a set of configurations C,

• a set of actions A, and

• a transition relation → ⊆ C × A × C.

Instead of (c, a, c′) ∈ → we write c ⟶^{a} c′. If c ⟶^{a} c′ then we say that there exists a transition from c to c′ labelled with a. If there exists a transition from c, we write c →. Otherwise, we write c ↛.

If every configuration has only finitely many outgoing transitions, i.e. for all c ∈ C, the set

T (c) = { ⟨a, c′⟩ | c ⟶^{a} c′ }

is finite, then the labelled transition system is called finitely branching. An alternative formulation of this finiteness condition is presented in

Definition B.2 A labelled transition system (C, A, →) is called finitely branching if the function

T : C → P (A × C)

defined by

T (c) = { ⟨a, c′⟩ | c ⟶^{a} c′ }

is an element of C → P_{f} (A × C).

For finitely branching labelled transition systems we have the following two properties.

Property B.3 A finitely branching labelled transition system (C, A, →) induces a function

Φ_{(C,A,→)} : (C → L) →^{\frac{1}{2}} (C → L)

defined by

Φ_{(C,A,→)} (ϕ)(c) = \{ \begin{matrix}0 & if c ↛ \\ \{ ⟨a, σ⟩ | c ⟶^{a} c′ ∧ σ ∈ ϕ (c′) \}∪ \\ \{ ⟨a, 0⟩ | c ⟶^{a} c′ ∧ ϕ (c′) = 0 \} & otherwise \end{matrix}

Proof See, e.g., Theorem 4.3.6 and Proposition 4.3.7 of [Bre94b]. □

Property B.4 A finitely branching labelled transition system (C, A, →) induces a function

Ψ_{(C,A,→)} : (C → B) →^{\frac{1}{2}} (C → B)

defined by

Ψ_{(C,A,→)} (ψ)(c) = \{ \begin{matrix}0 & if c ↛ \\ \{ ⟨a, ψ (c′)⟩ | c ⟶^{a} c′ \} & otherwise \end{matrix}

Proof See, e.g., Theorem 4.3.10 and Proposition 4.3.12 of [Bre94b]. □

Both Φ and Ψ are contractive functions from a nonempty complete metric space to itself. According to Banach’s theorem, Φ and Ψ have unique fixed points fix (Φ) and fix (Ψ), respectively.

A metric labelled transition system is a labelled transition system with some additional structure. That is, the set of configurations and the set of actions are both endowed with a complete metric.

Definition B.5 A metric labelled transition system is a triple (C, A, →) consisting of

• a complete metric space of configuration C,

• a complete metric space of actions A, and

• a transition relation → ⊆ C × A × C.

Because we have a metric on the sets of configurations and actions, the finiteness condition finitely branching can be generalized to compactly branching: every configuration has a compact set of outgoing transitions and transitioning is nonexpansive.

Definition B.6 A metric labelled transition system (C, A, →) is called compactly branching if the function

T : C → P (A × C)

defined by

T (c) = { ⟨a, c′⟩ | c ⟶^{a} c′ }

is an element of C →^{1} P_{k} (A × \frac{1}{2} · C).

Property B.3 and B.4 can be generalized as follows.

Property B.7 A compactly branching metric labelled transition system (C, A, →) induces a function

Υ_{(C,A,→)} : (C →^{1} L) →^{\frac{1}{2}} (C →^{1} L)

defined by

Υ_{(C,A,→)} (υ)(c) = \{ \begin{matrix}0 & if c ↛ \\ \{ ⟨a, σ⟩ | c ⟶^{a} c′ ∧ σ ∈ υ (c′) \}∪ \\ \{ ⟨a, 0⟩ | c ⟶^{a} c′ ∧ υ (c′) = 0 \} & otherwise \end{matrix}

Proof See Theorem 7.3.8 and Proposition 7.3.10 of [Bre94b]. □

Property B.8 A compactly branching metric labelled transition system (C, A, →) induces a function

Θ_{(C,A,→)} : (C →^{1} B) →^{\frac{1}{2}} (C →^{1} B)

defined by

Θ_{(C,A,→)} (θ)(c) = \{ \begin{matrix}0 & if c ↛ \\ \{ ⟨a, θ (c′)⟩ | c ⟶^{a} c′ \} & otherwise \end{matrix}

Proof See Proposition 7.4.1 and 7.4.3 of [Bre94b]. □

As before, both Υ and Θ are contractive functions from a nonempty complete metric space to itself. According to Banach’s theorem, Υ and Θ have unique fixed points fix (Υ) and fix (Θ), respectively.

C Generalized metrics

The justification of the definition of the generalized metric g_{B} (Definition 5.2) is presented and the characterization of g_{B} (Property 5.3.2) is proved.

First, we prove that there exists a unique generalized metric satisfying the recursive equation in Definition 5.2. We show that there exists a contractive function from a nonempty complete metric space to itself, the unique fixed point of which satisfies the equation uniquely.

Given a set X, the set X ×X → [0, 1], with [0, 1] endowed with the Euclidean metric (see Definition A.2), forms a nonempty complete metric space.

Property C.1 The subspace G_{X} of generalized metrics on X is complete.

Proof Let (g_{n})_{n} be a Cauchy sequence of generalized metrics on X converging to the function g. To conclude that g is a generalized metric we prove that, for all x, y, z ∈ X,

g (x, x)
= (lim_{n} g_{n}) (x, x)
= lim_{n} g_{n} (x, x)
= 0

and

g (x, z)

= (lim_{n} g_{n}) (x, z)
= lim_{n} g_{n} (x, z)
≤ lim_{n} g_{n} (x, y) + g_{n} (y, z)
= lim_{n} g_{n} (x, y) + lim_{n} g_{n} (y, z)
= g (x, y) + g (y, z).
□

On the nonempty complete metric space G_{B} we define the following contractive function.

Definition C.2 The function G : G_{B} →^{\frac{1}{2}} G_{B} is defined by

G (g) (B_{0}, B_{1}) = \{ \begin{matrix}0 & if B_{0}, B_{1} = 0 \\ sup \{ inf \{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g (B′_{0}, B′_{1})\} \\ | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \} | ⟨a_{0}, B′_{0}⟩ ∈ B_{0} \} & if B_{0}, B_{1} ≠ 0 \\ 1 & otherwise \end{matrix}

We leave it to the reader to verify that G maps generalized metrics to generalized metrics and that it is contractive. According to Banach’s theorem, the function G has a unique fixed point: the generalized metric g_{B} introduced in Definition 5.2.

We conclude this appendix with the proof of Property 5.3.2. The key step in the proof is replacing the infimum in the definition of g_{B} by the minimum.

Since we dropped one half of the Hausdorff metric in the definition of g_{B}, g_{B} is smaller than m_{B}.

Property C.3 For all B_{0}, B_{1} ∈ B,

g_{B} (B_{0}, B_{1}) ≤ m_{B} (B_{0}, B_{1}).

Proof We define, for all n ∈ IN,

g_{n} = \{ \begin{matrix}m_{B} & if n = 0 \\ G (g_{n−1}) & otherwise \end{matrix}

We can prove that, for all n ∈ IN and B_{0}, B_{1} ∈ B,

g_{n} (B_{0}, B_{1}) ≤ m_{B} (B_{0}, B_{1})

by induction on n. Consequently, for all B_{0}, B_{1} ∈ B,

g_{B} (B_{0}, B_{1})

= (lim_{n} g_{n}) (B_{0}, B_{1}) [Banach’s theorem]
= lim_{n} g_{n} (B_{0}, B_{1})
≤ m_{B} (B_{0}, B_{1}).
□

A metric is nonexpansive in both its arguments. This does not hold for generalized metrics in general. The generalized metric g_{B} is nonexpansive (with respect to m_{B}), and hence continuous, in both its arguments.

Property C.4 For all B, B_{0}, B_{1} ∈ B,

\begin{matrix}m_{[0,1]} (g_{B} (B_{0}, B), g_{B} (B_{1}, B)) ≤ m_{B} (B_{0}, B_{1}) \\ m_{[0,1]} (g_{B} (B, B_{0}), g_{B} (B, B_{1})) ≤ m_{B} (B_{0}, B_{1}) \end{matrix}

Proof For example,

m_{[0,1]} (g_{B} (B, B_{0}), g_{B} (B, B_{1}))
≤ max {g_{B} (B_{0}, B_{1}), g_{B} (B_{1}, B_{0})}
≤ m_{B} (B_{0}, B_{1}) [Property C.3]
□

From the above property we can conclude that we can replace the infimum in the definition of g_{B} by the minimum.

Property C.5 For all a_{0} ∈ A and B′_{0}, B_{1} ∈ B, with B_{1} ≠ 0,

inf \{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \}
= min \{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \}.

Proof Because, for all a_{0} ∈ A, the function

λa_{1} ∈ A.m_{A} (a_{0}, a_{1})

is nonexpansive, and for all B′_{0} ∈ B, the function

λB′_{1} ∈ B.g_{B} (B′_{0}, B′_{1})

is nonexpansive (Property C.4), for all a_{0} ∈ A and B′_{0} ∈ B, the function

λ⟨a_{1}, B′_{1}⟩ ∈ A × \frac{1}{2} · B. max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\}

is nonexpansive. Since all B_{1} ∈ B, with B_{1} ≠ 0, are compact subsets of A × \frac{1}{2} · B and the nonexpansive image of a compact set is compact (a consequence of Theorem III of [Ale27]), for all B_{1} ∈ B, with B_{1} ≠ 0, the set

\{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \}

is compact. Because the infimum of a compact subset of [0, 1] is the minimum, the desired result can be concluded. □

This brings us to the

Proof of Property 5.3.2 Let B_{0}, B_{1} ∈ B, with B_{0}, B_{1} ≠ 0, and ϵ, with 0 ≤ ϵ < 1.

g_{B} (B_{0}, B_{1}) ≤ ϵ

⟺ sup \{ inf \{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \} | ⟨a_{0}, B′_{0}⟩ ∈ B_{0} \} ≤ ϵ
⟺ ∀⟨a_{0}, B′_{0}⟩ ∈ B_{0} : inf \{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \} ≤ ϵ
⟺ ∀⟨a_{0}, B′_{0}⟩ ∈ B_{0} : min \{ max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} | ⟨a_{1}, B′_{1}⟩ ∈ B_{1} \} ≤ ϵ

[Property C.5]

⟺ ∀⟨a_{0}, B′_{0}⟩ ∈ B_{0} : ∃⟨a_{1}, B′_{1}⟩ ∈ B_{1} : max \{m_{A} (a_{0}, a_{1}), \frac{1}{2} · g_{B} (B′_{0}, B′_{1})\} ≤ ϵ
⟺ ∀⟨a_{0}, B′_{0}⟩ ∈ B_{0} : ∃⟨a_{1}, B′_{1}⟩ ∈ B_{1} : a_{0} = a_{1} ∧ g_{B} (B′_{0}, B′_{1}) ≤ 2 · ϵ

[A is endowed with the discrete metric]

⟺ ∀⟨a, B′_{0}⟩ ∈ B_{0} : ∃⟨a, B′_{1}⟩ ∈ B_{1} : g_{B} (B′_{0}, B′_{1}) ≤ 2 · ϵ.
□

Recent Publications in the BRICS Report Series

RS-95-30 Franck van Breugel. From Branching to Linear Metric Domains (and back). June 1995. 30 pp. Abstract appeared in Engberg, Larsen, and Mosses, editors, 6th Nordic Workshop on Programming Theory, NWPT ’6 Proceedings, 1994, pages 444-447.

RS-95-29 Nils Klarlund. An n log n Algorithm for Online BDD Re�nement. May 1995. 20 pp.

RS-95-28 Luca Aceto and Jan Friso Groote. A Complete Equational Axiomatization for MPA with String Iteration. May 1995. 39 pp.

RS-95-27 David Janin and Igor Walukiewicz. Automata for the μcalculus and Related Results. May 1995. 11 pp. To appear in Mathematical Foundations of Computer Science: 20th Int. Symposium, MFCS ’95 Proceedings, LNCS, 1995.

RS-95-26 Faith Fich and Peter Bro Miltersen. Tables should be sorted (on random access machines). May 1995. 11 pp. To appear in Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS, 1995.

RS-95-25 S�ren B. Lassen. Basic Action Theory. May 1995. 47 pp.

RS-95-24 Peter �rb�k. Can you Trust your Data? April 1995. 15 pp. Appears in Mosses, Nielsen, and Schwartzbach, editors, Theory and Practice of Software Development. 6th International Joint Conference CAAP/FASE, TAPSOFT ’95 Proceedings, LNCS 915, 1995, pages 575�590.

RS-95-23 Allan Cheng and Mogens Nielsen. Open Maps (at) Work. April 1995. 33 pp.

RS-95-22 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part II: A Behavioural Semantics and Full Abstractness. April 1995. 33 pp.

RS-95-21 Jesper G. Henriksen, Ole J. L. Jensen, Michael E. J�rgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders B. Sandholm. MONA: Monadic Second-Order Logic in Practice. May 1995. 17 pp.