Metric semantics from partial order semantics (Q1365795)

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.