_{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.

## No comments:

Post a Comment