I have recently read a few papers by Weng Kin Ho. He has a number of nice papers on domain theory, including a very nifty paper on an elegant implementation of exact real arithmetic in Haskell called ERCE. One thing that I discovered by reading some of his other papers is what he did with Martín Hötzel Escardó on what they call operational domain theory [2], or what Martín calls synthetic topology [3].
It is probably hard to explain what this is better than they do. I will only try to give a hint. To get a better understanding of it, their common paper [2] is recommended. Martín’s paper [3] is leisurely, but quite a bit longer, and you will need some time to appreciate what he has to say. Weng Kin extended the operational domain theory approach to deal with recursive types [4]: read this when you have absorbed the rest. It is technical, but it contains a few nice tricks!
The whole thing in synthetic domain theory is a constant interplay between topology and the semantics of programming languages. Instead of talking of programming languages, let me first talk about elementary logic.
Topology via logic
(The title of this section is an intended pointer to Steve Vickers’ book of the same name.)
One of the striking observations that Martín made some time ago is that a subset K of a topological space X is compact if and only if it has a continuous universal quantifier for open properties. I will spend the rest of this section explaining this.
The universal quantifier is this funny sign ∀ that reads “for all”. If you give me a property P that the elements of X may or may not satisfy, the formula ∀x in K.P(x) means “for every x in K, P is true of x“. It may be true (every element of K satisfied P) or false (some element of K violates P).
Formally, P is a map from X to S (Sierpiński space). Let me say that P is an open property if and only if the set of elements of X that satisfy P is open. In other words, an open property is the characteristic map χU of an open subset U of X. The formula ∀x in K.P(x) then simply means K ⊆ U.
Now fix K, and wonder about the map ∀K that maps every open property P=χU to the truth value of ∀x in K.P(x) in S. This is a map from [X → S] to S, two spaces that can be equipped with the Scott topologies of their orderings—we order functions pointwise. Then:
Lemma. ∀K is continuous if and only if K is compact.
Proof. Switching to the isomorphic view of open predicates P=χU as just opens U, ∀K is continuous if and only if the function that maps opens U to 1 if and only if K ⊆ U is Scott-continuous. This map is always monotonic, so the condition is equivalent to: for every directed family (Ui)i ∈ I of open subsets of X, K ⊆ ∪i ∈ IUi if and only if K ⊆ Ui for some i in I. This is the case exactly when K is compact, see Proposition 4.4.7 in the book. ☐
This in this sense that we can say that a subset is compact if and only if it has a continuous universal quantifier (for open predicates).
On the opposite, every subset has a continuous existential quantifier. I’ll let you check this by yourselves.
Programming languages
Every function is continuous in Scott semantics.!!!
Berger’s function, and improvements by Martin.!!!
Synthetic topology
You can now reverse !!!
— Jean Goubault-Larrecq (September 9th, 2016)
[1] Weng Kin Ho. Exact Real Calculator for Everyone. In W.-C. Yang , M. Majweski, T. Alwis, & I. K. Rana, (Eds.) Proceedings of the Eighteenth Asian Technology conference in Mathematics (ATCM) (pp. 1-15). Bombay, India: Mathematics and Technology, LLC., Dec 2014.
[2] Martín Hötzel Escardó and Weng Kin Ho. An operational domain theory and topology of a sequential programming language. Information and Computation 207(3), p. 411-437, Elsevier, 2009.
[3] Martín Hötzel Escardó. Synthetic topology of data types and classical spaces. ENTCS, Elsevier, volume 87, pages 21-156, November 2004.
[4] Weng Kin Ho. An operational domain-theoretic treatment of recursive types. Mathematical Structures in Computer Science, W. K. Ho, 24(1), p. 1-59, Feb 2014.