|
PDF (266 kb) DVI (61 kb) PostScript (compressed) (94 kb) A5 PS booklet (compressed) (75 kb) What are these? [13 Feb 2009] | with Wesley Phoa, unpublished, 1990. Plotkin [1976] introduced a powerdomain construction on domains in order to give semantics to a non-deterministic binary choice constructor, and later [1979] characterised it as the free semilattice. Smyth [1983] and Winskel [1985] showed that it could be interpreted in terms of modal predicate transformers and Robinson [1986] recognised it as a special case of Johnstone's [1982] Vietoris construction, which itself generalises the Hausdorff metric on the set of closed subsets of a metric space. The domain construction involves a curious order relation known as the Egli-Milner order. In this paper we relate the powerdomain directly to the free semilattice, which in a topos is simply the finite powerset, i.e. the object of (Kuratowski-)finite subobjects of an object. We show that the Egli-Milner order coincides (up to "double negation") with the intrinsic order induced by a family of "observable predicates." This problem originally arose in the context of the Effective topos, in which the observable predicates are the recursively enumerable subsets. However we find that the results of this paper hold for any elementary topos, and so by considering a (pre)sheaf topos (which the Effective topos is not) we may compare them with the classical approach. |
|
PDF (228 kb) DVI (55 kb) PostScript (compressed) (73 kb) A5 PS booklet (compressed) (66 kb) What are these? [13 Feb 2009] | Presented at Logic in Computer Science 6, Amsterdam, July 1991. We present an elementary axiomatisation of synthetic domain theory and show that it is sufficient to deduce the fixed point property and solve domain equations. Models of these axioms based on partial equivalence relations have received much attention, but there are also very simple sheaf models based on classical domain theory. In any case the aim of this paper is to show that an important theorem can be derived from an abstract axiomatisation, rather than from a particular model. Also, by providing a common framework in which both PER and classical models can be expressed, this work builds a bridge between the two. |
| This paper is not available to download. | with Giuseppe Rosolini, in preparation, presented at Mathematical Foundations of Program Semantics 14, London, May 1998. We find a topos F with an object Σ that satisfies the axioms for synthetic domain theory and for which the category of replete objects in F satisfies the abstract Stone duality, i.e. that the adjunction Σ(−)−|Σ(−) is monadic. |
This is www.PaulTaylor.EU/ASD/sdt.php and it was derived from ASD/sdt.tex which was last modified on 24 February 2009.