El-Zawawy, M. A.,
Semantic spaces in Priestley form,
, PhD thesis, Birmingham, University of Birmingham, UK, January, 2007.
AbstractThe connection between topology and computer science is based on two fundamental in- sights: the rst, which can be traced back to the beginning of recursion theory, and even intuitionism, is that computable functions are necessarily continuous when input and out- put domains are equipped with their natural topologies. The second, due to M. B. Smyth in 1981, is that the observable properties of computational domains are contained in the collection of open sets. The rst insight underlies Dana Scott's categories of semantics domains, which are certain topological spaces with continuous functions. The second in- sight was made fruitful for computer science by Samson Abramsky, who showed in his Domain Theory in Logical Form that instead of working with Scott's domains one can equivalently work with lattices of observable properties. Thus he established a precise link between denotational semantics and program logic. Mathematically, the framework for Abramsky's approach is that of Stone duality, which in general terms studies the relationship between topological spaces and their lattices of opens sets. While for his purposes, Abramsky could rely on existing duality results estab- lished by Stone in 1937, it soon became clear that in order to capture continuous domains, the duality had to be extended. Continuous domains are of interest to semantics because of the need to model the probabilistic behaviour and computation over real numbers. The extension of the Stone duality was achieved by Jung and Sunderhauf ¨ in 1996; the main out- come of this investigation is the realisation that the observable properties of a continuous space form a strong proximity lattice. The present thesis examines strong proximity lattices with the tools of Priestley duality, which was introduced in 1970 as an alternative to Stone's duality for distributive lattices. The advantage of Priestley duality is that it yields compact Hausdorff spaces and thus stays within classical topological ideas. The thesis shows that Priestley duality can indeed be extended to cover strong prox- imity lattices, and identies the additional structure on Priestley spaces that corresponds to the proximity relation. At least three different types of morphism have been dened between strong proximity lattices, and the thesis shows that each of them can be used in Priestley duality. The resulting maps between Priestley spaces are characterised and given a computational interpretation. This being an alternative to the JungSunderhauf ¨ duality, it is examined how the two dualities are related on the side of topological spaces. Finally, strong proximity lattices can be seen as algebras of the logic MLS, introduced by Jung, Kegelmann, and Moshier. The thesis examines how the central notions of MLS are transformed by Priestley duality.