Metric semantics from partial order semantics
In dealing with semantics of programming languages partial orders resp. metric spaces have been used with great benefit in order to provide a meaning to recursive and repetitive constructs. Various authors have attempted to bridge the gap between the metric and order setting. Some are led by the observation that the Scott topology of a cpo \(D\) is not Hausdorff, and hence not metrizable, and search for weaker notions of metric, as partial metric or quasi-uniformities. Another group investigates a generalization of both metric and partial order. We propose here an alternative view which is motivated by the following considerations: 1. Many structures that are used for modelling languages with communication and concurrency, i.e. strings, Mazurkiewicz traces, prime event structures, pomsets and various types of trees have been used in both in a partial order and a metric setting. We are interested in the following questions: First, if and how the partial order and the metric on a particular domain are related? Second, if and how the cpo semantics and the metric semantics of a general language on such a domain are related? 2. There are certain features of languages that can be easily modelled using a partially ordered domain but cause problems when a metric on the same domain is used instead, e.g. unguarded recursion, whereas other features behave the other way round, e.g. sequential composition is more easily treated using metric. Thus it might be desirable to switch from one setting to the other, depending on the language to be modelled. This paper presents two methods to define a metric on a subset \(M\) of a complete partial order \(D\) such that \(M\) is a complete metric spaces and the metric semantics on \(M\) coincides with the partial order semantics on \(D\). The first method is to add a `length' on a complete partial order which means a function \(\rho: D\to \mathbb{N}_0 \cup \{\infty\}\) of increasing power. The second uses pseudo rank orderings, i.e. monotone sequences of monotone functions \(\pi_n: D\to D\). Moreover, we show that SFP domains can be characterized as special kinds of rank ordered cpo's and discuss the connection between the Lawson topology and the topology induced by the associated metric.
- The connection between initial and unique solutions of domain equations in the partial order and metric approach
- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
- A category of compositional domain-models for separable Stone spaces.
- scientific article; zbMATH DE number 3883639 (Why is no real title available?)
- scientific article; zbMATH DE number 3924762 (Why is no real title available?)
- On the relationships between Scott domains, synchronization trees, and metric spaces
- scientific article; zbMATH DE number 1114330 (Why is no real title available?)
- Metric reasoning about λ-terms: The affine case
- Metric Semantics and Full Abstractness for Action Refinement and Probabilistic Choice
- Uniform completion versus ideal completion of posets with projections
- Temporal structures
- Metric semantics for true concurrent real time
- An introduction to metric semantics: Operational and denotational models for programming and specification languages
- Metric completion versus ideal completion
This page was built for publication: Metric semantics from partial order semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1365795)
