A Note on a Model of Synthetic Domain Theory

Marcelo P. Fiore^{∗} LFCS, The King’s Buildings Edinburgh EH9 3JZ Scotland

Giuseppe Rosolini^{†} DIMA, via Dodecaneso 35 16146 Genova Italy

Abstract

A model of synthetic domain theory embedding the category ω-Cpo of ω-complete posets and ω-continuous functions as a reflective exponential ideal is introduced, and an internal characterisation of ω-Cpo within the model is presented. An expanded version of this note, not including the last section, appears in [4].

Introduction

This note is concerned with models of Synthetic Domain Theory (SDT) encompassing traditional categories of domains used in denotational semantics [7, 14], showing that the synthetic approach generalises the standard theory of domains and suggests new problems to it.

Consider a (locally small) category of domains D with a (small) dense generator G equipped with a Grothendieck topology. Assume further that every cover in G is effective epimorphic in D. Then, by Yoneda, D embeds fully and faithfully in the topos of sheaves on G for the canonical topology, which thus provides a set-theoretic universe for our original category of domains. In this note we explore such a situation for a traditional category of domains and, in particular, show that the Grothendieck topos so arising yields a model of SDT in which the category of domains has an internal characterisation.

We present a model of SDT embedding the category ω-Cpo of posets with least upper bounds of countable chains (hence called ω-complete) and ω-continuous functions (i.e. monotone functions which preserve these lubs) as a reflective exponential ideal. In turn, ω-Cpo embeds the category of domains in the model, viz. the full subcategory of replete objects [8, 13], again as a reflective exponential ideal. The replete ω-complete partial orders may offer a new interesting notion of domain to the standard theory but, at the moment, no explicit description of them is known.

∗Research supported by EPSRC grant GR/J84205, Frameworks for Programming Language Semantics and Logic.

†Research supported by EC project no.6811, CLICS II, and MURST 40%.

1 The topos H of continuous \overline{ω}-paths

We begin by fixing notation. We denote the finite cardinals as 0 = ∅, …, n + 1 = {0, …, n}, … and write N for the collection {0, …, n, …} of finite cardinals. We write n for the ordinal (n, ⊆) and for a chain x_{0} ≤ … ≤ x_{n−1} in a poset P we write (x_{0}, …, x_{n−1}) for the monotone map n → P sending i to x_{i}. We further write ω for the ordinal (N, ⊆), and \overline{ω} for its successor ordinal 0 ⊆ … ⊆ n ⊆ … ⊆ N.

Consider the following full subcategories of ω-Cpo:

• the monoid L of endomaps on \overline{ω},

• the category F of finite products of \overline{ω}.

Remark 1.1 In ω-Cpo, \overline{ω} is a dense generator. Thus, the “Yoneda” functor Y: ω-Cpo → Set^{L^{op}}: D ↦ ω-Cpo(−, D) is full and faithful, and preserves limits and exponentials.

Write S(C) for the idempotent splitting of a category C, see [12, 6]. The splitting S(L) is equivalent to the full subcategory of ω-Cpo consisting of \overline{ω} and the non-empty finite ordinals.

Let H be the topos sh(S(L), can) of sheaves on S(L) for the canonical topology. It is useful to have various presentations of the topos.

Proposition 1.2 The inclusions

\xymatrix{L \ar@{^{(}->}[r] \ar@{^{(}->}[d] & F \ar@{^{(}->}[d] \\ S(L) \ar@{^{(}->}[r] & S(F)}

induce equivalences

[figure: sh(L, can); sh(F, can); ≃; H; ≃; sh(S(F), can); ≃; ≃; .]

Theorem 1.3 The functor Y: ω-Cpo → H presents ω-Cpo as a full reflective exponential ideal of H.

Henceforth we shall identify an ω-complete poset D with the sheaf Y (D) of its continuous \overline{ω}-paths.

2 H as a model of SDT

We write 1 for the terminal object Y (1), Σ for the sheaf of continuous \overline{ω}-paths Y (2) associated to the Sierpinski space 2, and ⊤: 1 → Σ for Y (1: 1 → 2).

In H, the map ⊤: 1 → Σ is a dominance, see [11]. It follows from loc.cit. that it induces a notion of composable partial map in H, with a representation. We shall denote by L the action of the representation functor on H which underlies the so-called lifting monad. This abstract construction extends a well-known behaviour on the category ω-Cpo. Indeed, the notion of partial map is that expected from partial computations, see [2]. In ω-Cpo one can consider partial maps defined on a Scott-open subset. A Scott-open subset is a monomorphism in ω-Cpo which reflects the order and whose image is upward closed and inaccessible by lubs of ω-chains. The representing functor adds an element below the given order.

The lifting monad migrates to other subcategories of H.

Proposition 2.1 The functor L: H → H restricts to the endofunctor on the subcategory ω-Cpo which represents partial maps defined on Scott-open subsets. Moreover, the functor L restricts to the sites defining H. In other words there are functors such that the diagram

[figure: S(L); L; S(F); ω-Cpo; Y; H; L; S(L); S(F); ω-Cpo; Y; H]

commutes up to isomorphism. As the inclusions are full, all restrictions induce monads.

Another functor representing a different kind of partial map can be defined on H: consider the notion of Scott-closed subset as just the complement of a Scott-open subset. Explicitly, a monomorphism in ω-Cpo is Scott-closed if it reflects the order and its image is closed downward and under lubs of ω-chains. The representing functor adds an element above the given order. This notion of partiality is that induced by the dominance ⊥: 1 → Σ, defined as Y (0: 1 → 2), in H.

So to see H as a model of the axioms of synthetic domain theory as in [8] we take the disjoint dominances ⊤: 1 → Σ and ⊥: 1 → Σ.

The map Σ^{[⊥,⊤]}: Σ^{Σ} → Σ^{1+1} is monic in H and the object Σ is a suplattice with countable joins Σ^{N} → Σ in H, because both properties hold in ω-Cpo.

Writing c for the canonical map from the initial L-algebra to the final L-coalgebra [5], we have that Σ^{c} is iso and so the main infinitary axiom of SDT holds.

Theorem 2.2 The topos H with the dominance ⊤: 1 → Σ is a model of the axioms of synthetic domain theory as in [8].

Remark 2.3 A slightly different collection of axioms, also denoting models of synthetic domain theory, appeared in the literature, see [13]. By the results in loc.cit., it follows that H with Σ is also such a model.

3 An internal characterisation of ω-Cpo

Recall from [9, 10] that an object F is called complete when F^{c} is iso. Now, consider the following notion (used implicitly in [3]): an object F is said to be path-transitive when, for t the unique mediating map in

[figure: 1; ⊥; ⊤; Σ; η_{Σ}; Σ; L⊥; Σ ∨ Σ; t; LΣ]

where η denotes the unit of the lifting monad, F^{t} is iso.

Theorem 3.1 ω-Cpo is equivalent to the full subcategory of H consisting of the complete, path-transitive, ¬¬-separated objects.

Acknowledgements. We thank Martin Hyland for inspiring discussions.

References

[1] A. Carboni, M.C. Pedicchio, and G. Rosolini, editors. Category Theory, Proc., Como 1990, volume 1488 of Lecture Notes in Mathematics. Springer-Verlag, 1991.

[2] M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University Press Distinguished Dissertations in Computer Science, 1996.

[3] M.P. Fiore. Enrichment and representation theorems for categories of domains and continuous functions. Available from

    http://hypatia.dcs.qmw.ac.uk, 1996.

[4] M.P. Fiore and G. Rosolini. Two models of Synthetic Domain Theory. To appear in the Journal of Pure and Applied Algebra, 1996.

[5] P. Freyd. Algebraically complete categories. In Carboni et al. [1], pages 95–104.

[6] P.J. Freyd and A. Scedrov. Categories and Allegories. North Holland Publishing Company, 1991.

[7] C.A. Gunter. Semantics of Programming Languages: Structures and Techniques. The MIT Press, 1992.

[8] J.M.E. Hyland. First steps in Synthetic Domain Theory. In Carboni et al. [1], pages 131–156.

[9] J.R. Longley. Realizability Toposes and Language Semantics. PhD thesis, Department of Computer Science, University of Edinburgh, 1995.

[10] J.R. Longley and A.K. Simpson. A uniform approach to domain theory in realizability models. Available from

http://hypatia.dcs.qmw.ac.uk, 1995.

[11] G. Rosolini. Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986.

[12] D.S. Scott. Relating theories of λ-calculus. In R. Hindley and J. Seldin, editors, To H.B. Curry: essays in combinatory logic lambda calculus and formalisms, pages 403–450. Academic Press, 1980.

[13] P. Taylor. The fixed point property in synthetic domain theory. In G. Kahn, editor, Proc. 6^{th} Symposium on Logic in Computer Science, pages 152–160. IEEE, 1991.

[14] G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.