10
$\begingroup$

Smyth's chapter in the handbook of logic in computer science and other references describe how metric spaces can be used as domains. I do understand that complete metric spaces give unique fixed points but I don't understand why metric spaces are important. I'd really appreciate any thoughts on the following questions.

What are good examples of the use of (ultra/quasi/pseudo)metric spaces in semantics? In particular related to any example: Why do we need the metric structure? What do $\omega$-CPOs lack that the metric supplies?

Also: Is the unique fixed point property important? What's a good example?

Thanks!

$\endgroup$
15
$\begingroup$

Relative to domain structure, metric structure gives you extra data on the carrier set. Basically, you can compare any two elements of a metric space and furthermore you know how much two elements are different, whereas in domains the order structure is partial, and you don't have a quantitative measure of how much elements differ.

Pragmatically, this extra structure is useful in that it makes solving domain equations hugely easier. Back in the 80s there were a lot of Dutch computer scientists using metric space equations to model concurrency, but it's also of current interest.

If you've been following the usual places (POPL/ICFP/ESOP/etc), you'll have noticed that so-called step-indexed models are big business these days, since they let you give models of languages with combinations of features (such as impredicative polymorphism and higher-order state) that are difficult to treat with classical domain-theoretic models. However, the constructions used in these models are hauntingly similar to solving domain equations, and it's natural to wonder what the heck the connection is. Lars Birkedal and his collaborators have had the general idea that solving domain equations on bisected (ie, distances between any two points are all of the form $2^{-n}$ for some $n$) ultrametric spaces is the secret denotational life of step-indexed models. See Birkedal, Stovring and Thamsborg's paper "The Category-Theoretic Solution of Recursive Metric Space Equations" for some recent work in this area.

Now, all this work has been focused on getting models at all, but that's not the only thing we're interested in -- we can't just replace partial orders with metric structure in a denotational model and expect it to mean exactly the same thing. So you might wonder what the impact of metric models on properties like full abstraction, for example.

Escardo showed in his 1999 paper "A Metric Model of PCF" that a straightforward metric model of PCF was adequate but not fully abstract -- the extra metric structure could be used to model timeout constants. Concretely, you could model a constant $\mathrm{timeout}\;n\;e$ which would raise an error if $e$ did not return in $n$ steps or fewer. This is information that a metric model can see, because it has distance information, but it's information a domain model can't, since the information order doesn't tell you "how evaluated" a value is.

This extra resolving power is both the strength and the weakness of metric techniques. In their note "Step Indexing: the Good, the Bad, and the Ugly", Benton and Hur show that the extra structure of step-indexed models is very useful for them give to give realizability-style correctness proofs of programming languages implemented in terms of bad low-level languages. However, the extra structure also keeps them from performing optimizations that are in some sense "too effective", because it might mess up the distance information. So it both helps and hurts them.

EDIT: I should also give an example of when Banach's fixed point theorem of metric spaces can be useful. In domains, we find fixed points by, basically, Kleene's fixed point theorem. This says that if we have a pointed domain $D$, and a continuous function $f$ on it, then iterating from $\bot$ gives us the least fixed point. This theorem makes no claims about the uniqueness of fixed points in general -- iterating from something other than $\bot$ can give us other fixed points. So if you want to consider recursion definitions on a domain, you have no choice but to admit nontermination into it.

However, you might not want to do that. For example, in my own recent research (with Nick Benton), I've been working on higher-order synchronous dataflow programming. Here, the idea is that we can model interactive programs through time as stream functions. Naturally, we want to consider recursive definitions (for example, imagine writing a function which receives a stream of numbers as inputs, and outputs a stream of numbers corresponding to the sum of the stream elements seen so far).

But an explicit goal of this work is to ensure that only well-founded definitions are allowed, while still allowing recursive definitions. So, I model streams as ultrametric spaces and functions on them as nonexpansive maps (as an aside, this generalizes the causality condition of reactive programming). Under the metric I use, a guarded definition on stream functions corresponds to a contractive function on streams, and so by Banach's fixed point theorem, a unique fixed point exists. Intuitively, the uniqueness property means that computing fixed points works the same no matter what element of the space we start with, so as a result we can compute fixed points of contractive functions on a space, even if the space doesn't have a minimal element in the sense of domain theory.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.