Synthetic topology

I've started reading about Martín Escardó's "synthetic topology", which seems closely related to (but not quite the same as) the ludics topological interpretation. The basic idea is that rather than topologizing a language by first specifying a partial order on data, then constructing open sets using that order, and finally showing that all definable functions are continuous—the approach in traditional domain theory—instead one starts at the end and simply declares continuous functions to be those definable in the language. An open set U of a datatype D is now defined by a continuous function χ_U : D → S from D into the Sierpinski space S. In classical topology, the Sierpinski space is simply the two point set {⊤, ⊥}, with open sets {{⊤, ⊥}, {⊤}, ∅}. In synthetic topology, S is a datatype with the single element ⊤; a computation of type S can either evaluate to ⊤, or else diverge, which is represented by ⊥. So the Sierpinski space essentially represents the observable results of computation, where we only distinguish between termination and non-termination. (In ludics, these two observable results are called daimon and faith.)

So again, an open set U of D is defined by U = χ_U^-1(⊤), where χ_U : D → S is definable in the underlying programming language. It follows immediately that U is closed under contextual equivalence, i.e. if d∈U and d ≈ d' then d'∈U. However, it is not necessarily the case that the collection of open sets is closed under (infinite or even finite) unions (as in classical topology). For this to be the case, given any two functions f,g : D → S, we have to be able to construct an h : D → S such that h(d) = ⊤ iff either f(d) = ⊤ or g(d) = ⊤. In other words, our language needs a sort of "parallel-or" construct.

I haven't gotten much further yet, but this looks interesting. Also, it seems that Escardó isn't just interested in applications to programming semantics, but in examining more traditional topological questions through synthetic topology.

A tutorial: "Synthetic topology of data types and classical spaces" by Martín Escardó.

A paper: "Operational domain theory and topology of sequential programming languages" by Martín Escardó and Weng Kin Ho.