Domains XII

In my last post, I said I would have trouble finding time to write anything up in August, and sadly, this came out true. Late August, I went to the Domains XII conference, and it may be a good idea if I gave a report on a few of the things I learned there.  Some, but not all, of the slides of talks are present on the conference page.

Before I start, let me mention I gave a talk there, which roughly covers Sections 7.1 through 7.5 of the book on quasi-metric spaces, completeness and completions.  If you are interested in this, it may give a shorter and more efficient introduction to those topics, before you read about them in the book.  Some of the proofs are also simpler.

All cartesian closed categories of quasi continuous domains consist of domains

Probably one of the most stunning results announced there, or so I think, was announced by Achim Jung.  This is common work with Kou Hui, Jia Xiaodong, Li Qingguo, and Zhao Haoran.  Achim did not use any slide, so I cannot direct you to any, but his blackboard talk was fantastic.  The result is, too.  It was recently published as All cartesian closed categories of quasicontinuous domains consist of domains. Theor. Comput. Sci. 594: 143-150 (2015).

Achim started his talk as follows.  We know of quite a few cartesian closed categories of domains, that is, whose objects are continuous dcpos.  (We always take morphisms to be all continuous maps, and I will always assume that in the sequel.)  There are the algebraic complete lattices, the continuous complete lattices, the algebraic bc-domains, the (continuous) bc-domains, the bifinite domains, RB-domains, FS-domains, and L-domains.  There are others as well, for example, any of the latter restricted to second-countable spaces.

That is fine.  However, all of them conflict in some precise sense with Claire Jones’ probabilistic powerdomain construction.  The latter is needed in giving semantics to higher-order probabilistic functional languages, and was developed in her PhD thesis.  The probabilistic powerdomain V(X) of a space X is, roughly speaking, the set of measures on X.  Jones uses the slightly different notion of continuous valuation instead of measure, as this is more practical, but that does not make much of a difference.  One of the landmark result in her PhD thesis (1990) is that the probabilistic powerdomain V(X) of a continuous dcpo X is again a continuous dcpo.  This is non-trivial.

We need the probabilistic powerdomain to interpret probabilistic choice (as one would expect), and we need cartesian-closedness to interpret higher-order computation, that is, functions as first-class objects, functions taking functions as arguments, etc.  Since continuous dcpos form a cosy category to do mathematics in, we would like to find a category of continuous dcpos that is both cartesian closed and closed under the probabilistic powerdomain construction.

Jones had already shown that this would be hard.  Precisely, the categories of bc-domains (or Scott-domains, whether algebraic or merely continuous) do not qualify.  She shows that, for one of the simplest bc-domains X, V(X) is not a bc-domain (p.88 of her PhD thesis).  X is just the three element set {0, 1, ⊤} with ⊤ above 0, 1, and 0 and 1 incomparable.  She shows that the measures ½δ0 and ½δ1 have no least upper bound, although they do have an upper bound (for example, ½δ⊤, or ½δ0+½δ1). In fact they have uncountably many minimal upper bounds, which is (almost) as far as we can imagine from being bounded-complete.

Our next hope would be to show that some other known category of continuous dcpos would be closed under the probabilistic powerdomain functor V.  Jones’ argument also rules out the L-domains, so only RB-domains and FS-domains remain (bifinite domains are excluded since V(X) is never algebraic).

Almost twenty years ago, Achim Jung and Regina Tix examined the question.  Their paper, aptly named the troublesome probabilistic powerdomain (in Third Workshop on Computation and Approximation, Proceedings, Electronic Notes in Theoretical Computer Science, vol 13, 1998, 23 pp.) gives incredibly weak results in that direction, but nobody has been able to say more since then.  What they showed is: the probabilistic powerdomain of a finite rooted tree is an RB-domain (in fact even a bc-domain), and the probabilistic powerdomain of a finite reversed rooted tree is an FS-domain.  They also showed that the probabilistic powerdomain of a stably compact dcpo is again stably compact, but simpler and more general proofs of that latter result have been given since then.

In an attempt to go beyond the difficulty, I turned to the larger category of quasi-continuous domains, and I have shown that the category of QRB-domains is closed under the probabilistic powerdomain functor.  In fact, I have invented QRB-domains precisely for that purpose — although showing that QRB-domains are closed under the probabilistic powerdomain functor is not trivial either.  The relevant papers are QRB-domains and the probabilistic powerdomain, Logical Methods in Computer Science 8(1:14), 2012, which shows that result under the additional constraint that the QRB-domains under consideration are second-countable; and QRB, QFS, and the probabilistic powerdomain, MFPS’14, ENTCS 308, pages 167-182. Elsevier Science Publishers, 2014, which shows the general result (i.e., not assuming second-countability), in addition to showing that QRB-domains are exactly the same as Li and Xu’s QFS-domains, and are also exactly the locally finitary, stably compact spaces.  I have discussed the latter in a previous post.

However, QRB-domains are themselves not a cartesian-closed category, as found by an anonymous referee of my first QRB paper.  Still, there was renewed hope that one might find other, cartesian-closed categories of quasi-continuous dcpos that would be closed under the probabilistic powerdomain functor.

What Jung, Kou, et al., have proved is that this hope is doomed.

This is great!  At least we know there is nothing new to look for here.

What they have proved is that, if you happened to find some new cartesian-closed category of quasi-continuous dcpos, then it would in fact consist of continuous dcpos only.

Since this post is starting to be a bit long, I will not try to tell you how this works, or at least not yet.  Let me just say their result relies on several ingredients:

  • an important idea of Kou, first, about so-called meet-continuous posets; this is important mathematics, and I would like to talk about it in more detail later; notably, the continuous dcpos are exactly those quasi-continuous dcpos that are also meet-continuous, a remarkable result by Kou, Liu and Luo;
  • Iwamura’s Lemma; without it, Kou had proved a similar result, in the world of second-countable quasi-continuous dcpos, and Iwamura’s Lemma allow them to go beyond; I have discussed Iwamura’s Lemma in a previous post;
  • the identification of certain canonical forbidden subposets, namely: given an infinite well-ordered chain C, consider the dcpo M(C) obtained by adjoint a new top element and another new element below the top element, but incomparable to all elements of C; consider also the same dcpo with a bottom element adjoined; these dcpos are QRB-domains that are not continuous; using Iwamura’s Lemma, they manage to show that every dcpo that fails to be meet-continuous must contain one of those as a retract.

Join-continuity + hypercontinuity = prime-continuity

Earlier on the same week, Ho Wengkin gave a talk on a very nice result by himself, Achim Jung, and Zhao Dongsheng, entitled join-continuity + hyper continuity = prime-continuity.
I’m afraid the title is perhaps giving no clue how nice the result is.  Above, I have said that the continuous dcpos are exactly the quasi-continuous dcpos that are also meet-continuous.
This is a pretty difficult theorem.  You can find a version of it in the bible of the field, continuous lattices and domains, by G. Gierz, K.-H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott (Theorem O-4.2), but that only applies on directed-complete semi lattices.  In the latter, you have a binary infimum operation (“meet”), and meet-continuity just means that meet is Scott-continuous.  However, there is an alternate way of expressing meet-continuity that does not mention the meet operation any longer, and one can then define the much larger class of meet-continuous posets.
It is with that new definition that one can show that the continuous dcpos are exactly the quasi-continuous dcpos that are also meet-continuous.
However, as I have said, this is a pretty difficult theorem.  Ho Wengkin had the idea that one might obtain a simpler proof through Stone duality.  That it would indeed produce a simpler proof was far from obvious, already because working in Stone duals usually involves added complications.  For example, the Stone dual of a quasi-continuous dcpo is a hyper continuous lattice, which is a complicated beast.  I have discussed them in a previous post, and tried to make them look as simple as I could, but I am not sure I succeeded.
Anyway, Wengkin observes that the Stone duals:
  • of quasi-continuous dcpos are hyper-continuous lattices
  • of meet-continuous dcpos are join-continuous lattices (not the lattices where the join, that is, the binary supremum operation, is Scott-continuous, mind you — that much is always true; instead, this is the order dual of meet-continuity, namely: binary suprema commute with filtered infima)
  • of continuous dcpos are prime-continuous lattices (=completely distributive complete lattice, by Raney’s Theorem; see Exercise 8.3.16 in the book; the duality statement itself is Theorem 8.3.43 in the book).
So one would obtain an alternate proof by showing that the prime-continuous lattices are exactly those hyper-continuous lattices that are also join-continuous.
That eventually boils down to pretty simple verifications, which are completely spelled out, in every detail, in slides 50—60 of Wengkin’s presentation (most of them being overlays).  This is a very short argument:
  • He shows that, in a join-continuous complete lattice L, if you consider finitely many elements m1, …, mn, then look at the complements C1, …, Cn of ↓m1, …, ↓mn, then inf (C1 ∩ … ∩ Cn) = supi=1, …, n inf Ci. This is a three-line proof using join-continuity twice.
  • Using one of the many equivalent definitions of hyper-continuity, he knows that in a hyper-continuous complete lattice L, every element u is the supremum of all the inf (C1 ∩ … ∩ Cn), where C1, …, Cn are obtained as above from finite subsets {m1, …, mn}, and we let the latter range over all those finite subsets whose downward-closure does not contain x.
    By the item above, x is then the supremum of all the complements of ↓m (for single points m) when m ranges over the points whose downward-closure does not contain x. And that is an alternate characterization of prime-continuity.

If you look at Wengkin’s slides carefully, you’ll also realize that this not only implies that continuity=quasi-continuity+meet-continuity for dcpos, but even for posets.  That is great.

 Other exciting talks

I will not describe the other talks in detail, but some of them were fascinating, intriguing, or both.

Klaus Keimel explained how domain theory arose naturally in the search for so-called trace operators on Banach algebras, by Elliott, Robert, and Santiago.  The latter was developed independently from domain theory, and Klaus investigated it, realizing that a good share of it was domain theory, and specifically the notion of abstract Cuntz semigroups.

An abstract Cuntz semigroup is an Abelian monoid that is also a continuous dcpo for which addition is continuous and respects the way-below relation (namely, if a ≪ a’ and b ≪ b’ then a+a’ ≪ b+b’).  He then defines pre-Cuntz semigroups as abstract bases for abstract Cuntz semigroups, and proceeds from there.

Although Klaus does not state it explicitly in his slides, there would be an equivalent topological definition of the latter, as an Abelian monoid with a topology that makes it a c-space in which addition is both continuous and almost open (see Proposition 4.10.9 in the book for the definition of almost open).  Since abstract bases and c-spaces are essentially the same thing (Exercise 8.3.46), the only thing to check is that preserving the way-below relation is equivalent to being almost open.  I’ll let you do that as an exercise.  You then obtain all Cuntz semigroups as sobrifications of pre-Cuntz semigroups.

Abbas Edalat showed how the notion of Clarke gradient, used to define extended notions of gradients of non-differentiable (but Lipschitz) forms on n-dimensional real vector spaces, could be reconstructed domain-theoretically, in a way that is in fact, much more natural, in a sense.

Equip the set of Lipschitz forms with the so-called L-topology, which is the coarsest topology that refines the sup norm topology and makes the Clarke gradient continuous.  He shows that the subspace of those Lipschitz forms that are C1, equipped with the induced topology, is the space of C1 Lipschitz forms with the familiar C1 norm topology. This subspace is dense in the space of all Lipschitz forms. We also have a familiar gradient map D from the smaller space to the space of Scott-continuous linear forms. The latter is a bc-domain, hence a densely injective topological space (Exercise 9.3.12), so D extends to a continuous map from the larger space of all Lipschitz forms to the space of Scott-continuous linear forms. We even know that D has a largest continuous extension. Abbas showed that this largest continuous extension is, in fact, exactly the Clarke gradient operator. There is a circularity here, as the L-topology is in fact defined in terms of the Clarke gradient, but the result remains non-obvious, and fascinating.

Paul Bilokon gave a talk to the effect that Wiener measure (the measure at work behind brownian motion) was obtained as a limit of domain-theoretic approximations in dcpo models, obtaining Willem Fouché’s celebrated result that Wiener measure is computable as a corollary.

There were many other interesting talks, but I guess that that should be enough for this month’s post!

— Jean Goubault-Larrecq (September 26th, 2015)jgl-2011