Powerdomains and hyperspaces IV: theories

type 'a SUITopSLatTerm = Var of 'a
                       | Zero
                       | Vee of 'a SUITopSlatTerm * 'a SUITopSLatTerm;;

where x, y, z are distinct variables.  The model is given by interpreting ∨ as union and 0 as the empty set, that is, by defining M_∨ as union and M₀ as the empty set.

If you prefer to reason categorically, given a signature Σ, there is a category of “sets with a function for each function symbol in Σ”.   (I am ignoring arities for the sake of readability.)  This is the category Alg_Σ of all Σ-algebras.

The forgetful functor to Set has a left adjoint Term_Σ, which maps every set V (yes, any set can play the role of a set of variables) to the set of terms over Σ and V.  The latter is a very simple kind of Σ-algebra: for each function symbol f, there is a map M_f, which maps every tuple of terms t₁, …, t_n to the term f (t₁, …, t_n).  So much for terms.

The unit of the adjunction, η : V → Term_Σ(V), maps every variable x to x itself, seen as a term.  (In our OCaml example, this map sends every variable x to Var(x) instead.)

Since Term_Σ(V) is the free Σ-algebra over the set V, for each set map ρ : V → D, there is a unique map of Σ-algebras, from Term_Σ(V) to D, that gives back ρ when precomposed with η : V → Term_Σ(V).  This is the interpretation map, the one that sends every term t to M[t] ρ.

Building the free sober T-algebra: first ideas

All right, now take a fixed theory T.  There is a known construction of a free continuous domain T-algebra over any continuous dcpo X [1, Section 6.1.2].  (A domain T-algebra is just a T-algebra, except the support D is a dcpo and the functions M_f are required to be Scott-continuous.)

The rough idea is not that complicated, but I have always been puzzled by how subtle it could be, and by the fact that this only worked for continuous dcpos.

This works as follows.  We start from Term_Σ(X)—think of that as a set of trees whose leaves are elements of X instead of variables.  You may need to pause on that.  There is nothing special about variables.  The set of variables can be anything we wish, and in particular X. Have you digested this?  If so, then we can go on.

We declare two terms s, t equivalent if and only if one can deduce the two inequalities s ≤ t and t ≤ s from the inequalities of the theory T, by the usual rules (I will be more precise below).  Then we consider the quotient of Term_Σ(X) by this equivalence, and consider that quotient as an abstract basis. To this end, we need to define an interpolative relation ≺ on that set (see Lemma 5.1.32 in the book).  We declare that (the equivalence class of) s directly approximates (the equivalence class of) t if and only if one can reach s, starting from t, by first going to a term u ≤ t, then replacing all the variables in u (which are just values in X) by values that are way-below in X, obtaining a new term v, then checking that s ≤ v.  The interpolative relation ≺ is the transitive closure of that relation of direct approximation [1, Lemma 6.1.5].  Finally, the rounded ideal completion of that abstract basis will give you the free object in the category of continuous T-algebras, over X [1, Theorem 6.1.6].

As for many things domain-theoretic, I had the feeling that this can be made clearer and more general by looking at the problem in a topological way instead.  My initial guess was to put a topology directly on Term_Σ(X), satisfying a few properties, and to take the sobrification of the resulting space. The properties that I had imagined were:

• η : X → Term_Σ(X), which maps every variable to itself as a term, is continuous;
• for each n-ary function symbol f, the map that sends every tuple of terms t₁, …, t_n to the term f (t₁, …, t_n), is continuous (we shall simply call f that map);
• every open U is upward-closed, in the sense that for every term s in U and for every term t such that we can deduce s ≤ t from the theory T, then t is in U.

The resulting topology would fail very badly to be T₀, because of the latter item. But sobrification, which in particular equates all the points that are in the same open subsets, would take care of that.

This approach does not work out of the box. We would need something like the coarsest topology satisfying the above. However, the requirement for f to be continuous is hard to enforce.  Requiring f to be separately continuous instead would probably give us a topology, but that is not quite the same thing.

Instead, we shall look at a simpler case first (the order-theoretic case).  We shall find our way through successive generalizations, the algebraic case, then the general topological case and finally the sober case.

If you ever get lost, keep in mind the following:

The free (ordered, or topological) T-algebra on X will always be a set of trees with function symbols from the signature Σ, and variables from X, suitably quotiented.

The only problem will be to find the right topology to put on this set of trees.  The discussion above shows that this is the real problem.

The order-theoretic case

Instead of working in the category of topological case, we first deal with the simpler case of quasi-orderings.  The situation is as follows.  Consider a quasi-ordered set X, and try to find the free quasi-order T-algebra on X.  A quasi-order T-algebra is a T-algebra with a quasi-ordering ≤ such that:

• for every inequality s ≤ t in the theory T, the model satisfies M[s] ρ ≤ M[t] ρ for every environment ρ;
• for every function symbol f, M_f is monotonic.

An order T-algebra is defined similarly, except that ≤ is required to be an ordering.

Given a quasi-ordered set X, we extend the quasi-ordering ≤ on X to one on Term_Σ(X) as the smallest relation ≤^* that satisfies the following.  We write ≤^* for the extension, so as to distinguish it clearly from ≤.

• (Extension) for all x, y in X, if x ≤ y in X, then x ≤^* y as terms, in Term_Σ(X);
• (Reflexivity) s ≤^* s for every s in Term_Σ(X);
• (Theory) given any inequality s ≤ t in T, for every environment ρ : V → Term_Σ(X), sρ ≤^* tρ; sρ denotes the result of replacing each variable x in s by the corresponding term ρ(x), and similarly for tρ (if you don’t mind being puzzled for a second, note that sρ is just the meaning [s]ρ of s in environment ρ, considering Term_Σ(X) itself as a T-algebra);
• (Transitivity) if s ≤^* t and t ≤^* u, then s ≤^* u;
• (Application) if s₁ ≤^* t₁, …, s_n ≤^* t_n, then f(s₁, …, s_n) ≤^* f(t₁, …, t_n), for every f in Σ, of arity n.

With the quasi-ordering ≤^*, Term_Σ(X) is a quasi-order-T-algebra. The map η : X → Term_Σ(X), which maps every variable x to itself as a term, is monotonic, by (Extension).

Finally, for every monotonic map β from X to the support D of a quasi-order-T-algebra M, β extends to a unique monotonic morphism Φ of quasi-order-T-algebras from Term_Σ(X) to M. For each term t, Φ(t) is defined by induction on t:

• for every x in X, Φ(x)=β(x);
• Φ(f (t₁, …, t_n)) = M_f (Φ(t₁), …, Φ(t_n)).

In other words, Term_Σ(X), with the quasi-ordering ≤^*, is the free quasi-order-T-algebra over the quasi-ordered set X, ≤. Good.

The quasi-ordering ≤^* is not in general an ordering, even if X is a poset. For example, if the theory T contains the axiom (associativity) (x ∨ y) ∨ z = x ∨ (y ∨ z), then the terms (s ∨ t) ∨ u and s ∨ (t ∨ u) will both be below each other, for all terms s, t, and u.

However, every quasi-ordering induces an equivalence relation: define s=^*t if and only if both s ≤^* t and t ≤^* s. For equivalence classes [s] and [t] (of s and t, respectively, under that equivalence relation), we define [s] ≤^* [t] if and only if s ≤^* t. This defines an ordering (not just a quasi-ordering), and the quotient poset Term_Σ(X)/=^* is then the free order-T-algebra over the poset X.

The algebraic case

Now consider an algebraic dcpo X.  Recall that a domain T-algebra is an order T-algebra in which the support D is a dcpo and where the functions M_f are Scott-continuous. We build the free domain T-algebra above X as follows. We first extract the poset K of finite elements of X. We then build the free quasi-order T-algebra on K. This is Term_Σ(K), with the quasi-ordering ≤^*, as we have just seen. (We could also take the free order T-algebra on K, Term_Σ(K)/=^*, but this really does not matter.) To obtain a dcpo from that, we build its ideal completion I(Term_Σ(K)).

The point of that construction is that finding continuous operations on an algebraic dcpo is exactly the same thing as finding monotonic operations on their poset of finite elements.  Therefore, finding the free domain T-algebra on an algebraic domain will reduce to the problem of finding the free (quasi-)order T-algebra on a poset, a problem we have just solved.

The ideal completion is dealt with in Definition 5.1.45, and Proposition 5.1.46 tells us that the ideal completion I(B) of a poset B is an algebraic dcpo, whose finite elements are isomorphic to B.  When B is merely quasi-ordered, the same results hold, except the finite elements of I(B) are isomorphic to the quotient of B by the equivalence relation induced by the quasi-ordering.

In particular, I(Term_Σ(K)) is an algebraic dcpo. There are a few properties we must check:

• η : X → I(Term_Σ(K)) is continuous: instead of defining it and checking that it is continuous afterwards, we can just build it so that it is continuous by definition. There is a map that sends each x in K to x itself, as an element of Term_Σ(K). Compose that with the inclusion of Term_Σ(K) into I(Term_Σ(K)) (which maps every term t to ↓t), so that we obtain a monotonic map from K to I(Term_Σ(K)). This has a unique continuous extension to X (see Exercise 5.1.62), and we call it η.
• Each function f in Σ is continuous, namely, Scott-continuous.  Call n the arity of f. We proceed as for η. First, f defines a monotonic map from Term_Σ(K)ⁿ to Term_Σ(K), by rule (Application). We obtain a monotonic map from Term_Σ(K)ⁿ to I(Term_Σ(K)) by composing with the inclusion of Term_Σ(K) into I(Term_Σ(K)). This extends to a unique continuous map from I(Term_Σ(K)ⁿ) to I(Term_Σ(K)). This is almost what we want, except that we need the domain of the map to be [I(Term_Σ(K))]ⁿ, not I(Term_Σ(K)ⁿ).  We are saved by the fact that ideal completions commute with finite products, up to natural isomorphism.  You can check it by hand.  Alternatively, use the following roundabout argument: ideal completion is sobrification (see comment after Exercise 8.2.48), and sobrification preserves product up to natural isomorphism (Theorem 8.4.8).
• I(Term_Σ(K)) satisfies all the inequalities of the theory T. Given any term t in Term_Σ(V), the meaning map [t], which maps every environment ρ : V → Term_Σ(K) to [t]ρ, is monotonic, as a composition of monotonic maps. Again, it extends to a unique continuous map, again written [t], from extended environments ρ’ : V → I(Term_Σ(K)) to I(Term_Σ(K)).  Since it is unique, it coincides with the unique continuous map defined by [x]ρ’ = ρ'(x), [f(t₁, …, t_n)]ρ’ = f ([t₁]ρ’, …, [t_n]ρ’), where the effect of f on the ideal completion was found in the last bulleted item.  To check that [s]ρ’ ≤ [t]ρ’ for every extended environment, it is enough to check that [s]ρ ≤ [t]ρ for every environment with values in Term_Σ(K). But we know that already, from the previous section on the ordered case.

Finally, for every continuous map β from X to the support D of a domain T-algebra M, β restricts to a continuous map from K to M.  We know from the previous section that β extends to a unique monotonic morphism Φ of quasi-order-T-algebras from Term_Σ(K) to M.   Since I is left adjoint to the forgetful functor from dcpos to orders (Exercise 5.5.3), Φ extends to a unique continuous map from I(Term_Σ(K)) to M. The same uniqueness arguments as above show that Φ commutes with application of f, for every function symbol f in Σ, so Φ is a continuous morphism of T-algebras.  Finally, it coincides with β not only on K, but on the whole of X, again by uniqueness of extensions.

We conclude that:

Theorem 1. Given any algebraic dcpo X, there is a free domain T-algebra on X, and it is algebraic as a dcpo.
This free domain T-algebra is the ideal completion I(Term_Σ(K)) of the quasi-order T-algebra of terms built from function symbols in Σ and from “variables” taken from the set K of finite elements of X.

This is important per se.  The continuous case can be obtained by realizing that, if X is continuous, then it is a retract of some algebraic dcpo Y  (see Theorem 5.1.48).  Then build the free domain T-algebra on Y, and construct the free domain T-algebra on X as a suitable retract of the former.  (Hint: both I and Term_Σ are functors.) This shows that every continuous dcpo has a free domain T-algebra on it, and that it is continuous. The construction from [1, Section 6.1.2] builds the same object, up to natural isomorphism, except in a more concrete way.

The topological case

Let us jump to the whole category of all T₀ topological spaces.  We wish to build the free T₀ topological T-algebra on X. A T₀ topological T-algebra is, as you can expect, a T-algebra M whose support is a T₀ topological space, and on which every function M_f is continuous.

To do so, we reduce to the previous case (again). Explicitly, we embed X in a much larger space, which will happen to be an algebraic dcpo.  Then we apply the previous construction to that large space, and carve out the needed bit from it.

To do so, let X be a T₀ space. We can embed it into an algebraic dcpo Y. The typical construction is to take the powerset P(O(X)) of the set O(X) of open subsets of X for Y; the embedding i : X → Y maps each point x in X to its set of open neighborhoods. (See Proposition 9.3.5.) Note that Y is also a complete lattice.

In the sequel, I will forget about i and simply consider that X is a subspace of an algebraic complete lattice Y.  I will then build the free T₀ topological T-algebra on X as a subspace A of the free domain T-algebra on the much larger space Y.

In the previous section, we have seen that there is a free domain T-algebra on Y. This is I(Term_Σ(K)), where K is the set of finite elements of Y, namely the set of finite sets of open subsets of X… but reasoning at that level of detail would get us lost. Simply call T(Y) the free domain T-algebra on Y, for the rest of this post.

We again forget about embeddings, and consider that Y itself appears as a subset of T(Y). If we were to be formal, that would be a topological embedding (not a T-algebra embedding). With those conventions, note that X is then an even smaller subspace of T(Y).

There is a subspace A of T(Y), built as the smallest subset that contains X and that is closed under application of function symbols f in Σ. (The effect of those function symbols is taken to be their effect in T(Y).) As such, A is not only a subspace, but also a sub-T-algebra.

It is now fairly easy to see that A is the free T₀ topological T-algebra on X.  For that, consider any continuous map β from X to (the underlying topological space) of a topological T-algebra M, with support D. To this end, we notice that β extends to a continuous map from Y to D, which then extends to a unique domain T-algebra morphism from T(Y) to M. Restrict the latter to A, obtaining a map β’. As the restriction of a continuous map, β’ is continuous. It is also a morphism of T-algebras. The fact that β’ is unique is obvious: we must have β'(x)=β(x) for every x in X, and β'(f(t₁, …, t_n)) = M_f (β’ (t₁), …, β’ (t_n)), and this suffices to define β’ uniquely on A.

Theorem 2.  For every T₀ topological space X, there is a free T₀ topological T-algebra on X.

Although it might look very abstract, that free T₀ topological T-algebra is just the set Term_Σ(X) of trees with “variables” taken from X, suitably quotiented and topologized. The reason for all the complication with ideal completions, embeddings into powersets and what have you is just to define the topology on that set of trees.

Let us return for a moment to the theory of unital inflationary topological semi-lattices. The terms are built from the constant 0, the binary symbol ∨ and variables. One must quotient those terms, considering ∨ as associative, commutative and idempotent, with 0 as neutral element. A moment’s reflection should convince you that this quotient is isomorphic to some set of finite subsets of X. For example, the equivalence class of the term x ∨ (y ∨ z) should look like the finite set {x, y, z}. However, the (inflationary) inequality also forces some other identifications, such as {x} = {x, y} if x ≤ y. The complex construction we have described above serves to put the right topology on this set of finite subsets.  Eventually, a canonical representative of a finite set will be its downward-closure (e.g., ↓{x, y, z}): the free T₀ topological T-algebra on X, where T is the theory of unital inflationary semi-lattices, is the set of finitary closed subsets of X, with some topology.  I’ll let you check that this is the lower Vietoris topology.  But please! do not try to check it directly.  The only nice way to do so that I know of is to check that the set of finitary closed subsets of X with the lower Vietoris topology is the unique (up to natural isomorphism) T₀ topological T-algebra on X; so it must coincide with what our tree-based construction yields, up to natural isomorphism.

Sober T-algebras

We had seen in part I that H(X) is the free sober T-algebra, for the theory T of unital inflationary semi-lattices.  The free T₀ topological T-algebra is a bit disappointing, as it contains only finitary closed sets, and free sober T-algebras look more promising.

So let us look for free sober T-algebras in general.  Sober T-algebras are just T₀ topological T-algebras whose support is sober.

Looking back at the construction of the previous section, we realize that A is not necessarily sober.  (The space of finitary closed subsets of a space, for one, is not sober, as its sobrification is in fact the whole of H(X).)  But it sobrification S(A) will be.  We claim that S(A) will be the sought after free sober T-algebra.

The topological embedding of A into T(Y) lifts to a topological embedding of S(A) into S(T(Y)) (Lemma 8.4.11). Furthermore, since T(Y) is an algebraic dcpo, hence sober, the latter is just T(Y). All this allows us to see S(A) as a sober subspace of T(Y).

Any continuous map from Aⁿ to a sober space extends to a unique continuous map from S(Aⁿ) to the same sober space (Lemma 8.2.44). Since S(Aⁿ) is naturally isomorphic to [S(A)]ⁿ (Theorem 8.4.8), we obtain that S(A) is also a Σ-algebra where the application of each function symbol is continuous. Inequalities are preserved, too, because sobrification preserves order, namely if f ≤ g as continuous maps, then S(f) ≤ S(g). (Exercise: use Lemma 8.2.42 for a definition of S(f).) Therefore S(A) is a sober T-algebra.

We have almost finished to prove that S(A) is the free sober T-algebra on X. Consider any continuous map β from X to (the underlying topological space) of a sober T-algebra M, with support D. This extends to a unique continuous morphism of T-algebras β’ from A to M, by the results of the previous section. In turn, β’ extends to a unique continuous map from S(A) to M, since M is sober.
Using arguments similar to some that we have already seen (uniqueness of extensions), that extension also commutes with applications of function symbols from Σ. Therefore it is also a morphism of T-algebras. We have proved:

Theorem 3.  For every T₀ topological space X, there is a free sober T-algebra on X.

Whew.  Done.  Of course, this free sober T-algebra will be naturally isomorphic to H(X) in case T is the theory of unital inflationary semilattices, by general category-theoretic arguments.

In general, it is very hard to find a concrete description of free sober T-algebras.  There are a few cases where this can be done.  We have seen the case of the Hoare powerspace.  I’ll talk some day about the Smyth powerspace, where the (inflationary) axiom is replaced by a similar one with the order reversed, and which, in nice cases, yields the powerspace of compact saturated subsets of X.  The case of the Plotkin powerdomain is a notoriously tough one.  One that has occupied me for some time is Daniele Varacca’s domains of indexed valuations [2].  That one is given by an inequational theory, but we have no idea what the free sober T-algebra in that case looks like, concretely.

— Jean Goubault-Larrecq (June 30th, 2015)

1. Samson Abramsky and Achim Jung.  Domain Theory.  Handbook of Logic in Computer Science, Oxford University Press, 1994, pages 1-168.
2. Daniele Varacca.  Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation.  PhD Thesis, Dept. of Computer Science, U. Aarhus, 2003.  BRICS Dissertation Series DS-03-14.