First, a Happy New Year 2017!
Today I would like to comment on a paper by Jimmie Lawson and Xiaoyong Xi [1], which explores a funny idea, due to X. Xi. What is really funny is that nobody seems to have ever thought of it before. I must admit that if I had had the same idea, I would probably have not known what to do with it, but they do something clever with it.
Dcpos of functions
A central problem of domain theory is to explore the structure of the dcpo [X → Y] of all Scott-continuous maps from a topological space X to a dcpo Y. Notably, to interpret the semantics of higher-order programs, a typical question is to find a category C of dcpos that is Cartesian-closed, and that boils down to requiring that [X → Y] is an object of C for all objects X and Y of C.
We have plenty of results in that line. The categories of continuous lattices, of bc-domains, of FS-domains, of RB-domains, of L-domains, are Cartesian-closed. To take a more particular example, in the case of bc-domains, [X → Y] is a bc-domain provided Y is a bc-domain, but we do not need X to be a bc-domain for that, and it is enough that X be a core-compact space (see [2, Proposition 2], an improvement over Proposition 5.7.13 in the book, which requires X to be core-coherent as well).
In most of those kinds of results, we show that [X → Y] has a basis of step functions. What Lawson and Xi show is that we can take something that is more sophisticated.
Let me remind you what a step function is. We assume that Y has a least element ⊥. An elementary step function U ↘ y maps every element of the open set U to y, and all other elements to ⊥. This is always a continuous map. A step function is any pointwise supremum of elementary step function, provided such a pointwise supremum exists. This is again a continuous map.
Pointwise directed suprema
The starting point of [1] is that [X → Y] is not just a dcpo, i.e., it is not just closed under suprema of directed families of maps, it is also closed under pointwise suprema of families of maps that are pointwise directed.
The difference may not be obvious, so let me illustrate.
A family (fi)i ∈ I is pointwise directed if and only if, for every point x ∈ X, the family (fi(x))i ∈ I is directed. This means that I is not empty and, for every x, for all i, j in I, there is a k∈I such that fi(x), fj(x) ≤ fk(x).
The important point is that k may depend on x. If (fi)i ∈ I were directed in the usual sense, then k should be the same for every x in X.
Every directed family of maps is pointwise directed, but the converse is wrong. For example, consider any family of continuous maps from X to [0, 1], with its usual ordering. This family is pointwise directed, because any family of reals is directed, in particular (fi(x))i ∈ I. Take, say, X to be the trivial dcpo Z of all non-positive integers with equality as ordering (i.e., no two distinct elements are comparable), I to be Z itself, and define fi(x) as 1 if x=i, 0 otherwise. As we have noticed, since every family of reals is directed, (fi)i ∈ I is pointwise directed. It is certainly not directed in the usual sense, because all the maps fi are incomparable.
As I have said earlier, [X → Y] is more than just a dcpo. It is closed under suprema of pointwise directed families, not just directed families.
Lemma [1, Lemma 3.2]. Let X be a topological space, and Y be a dcpo. For every pointwise directed family of continuous maps (fi)i ∈ I from X to Y, its pointwise supremum (the function that maps each x of X to supi ∈ I fi(x)) is continuous, hence is the supremum (in the usual, lattice-theoretic sense: the least of the upper bounds) of (fi)i ∈ I.
Proof. Let f(x)=supi ∈ I fi(x), for every x in X. Let V be an arbitrary open subset of Y, and x ∈ f-1(V). Since V is Scott-open, and f(x) is in V, fi(x) is in V for some i in I. Then fi-1(V) is an open neighborhood of x, and it is easy to see that it is included in f-1(V). Therefore f-1(V) is a neighborhood of each of its points, hence is itself open. ☐
Step functions
Following Proposition 5.7.13 of the book, say that a step function ⋁j (Uj ↘ yj) is far below a continuous map f if and only if Uj is way-below f-1(↟yj) for every j. Step functions far below f are automatically way-below f, when X is core-coherent (Lemma 5.7.12). Lawson and Xi call those (or a very close notion) approximating step functions.
Proposition 5.7.13 of the book states that if X is core-compact and core-coherent, and if Y is a bc-domain, then [X → Y] is a continuous dcpo, and that every continuous map is the supremum of a directed family of step functions far below it. Proposition 5.7.14 further states that [X → Y] is then a bc-domain.
The proof of Proposition 5.7.13 shows that if X is core-compact and core-coherent, but Y is only a continuous dcpo with bottom ⊥, then every continuous map is the supremum of a family of step functions far below it. The only reason why we require Y to be a bc-domain in Proposition 5.7.13 is to make sure that that family of step functions is directed.
Allowing ourselves to consider pointwise directed families of step functions, we can hope to obtain better results, or at least different results. Lawson and Xi achieve that by replacing step functions by pointwise suprema of finite pointwise directed families of elementary step functions.
The main theorem—to me— of [1] reads:
Theorem [1, Corollary 4.3]. Let X be core-compact and core-coherent, and Y be an RB-domain. Assume that Y has a bottom. Then [X → Y] is a continuous dcpo.
(The conclusion also holds if instead of requiring Y to have a bottom, we require X to be compact.) The plan of the proof is by successive reductions:
- If Y is a Scott-continuous retract of a bifinite domain Z, then [X → Y] is a Scott-continuous retract of [X → Z]: let r:Z → Y, be the retraction, with section s, then r o _ : [X → Z] → [X → Y] is a retraction, with section s o _. Since a retract of a continuous dcpo is a continuous dcpo, it suffices to show the theorem, assuming that Y is a bifinite domain (with bottom).
- If Y is a bifinite domain, that is, a limit in Top of an ep-system of finite T0 spaces Yj (i.e., of finite posets), then [X → Y] is the limit of a corresponding ep-system of spaces [X → Yj]. Since (projective) limits of ep-systems of continuous dcpos are continuous dcpos (with a basis given by the elements of the inductive limit in Top; to prove it, start from Lemma 9.6.7 in the book, then imitate subsequent developments), it suffices to show the theorem, assuming that Y is a finite poset.
Lawson and Xi do not literally proceed that way, but this is really what is at work here. At any rate, the crux of the argument is to look at the case where Y is finite, with a bottom element.
What they do, then, is to show that, assuming X core-compact and core-coherent, and Y finite with a bottom, then [X → Y] is a continuous dcpo.
However, the basis they use is not given by step functions — try even to define them here! — rather by pointwise directed suprema of finite families of elementary step functions.
Constructing a basis of finite pointwise directed suprema of elementary step functions
This is the most technical part of their work. In the bc-domain case, we could take finitely many elementary step functions, Uj ↘ yj, far below f, take their pointwise supremum, and that was again a (step) function far below f. In our case, such suprema do not exist in general, since Y is an arbitrary poset with bottom, not a semi-lattice.
Instead, following Lawson and Xi, we shall complete any finite family F of elementary step functions far below f to obtain a larger family F’ of elementary step functions, still far below f, in such a way that F’ is pointwise directed. (Moreover, F’ will be finite, too.)
Their pointwise supremum sup F’ will then exist: this is precisely the reason why we need F’ to be pointwise directed. sup F’ will also be continuous, and we observe that it will be way-below f:
Lemma. For every finite pointwise directed family F’ of continuous maps way-below f, sup F’ is also way-below f.
Proof. Let (gi)i ∈ I be a directed family of continuous maps with supremum g above f. For every f’ in F’, since f’ is way-below f, f’ ≤ gi for some i in I. Since (gi)i ∈ I is directed, and F’ is finite, we may take the same i for all f’ in F’. Then, for every x in X, sup F’ (x) ≤ gi (x). ☐
The case of two elementary step functions.
To build the family F’ from F, we first consider the case of just two elementary step functions far below f, U ↘ y and V ↘ z.
If U and V have empty intersection, then {U ↘ y, V ↘ z} is already pointwise directed, since at each point x one of the two functions is equal to ⊥. If y and z are comparable (y≤z or z≤y) then ⊥, y, z form a chain and again {U ↘ y, V ↘ z} is pointwise directed.
So the only interesting case is when U and V intersect and y and z are incomparable. Say that {U ↘ y, V ↘ z} is a critical pair in that case.
We look at all upper bounds of {y, z} in Y. Since Y is finite, some of these upper bounds are minimal, and we naturally call them the minimal upper bounds of {y, z}. There are only finitely many of them, since Y is finite.
Define a lift of {U ↘ y, V ↘ z} as any elementary step function W ↘ t far below f such that t is a minimal upper bound of {y, z}, and W is non-empty. (Lawson and Xi already require that W intersects U ∩ V, but that is unnecessary.) A finite family of lifts Wi ↘ ti of {U ↘ y, V ↘ z} is a covering of {U ↘ y, V ↘ z} if and only if the union of the open sets Wi contains U ∩ V.
Lemma [1, Lemma 3.6]. Let X be core-compact and core-coherent. Every critical pair of elementary step functions far below f, U ↘ y and V ↘ z, has a covering Wi ↘ ti, 1≤i≤m. Moreover the elements ti are exactly the minimal upper bounds of {y, z}.
Proof. From the definition of far below, U ⋐ f-1(↟y), that is, U ⋐ f-1(↑y), since ≪ and ≤ coincide on a finite poset. Similarly, V ⋐ f-1(↑z). By core-coherence, U ∩ V ⋐ f-1(↑y) ∩ f-1(↑z) = f-1(↑y ∩ ↑z) = ∪t f-1(↑t), where t enumerates the minimal upper bounds of {y, z}. Union is trivially a Scott-continuous operation on O(X), and O(X) is a continuous poset since X is core-compact. Proposition 5.1.66 of the book says that every Scott-continuous map on a continuous poset reflects the way-below relation. The way-below relation is ⋐ here. That union reflects way-below means that if A ⋐ ∪t Bt, where A and Bt are open, then there are open subsets Wt ⋐ Bt such that A ⊆ ∪t Wt. We apply this to A=U ∩ V and to Bt=f-1(↑t), remove the indices t for which Wt is empty, and we are done. ☐
Arbitrary finite families of elementary step functions.
We now consider the case of an arbitrary finite family F of elementary step functions far below f.
Lemma [1, Lemma 3.8]. Let F be a finite family of elementary step functions far below f. There is a finite family of elementary step functions F’ far below f that contains F and is pointwise directed.
Proof. Call height of an element y in Y the length of a longest increasing path from ⊥ to y. Note that, in the previous lemma,the height of each of the minimal upper bounds ti is strictly larger than the heights of both y and z. Let us call height of an elementary step function U ↘ y, the height of y if U is non-empty, 0 otherwise.
For every critical pair, pick a covering of it (as guaranteed by the previous lemma), and call it the covering of the critical pair.
Let F0=F. Build F1, the union of the coverings of critical pairs of F. The height of each element of F1 is strictly larger than the heights of elements of F, hence is at least 1.
Let now F2 be the union of the coverings of critical pairs {U ↘ y, V ↘ z} where U ↘ y is in F0 ∪ F1, and V ↘ z is in F1. This contains only functions of height at least 2.
Iterate: let F3 be the union of the coverings of critical pairs {U ↘ y, V ↘ z} where U ↘ y is in F0 ∪ F1 ∪ F2, and V ↘ z is in F2 (this contains only functions of height at least 3), etc.
The process must stop because Y has finite height, say at Fk. That means that all critical pairs at step k have an empty covering. However, for a critical pair {U ↘ y, V ↘ z}, U ∩ V is non-empty, and cannot be contained in an empty union: the covering of a critical pair cannot be empty. It follows that there is simply no critical pair at step k of the completion process.
Let F’ be F0 ∪ F1 ∪ F2 ∪ … ∪ Fk.
Before we proceed, note that the construction of F’ ensures that:
(*) the covering of every critical pair included in F’ is included in F’.
Indeed, given such a critical pair, one of the elements of the critical pair, call it V ↘ z, will be in Fj, for some index j that we can take minimal, and the other one, call it U ↘ y, will be in F0 ∪ F1 ∪ F2 ∪ … ∪ Fj. By construction, the covering of {U ↘ y, V ↘ z} is included in Fj+1, hence in F’.
It remains to show that F’ is pointwise directed. We pick an arbitrary point x in X, and two elementary step functions U ↘ y, V ↘ z in F’. We need to show that there is another elementary step function W ↘ t whose value at x is above the values of both U ↘ y and V ↘ z at x.
- This is clear if x is not in U: then (U ↘ y) (x)=⊥ is below (V ↘ z) (x), so we can take W ↘ t=V ↘ z.
- This is clear if x is not in V, by symmetry: we take W ↘ t=U ↘ y.
- If x is in U ∩ V, and y and z are comparable, say y≤z, then (U ↘ y) (x)=y≤z=(V ↘ z) (x), and we take W ↘ t=V ↘ z — W ↘ t=U ↘ y if instead z≤y.
- It remains to see what happens when x is in U ∩ V, and y and z are incomparable. By (*), the covering Wi ↘ ti, 1≤i≤m, of {U ↘ y, V ↘ z} is included in F’. By definition, the union of the open sets Wi contains U ∩ V. Let i be an index such that x is in Wi. We let W=Wi, t=ti: W ↘ t is in F’, and since W ↘ t is a lift of {U ↘ y, V ↘ z}, (W ↘ t) (x) = t is above both y = (U ↘ y) (x) and z = (V ↘ z) (x). (Recall that t is even a minimal upper bound of y and z.) ☐
The final step.
We can now conclude. Recall that X is assumed to be core-compact and core-coherent, and that Y is a finite poset with bottom. (The case Y an RB-domain with bottom is, as we have seen, pretty much of an automatic consequence.) We wish to show that [X → Y] is a continuous dcpo, with a basis of finite pointwise directed suprema of elementary step functions.
Let f be any continuous map from X to Y. Because X is core-compact, the set of elementary step functions far below f is non-empty, and its pointwise supremum if equal to f. Indeed, for every x in X and every y in Y, we show that there is an elementary step function U ↘ y far below f such that (U ↘ y) (x)=y: it suffices to pick U so that x ∈ U ⋐ f-1(↑y). (We are using the fact that Y is finite to obtain that ↑y is open. A similar, and only slightly more complex argument shows that f is the supremum of elementary step functions far below f for any poset Y whatsoever.)
The difficult point is to find a directed family of functions way-below f whose supremum equals f. Indeed, the family of elementary step functions fails to be directed in general. In the case of bc-domains, we could take the obvious choice: suprema of finite families of elementary step functions, also known as step functions. Since step functions do not exist in our case, we take the more elaborate collection of pointwise suprema sup F of finite pointwise directed families F of elementary step functions far below f. We have already noticed that sup F is then way-below f.
To show that this collection is directed, let F and G be two finite pointwise directed families of elementary step functions far below f. Then the completion H=(F ∪ G)’ of F ∪ G is a finite pointwise directed family of elementary functions far below f. Since H contains F, sup H ≥ sup F, and similarly sup H ≥ sup G. ☐
Final words
So we have learned that if X is core-compact and core-coherent, and Y is an RB-domain with bottom, then [X → Y] is a continuous dcpo. This improves on two known results:
- one that I have mentioned earlier in that post, that this was known to hold under the stronger assumption that Y is a bc-domain, in which case [X → Y] is not just a continuous dcpo, but even a bc-domain;
- another one, that the same result was known to hold when both X and Y are RB-domains (Theorem 9.6.24 in the book), in which case [X → Y] is not just a continuous dcpo, but even an RB-domain.
In the case that we have been looking at, we do not know more than the fact that [X → Y] is a continuous dcpo. Lawson and Xi show [1, Theorem 5.7] that if X is a coherent algebraic dcpo, and if Y is a bifinite domain with bottom, then [X → Y] is a bifinite domain again, and I will let you read the paper for yourselves to understand how this is proved.
However, beyond the mere results, one should probably remember the new construction of directed families of functions way-below a given f discovered by Lawson and Xi, based on finite pointwise directed suprema of elementary step functions, and on a clever completion procedure.
— Jean Goubault-Larrecq (January 12
- Lawson, Jimmie and Xi, Xiaoyong. Continuity of Function Spaces from Pointwise Directed Families of Characteristic Functions. Order 32(3), December 2014.