An Extension of Models of Axiomatic Domain Theory to Models of Synthetic Domain Theory

Marcelo P. Fiore^{⋆} and Gordon D. Plotkin^{⋆⋆}

Department of Computer Science Laboratory for Foundations of Computer Science University of Edinburgh, The King’s Buildings Edinburgh EH9 3JZ, Scotland

Abstract. We relate certain models of Axiomatic Domain Theory (ADT) and Synthetic Domain Theory (SDT). On the one hand, we introduce a class of non-elementary models of SDT and show that the domains in them yield models of ADT. On the other hand, for each model of ADT in a wide class we construct a model of SDT such that the domains in it provide a model of ADT which conservatively extends the original model.

Introduction

The aim of Axiomatic Domain Theory (ADT) is to axiomatise the structure needed on a category so that its objects can be considered to be domains (see [11, § Axiomatic Domain Theory]).

Models of axiomatic domain theory are given with respect to an enrichment base provided by a model of intuitionistic linear type theory [2, 3]. These enrichment structures consist of a monoidal adjunction C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} D between a cartesian closed category C and a symmetric monoidal closed category with finite products D, as well as with an ω-inductive fixed-point object (Definition 1.11 (2)). Roughly speaking, an ω-inductive fixed-point object is an initial algebra (for the endofunctor underlying the monad induced by the adjunction) arising as the colimit of a standard ω-chain, equipped with a global element invariant under successor. With respect to such a structure, a model of axiomatic domain theory is a D-category which is closed under suitable C-enriched type constructors (as, for example, products, higher types, and sums) and is C-algebraically compact. The rôle of algebraic compactness is to provide a universal method of solving recursive type equations [15]; in this context algebraic compactness is guaranteed by the usual completeness conditions on the model [28].

The canonical example of an enrichment base is obtained by taking:

– C = Cpo, the category of small cpos —ω-complete partial orders— and continuous functions;

⋆ Research supported by Typed Lambda Calculus network ERBCHRXCT920046. ⋆⋆ Research supported by an EPSRC Senior Fellowship.

– D = Cppo_{⊥}, the category of small cppos —ω-complete pointed partial orders— and strict continuous functions, with the symmetric monoidal closed structure given by the Sierpinski space, smash products, and strict exponentials; and

– the adjunction Cpo \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} Cppo_{⊥} with left adjoint given by lifting.

In this example, the inductive fixed-point object is the ordinal ω + 1 equipped with its limit point ω.

A typical model, with respect to the above enrichment base, is pCpo (the category of small cpos and partial continuous functions [27]); it has partial products, Kleisli (or partial) exponentials and finite coproducts (all yielding Cpo-functors), and it is Cpo-algebraically compact [8]. This example is representative of the class of models that we consider in this paper in that the lifting monad 𝕃 on Cpo allows us to recover the other data. Indeed, we have that Cppo_{⊥} ≅ Cpo^{𝕃} (the category of Eilenberg-Moore algebras for 𝕃) and that pCpo ≅ Cpo_{𝕃} (the Kleisli category for 𝕃). Moreover, as is well-known, the smash product is characterised by the property that for cppos P and Q, the canonical bistrict map P × Q → P ⊗ Q is universal among bistrict maps.

The models that we consider generalise the above example and are those given by a category C equipped with an initial object, a cartesian closed structure, a lifting monad 𝕃, and an inductive fixed-point object such that C^{𝕃} has tensor products and linear exponentials (respectively axiomatising smash products and strict exponentials) and C_{𝕃} is C-algebraically compact. It follows that C^{𝕃} is cartesian and that C_{𝕃} has partial products and Kleisli exponentials yielding C-functors. (In this paper we do not assume our models to have binary coproducts; however it seems possible to extend our analysis to obtain analogous results for this situation.)

The slogan of Synthetic Domain Theory (SDT) is that domains are sets and all functions between them are continuous (see [11, § Synthetic Domain Theory]). Thus, within a suitable universe of sets, generally taken to be a topos, one wishes to identify the sets which behave like domains. In this paper, following a suggestion of Hyland, we relate the axiomatic and synthetic viewpoints. In fact, we give a non-elementary version of SDT yielding a category of domains that complies with the axiomatic requirements (Theorem 3.1). And, as a main result (Theorem 3.4), for every small (Kleisli) ADT model (Definition 1.12 (2)) we construct a (Grothendieck) model of our SDT (Definition 2.13) whose domains yield a (Kleisli) ADT model conservatively extending the original model.

1 Axiomatic domain theory

We introduce the concepts and results of ADT needed in the rest of the paper. In Subsections 1.1 and 1.2 we recall the notions of lifting monad, tensor products and linear exponentials, and study them in presheaf toposes. In Subsections 1.3 and 1.4, we further recall the notions of partial products and Kleisli exponentials, and algebraic compactness, which respectively permit the interpretation of simple types (in Kleisli categories) and of recursive types. Finally, in Section 1.5 we define the class of ADT models that we will be interested in.

1.1 Lifting

We present an axiomatisation of lifting in terms of dominances [30] which is by now traditional; its connection with partiality is discussed briefly. (For details consult [8]).

Definition 1.1. (Dominance [30]) Let C be a category with a terminal object 1. An object Σ equipped with a subobject ⊤ : 1 ↪ Σ such that pullbacks of ⊤ (henceforth called ⊤-subobjects) always exist is called a ⊤-subobject classifier if every ⊤-subobject U ↪ A appears in a pullback

\begin{aligned}U & \overline{→} & 1 \\ A & ^{↓ ∩} & \overline{→} & Σ & \begin{matrix}↓ & ∩ \\ ⊤ \end{matrix} \end{aligned}

for a unique characteristic map A → Σ.

A ⊤-subobject classifier is called a dominance if ⊤^{∗} : C/Σ → C has a right adjoint, and ⊤-subobjects are closed under composition. (For details consult [30, 17]). ⊓ ⊔

Remark. In the context of SDT, the notion of dominance is only defined by the second requirement, as the first requirement generally holds in the universes of sets considered (e.g. locally cartesian closed categories with finite limits, such as toposes or quasitoposes).

Convention. We will use ↪ to indicate ⊤-subobjects.

A dominance ⊤ : 1 ↪ Σ in a category C allows one to consider partial maps with domain of definition a ⊤-subobject and action a C-map. To this end, one defines a ⊤-partial map A ⇀ B as (a representative of) an equivalence class of diagrams of the form A ↩ U → B with U ↪ A a ⊤-subobject where (A ↩ U → B) ≡ (A ↩ V → B) if for some U ≅ V, (A ↩ U) = (A ↩ V ≅ U) and (U → B) = (U ≅ V → B). Moreover, for a well-powered C, ⊤-partial maps form a category with the same objects as C, composition given by setting

[B ↩ V → C] ∘ [A ↩ U ⟶^{f} B] =^{def} [A ↩ U ↩ f^{−1}(V) → V → C], and

identities given by [A ↩ A → A].

In the context of a category with a dominance ⊤ : 1 ↪ Σ, writing Π_{⊤} for the right adjoint to ⊤^{∗}, we have, for every B ∈ | C |, that (Π_{⊤}B)^{∗}(⊤) ≅ B; hence obtaining a pullback diagram

\begin{matrix}B & \overline{→} & 1 \\ LB & ^{η_{B}↓ ∩} & \overline{_{Π_{⊤}B →}} & Σ & \begin{matrix}↓ & ∩ \\ ⊤ \end{matrix} & . \end{matrix}  (1)

Moreover, the ⊤-subobject η_{B} : B ↪ LB in (1) is a classifier of ⊤-partial maps with target B, in that every ⊤-partial map [A ↩ U → B] appears in a pullback

\begin{aligned}U & \overline{→} & B \\ A & ^{↓ ∩} & \overline{→} & LB & \begin{matrix}↓ & ∩ \\ η_{B} \end{matrix} \end{aligned}

for a unique characteristic map A → LB.

The following is well-known (see e.g. [17, 25, 8]):

Proposition 1.2. In a cartesian category, dominances induce commutative monads. ⊓ ⊔

Remark. For the notion of commutative monad see [20, 24]. The underlying endofunctor of the monad induced by a dominance ⊤ : 1 ↪ Σ is given by the composite C ^{Π_{⊤}}→ C/Σ → C where C/Σ → C is the domain functor.

Convention. We refer to the monad induced by a dominance as the lifting monad and denote it 𝕃; its underlying endofunctor and unit are respectively denoted L and η (this is consistent with the notation already used in (1)).

Further, the Kleisli category for a monad 𝕋 on a category C is denoted C_{𝕋}.

Given a dominance ⊤ : 1 ↪ Σ on a category C, the Kleisli category C_{𝕃} is isomorphic to the category of ⊤-partial maps as described above; and hence from now on we will feel free to regard a morphism A → B in C_{𝕃} either as a morphism A → LB in C or as a ⊤-partial map A ⇀ B.

Proposition 1.3. In a category with a strict initial object 0 and a dominance ⊤ : 1 ↪ Σ for which the map 0 → 1 is a ⊤-subobject, L0 ≅ 1. ⊓ ⊔

Lifting in presheaf toposes. We proceed to study lifting in presheaf toposes. Such a study was started by Rosolini in his thesis [30]; here we build on top of his work.

Convention. For a small category A, we write Â for the presheaf topos [A^{op}, Set] where, as usual, Set denotes the category of small sets and functions. Moreover, we always identify A with its image under the Yoneda embedding A ↪ Â. For a small category A with an initial object, we write Ã for the sheaf topos obtained by declaring that the empty cover covers the initial object; when the initial object is strict, Ã is simply the full subcategory of Â consisting of all those presheaves P for which P (0) ≅ 1.

Theorem 1.4. ([30]) Let A be a small category and let M be a class of admissible monos (i.e. closed under isomorphisms, composition and pullbacks along arbitrary maps). In Â, ⊤ : 1 ↪ Σ defined by Σ(A) =^{def} {[m] | m : U ↪ A in M} with action given by pullback and ⊤_{A} =^{def} [id_{A}], is a dominance. Moreover, O ↪ P is a ⊤-subobject in Â if and only if for all A → P with A ∈ | A | there exists U ↪ A in M such that

\begin{aligned}U & \overline{→} & O \\ A & ^{↓ ∩} & \overline{→} & P & ^{↓ ∩} & . \end{aligned}

⊓ ⊔

Corollary 1.5. Let A be a small category with a strict initial object 0 and a dominance ⊤ : 1 ↪ Σ for which the map 0 → 1 is a ⊤-subobject.

1. The Yoneda embedding A ↪ Â cuts down to an embedding A ↪ Ã.

2. The Yoneda embedding A ↪ Ã preserves the initial object and the dominance (i.e. in Ã, 0 is initial and ⊤ : 1 ↪ Σ is a dominance). Moreover, the diagram

\begin{aligned}A & ^{⊂} → & Ã & ^{⊂} → & Â \\ A & \begin{matrix}L \\ ↓ \end{matrix} & ^{⊂} → & Ã & ^{↓L} & ^{⊂} → & Â & ^{↓L} \end{aligned}

commutes up to isomorphism.

Proof. (1) Because 0 is initial in A.

(2) The first part follows from Theorem 1.4 using that the ⊤-subobjects of a sheaf in Ã are exactly the ⊤-subobjects in Â. The second part follows from:

Proposition 1.6. ([32]) Let S be a topos equipped with a dominance ⊤ : 1 ↪ Σ. For every topology j in S, if Σ is a j-sheaf then the lifting in S preserves the property of being a j-sheaf. ⊓ ⊔

⊓ ⊔

In the situation of the above corollary, the following result provides a description of lifting which is useful for determining its preservation properties with respect to colimits.

Theorem 1.7. Let A be a small category with a strict initial object 0 and a dominance ⊤ : 1 ↪ Σ for which the map 0 → 1 is a ⊤-subobject.

1. Let L^{∗} : Â → Â: P ↦ P ∘ L^{op}. For L_{!} : Â \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} Â: L^{∗}, the diagram

\begin{aligned}Ã & ^{⊂} → & Â \\ Ã & \begin{matrix}L \\ ↓ \end{matrix} & ^{⊂} → & Â & ^{↓L_{!}} \end{aligned}

commutes up to isomorphism.

2. L : Ã → Ã preserves non-empty connected colimits.

Proof. (1) For P ∈ | Â |, L_{!}P can be explicitly described as the P -valued partial maps with domain of definition a ⊤-subobject in A. Formally, we have

– For A ∈ | A |, L_{!}P A = {[A ↩ U → P] | U ↪ A in A, U → P in Â} where (A ↩ U → P) ≡ (A ↩ V → P) iff there exists U ≅ V such that (U ↪ A) = (U ≅ V ↪ A) and (U → P) = (U ≅ V → P).

– For A → B in A, L_{!}P (A → B)[B ↩ V → P] = [A ↩ U → V → P] where

\begin{aligned}U & \overline{→} & V \\ A & ^{↓ ∩} & \overline{→} & B & ^{↓ ∩} & . \end{aligned}

The unit of the adjunction P → L^{∗}L_{!}P is given by (A → P) ↦ [LA ↩ A → P].

For P ∈ | Ã |, it follows by construction that L_{!}P ∈ | Ã |; moreover P ↪ L_{!}P given by (A → P) ↦ [A ↩ A → P] is a classifier of ⊤-partial maps with target P in Ã.

(2) As Ã ↪ Â preserves non-empty connected colimits, for G non-empty and connected, every colimiting cone γ : Δ \underrightarrow{.} Q : G → Ã is colimiting in Â and, as L_{!} is a left adjoint, also L_{!}γ : L_{!}Δ \underrightarrow{.} L_{!}Q is colimiting in Â. Thus, Lγ : LΔ \underrightarrow{.} LQ is colimiting in Ã. ⊓ ⊔

Remark. Note that the proof of Theorem 1.7 (1) provides an explicit description of the lifting monad.

1.2 Tensor products and linear exponentials

We summarise standard material on tensor products and linear exponentials in categories of Eilenberg-Moore algebras (see [20, 21, 6, 18]) and study them in categories of lift-algebras over presheaf toposes.

Let 𝕋 = (𝕋, η, μ, st) be a commutative monad on a cartesian category C. We write st′ for the composite T (A) × B ≅ B × T (A) ^{st}→ T (B × A) ≅ T (A × B) and dst for either of the composites

(T (A) × T (B) ^{st′}→ T (A × T B) ^{T st}→ T^{2}(A × B) ^{μ}→ T (A × B))
= (T (A) × T (B) ^{st}→ T (T A × B) ^{T st′} → T^{2}(A × B) ^{μ}→ T (A × B)).

The category of Eilenberg-Moore algebras and homomorphisms for a monad 𝕋 on a category C is denoted C^{𝕋}. The structure map on an algebra X is denoted by ρ_{X} but generally left implicit. Algebra homomorphisms are indicated by ∘→. When we write X ∘→ Y, the objects X and Y are assumed to be algebras. For every object A and algebras X, Y, the objects T A and X × Y are algebras with ρ_{T A} and ρ_{X×Y} respectively taken to be μ_{A} and ⟨ρ_{X} ∘ T π_{1}, ρ_{Y} ∘ T π_{2}⟩.

For algebras X, Y, Z, a map h : X × Y → Z said to be a bihomomorphism whenever

\begin{matrix}(T (X) × T (Y) ^{ρ_{X}×ρ_{Y}} → X × Y ^{h}→ Z) \\ = (T (X) × T (Y) ^{dst}→ T (X × Y) ^{T h}→ T Z ^{ρ_{Z}}→ Z). \end{matrix}

Bihomomorphisms will be indicated by ∘∘→. The tensor product of algebras X and Y, is defined as the universal bihomomorphism X × Y ∘∘→ X ⊗ Y; that is, for every bihomomorphism X × Y ∘∘→ Z there exists a unique homomorphism X ⊗ Y ∘→ Z such that (X × Y ∘∘→ X ⊗ Y ∘→ Z) = (X × Y ∘∘→ Z). If C^{𝕋} has all tensor products then ⊗ endows C^{𝕋} with a symmetric monoidal structure with unit T 1. The map dst : T (A) × T (B) ∘∘→ T (A × B) is a bihomomorphism and its unique extension T (A) ⊗ T (B) ∘→ T (A × B) is an isomorphism with inverse

T (A×B) ^{⟨T π_{1},T π_{2}⟩} → T (A)×T (B)∘∘→T (A)⊗T (B). Thus, the adjunction C \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} C^{𝕋}

is monoidal (in the sense of [7]). Linear exponentials, denoted with ∘⇒ , are defined as the closed structure associated to tensor products (i.e. by the adjoint situation ⊗ X ⊣ X ∘⇒ : C^{𝕋} → C^{𝕋}).

If C^{𝕋} has reflexive coequalisers (i.e. coequalisers of parallel pairs f, g : X\overrightarrow{→}Y for which there exists h : Y → X such that f ∘ h = id = g ∘ h) one can define tensor products for every pair of algebras; viz. as the coequaliser in C^{𝕋} of

T (T (X) × T (Y)) ∘ μ∘T dst→ ; ∘_{T (ρ_{X}×ρ_{Y} )} → T (X × Y). A simple situation under which this may

be applied is given by the following proposition.

Proposition 1.8. If C has (reflexive) coequalisers and T preserves them then C^{𝕋} has (reflexive) coequalisers. ⊓ ⊔

If C is cartesian closed then the action of the functor T on morphisms can be internalised as a map \underline{T}_{A,B} : B^{A} → T B^{T A} defined as the exponential transpose

of the composite B^{A} × T A ^{st}→ T (B^{A} × A) ^{T e}→ T B, where e denotes the evaluation map. If, in addition, C has equalisers we can define X ∘⇒ Y as the

equaliser of Y^{X} \begin{aligned}Y^{ρ_{X}} & → \\ ρ_{Y} ^{T X}∘\underline{T}_{X,Y} & → \end{aligned} Y^{T X} in C with ρ_{X ∘⇒ Y} the unique map, given by

the universal property of equalisers, such that

\begin{matrix}(T (X ∘⇒ Y) ^{ρX ∘⇒ Y} → X ∘⇒ Y ^{>}→^{i} Y^{X}) \\ = (T (X ∘⇒ Y) ^{T i}→ T (Y^{X}) ^{λ(T (e)∘st′)} → T Y^{X} ^{ρ_{Y} ^{X}} → Y^{X}). \end{matrix}

In the context of the lifting monad over a presheaf topos we have:

Corollary 1.9. Let A be a small category with a strict initial object 0 and a dominance ⊤ : 1 ↪ Σ for which the map 0 → 1 is a ⊤-subobject. Then, Ã^{𝕃} has a symmetric monoidal closed structure given by Σ, tensor products, and linear exponentials. Moreover, the adjunction Ã \begin{matrix}⟶ \\ ⊥ \\ ⟵ \end{matrix} Ã^{𝕃} is monoidal. ⊓ ⊔

1.3 Partial products and Kleisli exponentials

Let 𝕋 be a commutative monad on a cartesian category C. The partial product functor ⊗ : C_{𝕋} × C_{𝕋} → C_{𝕋} acts as (A, B) ↦ A × B on objects and as (f, g) ↦ dst ∘ (f × g) on morphisms. As usual for higher types, exponentiation arises as a right adjoint to multiplication. In this case for every A ∈ | C |, we set ⊗ A ⊣ A⇀ ⇀ : C_{𝕋} → C and call A⇀ ⇀B, whenever it exists, the Kleisli exponential. When C is cartesian closed, A⇀ ⇀B exists and is simply given by (T B)^{A}. Moreover, the partial product and Kleisli exponential functors are C-enriched and permit the interpretation of simple types in C_{𝕋} [24].

1.4 Algebraic compactness

Algebraically compact categories [15] axiomatise the mathematical universes allowing a universal interpretation of recursive types. We recall the notion of algebraic compactness in an enriched setting as in [8].

Definition 1.10. (c.f. [15])

1. (Invariant object) An invariant object of an endofunctor F is specified by an isomorphism F X ≅ X.

2. (Free invariant object) For an endofunctor, an invariant object is said to be free if it is both an initial algebra and a final coalgebra.

3. (Algebraic compactness) For a cartesian category V, a V-category is said to be V-algebraically compact if (the underlying endofunctor of) every V-endofunctor on it admits a free invariant object. ⊓ ⊔

Remark. In general a stronger definition of algebraic compactness based on a notion of parametric free invariant object [28, 29] is more appropriate; however we do not go into the details here, as in the context of this paper both definitions are equivalent.

1.5 Kleisli ADT models

After introducing the notion of inductive fixed-point object we will be in a position to define Kleisli ADT models.

Definition 1.11. Consider a category with an initial object and a dominance.

1. We let Λ be the chain ⟨L^{n}(0 → 1)⟩ and, for every L-algebra α : LA → A, we define the cone ⟨α⟩ : Λ \underrightarrow{.} A inductively as follows: ⟨α⟩_{0} =^{def} (0 → A) and

⟨α⟩_{n+1} =^{def} L^{n+1}0 ^{L⟨α⟩_{n}} → LA ⟶^{α} A.

2. (Inductive fixed-point object) An inductive fixed-point object consists of an L-invariant object σ : L\overline{ω} ≅ \overline{ω} together with a global element 1 → \overline{ω} such that the cone ⟨σ⟩ : Λ \underrightarrow{.} \overline{ω} is colimiting and (1 → \overline{ω} ^{succ}→ \overline{ω}) = (1 → \overline{ω}) where succ =^{def} (\overline{ω} ^{⊂}^{η\overline{ω}}→ L\overline{ω} ≅ \overline{ω}). ⊓ ⊔

The essential difference between our fixed-point object and the one previously considered in [5] is its inductive nature, in that we require it to arise as the colimit of the standard chain generated by iterating the lifting functor.

Definition 1.12. 1. (Monadic base) A (lifting) monadic (enrichment) base is given by a category C equipped with an initial object, a cartesian closed structure, a dominance, and an inductive fixed-point object such that C^{𝕃} has tensor products and linear exponentials.

2. (KADT model) For a monadic base C, C_{𝕃} is said to be a Kleisli ADT model if it is C-algebraically compact. ⊓ ⊔

KADT models with finite coproducts yield models of FPC (as in [8, Definition 8.3.1]) and hence allow the interpretation of the metalanguage FPC [27].

Remark. A subtle consequence of the above definition is that the map 0 → 1 is a ⊤-subobject. Indeed, observing that 0 is initial, and hence also terminal, in C_{𝕃} (as C_{𝕃} is C-algebraically compact), the claim follows from the existence of a partial map 1 ⇀ 0 using that 0 is strict. Hence, the dominance ⊤ : 1 ↪ Σ cannot be trivial unless C is.

Algebraic compactness may be achieved under certain completeness conditions (see e.g. [8, 28]) for so-called ep-sequences. Rather than defining epsequences we will observe the following which we need later.

Let C be a monadic base and let K be a C^{𝕃}-category.

1. Ep-sequences in K are chains of retractions equipped with certain extra structure.

2. In K the limit/colimit coincidence [35] holds for ep-sequences [28].

3. Assuming that K has an enriched zero object 0, every C-endofunctor F on K induces the standard ep-sequence ⟨F^{n}(0\overleftarrow{→}F 0)⟩ whose bilimit, whenever it exists, is preserved by the functor.

Theorem 1.13. ([28]) If K has an enriched zero object and bilimits of ep-sequences then it is C-algebraically compact. ⊓ ⊔

For a monadic base C, we may apply the above remarks to the C-endofunctor L on C^{𝕃}. Writing ⊤ : 1 ↪ Σ for the dominance, the standard ep-sequence induced by L is ⟨L^{n}(1 \begin{matrix}←∘ \\ ∘→ \end{matrix} Σ)⟩ with ⟨L^{n}(1 ∘→Σ)⟩ = LΛ (see Definition 1.11 (1)). Moreover, writing σ : L\overline{ω} ≅ \overline{ω} for the inductive fixed-point object, since the cone ⟨σ⟩ : Λ \underrightarrow{.} \overline{ω} is colimiting in C and the free functor C → C^{𝕃} preserves colimits it follows that L⟨σ⟩ : LΛ {. \atop ∘→} L\overline{ω} is colimiting in C^{𝕃}. Now, by the limit/colimit coincidence, the cocone π : L\overline{ω} {. \atop ∘→} ⟨L^{n}(1 ←∘ Σ)⟩ induced by the coalgebra Lσ^{−1} (i.e. defined by π_{0} =^{def} (L\overline{ω} ∘→ 1) and π_{n+1} =^{def} L(π_{n} ∘ σ^{−1})) is limiting in C^{𝕃}. Finally, as the forgetful functor C^{𝕃} → C preserves limits, we have that

π ∘ σ : \overline{ω} ≅ L\overline{ω} \underrightarrow{.} ⟨L^{n}(1 ← Σ)⟩ is limiting in C;  (2)

and hence L\overline{ω} ≅ \overline{ω} is a free L-invariant object. Thus, in a monadic base the global element 1 → \overline{ω} of the inductive fixed-point object is characterised by the equation (1 → \overline{ω} ^{succ} → \overline{ω}) = (1 → \overline{ω}).

2 Synthetic domain theory

We develop a non-elementary version of SDT. On the one hand, we follow closely the approach of Longley and Simpson [22, 23] in that we adopt their completeness axiom (Axiom 1) and identify domains with well-complete objects (Definition 2.6 (2)); on the other hand, we depart notably from their approach in that we impose a non-elementary axiom (Axiom 3) stating that the initial lift-algebra in the ambient topos is inductive, in that it arises as a colimit of the standard chain.

2.1 Orthogonality

Orthogonality [12] plays a crucial rôle in understanding well-complete objects (see Theorem 2.7 (1)), in this subsection we recall the notion together with various useful observations about it.

Definition 2.1 (Orthogonality). 1. An object A is said to be orthogonal to a map D → C whenever for every map D → A there exists a unique C → A such that (D → A) = (D → C → A). For a category C and a class J of maps in it we define O(C, J) as the full subcategory of C consisting of all those objects orthogonal to every map in J.

2. In a cartesian closed category, an object A is internally orthogonal to a map g : D → C whenever A^{g} : A^{C} → A^{D} is iso. ⊓ ⊔

Intuitively, an object is orthogonal to a map whenever it believes (or, as Lawvere will put it, perceives) that the map is iso. Internal orthogonality corresponds to a parameterised version of orthogonality.

Proposition 2.2. In a cartesian closed category C,

1. An object is internally orthogonal to a map g if and only if it is orthogonal to g × C, for every object C.

2. For a colimiting cone Δ \underrightarrow{.} C : G → C, if an object is orthogonal to g × Δ_{n} for every n ∈ | G |, then it is orthogonal to g × C. ⊓ ⊔ Proposition 2.3. 1. If an object is orthogonal to a map then so is every retract

of the object.

2. The embedding O(C, J) ↪ C creates limits. ⊓ ⊔

Proposition 2.4. Let C be a cartesian closed category and let J be a class of maps in C satisfying the following closure property:

(Parameterisation) For g ∈ J and C ∈ | C |, g × C ∈ J.

Then, O(C, J) is a full sub-cartesian exponential ideal of C. ⊓ ⊔

2.2 SDT models

We assume a topos S with NNO ℕ and equipped with a dominance ⊤ : 1 ↪ Σ. We have that Σ is a subobject of the subobject classifier Ω; in fact,

\begin{aligned}1 & \overline{→} & 1 \\ Σ & ^{⊤↓ ∩} & ^{>} → & Ω & \begin{matrix}↓ & ∩ \\ true \end{matrix} & . \end{aligned}

The following is folklore [31, 19, 34]:

Proposition 2.5. The lifting functor L has an initial algebra ι : LI ≅ I and a final coalgebra φ : F ≅ LF with a unique global element 1 → F such that (1 → F ^{⊂} ^{η_{F}}→ LF ≅ F) = (1 → F). Moreover, the canonical map κ : I → F (characterised by the equation Lκ = φ ∘ κ ∘ ι) is mono. ⊓ ⊔

We have the following internal description:

F = {p ∈ Σ^{ℕ} | ∀ n ∈ ℕ. p_{n+1} ⇒ p_{n}}

and so the inclusion F ⊆ Σ^{ℕ} is a section with retraction Σ^{ℕ} → F mapping f to λn ∈ ℕ. ⋀_{0≤i≤n} f_{i}.

Definition 2.6. ([22, 23])

1. (Complete object) An object is complete whenever it is internally orthogonal to the canonical map I^{>}→ F.

2. (Well-complete object) An object A is well-complete whenever LA is complete. We write WC(S) for the full subcategory of well-complete objects in S. ⊓ ⊔

Intuitively, an object A is complete whenever it believes that every “parameterised I-chain in A” has a unique “extension” to a “parameterised F-chain in A” (see Proposition 2.2 (1)).

Notice that an object A is well-complete if and only if it is orthogonal, with respect to ⊤-partial maps, to κ × C : I × C ^{>}→ F × C for every C. That is, when for every ⊤-partial map I × C ⇀ A there exists a unique ⊤-partial map F × C ⇀ A such that (I × C ⇀ A) = (I × C ^{>}→ F × C ⇀ A).

Axiom 1 (Completeness axiom [23]). Σ is complete. ⊓ ⊔

The completeness axiom establishes, for every C ∈ | S |, a bijective correspondence

(κ × C)^{−1}( ) : ΣSub(F × C) ≅ S(F × C, Σ) ≅ S(I × C, Σ) ≅ ΣSub(I × C)
f ↦ f ∘ (κ × C) (3)

where ΣSub(A) denotes the collection of ⊤-subobjects of A.

We characterise well-completeness in terms of orthogonality and study closure properties of well-complete objects.

Theorem 2.7. 1. (Intrinsic characterisation of WC) For J the smallest family of maps in S containing the canonical map I^{>}→ F and satisfying the following closure properties:

(Parameterisation) For g ∈ J and C ∈ | S |, g × C ∈ J.

(Stability) For D → C in J and U ↪ C a ⊤-subobject,

\begin{aligned}V & \overline{→} & U \\ D & ^{↓ ∩} & \overline{→} & C & ^{↓ ∩} \end{aligned} ⇒ V → U in J,

we have WC(S) = O(S, J).

2. (c.f. [23]) Σ is well-complete.

3. (c.f. [23]) WC(S) is closed under lifting.

4. (c.f. [23]) Well-complete objects are also complete.

Proof. (1) First observe that

J = \{V ↪ U | \begin{matrix}V & ^{>}  → & U \\ I × C & ^{↓ ∩} & ^{>}κ × C → & F × C & ^{↓ ∩} \end{matrix} C ∈ | S |\}.

(⊆) Let A be a well-complete object. In the situation

\begin{aligned}V & ^{>} → & U \\ I × C & ^{↓ ∩} & ^{>}κ × C → & F × C & ^{↓ ∩} \end{aligned}

every map V → A yields the ⊤-partial map [I × C ↩ V → A] with a unique extension [F × C ↩ W → A] such that

\begin{aligned}V & ^{>}  → & W \\ I × C & ^{↓ ∩} & ^{>}κ × C → & F × C & ^{↓ ∩} \end{aligned} and (V → A) = (V ^{>}→ W → A).

And since, by (3), [W ↪ F × C] = [U ↪ F × C] we are done.

(⊇) For a ⊤-partial map [I × C ↩ V → A], by (3) and orthogonality, there exist unique U ↪ F × C and U → A such that

\begin{aligned}V & ^{>}  → & U \\ I × C & ^{↓ ∩} & ^{>}κ × C → & F × C & ^{↓ ∩} \end{aligned}and (V → A) = (V ^{>}→ U → A);

hence we are done.

(2) Because in the situation

\begin{aligned}V & ^{>} → & U \\ I × C & ^{↓ ∩} & ^{>}κ × C → & F × C & ^{↓ ∩} \end{aligned}

we have (V → Σ) = (V ^{>}→U → Σ) if and only if (U → Σ) = (U ↪ F×C → Σ) where

\begin{aligned}V & \overline{→} & 1 \\ I × C & ^{↓ ∩} & \overline{→} & Σ & \begin{matrix}↓ & ∩ \\ ⊤ \end{matrix} \end{aligned} and (I × C → Σ) = (I × C ^{>}^{κ×C} → F × C → Σ).

(3) Using that Σ is well-complete and the closure under (Stability) of J one can adapt the argument of Proposition 1.6 to well-completeness (see [9, Lemma 11.16]).

(4) A well-complete object A is also complete, by Proposition 2.2 (1) and 2.3 (2) because

\begin{aligned}A & \overline{→} & 1 \\ LA & ^{↓ ∩} & \overline{→} & Σ & ^{↓ ∩} \end{aligned}

in S. ⊓ ⊔

Corollary 2.8. Let W be a subcategory of S containing the terminal object and closed under lifting. Then, the following are equivalent:

– Every object in W is well-complete.

– Every object in W is complete.

If, in addition, W is an exponential ideal of S then a further equivalent statement is:

– Every object in W is orthogonal to the canonical map I^{>}→ F. ⊓ ⊔ Corollary 2.9. (c.f. [23])

1. WC(S) is a full sub-cartesian exponential ideal of S.

2. φ : F ≅ LF remains a final L-coalgebra in WC(S).

Proof. (1) By Proposition 2.4 and Theorem 2.7 (1).

(2) Because F is a retract of Σ^{ℕ} which, by Corollary 2.9 (1), is well-complete. ⊓ ⊔

Axiom 2 ([17]). The map 0 → 1 is a ⊤-subobject. ⊓ ⊔

Corollary 2.10. The initial object in S is also initial in WC(S).

Proof. By Proposition 2.3 (2) because, by Axiom 2,

\begin{aligned}0 & ^{⊂} → & 1 \\ 1 & ^{↓ ∩} & \overline{→} & Σ & \begin{matrix}↓ & ∩ \\ ⊤ \end{matrix} \end{aligned}

in S. ⊓ ⊔

Proposition 2.11. ([23]) In WC(S), φ^{−1} : LF ≅ F is an initial L-algebra; and hence is free. ⊓ ⊔

Our main means for relating axiomatic and synthetic domain theory is the following axiom.

Axiom 3. The cone ⟨ι⟩ : Λ → I (see Definition 1.11 (1)) is colimiting in S. ⊓ ⊔

Proposition 2.12. In WC(S), the cone ⟨φ^{−1}⟩ : Λ → F is colimiting; and hence F becomes an inductive fixed-point object.

Proof. Let γ : Λ \underrightarrow{.} C be a cone with C a well-complete object. As κ is the unique mediating morphism between ⟨ι⟩ and ⟨φ^{−1}⟩ and C is orthogonal to it, we have that a map F → C mediates between ⟨φ^{−1}⟩ and γ if and only if, for I → C the unique mediating morphism between ⟨ι⟩ and γ, (I → C) = (I ^{>} ^{κ}→ F → C).

⊓ ⊔

Finally, we are in a position to define Grothendieck SDT models.

Definition 2.13 (GSDT model). A Grothendieck SDT model is given by a Grothendieck topos equipped with a dominance such that its induced lifting functor has rank (i.e. it preserves α-filtered colimits for some regular cardinal α), in which Axioms 1–3 hold. ⊓ ⊔

Remark. The above should only be taken as a working definition. For example, if in the notion of GSDT model we replace the condition “the lifting functor has rank” by “the lifting functor preserves reflexive coequalisers” our results remain valid.

As lifting preserves non-empty connected limits [17, Proposition 2.2.1], in GSDT models the final lift-coalgebra can be computed as the limit of the chain ⟨L^{n}(1 ← Σ)⟩.

Example 2.14. The presheaf toposes on

1. the monoid of continuous endomorphisms on ω + 1, and

2. the monoid of stable endomorphisms on (ω + 1) × 2 (where 2 denotes the Sierpinski space)

are GSDT models.

Remark. Refinements of these models have been introduced and studied in [14]. ⊓ ⊔

In GSDT models, an extrinsic characterisation of the well-complete objects is available.

Theorem 2.15 (Extrinsic characterisation of WC). For a GSDT model S, WC(S) is the largest full sub-cartesian reflective exponential ideal of S closed under lifting and such that the reflection of the initial lift-algebra is free.

Proof. We only show that WC(S) is reflective in S. We will use the following: for a locally presentable category C and a set J of maps in it, O(C, J) is reflective in C (see [4, Corollary I.5.4.8]).

Since Grothendieck toposes are locally presentable, it is enough to show that WC(S) = O(S, J_{P}) for some set J_{P}. Indeed, we may take

J_{P} = \{V ↪ U | \begin{matrix}V & ^{>}  → & U \\ I × C & ^{↓ ∩} & ^{>}κ × C → & F × C & ^{↓ ∩} \end{matrix} C ∈ PS\}.

where PS is a set of representatives of the presentable objects in S.

It also follows that WC(S) is locally presentable (see [1, 1.40]). ⊓ ⊔

Remark. Theorem 2.15 does not rely on the rank condition on the lifting functor.

3 Relating ADT and SDT

We relate models of axiomatic and synthetic domain theory. On the one hand, in Subsection 3.1, for every GSDT model S, we establish that WC(S) is a monadic base and that WC(S)_{𝕃} is a KADT model. On the other hand, in Subsection 3.2, for every small monadic base C yielding a KADT model, we show that C̃ is a GSDT model such that its associated monadic base WC(C̃) and KADT model conservatively extend those of C.

Our restriction to small models in Subsection 3.2 should not be a serious one. More generally, one would expect to account for locally small models with a small dense generator [4, Definition I.4.5.4]. And this situation is general enough to cover such traditional categories of domains as Cpo and Cpo_{∧} (the category of small cpos with continuous pullbacks and stable functions), for which one may respectively take the monoids of Example 2.14 as dense generators.

3.1 Restricting SDT models to ADT models

The domains in a GSDT model yield a KADT model.

Theorem 3.1. For a GSDT model S, WC(S) is a monadic base and WC(S)_{𝕃} is a KADT model.

Proof. WC(S) has the required structure by Corollaries 2.9 and 2.10, Theorem 2.7 (2)–(3), and Proposition 2.12; WC(S)^{𝕃} admits tensor products and linear exponentials because it is locally presentable (and hence complete and cocomplete) as so is S^{𝕃} (because S is locally presentable and L has rank — see [4, Proposition II.4.3.6] and [1, 2.78]) and WC(S)^{𝕃} = O(S^{𝕃}, F^{𝕃}J_{P}) where F^{𝕃}J_{P} is the image of J_{P} under the free functor S → S^{𝕃}; finally to see that WC(S)_{𝕃} is WC(S)-algebraically compact, by Theorem 1.13, it suffices to show that WC(S)_{𝕃} has bilimits of ep-sequences. For a quick argument observe that the cocompleteness of WC(S) and the following:

Theorem 3.2. ([8, Theorem 5.3.14]) Let C be a category with a dominance. For a diagram Δ in C, if LΔ has colimit in C then Δ has colimit in C_{𝕃}. ⊓ ⊔

imply that every diagram in WC(S) has colimit in WC(S)_{𝕃}. Then, as epsequences are chains of retractions, every ep-sequence in WC(S)_{𝕃} has sections in WC(S) and hence we are done.

Remark. An argument that relies on the completeness (rather than the cocompleteness) of WC(S) is also available: for every ep-sequence ⟨A_{n} \underrightarrow{↼} A_{n+1}⟩ in WC(S)_{𝕃}, the sequence ⟨L(A_{n} \underrightarrow{↼} A_{n+1})⟩ is an ep-sequence in WC(S) (because L : WC(S)_{𝕃} → WC(S) is WC(S)-enriched) and since ⟨L(A_{n} ↼ A_{n+1})⟩ has limit in WC(S), by the limit/colimit coincidence, ⟨L(A_{n} → A_{n+1})⟩ has colimit in WC(S) and, by Theorem 3.2, ⟨A_{n} → A_{n+1}⟩ has colimit in WC(S)_{𝕃}.

⊓ ⊔

Remark. In the proof of Theorem 3.1, note the use of the Grothendieck assumption on S and the rank assumption on L to guarantee enough completeness and cocompleteness on WC(S), WC(S)^{𝕃} and WC(S)_{𝕃}.

From Theorem 1.13 we further obtain:

Corollary 3.3. For a GSDT model S, WC(S)^{𝕃} is WC(S)-algebraically compact. ⊓ ⊔ 3.2 Extending ADT models to SDT models

We incorporate monadic bases and KADT models to the synthetic setting via Yoneda:

Theorem 3.4 (Conservative-extension theorem). Let C be a small monadic base yielding a KADT model.

1. The Yoneda embedding C ↪ C̃ preserves the initial object, limits, exponentials, the final lift-coalgebra, and the dominance. Moreover,

\begin{aligned}C & ^{⊂} → & C̃ \\ C & \begin{matrix}L \\ ↓ \end{matrix} & ^{⊂} → & C̃ & ^{↓L} \end{aligned}

commutes up to isomorphism.

2. The Yoneda embedding C ↪ C̃ cuts down to an embedding C ↪ WC(C̃).

3. The topos C̃ is a GSDT model; and hence WC(C̃) is a monadic base yielding a KADT model. The embeddings C ↪ WC(C̃) ↪ C̃ preserve the initial object, limits, exponentials, the final lift-coalgebra, and the dominance. Moreover,

\begin{aligned}C & ^{⊂} → & WC(C̃) & ^{⊂} → & C̃ \\ C & \begin{matrix}L \\ ↓ \end{matrix} & ^{⊂} → & WC(C̃) & \begin{matrix}L \\ ↓ \end{matrix} & ^{⊂} → & C̃ & ^{↓L} \end{aligned}

commutes up to isomorphism.

4. The embeddings C ↪ WC(C̃) ↪ C̃ yield embeddings C_{𝕃} ↪ WC(C̃)_{𝕃} ↪ C̃_{𝕃} that preserve partial products and Kleisli exponentials. If a diagram in C_{𝕃} has limit both in C_{𝕃} and WC(C̃)_{𝕃} then the limit in C_{𝕃} is preserved by the embedding C_{𝕃} ↪ WC(C̃)_{𝕃}; such diagrams include the cochains of retractions of standard ep-sequences.

5. For a C-endofunctor F on C_{𝕃} and a WC(C̃)-endofunctor F′ on WC(C̃)_{𝕃} satisfying

\begin{aligned}C_{𝕃} & ^{⊂} → & WC(C̃)_{𝕃} \\ C_{𝕃} & ^{F↓} & ^{⊂} → & WC(C̃)_{𝕃} & ^{↓F′} & , \end{aligned}

a free F -invariant object becomes a free F′-invariant object.

Proof. (1) We only note that the embedding C ↪ C̃ preserves the final liftcoalgebra because, by (2), it is computed as a limit.

(2) By Corollary 2.8 we need only show that every object in C is complete.

Recall that the lifting on C̃ preserves connected colimits (Theorem 1.7 (2)) and hence the cone ⟨ι⟩ : Λ \underrightarrow{.} I is colimiting in C̃. Moreover, writing σ : L\overline{ω} ≅ \overline{ω}

for the inductive fixed-point object, (Λ ^{⟨σ⟩} → \overline{ω}) = (Λ ^{⟨φ^{−1}⟩} → F ≅ \overline{ω}) is colimiting

in C and since (Λ ^{⟨ι⟩}→ I ^{>} ^{κ}→ F) = (Λ ^{⟨φ^{−1}⟩} → F) it follows that every object in C is orthogonal to κ. The result follows from the following equivalences:

∀ D ∈ | C |. D is orthogonal to κ
iff ∀ D ∈ | C |. ∀ C ∈ | C |. D^{C} is orthogonal to κ
iff ∀ D ∈ | C |. ∀ C ∈ | C |. D is orthogonal to κ × C
iff ∀ D ∈ | C |. ∀ P ∈ | C̃ |. D is orthogonal to κ × P

(by Proposition 2.2 (2)

because every presheaf is a colimit of representables)

iff ∀ D ∈ | C |. D is complete

(by Proposition 2.2 (1)).

(3) C̃ is a GSDT model by Theorems 3.4 (1) and 1.7 (2).

(4) We only consider the preservation of limits of diagrams in C_{𝕃} with limits both in C_{𝕃} and WC(C̃)_{𝕃}.

Let D \underrightarrow{.} Δ : G → C_{𝕃} and P \underrightarrow{.} Δ : G → WC(C̃)_{𝕃} be limiting and let D → P be the unique mediating morphism between them. Since the embedding C ↪ WC(C̃) and the forgetful functors C_{𝕃} → C and WC(C̃)_{𝕃} → WC(C̃) preserve limits, it follows that L(D → P) is iso. Finally, as L reflects isos [8, Proposition 3.2.11 (4)], also D → P is iso.

(5) Follows from a generalisation of [8, Theorems 7.1.5 and 7.3.11 (6)] in the context of [28]. ⊓ ⊔

Remark. There is an alternative synthetic viewpoint of domains (à la [17, 36]) via replete objects [16]. In general a conservative-extension result in which domains are taken to be the replete objects (rather than the well-complete ones) is impossible, because embeddings that preserve dominances reflect the property of being a replete object and there are models of ADT in which not every object is replete (e.g. in the category Cpo as recently discovered by Makkai and Rosolini [33], and in the category VPoset_{∧} introduced in [10]).

4 Comments on our approach

This paper is an initial investigation of the relation between axiomatic and synthetic domain theory. For this, we had to restrict both the axiomatic and the synthetic (à la [22, 23]) approaches.

– On the axiomatic side, one may, more generally, work with models arising from an arbitrary commutative monad or even from a monoidal adjunction, and may also work with other models than the Kleisli category (e.g. the category of Eilenberg-Moore algebras). Since the synthetic approach is currently restricted to lifting monads we restricted the axiomatic models to those arising from them.

Concerning the extension of ADT models based on Eilenberg-Moore algebras to SDT models we only have partial results (among which is Corollary 3.3).

– On the synthetic side, the trend has been to investigate realisability models [30, 26, 13, 23] (though see [30, 36, 14]). Here our main means for finding models of ADT within models of SDT (via well-complete objects [23]) is a non-elementary axiom (Axiom 3) that is not satisfied in that setting. In this context it is worth noting our extrinsic characterisation of well-complete objects (Theorem 2.15) which is not known to hold of realisability models.

Therefore reconciling both approaches completely is an open problem.

Acknowledgements. Our approach to SDT has been shaped by ideas of Alex Simpson. Discussions with Martin Hyland and Pino Rosolini were also very helpful. The diagrams were drawn with Paul Taylor’s commutative-diagrams package.

References

1. J. Adámek and J. Rosický: Locally Presentable and Accessible Categories. Cambridge University Press, 1994.

2. P.N. Benton, G.M. Bierman, J.M.E. Hyland, and V.C.V. de Paiva: Linear lambda calculus and categorical models revisited. In E. Börger et al., editor, Selected Papers from Computer Science Logic ’92, volume 702 of Lecture Notes in Computer Science, 1993.

3. G.M. Bierman: What is a categorical model of intuitionistic linear logic? In M. Dezani-Ciancaglini and G.D. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, 1995.

4. F. Borceux: Handbook of Categorical Algebra. Cambridge University Press, 1994.

5. R.L. Crole and A.M. Pitts: New foundations for fixpoint computations: FIXhyperdoctrines and the FIX-logic. Information and Computation, 98:171–210, 1992.

6. B. Day: On closed categories of functors. In G.M. Kelly, editor, Sidney Category Seminar 1972/1973, volume 420 of Lecture Notes in Mathematics, pages 20–54. Springer-Verlag, 1972.

7. S. Eilenberg and G. M. Kelly: Closed categories. In S. Eilenberg, D.K. Harrison, S. MacLane, and H. Rohrl, editors, Proceedings of the Conference on Categorical Algebra. Springer-Verlag, 1966. La Jolla, 1965.

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

9. M.P. Fiore: Enrichment and representation theorems for categories of domains and continuous functions. Available from http://www.dcs.ed.ac.uk/home/mf/ as

rep.dvi, 1996.

10. M.P. Fiore: An enrichment theorem for an axiomatisation of categories of domains and continuous functions. To appear in Mathematical Structures in Computer Science —Proceedings of the Workshop LDPL’95, 1997.

11. M.P. Fiore, A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, and I. Stark: Domains and denotational semantics: History, accomplishments and open problems. In number 59 of Bulletin of the European Association for Theoretical Computer Science, pages 227–256, June 1996.

12. P. Freyd and G.M. Kelly: Categories of continuous functors, I. Journal of Pure and Applied Algebra, 2:169–191, 1972.

13. P.J. Freyd, P. Mulry, G. Rosolini, and D.S. Scott: Extensional PERs. Information and Computation, 98:211–227, 1992.

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

15. P.J. Freyd: Algebraically complete categories. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory, volume 1488 of Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

16. J.M.E. Hyland and E. Moggi: The S-replete construction. In D. Pitt, D. Rydeheard, and P. Johnstone, editors, Proceedings of the 6^{th} International Conference, CTCS’95, volume 953 of Lecture Notes in Computer Science, pages 96–116. Springer-Verlag, 1995.

17. J.M.E. Hyland: First steps in Synthetic Domain Theory. In A. Carboni, M.C. Pedicchio, and G. Rosolini, editors, Category Theory, volume 1488 of Lecture Notes in Mathematics, pages 95–104. Springer-Verlag, 1991.

18. B. Jacobs: Semantics of weakening and contraction. Annals of Pure and Applied Logic, 69:73–106, 1994.

19. M. Jibladze: A presentation of the initial lift-algebra. To appear in the Journal of Pure and Applied Algebra, 1996.

20. A. Kock: Monads on symmetric monoidal closed categories. Arch. Math. (Basel), 21:1–10, 1970.

21. A. Kock: Closed categories generated by commutative monads. J. Austr. Math. Soc., XII:405–424, 1971.

22. J.R. Longley: Realizability Toposes and Language Semantics. PhD thesis, Department of Computer Science, University of Edinburgh, 1995.

23. J.R. Longley and A.K. Simpson: A uniform approach to domain theory in realizability models. To appear in Mathematical Structures in Computer Science — Proceedings of the Workshop LDPL’95, 1997.

24. E. Moggi: Notions of computation and monads. Information and Computation, 93(1):55–92, Jul 1991.

25. P. S. Mulry: Monads and algebras in the semantics of partial data types. Theoretical Computer Science, 99:141–155, 1992.

26. W. Phoa: Effective domains and intrinsic structure. In 5^{th} LICS Conf., pages 366–377. IEEE, Computer Society Press, 1990.

27. G.D. Plotkin: Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School, 1985.

28. G.D. Plotkin: Algebraic completeness and compactness in an enriched setting. Invited lecture given at the Workshop on Logic, Domains, and Programming Languages. Darmstadt, 1995.

29. J. Power and G. Rosolini: Fixpoint operators for domain equations. Available

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

30. G. Rosolini: Continuity and Effectiveness in Topoi. PhD thesis, University of

Oxford, 1986. Available from http://hypatia.dcs.qmw.ac.uk/.

31. G. Rosolini:  Notes on Synthetic Domain Theory.  Available from

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

32. G. Rosolini: Private communication, 1996.

33. G. Rosolini. Studying repleteness in the category of cpos. To appear in Electronic Notes in Theoretical Computer Science —Proceedings of MFPS XIII Conf., 1997.

34. A.K. Simpson: Private communication, 1996.

35. M.B. Smyth and G.D. Plotkin: The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4):761–783, 1982.

36. P. Taylor: The fixed point property in synthetic domain theory. In 6^{th} LICS Conf., pages 152–160. IEEE, Computer Society Press, 1991.