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

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.

By abstracting from the branching structure of the branching domain B we arrive at the linear domain L. This abstraction operator—called linearize operator in the sequel—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 metric labelled transition system. This metric labelled transition system is compactly branching—being a generalization of finitely branching. As a consequence, we can apply a theorem—being a generalization of a theorem reminiscent to König’s lemma—obtaining the linearize operator lin. The additional metric structure of a metric labelled transition system (with respect to a labelled transition systems) is essential in the above. Similarly, we can linearize 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].

∗This work was carried out during a visit of BRICS, Department of Computer Science, University of Aarhus, Denmark with financial support of BRICS.

†The author is supported by the Netherlands Organization for Scientific Research.

Also the linear domain L can be viewed as a compactly branching metric labelled transition system. This can be done in two obvious ways. Both compactly branching metric labelled transition systems give rise to a branch operator: branch_{0} and branch_{1}.

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

The linearize and branch operators are related as follows:

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

We make the relationship between the linearize and branch operators even more precise. We follow the work of Nielsen and Winskel et al. [Win84, SNW93, WN94] using category theory—in particular functors—to classify the domains. The linear and branching domains are both turned into a quasimetric space which induces a preorder and hence a category. Lately, there is a growing interest in quasimetric spaces. See, e.g., Wagner’s thesis [Wag94] and Flagg and Kopperman’s [FK94]. The quasimetrics are obtained from the metrics the d omains are endowed with by dropping one half of the Hausdorff metric. The morphisms of the branching domain can be seen as simulations and the morphisms of the linear domains can be viewed simply as inclusion functions. The linearize operator and both the branch operators are functors. These functors form a reflection and a coreflection—our main result.

[figure: L  B]

By means of this reflection and coreflection we have expressed that the linear domain L can be embedded in the branching domain B. These adjunctions can also be used for the transfer of (categorical) techniques from one domain to the other.

The details of the above will appear in [Bre95].

References

[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, 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.

[Bre95] F. van Breugel. From Branching to Linear Metric Domains (and back). BRICS report, University of Aarhus, Aarhus, 1995. To appear.

[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.

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

[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.

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

[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, June 1994. Draft.

[Win84] G. Winskel. Synchronization Trees. Theoretical Computer Science, 34(1/2):33–82, 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.