{"id":664,"date":"2015-06-30T17:03:46","date_gmt":"2015-06-30T15:03:46","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=664"},"modified":"2022-11-19T15:30:09","modified_gmt":"2022-11-19T14:30:09","slug":"powerdomains-and-hyperspaces-iv-theories","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=664","title":{"rendered":"Powerdomains and hyperspaces IV: theories"},"content":{"rendered":"<p>Last time, we concluded with a mysterious observation. \u00a0There is a theory, that of\u00a0unital\u00a0inflationary topological semi-lattices, which plays a fundamental role in the study of the Hoare powerspace. \u00a0On the one hand,\u00a0<strong>H<\/strong>(X) is the free sober such thing. \u00a0On the other hand, the algebras of the\u00a0<strong>H<\/strong> monad are exactly those things that are sober. \u00a0We shall investigate that by looking at theories themselves, and show how those constructions arise from a logical perspective.<\/p>\n<h2>Terms, inequalities, theories<\/h2>\n<p>In the rest, we shall consider a language of first-order terms over a given signature \u03a3. \u00a0A signature is just a set of so-called function symbols, together with their arities, that is, the number of arguments they take. \u00a0For unital inflationary topological semi-lattices, the signature would contain two symbols,\u00a0\u2228 of arity 2, and 0 of arity 0.<\/p>\n<p>We also consider a set\u00a0<strong>V<\/strong> of so-called variables.<\/p>\n<p>A term over the signature\u00a0\u03a3 and the set <strong>V<\/strong> of variables is a finite tree whose vertices are:<\/p>\n<ul>\n<li>either variables from <strong>V<\/strong>, and have no direct successor (those are <em>leaves<\/em>),<\/li>\n<li>or are labeled with function symbols <em>f<\/em> from\u00a0\u03a3, and have\u00a0<em>n<\/em> direct successors, where\u00a0<em>n<\/em> is the arity of\u00a0<em>f<\/em>.<\/li>\n<\/ul>\n<p>Such terms are usually written as strings, such as\u00a0<em>f<\/em>(<em>g<\/em>(<em>a<\/em>, <em>x<\/em>),\u00a0<em>a<\/em>). \u00a0The latter denotes a tree whose root is labeled\u00a0<em>f<\/em>, of arity\u00a0<em>2<\/em>. \u00a0Its two direct successors are the trees\u00a0<em>g<\/em>(<em>a<\/em>, <em>x<\/em>) and\u00a0<em>a<\/em>. \u00a0The first one is itself a tree whose root is labeled\u00a0<em>g<\/em>, of arity 2, with two direct successors\u00a0<em>a<\/em> and <em>x<\/em>. \u00a0I am assuming that <em>x<\/em> is a variable here. \u00a0The constant\u00a0<em>a<\/em>\u00a0is a\u00a0tree labeled\u00a0<em>a<\/em>, of arity 0, and has no direct successor, just like variables. \u00a0(We should write\u00a0<em>a<\/em>(), but\u00a0<em>a<\/em> is more readable.)<\/p>\n<p>For\u00a0unital inflationary topological semi-lattices, we would have terms of the form\u00a0\u2228(\u2228(<em>a<\/em>,\u00a0<em>b<\/em>), <em>c<\/em>), for example. \u00a0We find it more practical to write\u00a0<em>s<\/em>\u00a0\u2228\u00a0<em>t<\/em> instead of\u00a0\u2228(<em>s<\/em>,\u00a0<em>t<\/em>).<\/p>\n<p>The type of terms over a signature is easily encoded in a type of computer data, provided the signature is finite. \u00a0For example, one can specify the set of terms over the signature \u2228, 0 as follows in <a title=\"OCaml\" href=\"https:\/\/ocaml.org\/\">OCaml<\/a>:<\/p>\n<pre>type 'a SUITopSLatTerm = Var of 'a\n                       | Zero\n                       | Vee of 'a SUITopSlatTerm * 'a SUITopSLatTerm;;<\/pre>\n<p>Here <code>Zero<\/code> denotes 0, <code>Vee<\/code> (<em>s<\/em>, <em>t<\/em>) denotes <em>s<\/em>\u00a0\u2228\u00a0<em>t<\/em>, and <code>Var<\/code>(<em>x<\/em>) denotes the variable <em>x<\/em>.<\/p>\n<p>We specify a theory by listing\u00a0<em>inequalities<\/em>, of the form\u00a0<em>s<\/em> \u2264\u00a0<em>t<\/em>, for pairs of terms\u00a0<em>s<\/em> and\u00a0<em>t<\/em>. \u00a0We also take\u00a0<em>s<\/em>=<em>t<\/em> to denote the pair of inequalities\u00a0<em>s<\/em> \u2264\u00a0<em>t<\/em> and\u00a0<em>t<\/em> \u2264\u00a0<em>s<\/em>. \u00a0Variables are universally quantified. \u00a0That means that, if we write, say,\u00a0<em>x<\/em> \u2264\u00a0<em>x<\/em>\u00a0\u2228\u00a0<em>y<\/em> as inequality, where\u00a0<em>x<\/em> and\u00a0<em>y<\/em> are variables, then we mean that\u00a0<em>s<\/em> should be below\u00a0<em>s<\/em>\u00a0\u2228\u00a0<em>t<\/em> for all values\u00a0<em>s<\/em> and\u00a0<em>t<\/em>. \u00a0Oh, oops, I haven&#8217;t mentioned that inequalities should have a <em>meaning<\/em>.<\/p>\n<h2>Algebras, models<\/h2>\n<p>Meaning is given by what logicians call a\u00a0<em>model<\/em>. \u00a0A \u03a3-algebra <em>M<\/em> is just a set <em>D<\/em> (the <em>support<\/em> of <em>M<\/em>), together with an\u00a0<em>n<\/em>-ary function <em>M<sub>f<\/sub><\/em>\u00a0from <em>D<sup>n<\/sup><\/em> to <em>D<\/em>\u00a0for each function symbol <em>f<\/em> in \u03a3. \u00a0An <em>environment<\/em>\u00a0\u03c1 is a map from <strong>V<\/strong> to <em>D<\/em>, serving to interpret the variables. Then one can interpret each term\u00a0<em>t<\/em> in\u00a0<em>D<\/em>, modulo \u03c1, as an element <em>M<\/em>[<em>t<\/em>] \u03c1\u00a0of <em>D<\/em> defined recursively by:<\/p>\n<ul>\n<li><em>M<\/em>[<em>x<\/em>] \u03c1 = \u03c1 (<em>x<\/em>) for every variable\u00a0<em>x<\/em>;<\/li>\n<li><em>M<\/em>[<em>f<\/em>(<em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em>)] \u03c1 = <em>M<sub>f<\/sub><\/em> (<em>M<\/em> [<em>t<\/em><sub>1<\/sub>] \u03c1, &#8230;, <em>M<\/em> [<em>t<sub>n<\/sub><\/em>] \u03c1).<\/li>\n<\/ul>\n<p>A\u00a0<em>model<\/em> of\u00a0<strong>T<\/strong>, also known as a <em><strong>T<\/strong>-algebra<\/em>, is a \u03a3-algebra that satisfies all inequalities of\u00a0<strong>T<\/strong>, in the sense that, for each equality\u00a0<em>s<\/em>=<em>t<\/em> in the theory\u00a0<strong>T<\/strong>, the model satisfies\u00a0<em>M<\/em>[<em>s<\/em>] \u03c1 =\u00a0<em>M<\/em>[<em>t<\/em>] \u03c1 for every environment\u00a0\u03c1. \u00a0(What about\u00a0<em>in<\/em>equalities? \u00a0 Allow me to only consider equalities here, for simplicity. \u00a0I will deal with inequalities below, in the &#8216;The order-theoretic case&#8217; section. \u00a0The following example will use one inequality, so you&#8217;ll have to overlook the simplification for a second.)<\/p>\n<p>For example,\u00a0<strong>H<\/strong>(<em>X<\/em>) is a model of the theory of\u00a0unital\u00a0inflationary topological semi-lattices, given by the following inequalities:<\/p>\n<ul>\n<li>(unit) <em>x<\/em>\u00a0\u2228 0 = <em>x<\/em><\/li>\n<li>(associativity) (<em>x<\/em>\u00a0\u2228 <em>y<\/em>) \u2228 <em>z<\/em>\u00a0= <em>x<\/em>\u00a0\u2228 (<em>y<\/em>\u00a0\u2228 <em>z<\/em>)<\/li>\n<li>(commutativity) <em>x<\/em>\u00a0\u2228 <em>y<\/em>\u00a0= <em>y<\/em>\u00a0\u2228 <em>x<\/em><\/li>\n<li>(idempotence) <em>x<\/em>\u00a0\u2228 <em>x<\/em>\u00a0= <em>x<\/em><\/li>\n<li>(inflationary) <em>x<\/em>\u00a0\u2264 <em>x<\/em>\u00a0\u2228 <em>y<\/em><\/li>\n<\/ul>\n<div>\n<p>where\u00a0<em>x<\/em>,\u00a0<em>y<\/em>,\u00a0<em>z<\/em> are distinct variables. \u00a0The model is given by interpreting \u2228 as union and 0 as the empty set, that is, by defining <em>M<\/em><sub>\u2228<\/sub> as union and <em>M<\/em><sub>0<\/sub> as the empty set.<\/p>\n<p>If you prefer to reason categorically, given a signature \u03a3, there is a category of &#8220;sets with a function for each function symbol in \u03a3&#8221;. \u00a0\u00a0(I am ignoring arities for the sake of readability.) \u00a0This is the category <strong>Alg<\/strong><sub>\u03a3<\/sub>\u00a0of all \u03a3-algebras.<\/p>\n<p>The forgetful functor to\u00a0<strong>Set<\/strong> has a left adjoint <em>Term<\/em><sub>\u03a3<\/sub>, which maps every set\u00a0<strong>V<\/strong> (yes, <em>any<\/em> set can play the role of a set of variables) to the set of terms over\u00a0\u03a3 and\u00a0<strong>V<\/strong>. \u00a0The latter is a very simple kind of \u03a3-algebra: for each function symbol\u00a0<em>f<\/em>, there is a map <em>M<sub>f<\/sub><\/em>, which maps every tuple of terms <em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em> to the term <em>f<\/em> (<em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em>). \u00a0So much for terms.<\/p>\n<p>The unit of the adjunction, \u03b7 :\u00a0<strong>V<\/strong>\u00a0\u2192\u00a0<em>Term<\/em><sub>\u03a3<\/sub>(<strong>V<\/strong>), maps every variable\u00a0<em>x<\/em> to <em>x<\/em> itself, seen as a term. \u00a0(In our OCaml example, this map sends every variable x to <code>Var<\/code>(<em>x<\/em>) instead.)<\/p>\n<p>Since\u00a0<em>Term<\/em><sub>\u03a3<\/sub>(<strong>V<\/strong>) is the free \u03a3-algebra over the set <strong>V<\/strong>, for each set map \u03c1 : <strong>V<\/strong> \u2192 <em>D<\/em>, there is a unique map of \u03a3-algebras, from <em>Term<\/em><sub>\u03a3<\/sub>(<strong>V<\/strong>) to <em>D<\/em>, that gives back \u03c1 when precomposed with \u03b7 : <strong>V<\/strong> \u2192 <em>Term<\/em><sub>\u03a3<\/sub>(<strong>V<\/strong>). \u00a0This is the interpretation map, the one that sends every term\u00a0<em>t<\/em> to\u00a0<em>M<\/em>[<em>t<\/em>] \u03c1.<\/p>\n<h2>Building the free sober T-algebra: first ideas<\/h2>\n<p>All right, now take a fixed theory\u00a0<strong>T<\/strong>. \u00a0There is a known construction of a free continuous domain <strong>T<\/strong>-algebra\u00a0over any continuous dcpo <em>X<\/em> [1, Section 6.1.2]. \u00a0(A domain\u00a0<strong>T<\/strong>-algebra is just a\u00a0<strong>T<\/strong>-algebra, except the support <em>D<\/em> is a dcpo and the functions <em>M<sub>f<\/sub><\/em> are required to be Scott-continuous.)<\/p>\n<p>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.<\/p>\n<p>This works as follows. \u00a0We start from <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>)\u2014think of that as a set of trees whose leaves are elements of <em>X<\/em> instead of variables. \u00a0You may need to pause on that. \u00a0There is nothing special about variables. \u00a0The set of variables can be anything we wish, and in particular\u00a0<em>X<\/em>. Have you digested this? \u00a0If so, then we can go on.<\/p>\n<p>We declare two terms <em>s<\/em>, <em>t<\/em> equivalent if and only if one can deduce the two inequalities\u00a0<em>s<\/em> \u2264\u00a0<em>t<\/em> and\u00a0<em>t<\/em> \u2264\u00a0<em>s<\/em> from the inequalities of the theory\u00a0<strong>T<\/strong>, by the usual rules (I will be more precise below). \u00a0Then we consider the quotient of <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>) by this equivalence, and consider that quotient as an abstract basis. To this end, we need to define an interpolative relation \u227a on that set (see Lemma 5.1.32 in the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>). \u00a0We declare that (the equivalence class of)\u00a0<em>s<\/em> directly approximates (the equivalence class of)\u00a0<em>t<\/em> if and only if one can reach\u00a0<em>s<\/em>, starting from\u00a0<em>t<\/em>, by first going to a term\u00a0<em>u<\/em> \u2264\u00a0<em>t<\/em>, then replacing all the variables in\u00a0<em>u<\/em> (which are just values in\u00a0<em>X<\/em>) by values that are way-below in <em>X<\/em>, obtaining a new term\u00a0<em>v<\/em>, then checking that\u00a0<em>s<\/em> \u2264\u00a0<em>v<\/em>. \u00a0The interpolative relation\u00a0\u227a is the transitive closure of that relation of direct approximation [1, Lemma 6.1.5]. \u00a0Finally, the rounded ideal completion of that abstract basis will give you the free object in the category of continuous\u00a0<strong>T<\/strong>-algebras, over\u00a0<em>X<\/em> [1, Theorem 6.1.6].<\/p>\n<p>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. \u00a0My initial guess was to put a topology directly on <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>), satisfying a few properties, and to take the sobrification of the resulting space. The properties that I had imagined were:<\/p>\n<ul>\n<li>\u03b7 : <em>X<\/em> \u2192 <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>), which maps every variable to itself as a term, is continuous;<\/li>\n<li>for each <em>n<\/em>-ary function symbol\u00a0<em>f<\/em>, the map that sends every tuple of terms <em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em> to the term <em>f<\/em> (<em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em>), is continuous (we shall simply call\u00a0<em>f<\/em> that map);<\/li>\n<li>every open <em>U<\/em> is upward-closed, in the sense that for every term <em>s<\/em> in <em>U<\/em> and for every term <em>t<\/em> such that we can deduce <em>s<\/em> \u2264 <em>t<\/em> from the theory <strong>T<\/strong>, then <em>t<\/em> is in <em>U<\/em>.<\/li>\n<\/ul>\n<p>The resulting topology would fail very badly to be T<sub>0<\/sub>, 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.<\/p>\n<p>This approach does not work out of the box. We would need something like the coarsest topology satisfying the above. However, the requirement for <em>f<\/em> to be continuous is hard to enforce. \u00a0Requiring\u00a0<em>f<\/em> to be\u00a0<em>separately<\/em> continuous instead would probably give us a topology, but that is not quite the same thing.<\/p>\n<p>Instead, we shall look at a simpler case first (the\u00a0<em>order-theoretic<\/em> case). \u00a0We shall find our way through successive generalizations, the\u00a0<em>algebraic<\/em> case, then the general\u00a0<em>topological<\/em> case and finally the <em>sober<\/em> case.<\/p>\n<p>If you ever get lost, keep in mind the following:<\/p>\n<blockquote><p>The free (ordered, or topological)\u00a0<strong>T<\/strong>-algebra on <em>X<\/em>\u00a0will always be a set of trees with function symbols from the signature\u00a0\u03a3, and variables from\u00a0X, suitably quotiented.<\/p><\/blockquote>\n<p>The only problem will be to find the right topology to put on this set of trees. \u00a0The discussion above shows that this is the real problem.<\/p>\n<h2>The order-theoretic case<\/h2>\n<p>Instead of working in the category of topological case, we first deal with the simpler case of quasi-orderings. \u00a0The situation is as follows. \u00a0Consider a quasi-ordered set\u00a0<em>X<\/em>, and try to find the free quasi-order\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em>. \u00a0A\u00a0<em>quasi-order\u00a0<strong>T<\/strong>-algebra<\/em> is a\u00a0<strong>T<\/strong>-algebra with a quasi-ordering \u2264 such that:<\/p>\n<ul>\n<li>for every inequality\u00a0<em>s<\/em>\u00a0\u2264\u00a0<em>t<\/em>\u00a0in the theory\u00a0<strong>T<\/strong>, the model satisfies\u00a0<em>M<\/em>[<em>s<\/em>] \u03c1 \u2264\u00a0<em>M<\/em>[<em>t<\/em>] \u03c1 for every environment\u00a0\u03c1;<\/li>\n<li>for every function symbol\u00a0<em>f<\/em>, <em>M<sub>f<\/sub><\/em>\u00a0is monotonic.<\/li>\n<\/ul>\n<p>An\u00a0<em>order\u00a0<strong>T<\/strong>-algebra<\/em> is defined similarly, except that \u2264 is required to be an ordering.<\/p>\n<p>Given a quasi-ordered set <em>X<\/em>, we extend the quasi-ordering \u2264 on <em>X<\/em> to one on <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>) as the smallest relation \u2264<sup>*<\/sup>\u00a0that satisfies the following. \u00a0We write \u2264<sup>*<\/sup> for the extension, so as to distinguish it clearly from \u2264.<\/p>\n<ul>\n<li>(Extension) for all <em>x<\/em>, <em>y<\/em> in <em>X<\/em>, if <em>x<\/em> \u2264 <em>y<\/em> in <em>X<\/em>, then <em>x<\/em> \u2264<sup>*<\/sup> <em>y<\/em> as terms, in <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>);<\/li>\n<li>(Reflexivity) <em>s<\/em> \u2264<sup>*<\/sup>\u00a0<em>s<\/em> for every\u00a0<em>s<\/em> in <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>);<\/li>\n<li>(Theory) given any inequality\u00a0<em>s<\/em> \u2264\u00a0<em>t<\/em> in\u00a0<strong>T<\/strong>, for every environment \u03c1 : <strong>V<\/strong> \u2192 <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>), <em>s<\/em>\u03c1 \u2264<sup>*<\/sup> <em>t<\/em>\u03c1; <em>s<\/em>\u03c1 denotes the result of replacing each variable <em>x<\/em> in <em>s<\/em> by the corresponding term \u03c1(<em>x<\/em>), and similarly for <em>t<\/em>\u03c1 (if you don&#8217;t mind being puzzled for a second, note that\u00a0<em>s<\/em>\u03c1 is just the meaning [<em>s<\/em>]\u03c1 of\u00a0<em>s<\/em> in environment\u00a0\u03c1, considering <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>) itself as a <strong>T<\/strong>-algebra);<\/li>\n<li>(Transitivity) if\u00a0<em>s<\/em> \u2264<sup>*<\/sup>\u00a0<em>t<\/em> and\u00a0<em>t<\/em> \u2264<sup>*<\/sup>\u00a0<em>u<\/em>, then\u00a0<em>s<\/em> \u2264<sup>*<\/sup>\u00a0<em>u<\/em>;<\/li>\n<li>(Application) if <em>s<\/em><sub>1<\/sub> \u2264<sup>*<\/sup> <em>t<\/em><sub>1<\/sub>, &#8230;, <em>s<sub>n<\/sub><\/em> \u2264<sup>*<\/sup> <em>t<sub>n<\/sub><\/em>, then\u00a0<em>f<\/em>(<em>s<\/em><sub>1<\/sub>, &#8230;, <em>s<sub>n<\/sub><\/em>) \u2264<sup>*<\/sup> <em>f<\/em>(<em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em>), for every <em>f<\/em> in \u03a3, of arity <em>n<\/em>.<\/li>\n<\/ul>\n<p>With the quasi-ordering \u2264<sup>*<\/sup>, <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>) is a quasi-order-<strong>T<\/strong>-algebra. The map \u03b7 : <em>X<\/em> \u2192 <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>), which maps every variable <em>x<\/em> to itself as a term, is monotonic, by (Extension).<\/p>\n<p>Finally, for every monotonic map \u03b2 from <em>X<\/em> to the support <em>D<\/em> of a quasi-order-<strong>T<\/strong>-algebra <em>M<\/em>, \u03b2 extends to a unique monotonic morphism \u03a6 of quasi-order-<strong>T<\/strong>-algebras from <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>) to <em>M<\/em>. For each term <em>t<\/em>, \u03a6(<em>t<\/em>) is defined by induction on <em>t<\/em>:<\/p>\n<ul>\n<li>for every\u00a0<em>x<\/em> in\u00a0<em>X<\/em>,\u00a0\u03a6(<em>x<\/em>)=\u03b2(<em>x<\/em>);<\/li>\n<li>\u03a6(<em>f<\/em> (<em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em>)) = <em>M<sub>f<\/sub><\/em> (\u03a6(<em>t<\/em><sub>1<\/sub>), &#8230;, \u03a6(<em>t<sub>n<\/sub><\/em>)).<\/li>\n<\/ul>\n<p>In other words, <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>), with the quasi-ordering \u2264<sup>*<\/sup>, is the free quasi-order-<strong>T<\/strong>-algebra over the quasi-ordered set\u00a0<em>X<\/em>, \u2264. Good.<\/p>\n<p>The quasi-ordering \u2264<sup>*<\/sup> is not in general an ordering, even if <em>X<\/em> is a poset. For example, if the theory <strong>T<\/strong> contains the axiom (associativity) (<em>x<\/em>\u00a0\u2228 <em>y<\/em>) \u2228 <em>z<\/em>\u00a0= <em>x<\/em>\u00a0\u2228 (<em>y<\/em>\u00a0\u2228 <em>z<\/em>), then the terms (<em>s<\/em>\u00a0\u2228 <em>t<\/em>) \u2228 <em>u<\/em>\u00a0and <em>s<\/em>\u00a0\u2228 (<em>t<\/em>\u00a0\u2228 <em>u<\/em>) will both be below each other, for all terms <em>s<\/em>, <em>t<\/em>, and <em>u<\/em>.<\/p>\n<p>However, every quasi-ordering induces an equivalence relation: define\u00a0<em>s<\/em>=<sup>*<\/sup><em>t<\/em> if and only if both <em>s<\/em> \u2264<sup>*<\/sup> <em>t<\/em> and <em>t<\/em> \u2264<sup>*<\/sup> <em>s<\/em>. For equivalence classes [<em>s<\/em>] and [<em>t<\/em>] (of <em>s<\/em> and <em>t<\/em>, respectively, under that equivalence relation), we define [<em>s<\/em>] \u2264<sup>*<\/sup> [<em>t<\/em>] if and only if <em>s<\/em> \u2264<sup>*<\/sup> <em>t<\/em>. This defines an ordering (not just a quasi-ordering), and the quotient poset <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>)\/=<sup>*<\/sup> is then the free order-<strong>T<\/strong>-algebra over the poset\u00a0<em>X<\/em>.<\/p>\n<h2>The algebraic case<\/h2>\n<p>Now consider an algebraic dcpo\u00a0<em>X<\/em>. \u00a0Recall that a domain\u00a0<strong>T<\/strong>-algebra is an order\u00a0<strong>T<\/strong>-algebra in which the support <em>D<\/em> is a dcpo and where the functions <em>M<sub>f<\/sub><\/em> are Scott-continuous. We build the free domain\u00a0<strong>T<\/strong>-algebra above <em>X<\/em> as follows. We first extract the poset <em>K<\/em> of finite elements of <em>X<\/em>. We then build the free quasi-order <strong>T<\/strong>-algebra on <em>K<\/em>. This is <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>), with the quasi-ordering \u2264<sup>*<\/sup>, as we have just seen. (We could also take the free order <strong>T<\/strong>-algebra on <em>K<\/em>, <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)\/=<sup>*<\/sup>, but this really does not matter.) To obtain a dcpo from that, we build its ideal completion <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)).<\/p>\n<p>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. \u00a0Therefore, finding the free domain\u00a0<strong>T<\/strong>-algebra on an algebraic domain will reduce to the problem of finding the free (quasi-)order\u00a0<strong>T<\/strong>-algebra on a poset, a problem we have just solved.<\/p>\n<p>The ideal completion is dealt with in Definition 5.1.45, and Proposition 5.1.46 tells us that the ideal completion <strong>I<\/strong>(<em>B<\/em>) of a poset <em>B<\/em>\u00a0is an algebraic dcpo, whose finite elements are isomorphic to\u00a0<em>B<\/em>. \u00a0When\u00a0<em>B<\/em> is merely quasi-ordered, the same results hold, except the finite elements of\u00a0<strong>I<\/strong>(<em>B<\/em>) are isomorphic to the quotient of\u00a0<em>B<\/em> by the equivalence relation induced by the quasi-ordering.<\/p>\n<p>In particular, <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) is an algebraic dcpo. There are a few properties we must check:<\/p>\n<ul>\n<li>\u03b7 : <em>X<\/em> \u2192 <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) 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 <em>x<\/em> in <em>K<\/em> to <em>x<\/em> itself, as an element of\u00a0<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>). Compose that with the inclusion of <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>) into <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) (which maps every term <em>t<\/em> to \u2193<em>t<\/em>), so that we obtain a monotonic map from <em>K<\/em> to <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)). This has a unique continuous extension to <em>X<\/em> (see Exercise 5.1.62), and we call it \u03b7.<\/li>\n<li>Each function\u00a0<em>f<\/em> in \u03a3 is continuous, namely, Scott-continuous. \u00a0Call <em>n<\/em> the arity of <em>f<\/em>. We proceed as for \u03b7. First,\u00a0<em>f<\/em> defines a monotonic map from <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)<em><sup>n<\/sup><\/em> to <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>), by rule (Application). We obtain a monotonic map from <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)<em><sup>n<\/sup><\/em> to <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) by composing with the inclusion of <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>) into <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)). This extends to a unique continuous map from <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)<em><sup>n<\/sup><\/em>) to <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)). This is almost what we want, except that we need the domain of the map to be [<strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>))]<em><sup>n<\/sup><\/em>, not <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)<em><sup>n<\/sup><\/em>). \u00a0We are saved by the fact that ideal completions commute with finite products, up to natural isomorphism. \u00a0You can check it by hand. \u00a0Alternatively, 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).<\/li>\n<li><strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) satisfies all the inequalities of the theory <strong>T<\/strong>. Given any term <em>t<\/em> in <em>Term<\/em><sub>\u03a3<\/sub>(<strong>V<\/strong>), the meaning map [<em>t<\/em>], which maps every environment \u03c1 : <strong>V<\/strong> \u2192 <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>) to [<em>t<\/em>]\u03c1, is monotonic, as a composition of monotonic maps. Again, it extends to a unique continuous map, again written [<em>t<\/em>], from extended environments \u03c1&#8217; : <strong>V<\/strong> \u2192 <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) to <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)). \u00a0Since it is unique, it coincides with the unique continuous map defined by [<em>x<\/em>]\u03c1&#8217; =\u00a0\u03c1'(<em>x<\/em>), [<em>f<\/em>(<em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em>)]\u03c1&#8217; = <em>f<\/em> ([<em>t<\/em><sub>1<\/sub>]\u03c1&#8217;, &#8230;, [<em>t<sub>n<\/sub><\/em>]<em>\u03c1&#8217;<\/em>), where the effect of\u00a0<em>f<\/em> on the ideal completion was found in the last bulleted item. \u00a0To check that [<em>s<\/em>]\u03c1&#8217; \u2264 [<em>t<\/em>]\u03c1&#8217; for every extended environment, it is enough to check that [<em>s<\/em>]\u03c1 \u2264 [<em>t<\/em>]\u03c1 for every environment with values in <em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>). But we know that already, from the previous section on the ordered case.<\/li>\n<\/ul>\n<p>Finally,\u00a0for every continuous map \u03b2 from\u00a0<em>X<\/em>\u00a0to the support\u00a0<em>D<\/em>\u00a0of a domain\u00a0<strong>T<\/strong>-algebra\u00a0<em>M<\/em>, \u03b2 restricts to a continuous map from <em>K<\/em>\u00a0to <em>M<\/em>. \u00a0We know from the previous section that \u03b2 extends to a unique monotonic morphism \u03a6 of quasi-order-<strong>T<\/strong>-algebras from\u00a0<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>) to\u00a0<em>M<\/em>. \u00a0 Since\u00a0<strong>I<\/strong> is left adjoint to the forgetful functor from dcpos to orders (Exercise 5.5.3),\u00a0\u03a6 extends to a unique continuous map from <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) to <em>M<\/em>. The same uniqueness arguments as above show that \u03a6 commutes with application of <em>f<\/em>, for every function symbol <em>f<\/em> in \u03a3, so \u03a6 is a continuous morphism of <strong>T<\/strong>-algebras. \u00a0Finally, it coincides with\u00a0\u03b2 not only on\u00a0<em>K<\/em>, but on the whole of\u00a0<em>X<\/em>, again by uniqueness of extensions.<\/p>\n<p>We conclude that:<\/p>\n<p><strong>Theorem 1.<\/strong>\u00a0Given any algebraic dcpo\u00a0<em>X<\/em>, there is a free domain\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em>, and it is algebraic as a dcpo.<br \/>\nThis free domain\u00a0<strong>T<\/strong>-algebra\u00a0is the ideal completion <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)) of the quasi-order <strong>T<\/strong>-algebra of terms built from function symbols in \u03a3 and from &#8220;variables&#8221; taken from the set <em>K<\/em> of finite elements of <em>X<\/em>.<\/p>\n<p>This is important per se. \u00a0The continuous case can be obtained by realizing that, if\u00a0<em>X<\/em> is continuous, then it is a retract of some algebraic dcpo\u00a0<em>Y<\/em> \u00a0(see Theorem 5.1.48). \u00a0Then build the free domain\u00a0<strong>T<\/strong>-algebra on\u00a0<em>Y<\/em>, and construct the free domain\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em> as a suitable retract of the former. \u00a0(Hint: both\u00a0<strong>I<\/strong> and <em>Term<\/em><sub>\u03a3<\/sub> are functors.) This shows that every continuous dcpo has a free domain <strong>T<\/strong>-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.<\/p>\n<h2>The topological case<\/h2>\n<p>Let us jump to the whole category of all T<sub>0<\/sub> topological spaces. \u00a0We wish to build the free T<sub>0<\/sub> topological <strong>T<\/strong>-algebra on <em>X<\/em>. A T<sub>0<\/sub> topological <strong>T<\/strong>-algebra is, as you can expect, a <strong>T<\/strong>-algebra <em>M<\/em> whose support is a T<sub>0<\/sub> topological space, and on which every function <em>M<sub>f<\/sub><\/em> is continuous.<\/p>\n<p>To do so, we reduce to the previous case (again). Explicitly, we embed\u00a0<em>X<\/em> in a much larger space, which will happen to be an algebraic dcpo. \u00a0Then we apply the previous construction to that large space, and carve out the needed bit from it.<\/p>\n<p>To do so, let <em>X<\/em> be a T<sub>0<\/sub> space. We can embed it into an algebraic dcpo <em>Y<\/em>. The typical construction is to take the powerset <strong>P<\/strong>(<strong>O<\/strong>(<em>X<\/em>)) of the set <strong>O<\/strong>(<em>X<\/em>) of open subsets of <em>X<\/em> for <em>Y;\u00a0<\/em>the embedding <em>i<\/em> : <em>X<\/em> \u2192 <em>Y<\/em> maps each point <em>x<\/em> in <em>X<\/em> to its set of open neighborhoods. (See Proposition 9.3.5.) Note that\u00a0<em>Y<\/em> is also a complete lattice.<\/p>\n<p>In the sequel, I will forget about <em>i<\/em> and simply consider that <em>X<\/em> is a subspace of an algebraic complete lattice <em>Y<\/em>. \u00a0I will then build the free T<sub>0<\/sub> topological\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em> as a subspace\u00a0<em>A<\/em> of the free domain\u00a0<strong>T<\/strong>-algebra on the much larger space\u00a0<em>Y<\/em>.<\/p>\n<p>In the previous section, we have seen that there is a free domain\u00a0<strong>T<\/strong>-algebra on\u00a0<em>Y<\/em>. This is <strong>I<\/strong>(<em>Term<\/em><sub>\u03a3<\/sub>(<em>K<\/em>)), where <em>K<\/em> is the set of finite elements of <em>Y<\/em>, namely the set of finite sets of open subsets of <em>X<\/em>&#8230; but reasoning at that level of detail would get us lost. Simply call T(<em>Y<\/em>) the free domain <strong>T<\/strong>-algebra on <em>Y<\/em>, for the rest of this post.<\/p>\n<p>We again forget about embeddings, and consider that <em>Y<\/em> itself appears as a subset of T(<em>Y<\/em>). If we were to be formal, that would be a topological embedding (not a <strong>T<\/strong>-algebra embedding). With those conventions, note that <em>X<\/em> is then an even smaller subspace of T(<em>Y<\/em>).<\/p>\n<p>There is a subspace <em>A<\/em> of T(<em>Y<\/em>), built as the smallest subset that contains <em>X<\/em> and that is closed under application of function symbols <em>f<\/em> in \u03a3. (The effect of those function symbols is taken to be their effect in T(<em>Y<\/em>).) As such, <em>A<\/em> is not only a subspace, but also a sub-<strong>T<\/strong>-algebra.<\/p>\n<p>It is now fairly easy to see that\u00a0<em>A<\/em> is the free T<sub>0<\/sub> topological\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em>. \u00a0For that, consider any continuous map \u03b2 from <em>X<\/em> to (the underlying topological space) of a topological <strong>T<\/strong>-algebra <em>M<\/em>, with support <em>D<\/em>. To this end, we notice that \u03b2 extends to a continuous map from <em>Y<\/em> to <em>D<\/em>, which then extends to a unique domain <strong>T<\/strong>-algebra morphism from T(<em>Y<\/em>) to <em>M<\/em>. Restrict the latter to <em>A<\/em>, obtaining a map \u03b2&#8217;. As the restriction of a continuous map, \u03b2&#8217; is continuous. It is also a morphism of <strong>T<\/strong>-algebras. The fact that \u03b2&#8217; is unique is obvious: we must have \u03b2'(<em>x<\/em>)=\u03b2(<em>x<\/em>) for every <em>x<\/em> in <em>X<\/em>, and \u03b2'(<em>f<\/em>(<em>t<\/em><sub>1<\/sub>, &#8230;, <em>t<sub>n<\/sub><\/em>)) = <em>M<sub>f<\/sub><\/em> (\u03b2&#8217; (<em>t<\/em><sub>1<\/sub>), &#8230;, \u03b2&#8217; (<em>t<sub>n<\/sub><\/em>)), and this suffices to define \u03b2&#8217; uniquely on <em>A<\/em>.<\/p>\n<p><strong>Theorem 2.<\/strong> \u00a0For every T<sub>0<\/sub> topological space <em>X<\/em>, there is a free T<sub>0<\/sub> topological <strong>T<\/strong>-algebra on <em>X<\/em>.<\/p>\n<p>Although it might look very abstract, that free T<sub>0<\/sub> topological\u00a0<strong>T<\/strong>-algebra is just the set <em>Term<\/em><sub>\u03a3<\/sub>(<em>X<\/em>) of trees with &#8220;variables&#8221; taken from <em>X<\/em>, 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.<\/p>\n<p>Let us return for a moment to the theory of unital\u00a0inflationary topological semi-lattices. The terms are built from the constant 0, the binary symbol \u2228 and variables. One must quotient those terms, considering \u2228 as associative, commutative and idempotent, with 0 as neutral element. A moment&#8217;s reflection should convince you that this quotient is isomorphic to some set of finite subsets of <em>X<\/em>. For example, the equivalence class of the term <em>x<\/em> \u2228 (<em>y<\/em> \u2228 <em>z<\/em>) should look like the finite set {<em>x<\/em>, <em>y<\/em>, <em>z<\/em>}. However, the (inflationary) inequality also forces some other identifications, such as {<em>x<\/em>} = {<em>x<\/em>, <em>y<\/em>} if <em>x<\/em> \u2264 <em>y<\/em>. The complex construction we have described above serves to put the right topology on this set of finite subsets. \u00a0Eventually, a canonical representative of a finite set will be its downward-closure (e.g., \u2193{<em>x<\/em>,\u00a0<em>y<\/em>,\u00a0<em>z<\/em>}): the free T<sub>0<\/sub> topological\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em>, where\u00a0<strong>T<\/strong> is the theory of unital inflationary semi-lattices, is the set of finitary closed subsets of\u00a0<em>X<\/em>, with some topology. \u00a0I&#8217;ll let you check that this is the lower Vietoris topology. \u00a0But please! do not try to check it directly. \u00a0The only nice way to do so that I know of is to check that the set of finitary closed subsets of\u00a0<em>X<\/em> with the lower Vietoris topology is the unique (up to natural isomorphism) T<sub>0<\/sub> topological\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em>; so it must coincide with what our tree-based construction yields, up to natural isomorphism.<\/p>\n<h2>Sober T-algebras<\/h2>\n<p>We had seen in <a title=\"Powerdomains and hyperspaces I: closed and open subsets\" href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=585\">part I<\/a> that\u00a0<strong>H<\/strong>(<em>X<\/em>) is the free\u00a0<em>sober<\/em>\u00a0<strong>T<\/strong>-algebra, for the theory\u00a0<strong>T<\/strong> of unital inflationary semi-lattices. \u00a0The free T<sub>0<\/sub> topological\u00a0<strong>T<\/strong>-algebra is a bit disappointing, as it contains only finitary closed sets, and free sober\u00a0<strong>T<\/strong>-algebras look more promising.<\/p>\n<p>So let us look for free sober\u00a0<strong>T<\/strong>-algebras in general. \u00a0Sober\u00a0<strong>T<\/strong>-algebras are just T<sub>0<\/sub> topological\u00a0<strong>T<\/strong>-algebras whose support is sober.<\/p>\n<p>Looking back at the construction of the previous section, we realize that\u00a0<em>A<\/em> is not necessarily sober. \u00a0(The space of finitary closed subsets of a space, for one, is not sober, as its sobrification is in fact the whole of\u00a0<strong>H<\/strong>(<em>X<\/em>).) \u00a0But it sobrification <strong>S<\/strong>(<em>A<\/em>) will be. \u00a0We claim that\u00a0<strong>S<\/strong>(<em>A<\/em>) will be the sought after free sober\u00a0<strong>T<\/strong>-algebra.<\/p>\n<p>The topological embedding of <em>A<\/em> into T(<em>Y<\/em>) lifts to a topological embedding of <strong>S<\/strong>(<em>A<\/em>) into <strong>S<\/strong>(T(<em>Y<\/em>)) (Lemma 8.4.11). Furthermore, since T(<em>Y<\/em>) is an algebraic dcpo, hence sober, the latter is just T(<em>Y<\/em>). All this allows us to see <strong>S<\/strong>(<em>A<\/em>) as a sober subspace of T(<em>Y<\/em>).<\/p>\n<p>Any continuous map from <em>A<sup>n<\/sup><\/em> to a sober space extends to a unique continuous map from <strong>S<\/strong>(<em>A<sup>n<\/sup><\/em>) to the same sober space (Lemma 8.2.44). Since <strong>S<\/strong>(<em>A<sup>n<\/sup><\/em>) is naturally isomorphic to [<strong>S<\/strong>(<em>A<\/em>)]<em><sup>n<\/sup><\/em> (Theorem 8.4.8), we obtain that <strong>S<\/strong>(<em>A<\/em>) is also a \u03a3-algebra where the application of each function symbol is continuous. Inequalities are preserved, too, because sobrification preserves order, namely if <em>f<\/em> \u2264 <em>g<\/em> as continuous maps, then <strong>S<\/strong>(<em>f<\/em>) \u2264 <strong>S<\/strong>(<em>g<\/em>). (Exercise: use Lemma 8.2.42 for a definition of <strong>S<\/strong>(<em>f<\/em>).) Therefore <strong>S<\/strong>(<em>A<\/em>) is a sober\u00a0<strong>T<\/strong>-algebra.<\/p>\n<p>We have almost finished to prove that\u00a0<strong>S<\/strong>(<em>A<\/em>) is the free sober\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em>. Consider any continuous map \u03b2 from <em>X<\/em> to (the underlying topological space) of a sober <strong>T<\/strong>-algebra <em>M<\/em>, with support <em>D<\/em>. This extends to a unique continuous morphism of <strong>T<\/strong>-algebras \u03b2&#8217; from <em>A<\/em> to <em>M<\/em>, by the results of the previous section. In turn, \u03b2&#8217; extends to a unique continuous map from <strong>S<\/strong>(<em>A<\/em>) to <em>M<\/em>, since <em>M<\/em> is sober.<br \/>\nUsing arguments similar to some that we have already seen (uniqueness of extensions), that extension also commutes with applications of function symbols from \u03a3. Therefore it is also a morphism of <strong>T<\/strong>-algebras. We have proved:<\/p>\n<p><strong>Theorem 3.<\/strong>\u00a0\u00a0For every T<sub>0<\/sub>\u00a0topological space\u00a0<em>X<\/em>, there is a free sober\u00a0<strong>T<\/strong>-algebra on\u00a0<em>X<\/em>.<\/p>\n<p>Whew. \u00a0Done. \u00a0Of course, this free sober <strong>T<\/strong>-algebra will be naturally isomorphic to <strong>H<\/strong>(<em>X<\/em>) in case <strong>T<\/strong> is the theory of unital inflationary semilattices, by general category-theoretic arguments.<\/p>\n<p>In general, it is very hard to find a concrete description of free sober\u00a0<strong>T<\/strong>-algebras. \u00a0There are a few cases where this can be done. \u00a0We have seen the case of the Hoare powerspace. \u00a0I&#8217;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\u00a0<em>X<\/em>. \u00a0The case of the Plotkin powerdomain is a notoriously tough one. \u00a0One that has occupied me for some time is Daniele Varacca&#8217;s domains of indexed valuations [2]. \u00a0That one is given by an inequational theory, but we have no idea what the free sober\u00a0<strong>T<\/strong>-algebra in that case looks like, concretely.<\/p>\n<p style=\"text-align: right;\">\u2014 <a href=\"https:\/\/www.lsv.ens-paris-saclay.fr\/~goubault\/?l=en\" rel=\"attachment wp-att-993\">Jean Goubault-Larrecq<\/a>\u00a0(June 30th, 2015)<img loading=\"lazy\" decoding=\"async\" class=\"wp-image-993 alignright\" src=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/wp-content\/uploads\/2016\/08\/jgl-2011.png\" alt=\"jgl-2011\" width=\"32\" height=\"44\" \/><\/p>\n<ol>\n<li>Samson Abramsky and Achim Jung. \u00a0<a title=\"Domain theory\" href=\"https:\/\/www.cs.bham.ac.uk\/~axj\/pub\/papers\/handy1.pdf\"><em>Domain Theory<\/em><\/a>. \u00a0Handbook of Logic in Computer Science, Oxford University Press, 1994, pages 1-168.<\/li>\n<li>Daniele Varacca. \u00a0<em>Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation<\/em>. \u00a0PhD Thesis, Dept. of Computer Science, U. Aarhus, 2003. \u00a0<a title=\"Indexed valuations\" href=\"https:\/\/www.brics.dk\/DS\/03\/14\/BRICS-DS-03-14.pdf\">BRICS Dissertation Series DS-03-14<\/a>.<\/li>\n<\/ol>\n<div><\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Last time, we concluded with a mysterious observation. \u00a0There is a theory, that of\u00a0unital\u00a0inflationary topological semi-lattices, which plays a fundamental role in the study of the Hoare powerspace. \u00a0On the one hand,\u00a0H(X) is the free sober such thing. \u00a0On the &hellip; <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=664\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"open","ping_status":"open","template":"","meta":{"_crdt_document":"","footnotes":""},"class_list":["post-664","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/664","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=664"}],"version-history":[{"count":42,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/664\/revisions"}],"predecessor-version":[{"id":5957,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/664\/revisions\/5957"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=664"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}