The Fixed Point Property in Synthetic Domain Theory

Paul Taylor

1991

Abstract 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.

1 Axioms

Synthetic Domain Theory is the study of the dictum that domains are sets and all set-theoretic functions between domains are “continuous” or “computable.” Plainly we cannot mean “sets” in the classical sense, so we have have to work in an (elementary) topos E and by a set we mean an object of E. Since we intend to interpret recursion, we assume that E also has a natural numbers object, ℕ.

In a topos, definable subobjects and predicates are classified by an object Ω, which means that any subobject is uniquely expressible as a pullback of {⊤} : 1 → Ω. However not all predicates are computable, i.e. verifiable by a program whose output type includes ⌜tyes⌝ and non-termination: the non-termination predicate on the class of programs is a very important counterexample. Nevertheless, the following clearly are satisfied by the class of semi-decidable predicates:

1. The pullback (inverse image) f^{∗}ϕ of a semi-decidable predicate ϕ along a map f : X → Y is semi-decidable, by the program which first filters its input through f. (We cannot say the same of recursively enumerable subsets without making enumerability assumptions about the types themselves.) Therefore the class is classified by an object Σ, analogous to Ω.

2. Predicates with the same extension we regard as the same, so Σ is in fact a subobject of Ω.

3. By performing side-effect-free tests in succession, the class is closed under finite conjunction or intersection, so Σ is a sub-∧-semilattice.

4. By performing tests in parallel, the class is closed under disjunction or union, so Σ is a sublattice of Ω (including ⊤ and ⊥).

5. Recursively-indexed tests may also be performed in parallel, so Σ ⊂ Ω is closed under ℕindexed joins.

Now consider a map ϕ : Σ → Σ. Postcomposition with this transforms semidecidable predicates X → Σ into others by means of “additional computation” which may make whatever use it sees fit of the result of the first predicate, but not of the data. All that such a transformation can do is

• output some value ϕ(⊥) “anyway”, • and then if it gets some input (i.e. the first predicate has been satisfied), output some

“better” value ϕ(⊤).

Of course ϕ(⊥) ⇒ ϕ(⊤), but what we are saying is that ϕ is uniquely determined by these two values (which may be arbitrary elements of Σ so long as this implication holds). So,

Phoa Principle: Σ^{Σ}, the object of endofunctions of the semi-decidable predicate classifier, is isomorphic to {⟨σ, τ⟩ : σ, τ ∈ Σ, σ ⇒ τ}.

It turns out that this curious axiom is very powerful.

Finally there is a higher-order principle. Any functional Φ : Σ^{ℕ} → Σ which purports to test for universal truth really only tests up to some “large” number.

Scott Principle: For Φ : Σ^{Σ^{ℕ}}, if Φ(λn.⊤) then ∃m.Φ(λn.n < m).

From this axiom we are able to deduce the fixed point property and other basic results of domaintheoretic interest, as we shall show in section 4.

Definition 1.1 A model of synthetic domain theory is a pair (E, Σ), where E is an elementary topos having subobject classifier Ω and a natural numbers object ℕ, and Σ is a subobject of Ω which is closed under finite meets and countable joins and satisfies the Phoa and Scott Principles.

We still have to specify which sets are domains. Clearly we want computational objects X to satisfy the

Weak Leibniz Principle: any two points which satisfy the same semi-decidable predicates are in fact the same.

However this property of terms is insufficient for the fixed point property (it generalises the T_{0} axiom for spaces, whereas we need at least chain-completeness) and we need the analogous (stronger) property for types:

Strong Leibniz Principle: if p : X → Y induces a bijection between semi-decidable predicates, where Y satisfies the Weak Leibniz Principle, then p is an isomorphism.

Finally, for an object to have the fixed point property it must also satisfy

Focality: there is a point ⊥ ∈ X which has no non-trivial semi-decidable property.

Definition 1.2 In a model of synthetic domain theory, a predomain is an object satisfying the Strong Leibniz Principle, and a domain is a focal predomain.

The next section will present the essential results on the weak and strong Leibniz principles, most of which are due to Wesley Phoa and Martin Hyland respectively.

2 Domains

Focality is suggestive of the concept which, in practice, has been primary in classical domain theory, namely the information order. We prefer to regard semi-decidable properties as the primary concept, but the derived notion is very useful:

Definition 2.1 For x, y ∈ X, write x ⊑ y for ∀ϕ ∈ Σ^{X}.ϕ(x) ⇒ ϕ(y).

Exercise 2.2 All functions are monotone with respect to this order, and ⊥, if it exists, is the least element. The Weak Leibniz Principle holds iff the relation is antisymmetric. □

Just as the class of semi-decidable predicates on all objects is obtained by “parallel transport” (using pullbacks) from the generic predicate 1 → Σ, so the order is obtained from ⇒. However it is rather important that if we apply this to objects (such as domains) for which there is already some well-established order relation, then ⊑ must coincide with this relation. For example, • (Σ, ⇒) itself. In particular ⊥ ⊑ ⊤ says that every function ϕ : Σ → Σ satisfies ϕ(⊥) ⇒ ϕ(⊤).

We did explicitly assume this (as part of Phoa’s Principle), but notice that it means that negation does not restrict to Σ; this expresses the insolubility of the Halting Problem.

• On the finite powerset, K(X), ⊑ turns out to be not inclusion, ⊂, but essentially the Egli-Milner order, so the predomain reflection is the Plotkin powerdomain.

• 2 =^{def} 1 + 1 is ⊑-discrete and (in the Effective Topos, at least) Ω is ⊑-indiscrete, so Σ lies strictly between them. One can also show that it is connected, i.e. 2^{Σ} ≅ 2, and does not have arbitrary joins.

• (Σ-)partial functions on ℕ. The lift, ℕ_{⊥}, has the inclusion order (cf. Lemma 3.5) and the function-space (ℕ_{⊥})^{ℕ} has the pointwise order by Proposition 2.13.

Lemma 2.3 ⊑ and ⇒ coincide on Σ, and more generally ⊑ on Σ^{X} is inclusion. Proof Let f, g ∈ Σ^{X}. If f ⊑ g then with ϕ = λh.hx in the definition of ⊑ we have fx ⇒ gx. Conversely, if ∀x.fx ⇒ gx then σ ↦ λx.fx ∨ (σ ∧ gx) defines a (monotone) function Σ → Σ^{X} whose value at ⊥ is f and at ⊤ is g. But ⊥ ⊑ ⊤ so f ⊑ g. □

Another way to reformulate the Weak Leibniz Principle (due to Phoa, who calls such objects Σ-spaces) is to say that the map

ϵ_{X} : X → Σ^{Σ^{X}}  by  x ↦ λf.fx

is mono, which suggests forming the epi-mono factorisation of ϵ_{X}. We shall express the Strong Leibniz Principle in the same way, weakening the notion of epi by considering maps to Σ only (not to all objects) and correspondingly strengthening the notion of mono.

Definition 2.4 p : X → Y is called Σ-epi if it induces a mono Σ^{p} : Σ^{Y} → Σ^{X}. This means that if we are given

[figure: X; p; Y; f; g; Σ]

with p; f = p; g then f = g; this also extends to powers of Σ and, as we shall see, (pre)domains. If Σ^{p} is an isomorphism, so any map X → Σ extends uniquely to a map from Y, we say p is Σ-equable.

Exercise 2.5 If a map is Σ-epi, then it is epi with respect to (maps to) any weakly Leibniz object. □

Lemma 2.6 Any map f : X → Z has a factorisation X → Y_{0} → Z as a Σ-epi followed by a mono which is extremal in the sense that if X → Y → Z is another factorisation of this kind then there is a unique map Y → Y_{0} making the triangles commute. Proof (Sketch) Such factorisations are determined by subobjects of Z. The class of such subobjects is definable in the internal language and can be shown to be closed under (inhabited) unions, so has a greatest member. □

If the Σ-epi part of a map is an isomorphism, we temporarily call the map an extremal mono. After showing that the two classes are closed under composition, it is a standard exercise to prove

Proposition 2.7 Σ-epis and extremal monos form a factorisation system. □

Just as Phoa applied the standard epi-mono factorisation to obtain the Weak Leibniz (Σ-space in his terminology) reflection of X, so we shall now write

[figure: X; p_{X}; SX; e_{X}; Σ^{Σ^{X}}]

for our factorisation of ϵ_{X}.

Lemma 2.8 p_{X} is the extremal Σ-equable map out of X. Proof One can easily show that Σ^{p} : Σ^{Y} → Σ^{X} is split epi iff p : X → Y factors into ϵ_{X}. Hence p is Σ-equable iff it is Σ-epi and factors into ϵ_{X}. The result is then a special case of Lemma 2.6. □

Lemma 2.9 X is a predomain iff ϵ_{X} is an extremal mono. Proof The definition of a predomain (the Strong Leibniz Principle, which Hyland calls Σ-replete) says exactly that it has no nontrivial Σ-equable map out of it, i.e. p_{X} is an isomorphism. □

Corollary 2.10 If Z is a predomain, p : X → Y is Σ-epi and the square

[figure: X; p; Y; Z; ϵ_{Z}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{Σ^{Z}}]

commutes, then there is a unique diagonal fill-in. Proof This is the universality property of a factorisation system. □

Proposition 2.11 p_{X} : X → SX is the unit of the reflection of X into the full subcategory of predomains. Proof We check that SX is a predomain. Since ϵ is natural and p_{X} is Σ-equable the diagram

[figure: SX; ϵ_{SX}; Σ^{Σ^{SX}}; X; p_{X}; ϵ_{X}; Σ^{Σ^{X}}; ≅ Σ^{Σ^{p_{X}}}; e_{X}]

commutes, so the top map is extremal mono because the diagonal is. Corollary 2.10 with p = p_{X} ∗ X → SX now shows that p_{X} is the required unit. □

Further to Corollary 2.10, using the same method as Lemma 2.3, we have

Lemma 2.12 If x ⊑ y in a predomain X then there is a unique function h∗Σ → X with h(⊥) = x and h(⊤) = y. □

We note without proof (since these facts are not directly relevant to our interest in the Fixed Point Property) that:

1. the full subcategory of predomains is the smallest (full, replete) reflective subcategory containing Σ.

2. the reflection preserves focality, and lifting preserves both Leibniz principles.

3. the reflection preserves finite products, and taking the product with an object preserves Σ-epis.

4. the category of (pre)domains is an exponential ideal (i.e. if X is a (pre)domain and Y is arbitrary then X^{Y} remains a (pre)domain).

We shall, however, need the

Proposition 2.13 (Phoa) The order on limits and exponentials of predomains is pointwise. Proof Apply Lemma 2.12 to each component; by uniqueness we have a cone or function, and hence a map from Σ to the limit or exponential. □

The full subcategories of objects satisfying either Leibniz principle and/or focality are in fact relatively cartesian closed. We cannot interpret second order polymorphism without additional axioms which would exclude the simple sheaf models.

3 Ordinals

In order to study chain-completeness we need to consider the domain whose definable points form an increasing sequence of order-type ω + 1. Before we can do this we need a good grasp of the corresponding finite domains of which this is the (bi)limit.

Adopting a standard convention,

n =^{def} {0, 1, 2, …, n − 1}

which, although it is a discrete object (simply the n-fold coproduct of copies of the terminal object), we shall consider to have “the usual order” in the sense that monotone and antitone functions f : n → Σ are defined in the obvious way, namely ∀r.f(r) ⇒ f(r + 1) and ∀r.f(r + 1) ⇒ f(r) respectively.

Notation 3.1 Let ˜0 =^{def} 0, and { \atop n + 1} be the set of antitone sequences n → Σ; these objects will be called (finite) ordinals. Note that g ∈ ñ is defined by g(0), …, g(n − 2). The particular antitone functions

\overline{r} =^{def} (λi.i < r)

will be called numerals.

Lemma 3.2 n → ñ is Σ-epi. Proof (Sketch) It is a retract of 2^{n−1} → Σ^{n−1}, which is Σ-epi by Phoa’s Principle. □

Proposition 3.3 Any function n → Σ which is monotone in the ad hoc sense which we have used extends uniquely to a function ñ → Σ (which is automatically monotone in the intrinsic (⊑) sense)

Proof Let f ∈ { \atop n + 1}, g ∈ ñ and consider

ϕ(f, g) =^{def} f(0) ∧ ⋀_{i=1}^{n−1} [f(i) ∨ g(n − 1 − i)]

Then λg.ϕ(f, g) ∈ Σñ maps to f ∈ { \atop n + 1}. We have already shown that this must be unique. □ In other words, { \atop n + 1} ≅ Σñ, and under this isomorphism,

\overline{0} ↦ λg.⊥
\overline{r + 1} ↦ λg.g(n − 1 − r)
\overline{n} ↦ λg.⊤

Redefining the ordinals as ˜0 = ∅, ˜1 = 1, ˜2 = Σ, ˜3 = Σ^{Σ}, ˜4 = Σ^{Σ^{Σ}} and so on, the numerals are

\overline{r} = λx_{0}.x_{0}(λx_{1}.x_{1}(⋯ (λx_{r−1}.x_{r−1}(λx_{r}.⊥)) ⋯))
\overline{n − 1 − r} =
λx_{0}.x_{0}(λx_{1}.x_{1}(⋯ (λx_{r−1}.x_{r−1}(λx_{r}.⊤)) ⋯))

where 0 ≤ r ≤ \frac{n}{2} − 1. In the case of n = 2m + 1, the middle numeral \overline{m} is an exception:

λx_{0}.x_{0}(λx_{1}.x_{1}(⋯ (λx_{m−2}.x_{m−2}(λx_{m−1}.x_{m−1})) ⋯))

In all of these formulae, the type of x_{i} is (n − 2i − 1)^{∼}.

There is a third way to express finite ordinals. Recall that X_{⊥}, the lift or Σ-partial map classifier is given by the set of q ∈ Ω^{X} which have at most one element (i.e. ∀x_{1}, x_{2} ∈ q.x_{1} = x_{2}) and whose inhabitation is a Σ-predicate (i.e. ∀x ∈ X.(x ∈ q) ∈ Σ).

Lemma 3.4 { \atop n + 1} ≅ ñ_{⊥} with \overline{0} ↦ ∅ and \overline{r + 1} ↦ \{\overline{r}\}, where f ∈ { \atop n + 1} is associated with q ⊂ ñ by

f ↦ {g ∈ ñ : f(0) ∧ ⋀_{i=0}^{n−2}[g(i) = f(i + 1)]}

q ↦ λi. \{ \begin{matrix}∃g ∈ ñ.g ∈ q & if i = 0 \\ ∃g ∈ ñ.g ∈ q ∧ g(i − 1) & otherwise \end{matrix}

In this representation the ordinals become ˜0 = ∅, ˜1 = ∅_{⊥}, ˜2 = ∅_{⊥⊥} etc. and the numerals \overline{0} = ∅, \overline{1} = \{∅\}, \overline{2} = \{\{∅\}\}, etc. □

Lemma 3.5 The order relation f ⊑ g on { \atop n + 1} is as follows:

• as antitone functions n → Σ, pointwise,

∀i ∈ n.f(i) ⇒ g(i)

• as predicates on ñ, pointwise, i.e.

∀p ∈ ñ.f(p) ⇒ g(p)

• as partial elements of ñ, according to the lower or Hoare order f ⊑^{♭} g,

∀f_{1} ∈ f.∃g_{1} ∈ g.f_{1} ⊑ g_{1}

• as iterated partial elements,

∀f_{1} ∈ f.∃g_{1} ∈ g. … ∀f_{n} ∈ f_{n−1}.∃g_{n} ∈ g_{n−1}.⊤
□

Our use of numbers n in the elementary topos E may be interpreted to have been external so far, but the aim is to form their limit; to define this internally in the topos requires the existence of the natural numbers object, ℕ.

Definition 3.6 The standard diagram is defined by

[figure: \overline{3}; ⋯]

[figure: \overline{2}; \overline{2}; ⋯]

[figure: \overline{1}; \overline{1}; \overline{1}; ⋯]

[figure: \overline{0}; \overline{0}; \overline{0}; \overline{0}; ⋯]
[figure: ˜1; ◁; ˜2; ◁; ˜3; ◁; ˜4; ◁; ⋯]

f ∈ ñ ↦ λj. \{ \begin{matrix}f(j) & 0 ≤ j ≤ n − 2 \\ f(n − 2) & j = n − 1 \end{matrix}
λi.g(i) ← g ∈ { \atop n + 1}

The colimit of the embeddings in this diagram in the category of (pre)domains is called ω̃.

Lemma 3.7 Let X be a predomain. Then every monotone sequence f : n → X (or f : ℕ → X) extends uniquely to a map g : ñ → X (respectively g : ω̃ → X) with ∀n.g(\overline{n}) = f(n).

Proof The map n → X → Σ^{Σ^{X}} extends uniquely to a map from ñ by Proposition 3.3.

[figure: n; ñ; X; ϵ_{X}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{Σ^{X}}; . . . . . . . . . . . . . . . .]

Then since n → ñ is Σ-epi this factors through X by Corollary 2.10. For the infinite case, restriction to initial segments defines (using uniqueness) a cocone on the standard diagram and hence a map from the colimit. □

Corollary 3.8 Σω̃ ≅ Anti(ℕ, Σ), the object of monotone sequences ℕ → Σ. □

Proposition 3.9 The limit of the diagram of projections is Anti(ℕ, Σ), the object of antitone sequences ℕ → Σ. The order is pointwise and has a top element, \overline{ω} = (λn.⊤). Proof The projections are just restriction to initial segments. The order is pointwise by Proposition 2.13. □

4 The Fixed Point Property

Everybody knows that in the category of chain-complete posets with ⊥ and functions preserving joins of chains, every endofunction of an object has a least fixed point. Moreover almost everybody knows that for sequences of embedding-projection pairs (such as in the previous section) in this category, the limit of the projections is isomorphic to the colimit of the embeddings, and that this result is the basis of the iterative solution of recursive domain equations. In this section we shall show that these three properties are all equivalent to Scott’s Principle.

Lemma 4.1 There is a unique map ω̃ → Anti(ℕ, Σ) which preserves the numerals. There is also a unique endofunction of each of these objects which acts as the successor on the numerals; as an endofunction of Anti(ℕ, Σ) it has a unique fixed point, namely the top element \overline{ω} = λn.⊤. Proof Examples of Lemma 3.7. □

As well as the standard diagram, it is convenient to consider the augmented standard diagram, in which each domain has an additional top element (+) and these are preserved by the embeddings and projections; we shall write ω^{+} for its colimit. The definable points of the limit of course have order-type ω +2, and similar results hold for ω^{+} as for ω̃. In particular, just as Lemma 3.7 allowed us to extend a monotone sequence f : ℕ → X to a function g : ω̃ → X, so if we also have a bound x for the sequence, there is a unique function g : ω^{+} → X which also has g(+) = x.

Lemma 4.2 Suppose that the successor function s : ω̃ → ω̃ has a fixed point, ∞. Then

• ∀n.\overline{n} ⊑ ∞ in ω̃.

• the image of ∞ in Anti(ℕ, Σ) is ⊤ = \overline{ω} and in ω^{+} (which we also call ∞) lies below +.

• If g is the extension of some sequence f as in Lemma 3.7, then g(∞) is the least upper bound.

• least upper bounds of monotone sequences are preserved by all functions between predo-

mains. Proof The first part is an easy induction. For the second, the image of a fixed point of the successor on ω̃ must be the unique fixed point of the successor on Anti(ℕ, Σ). Then f(n) = g(\overline{n}) ⊑ g(∞) by monotonicity, and for the same reason g(∞) ⊑ g(+) = x for any upper bound x. Finally if h : X → Y is any map between predomains, by uniqueness the extension of f ; h must be g ; h and in particular h preserves the least upper bound. □

Corollary 4.3 If s : ω̃ → ω̃ has a fixed point then (Σ has countable joins and) Scott’s Principle holds. Proof Any functional Φ : Σ^{ℕ} → Σ preserves the directed join \overline{ω} = ⋁ ; \overline{n} in Anti(ℕ, Σ) ⊂ Σ^{ℕ}. □

Proposition 4.4 If Scott’s Principle holds then ω̃ ≅ Anti(ℕ, Σ). Proof Since ω̃ is defined as a predomain reflection, it suffices to show that associating f ∈ Anti(ℕ, Σ) ≅ Σω̃ with F ∈ Σ^{Anti(ℕ,Σ)} by

F ↦ λn.F (\overline{n})
f ↦ λg.f(0) ∨ ∃n.f(n + 1) ∧ g(n)

gives an isomorphism. But f ↦ F ↦ f gives

f ↦ λm.f(0) ∨ ∃n.f(n + 1) ∧ n < m
≡ λm.f(m) ≡ f

The other way, we have to show that, for all F : Anti(ℕ, Σ) → Σ and g ∈ Anti(ℕ, Σ),

F g ⟺ F (\overline{0}) ∨ ∃n.(F (\overline{n + 1}) ∧ g(n))

where [⇐] follows easily from the fact that g(n) ≡ (\overline{n + 1} ⊑ g).

Consider first the corresponding finite problem for given m ∈ ℕ:

F g′ ⟺ F \overline{0} ∨ ⋁_{n<m} F (\overline{n + 1}) ∧ g′(n)

for g′ ∈ m̃. This clearly holds if g′ is a numeral, and hence in general since both sides are Σ-predicates and m → m̃ is Σ-epi (cf. Proposition 3.3).

We can reduce the infinite problem to this using Scott’s Principle: consider

Φ =^{def} λh : Σ^{ℕ}.F (λn.gn ∧ hn)

then F g ≡ Φ\overline{ω} ⇒ ∃m.Φ\overline{m}. This means that for some m, F g ≡ F g′ holds, where

g′ =^{def} λn. \{ \begin{matrix}gn & if n < m \\ ⊥ & otherwise \end{matrix}

but we have shown that the result is valid in this case. □

Theorem 4.5 Assuming Phoa’s Principle, the following are equivalent:

[LCC] The limit-colimit coincidence for sequences of embedding-projection pairs in the category of (pre)domains.

[FP] Every endofunction of a domain has a least fixed point.

[DC] Every (pre)domain is chain-complete and every function between (pre)domains preserves joins of chains.

[SP] Scott’s Principle holds. Proof The general implications [DC]⇒[LCC] and [DC]⇒[FP] are well known. We have just shown that [SP] implies [LCC] for the standard diagram, which trivially implies [FP] for ω̃. By Lemma 4.2, [FP] for ω̃ implies [DC] in general, and [SP] is a special case of this. □

5 Models

It will be obvious to the reader that the intellectual (though not the logical) reliance of this paper on the work of Hyland, Rosolini and Phoa is very heavy. Giuseppe Rosolini was the first to study the object Σ in detail, concretely as the class of termination predicates

{ϕ : ∃n.ϕ ↔ {n}(n)↓}

in the Effective Topos and abstractly as a dominance. Phoa developed the domain theory of complete Σ-spaces based on this. However for the benefit of those interested in classical (“cpo”) domain theory, we shall conclude by presenting a scheme of sheaf models in which classical categories of domains can be embedded. In essence these date back to Scott’s earliest work on denotational semantics.

Recall that the slogan of synthetic domain theory is that “domains are sets,” and a very old result in category theory known as the Yoneda Lemma gives us this directly. If C is any small category then the functor category Set^{C^{op}} is a topos, which is to say a “category of sets,” and C is fully embedded in it (the images of the objects are called representables). In other words, we specify some objects we want to call sets, together with (all) the functions between them, and lo and behold we have a category of sets including the given ones. Moreover any products (indeed limits) and exponentials which exist in C are preserved.

The most elementary application of this to domain theory is to refute the non-existence of set-theoretic models of the untyped λ-calculus. If we have some combinatory or topological model Λ with endomorphism monoid M (a category with one object, which we may as well call Λ), then the topos Set^{M^{op}} has an object, (the image of) Λ, with Λ^{Λ} ◁ Λ or, for a λη-model, Λ^{Λ} ≅ Λ.

Functor-category (presheaf) models like this in fact already provide models of synthetic domain theory, albeit littered with ¬¬ signs throughout the definitions and results: take Λ to be any topological model such as Scott’s P ω or D_{∞}, and Σ(Λ) to be its Scott topology with the obvious M-action. This construction is nothing more than the natural continuation of the category of retracts construction in [S76], where in addition to retracts, products and exponentials we have other set-theoretic structure such as equalisers, colimits and powersets.

[Although we do not appear to be using the topological structure, the method is not immediately applicable to term models or simply the monoid of partial recursive functions on ℕ. The reason for this is that the natural numbers object in the topos (which in the latter case is called after Phil Mulry) is essentially the same as in the outside world and so admits non-recursive (or non-λ-definable) functions. It is necessary to replace ℕ in our axiomatisation with an object N which has similar but weaker inductive properties.]

In order to eliminate the double negations, we have to impose a Grothendieck topology; for the definitions and elementary results the reader is referred to any of the topos-theoretic books in the bibliography. The minimal and maximal topologies in the conditions which follow are known as the countable open cover and canonical topologies.

Definition 5.1 A Scott site is a small full subcategory C of either the category of topological spaces and continuous maps or of the category of locales, together with a Grothendieck topology J on C satisfying for each X ∈ C:

1. the Tychonov product X × P ω is a retract (quâ space or locale) of some object of C.

2. For U, V ⊂ X open, if

∀Y →^{f} X in C. f^{∗}U = Y ⇒ f^{∗}V = Y

then U ⊂ V.

3. For U = ⋃_{i∈I} U_{i} ⊂ X a countable union of opens, the sieve

R = {Y →^{f} X in C : ∃i ∈ I.f^{∗}U_{i} = f^{∗}U}

J-covers X.

4. Every covering sieve is colimiting for the biggest diagram in C for which it is a cocone.

The corresponding Scott topos is E = Shv(C, J) and the Scott model is (E, Σ), where Σ(X) is the open-set lattice of X. The choice of the open-set lattice is precisely Scott’s thesis, that a map is “computable” iff it is continuous.

Examples 5.2

• Let Λ be a topological model of the λ-calculus, i.e. a locally compact T_{0} but not T_{1} space or locale for which Λ^{Λ} (with the compact-open topology) is a retract of Λ, e.g. any of the well-known domain models, and C = {Λ}.

• Let C be any small cartesian closed category of cpos, such as countably based Scott domains or SFP.

Then with the (countable) open cover topology or the canonical topology we have a Scott model.

Theorem 5.3 (Shv(C, J), Σ) is a model of synthetic domain theory containing C. Proof We shall just sketch the relevance of the conditions, assuming (without loss of generality) that C is closed under retracts and includes some pointed space, so that P ω and the Sierpiński space (which represents Σ) are objects.

1. In order to prove Scott’s principle we need to show something about any

Φ ∈ E(X, Σ^{Σ^{X}}) ≅ E(X × P ω, Σ) ≅ Σ(X × P ω)

namely that, being an open set containing U × \{ω\}, it is of the form ⋃_{n} U_{n} × ↑ \overline{n}. Phoa’s principle is even simpler: any

ϕ ∈ E(X, Σ^{Σ}) ≅ Σ(X × Σ)

must be (ϕ(⊥) × Σ) ∪ (ϕ(⊤) × {⊤}).

2. This is precisely what we need to ensure that Σ → Ω is mono; the condition holds automatically for spaces or for a category closed under open sublocales.

3. Σ-predicates correspond to open sets, and this condition ensures that countable unions of such subobjects are given by unions of open sets.

4. The final condition is precisely what is required to make all the representables (in particular Σ, which is the Sierpiński space), sheaves. □

Conclusion

Having made this construction we can compare the Leibniz principles and other synthetic concepts with classical ones such as T_{0}, sobriety and so on. In doing so we must be careful to distinguish between external or global properties, and internal or local ones whose values are generalised elements of Ω; for this reason it is inappropriate to make formal statements here. Let us just say that, in an appropriate sense and with mild additional assumptions (e.g. C has binary products), ⊑ does correspond to the specialisation order, the Leibniz principles correspond to T_{0} and sobriety, and products and function-spaces are preserved.

Hence the major contructs of domain theory — interpreting the λ-calculus, fixed points, domain equations and, indeed, powerdomains — remain intact. It is not difficult to see, for example, that the interpretations of (definable) data types will always be bifinite, and there is much more of the large body of classical intuition and construction which can be brought across.

My personal view is that the study of domain theory by bit-picking should be brought to a close. The advantage of the category of predomains of a model of synthetic domain theory is that it is complete and cocomplete, which no classical category of predomains apart from CPO is. It also admits any set-theoretical constructions (such as the finite powerset), so long as these are followed by the reflection functor.

The relevance of the Scott toposes is that we can begin to see how to reformulate synthetically the good intuitions of denotational semantics (which derive from Scott’s thesis) and thereby reapply them to the effective models, replacing continuity with recursion.

Bibliography

[B] J.L. Bell, Toposes and local set theories, Oxford logic guides 14, Oxford University Press, 1988.

[F] M.P. Fourman, The Logic of Topoi, in: J. Barwise, ed., Handbook of Mathematical Logic, North-Holland, 1977, 1053–1090.

[HS] R. Hindley and J. Seldin, eds., To H.B. Curry: essays in combinatory logic, lambda calculus and formalisms, Academic Press, 1980

[H82] J.M.E. Hyland, The effective topos, in: A.S. Troelstra & D. van Dalen,, eds., Brouwer centenary symposium, North Holland, 1982.

[HJP] J.M.E. Hyland, P.T. Johnstone and A.M. Pitts, Tripos theory, Proc. Camb. Philos. Soc. 88 (1980) 205–232.

[J77] P.T. Johnstone, Topos Theory, Academic Press, 1977.

[K] A. Kock, Synthetic differential geometry, LMS lecture notes, Cambridge University Press, 1981.

[L] J. Lambek, From λ-calculus to cartesian closed categories, in: Hindley & Seldin.

[LS] J. Lambek and P.J. Scott, Introduction to higher order categorical logic, Cambridge studies in advanced mathematics 7, Cambridge University Press, 1986.

[MR] M. Makkai and G. Reyes, First order categorical logic, Lecture notes in Mathematics 611, Springer, 1977.

[PS] M.B. Smyth and G.D. Plotkin, The Categorical Solution of Recursive Domain Equations, Dept. Artif. Intell. Research Report 60 (1978), Univ. Edinburgh.

[P90] W.K.-S. Phoa, Effective Domains and Intrinsic Structure, in: Logic in Computer Science (Philadelphia, 1990), IEEE Computer Society Press, 366–378.

[PT] W.K.-S. Phoa and P. Taylor, The Synthetic Plotkin Powerdomain, in preparation.

[R86] G. Rosolini, Continuity and effectiveness in topoi, Ph. D. thesis, Carnegie-Mellon University, 1986.

[R87] G. Rosolini, Categories and effective computation, in: D. Pitt, ed., Category Theory and Computer Science (Edinburgh, 1987), Lecture Notes In Computer Science 240, Springer, 1987.

[S80] D.S. Scott, Relating theories of the λ-calculus, in Hindley & Seldin.

[S76] D.S. Scott, Data types as lattices, SIAM J. Comput. 5 (1986) 522–587

[T87] P. Taylor, Homomorphisms, bilimits and saturated domains — some very basic domain theory, Manuscript, 1987.

Acknowledgements

The author is supported by • (UK) SERC project GR/E 80626, Foundational Structures in Computer Science, and

• (EC) Esprit project BRA 3003, Categorical Logic in Computer Science and is also deeply indebted to Martin Hyland for many discussions of this work.