Construction of a cms on a given cpo
Christel Baier, Mila Majster-Cederbaum · MADOC (University of Mannheim) · 1995
In dealing with denotational 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. This paper presents two methods to define a metric on a subset M of a cpo D such that M is a complete metric spaces and the metric semantics on M coincides with the cpo semantics on D when the same semantic operators are used. The first method is to add a 'length' on a cpo which means a function ρ : D → IN 0 ∪{∞} of increasing power. The second is based on the ideas of [9] and uses pseudo rank orderings, i.e. monotone sequences of monotone functions ϖn : D → D. We show that SFP domains can be characterized as special kinds of rank orderded cpo's. We also discuss the connection between the Lawson topology and the topology induced by the metric.