An Axiomatisation of Computationally Adequate Domain Theoretic Models of FPC

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

<mf@dcs.ed.ac.uk>      <gdp@dcs.ed.ac.uk>

April 1994

Synopsis

Categorical models of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types) are defined. Then, domain-theoretic models of FPC are axiomatised and a wide subclass of them —the non-trivial and absolute ones— are proved to be both computationally sound and adequate.

Examples include: the category of cpos and partial continuous functions and functor categories over it.

1 Introduction

This paper is an investigation into axiomatic categorical domain theory as needed for the denotational semantics of deterministic programming languages. We particularly consider a metalanguage FPC, a typed functional language with sums, products, exponentials and recursive types equipped with a call-by-value operational semantics (see [Plo85, Gun92]). We wish to axiomatise domain-theoretic models of FPC and prove that they provide a computationally sound and adequate denotational semantics.

Such a theorem holds for pCpo [Plo85], the category of small cpos (posets, possibly without bottom, closed under lubs of ω-chains) and partial continuous functions. The aim of this paper is to generalise to a wide class of order-enriched categories (Section 2); one can compare this endeavour to [SP82, Fre90, Fre92] where a similar programme was carried out for the solution of recursive domain equations.

In order to provide a direct semantic treatment of non-termination, we consider order-enriched categories of partial maps (Section 3). Computational soundness for FPC is then that if the evaluation of a program terminates its denotation is total; adequacy is the converse implication. Here programs are taken to be closed terms of any closed type.

The categorical structure needed for interpreting the type constructors of FPC is discussed (Section 4) in the order-enriched setting. A uniform treatment of type constructors with mixed variance is provided by transforming them into covariant type constructors on universal involutory categories (those that are self-dual via an involution). One can then interpret recursive types (Section 5) following [Fre91] and using a notion of parameterised algebraic compactness.

Categorical models of FPC are defined to be parameterised algebraically compact partial cartesian closed categories with finite coproducts; they enable a denotational semantics to be given (Section 6). Abstract examples of categorical models are provided by domain-theoretic models; the leading example of such a model is —naturally— pCpo. These models are specified by order-theoretic conditions intended to be easy to verify.

The main technical contribution of the paper (Section 7) is that non-trivial domain-theoretic models of FPC satisfying an absoluteness axiom are computationally sound and adequate.

It follows that the domain-theoretic model specified by pCpo —as well as many full subcategories of domains— is computationally adequate. Other examples are functor categories over pCpo. Categories of stable functions may provide further models as may synthetic domain theory [Tay91] —though internally in a topos.

∗Research partially supported by Fundación Antorchas and The British Council grant ARG 2281/14/6 and SERC grant RR30735.

†Research supported by an SERC Senior Fellowship.

Our proof of adequacy depends on certain formalapproximation relations between semantic and syntactic values (see Subsection 7.2). Lemma 7.11 identifies the essential properties needed to prove their existence. Recently, a new method of proof has been proposed by Pitts [Pit93] in the context of Cppo_{⊥} (the category of small pointed cpos and strict continuous functions). We hope his approach will extend to our axiomatic setting. We also wonder whether there is an abstract version of Abramsky’s approach to adequacy via Stone duality [Abr90].

We have taken both partiality and order as primitive notions. An attractive alternate possibility would be to take partiality as the sole primitive notion. In Section 3 a definition of the order in terms of totality is proposed. It would be interesting to find natural axioms on partiality which would yield an (absolute) domain-theoretic model. Such axioms would provide a computational justification of Scott’s original consideration of ordered structures. (For an initial investigation in this direction see [Fio94].) A related possibility is to generalise from order-enrichment to general enrichment. The first problem there is to provide a good notion of V-domain-structure; any V-category with such a structure should yield a V-category of partial maps. As to adequacy, we believe that if Lemma 7.11 generalises to arbitrary cartesian V, the formal-approximation relations can be extracted.

It seems that so straightforward an adequacy theorem would not be available if one instead axiomatised Cppo (the category of small pointed cpos and continuous functions) —see [MC88]. The essential difficulty is that the least element does not correspond to non-termination at higher types. Again, although pCpo is equivalent to Cppo_{⊥} they are conceptually different. The first seems computationally more natural, fitting with standard formulations of recursion theory that emphasise partial functions. The latter has a natural generalisation to models of intuitionistic linear type theory with recursion [Plo93]; the connection with operational notions is unclear.

It would be interesting to make abstract categorical studies of other notions of computation, for example nondeterminism or probabilistic computation. There behaviour concerns more than termination and semantics more than existence and one should extend the metalanguage, e.g. with a construct for (probabilistic) choice. One might even investigate notions of computation in general. Semantical suggestions have been made: Moggi has proposed the use of Kleisli categories [Mog89]; models of linear type theory with recursion form another possibility. However, a correspondingly general view of behaviour is completely lacking.

2 Order-enriched category theory

For a thorough treatment of enriched category theory consult [Kel82]. In the rest of the paper we let V stand for either Poset (the category of small posets and monotone functions) or Cpo (the category of small cpos and continuous functions). But we stress that all our V-notions with their associated results generalise to arbitrary cartesian V (see [Fio94]).

A Poset-category (Cpo-category) is a locally small category whose hom-sets come equipped with a partial order (complete partial order) with respect to which composition of morphisms is a monotone (continuous) operation.

Both Poset and Cpo with each hom-set ordered pointwise are examples of Poset-categories; Cpo is even a Cpo-category.

The terminal V-category 1 has a singleton set of objects while the only hom is the terminal object in V. The product, A × B, of the V-categories A and B, is the V-category with | A × B | = | A | × | B |, and homs defined as

(A × B)((A, B), (A′, B′)) = A(A, A′) × B(B, B′).

For a V-category A its dual, A^{op}, is the V-category with the same objects as A, but with A^{op}(A, A′) = A(A′, A). Notice that the order in each hom remains unchanged.

A V-functor F : A → B between V-categories A and B, consists of a mapping associating every A ∈ | A | with some F A ∈ | B | and a functorial mapping associating every A, A′ ∈ | A | with some F_{A,A′} : A(A, A′) → B(F A, F A′) in V. An ordinary functor F : A → B is said to V-enrich if for every A, A′ ∈ | A |, the function F_{A,A′} is in V.

A V-adjunction χ : F ⊣ U : A → B is given by V-categories A and B, V-functors F : B → A and U : A → B, and a natural isomorphism

χ : A(F , ) ≅ B( , U ) : B^{op} × A → V.

A Poset-adjunction involving Cpo-categories establishes a Cpo-adjunction because the inclusion functor Cpo → Poset creates isomorphisms.

3 Partial maps

For a thorough survey of categories of partial maps consult [RR88].

Definition 3.1 [Mog86, Ros86] A domain structure is a pair (K, D) consisting of a category K and a wellpowered category D, such that D is a full-on-objects subcategory of K all of whose morphisms are monos in K, with the following closure property: every diagram X ⟶^{f} A ↢^{n} D with f ∈ K and n ∈ D has a pullback in

K and if X ↢^{f^{−1}(n)} f^{−1}(D) ⟶^{n^{∗}f} D is any such pullback then f^{−1}(n) ∈ D. □

Convention. K is called the category of total maps, and D is called the category of admissible monos. For every A ∈ | D |, we write D(A) for the representative small set of subobjects of A in D guaranteed by wellpowerness.

Definition 3.2 The category of partial maps p(K, D) induced by a domain structure (K, D) has the same objects as K; a partial map [m, f] : A ⇀ B is an equivalence class of spans A ↢^{m} D ⟶^{f} B in D × K, where two spans A ↢^{m} D ⟶^{f} B and A ↢^{n} E ⟶^{g} B are equivalent iff m = n ∘ i and f = g ∘ i for some isomorphism i : D ≅ E. Composition of partial maps is given as for relations, by pullback; identities have the form [id_{A}, id_{A}]. □

Convention. When D is clear from the context we simply write pK.

K appears as a full-on-objects subcategory of pK via the faithful inclusion functor J : K → pK sending a total map f to the partial map [id, f]. To indicate that a partial map u is total (i.e. it is in the image of J) we write u ↓.

The motivating example of a domain structure is (Cpo, Σ) where Σ is the subcategory of Cpo consisting of all those order-reflecting monos whose subobjects are Scott-open. We have: p(Cpo, Σ) ≅ pCpo.

We now consider the interaction of partiality and order-enrichment.

Definition 3.3 Given a domain structure (K, D) and a Poset-enrichment ⊑ for K, we define a partial order ⊏ ∼_{A,B} on every pK(A, B) by setting u ⊏ ∼_{A,B} v iff for every x : X → A,

u ∘ x ↓ ⇒ (v ∘ x ↓ ∧ u ∘ x ⊑_{X,B} v ∘ x). □

Proposition 3.4 For every [m, f], [n, g] : A ⇀ B,

[m, f] ⊏ ∼ [n, g] ⟺ m = n ∘ i ∧ f ⊑ g ∘ i for unique i.□

See [Fio93] for characterisations of when categories of partial maps induced by arbitrary domain structures or uniform domain structures (in the sense of the definition below) respectively Poset-enrich or Cpoenrich with respect to ⊏ ∼ .

Definition 3.5 A domain structure (K, D) is said to be uniform if whenever ⟨[m_{k}]⟩ is an ω-chain in D(A) with lub [m], where m_{k} : D_{k} ↣ A and m : D ↣ A, it follows that μ : ⟨D_{k}, m_{k+1}^{−1}(m_{k})⟩ \underrightarrow{.} D is colimiting in K where μ_{k} = m^{−1}(m_{k}). □

The explicit distinction between partial and total maps can be used to define a contextual approximation preorder: for u, v : A ⇀ B,

u ⊏ ∼^{c} v ⟺ ∀ context C[ ] in pK. C[u] ↓ ⇒ C[v] ↓

where a context is an incomplete composite w ∘ ∘ x. The description of partial maps based on domain structures provides another computationally natural notion of approximation. For this purpose, admissible monos are regarded as predicates describing observable properties. The specialisation preorder for partial maps is defined as follows:

u ⊏ ∼^{s} v : A ⇀ B in pK

⟺

u^{−1}( ) ⊆ v^{−1}( ) : D(B) → D(A) in Poset

where the inverse image of [n] under [m, f] is [m ∘ f^{−1}(n)].

The notions of approximation obtained by testing and by observing partial maps coincide. Writing ⊏ ∼ for either of them and ⊑ for the restriction to total maps, it can be shown that if ⊑ is a partial order (as in Cpo) then ⊏ ∼ arises from ⊑ as in the more general situation considered in Definition 3.3. (For details see [Fio94].)

4 Type constructors

4.1 Binary partial products

Let K have binary products. The partial pairing of u = [m, f] : B ⇀ A_{1} and v = [n, g] : B ⇀ A_{2} is the partial map B ⇀ A_{1} × A_{2} defined by

⟨⟨u, v⟩⟩ = [m ∩ n, ⟨f ∘ m^{−1}(n), g ∘ n^{−1}(m)⟩]

where ⟨ , ⟩ is the pairing of total maps. The product functor × : K×K → K extends to a partial product functor ⊗ : pK×pK → pK sending a pair of objects (A, B) to A × B and a pair of partial maps (u, v) to ⟨⟨u ∘ π_{1}, v ∘ π_{2}⟩⟩.

Proposition 4.1 Let (K, ⊑) and (pK, ⊏ ∼ ) be Posetcategories. If K has binary Poset-products then ⊗ Poset-enriches. □

4.2 Partial exponentials

As usual for higher types, exponentiation arises as right adjoint to multiplication. In our case, we let K have binary products and for every A ∈ | K |, we ask that pλ : ⊗A ⊣ A⇀ ⇀ : pK → K is an adjunction. We write ε for the counit of this adjunction and call each A⇀ ⇀B a partial-exponential. Partial-exponentials extend to a functor ⇀ ⇀ : pK^{op} × pK → pK sending pairs of objects (A, B) to A⇀ ⇀B and pairs of partial maps (u, v) to pλ(v ∘ ε ∘ (id ⊗ u)).

Definition 4.2 [LM84] A category of partial maps pK is partial cartesian closed if K is cartesian and pK has partial exponentials. □

Proposition 4.3 Let (K, D) be a uniform domain structure and let ⊑ be a Cpo-enrichment for K such that (pK, ⊏ ∼ ) is a Cpo-category. Assume pK is partial cartesian closed. If × : K × K → K Cpo-enriches then so does ⊗ : pK × pK → pK. □

Proposition 4.4 Let (K, ⊑) and (pK, ⊏ ∼ ) be Posetcategories. Assume K has binary Poset-products. If pλ determines a Poset-adjunction then ⇀ ⇀ Posetenriches.

Moreover, whenever (K, ⊑) and (pK, ⊏ ∼ ) are Cpocategories, if ⊗ Cpo-enriches then so does ⇀ ⇀ .

□

4.3 Colimits

Proposition 4.5 Let J ⊣ L : (pK, ⊏ ∼ ) → (K, ⊑) be a Poset-adjunction.

1. If K has binary Poset-coproducts then so does pK.

2. Assuming K has a terminal object, if K has colimits of ω-chains of embeddings then so does pK.□

4.4 Involutory categories

Following a suggestion of John Power, we focus on involutory categories (those that are self-dual via an involution). This enables us to transform mixedvariance functors into covariant ones in a universal way.

Definition 4.6 The large category InvCAT of involutory locally small categories has objects (C, ( )^{c}) where C ∈ | CAT | and ( )^{c} : C → C^{op} is an involution; a morphism F : (A, ( )^{a}) → (B, ( )^{b}) is a functor F : A → B such that F^{op} ∘ ( )^{a} = ( )^{b} ∘ F; and composition and identities as in CAT. □

Examples of involutory categories abound: for every C ∈ | CAT |, (C̆, ( )^{§}) = (C^{op} × C, ⟨Π_{2}, Π_{1}⟩) is involutory. As a morphism F : (Ă, ( )^{§}) → (B̆, ( )^{§}) is a functor such that F (f′, f)_{1} = F (f, f′)_{2}, functors in InvCAT are called symmetric. We also call objects X such that X = X^{c} symmetric. Thus, F X is symmetric if F and X are.

The involutory categories (B̆, ( )^{§}) are universal in that they are characterised by a natural bijective correspondence

B A F̆ (A, ( )^{a})  (B̆, ( )^{§}) symmetric F

given by the mapping F ↦ F̆ = ⟨F^{op} ∘ ( )^{a}, F ⟩. This property allows us to turn mixed-variance functors on a category C into covariant symmetric functors on C̆.

Note that InvCAT is cartesian with terminal object (1, Id) and products (A, ( )^{a}) × (B, ( )^{b}) = (A × B, ( )^{a} × ( )^{b}).

5 Recursive types

In [Fre91, Fre92], Peter Freyd defined an algebraically complete category as one such that each of its endofunctors has an initial algebra and remarked that this should be understood in a 2-categorical setting; that is, a setting in which the phrase “every endofunctor” refers to an understood class. For us, this will be determined by enrichment. One possibility is:

Definition 5.1 (c.f. [Fre91]) A V-category is V-algebraically complete if every V-endofunctor on it has an initial algebra. □

Algebraic completeness guarantees the existence of parameterised initial algebras. Let A be V-algebraically complete and F : X × A → A be a V-functor. As for every X ∈ | X | we have that F (X, ) : A → A is a V-functor, we can set (F^{†}X, ι_{X}^{F}) to be an initial F (X, )-algebra. To extend the action of F^{†} to morphisms, for every f : X → X′ in X, let F^{†}f : F^{†}X → F^{†}X′ be the unique F (X, )-algebra morphism from (F^{†}X, ι_{X}^{F}) to ( F^{†}X′, ι_{X′}^{F} ∘ F (f, F^{†}X′) ). By the universal property of initial algebras, F^{†} is a functor X → A and, by construction, ι^{F} is a natural transformation F ⟨Id, F^{†}⟩ \underrightarrow{.} F^{†}. The pair (F^{†}, ι^{F}) is called an initial parameterised F -algebra.

Unfortunately F^{†} need not V-enrich. To see this let Z be the Poset-category induced by the ordered monoid Z = (ℤ, ≤, 0, +) and consider the Poset-functor F : Z × Z → Z : (m, n) ↦ m + 2n. Every i ∈ ℤ is an initial algebra for F (Z, ) : Z → Z : n ↦ 2n and F^{†}m is a morphism from i to i + F (m, F^{†}Z) = i + m iff F^{†}m = −m, hence F^{†} : Z → Z does not Posetenrich.

Definition 5.2 A V-category A is parameterised V-algebraically complete if it is V-algebraically complete and for every V-functor F : X × A → A and every family {ι_{X}^{F} : F (X, F^{†}X) → F^{†}X}_{X ∈ | X |} of initial F (X, )-algebras, the induced functor F^{†} : X → A V-enriches.

A parameterisation (( )^{†}, ι^{( )}) on A is a pair of mappings that associates every V-functor F : X × A → A with a V-functor F^{†} : X → A and a natural transformation ι^{F} : F ⟨Id, F^{†}⟩ \underrightarrow{.} F^{†} such that (F^{†}, ι^{F}) is an initial parameterised F -algebra. □

Convention. From now on, in the situation of the above definition, the family of initial algebras determining F^{†} will be left implicit.

Definition 5.3 1. (c.f. [Fre91]) A V-category is V-algebraically compact if it is V-algebraically complete and the initial algebra of every V-endofunctor on it is free, in the sense that its inverse is a final coalgebra.

2. A V-category is parameterised V-algebraically compact if it is V-algebraically compact and parameterised V-algebraically complete. □

Theorem 5.4 1. [Fio94] (c.f. [Bar92, Adá93]) A Cpo-category with an e-initial object (an initial object such that every morphism with it as source is an embedding) and colimits of ω-chains of embeddings is Cpo-algebraically complete.

2. [Fre92] A Cpo-algebraically complete category with pointed homs and strict composition is Cpoalgebraically compact.

3. Cpo-algebraic completeness (resp. compactness) implies parameterised Cpo-algebraic completeness (resp. compactness). □

Theorem 5.5 [Product Theorem] (c.f. [Fre91]) If A and B are parameterised V-algebraically compact then so is A × B. □

Algebraic compactness is a self-dual property. Hence:

Corollary 5.6 1. If A is (parameterised) V-alge-braically compact then so is A^{op}.

2. If A is parameterised V-algebraically compact then so is Ă. □

The last property of compactness that will be needed is that symmetric functors are closed under initial parameterised algebras:

Theorem 5.7 Let X and A be V-categories. Assume that A is parameterised V-algebraically compact. For a symmetric V-functor F : X̆ × Ă → Ă, every initial parameterised F -algebra (F^{†}, ι^{F}) canonically induces an initial parameterised F -algebra (F^{‡}, φ^{F}) such that F^{‡} is a symmetric V-functor and φ_{X}^{§} = φ_{X}^{−1} for every symmetric X. □

Remark. When X = 1 and F = Ğ for G : Ă → A, the above theorem provides a canonical and minimal fixed-point for G.

6 FPC

6.1 The Language

The grammar of FPC requires two syntax classes of variables: type variables (ranged over by T) and expression variables (ranged over by x). The syntax of the language is as follows:

Types τ ::= T | τ_{1} + τ_{2} | τ_{1} × τ_{2} | τ_{1}⇀ ⇀τ_{2} | μT.τ, Expressions

e ::= x | inl_{τ_{1},τ_{2}}(e) | inr_{τ_{1},τ_{2}}(e) |

                                                         case e of inl(x_{1}).e_{1} or inr(x_{2}).e_{2} |

⟨e_{1}, e_{2}⟩ | fst(e) | snd(e) | λx : τ.e | e_{1}(e_{2}) |

intro_{μT.τ} (e) | elim(e).

A well-formed type Θ ⊢ τ consists of a list of distinct type variables Θ and a type τ whose free type variables appear in Θ. Well-formed expression contexts Θ ⊢ Γ are finite mappings assigning well-formed types to expression variables. For the definition of well-formed expressions Θ, Γ ⊢ e : τ see [Gun92].

6.2 Operational semantics

The operational semantics is defined by an evaluation relation (⇝) on expressions. The call-by-value evaluation rules are:

var  \overline{x ⇝ x}

+Il \frac{e ⇝ v}{inl(e) ⇝ inl(v)} +Ir \frac{e ⇝ v}{inr(e) ⇝ inr(v)}

+El  \frac{e ⇝ inl(v) e_{1}[x_{1} ↦ v] ⇝ v′}{case e of inl(x_{1}).e_{1} or inr(x_{2}).e_{2} ⇝ v′}

+Er  \frac{e ⇝ inr(v) e_{2}[x_{2} ↦ v] ⇝ v′}{case e of inl(x_{1}).e_{1} or inr(x_{2}).e_{2} ⇝ v′}

×I  \frac{e_{1} ⇝ v_{1} e_{2} ⇝ v_{2}}{⟨e_{1}, e_{2}⟩ ⇝ ⟨v_{1}, v_{2}⟩}

×E_{1}  \frac{e ⇝ ⟨v_{1}, v_{2}⟩}{fst(e) ⇝ v_{1}}  ×E_{2}  \frac{e ⇝ ⟨v_{1}, v_{2}⟩}{snd(e) ⇝ v_{2}}

⇀ ⇀I  \overline{λx : τ.e ⇝ λx : τ.e}

⇀ ⇀E  \frac{e_{1} ⇝ λx : τ.e e_{2} ⇝ v e[x ↦ v] ⇝ v′}{e_{1}(e_{2}) ⇝ v′}

μI  \frac{e ⇝ v}{intro(e) ⇝ intro(v)}

μE  \frac{e ⇝ intro(v)}{elim(e) ⇝ v}

The expressions v such that v ⇝ v, called values, are characterised by the grammar,

Values v ::= x | inl_{τ_{1},τ_{2}}(v) | inr_{τ_{1},τ_{2}}(v) |

⟨v_{1}, v_{2}⟩ | λx : τ. e | intro_{μT.τ} (v).

For closed τ, we define

Values(τ) = {v ∈ Values | ⊢ v : τ},
Programs(τ) = {p ∈ Expressions | ⊢ p : τ}.

Convention. We write Θ, Γ ⊢ e ⇝ v : τ to indicate that Θ, Γ ⊢ e : τ is derivable and that e ⇝ v. We also write Θ, Γ ⊢ e ✓ : τ when Θ, Γ ⊢ e ⇝ v : τ for some value v.

6.3 Categorical models

Essentially, the categorical structure needed to interpret FPC is a parameterised algebraically compact partial cartesian closed category with finite coproducts.

Definition 6.1 A V-model of FPC is specified by

• a domain structure (K, D),

• a V-enrichment for pK,

• V-functors +, ⊗ : pK × pK → pK and ⇀ ⇀ : pK^{op} × pK → pK, and

• mappings ( )^{†} and ι^{( )} associating every V-functor F : X × pK → pK with a V-functor F^{†} : X → pK and a natural transformation ι^{F} : F ⟨Id, F^{†}⟩ \underrightarrow{.} F^{†}

such that

• the underlying functors of +, ⊗ and ⇀ ⇀ are, respectively, coproduct, partial product and partial exponential functors, and

• pK is parameterised V-algebraically compact with parameterisation (( )^{†}, ι^{( )}). □

Remark. It follows that pK has zero object 0 (viz. a free Id_{pK}-algebra), K has terminal object 1 = 0⇀ ⇀0 and J ≅ ⊗ 1 : K → pK has right adjoint.

6.4 Denotational semantics

Until the end of this subsection fix a V-model of FPC. Well-formed types, Θ ⊢ τ, are interpreted as symmetric functors [[Θ ⊢ τ]] : p̆K ^{| Θ |} → p̆K and wellformed expressions, Θ, Γ ⊢ e : τ, are interpreted as families of partial maps

[[Θ, Γ ⊢ e : τ]]_{A} : [[Θ ⊢ Γ]](A)_{2} ⇀ [[Θ ⊢ τ]](A)_{2}

for A ∈ | p̆K | ^{| Θ |} symmetric.

6.4.1 Interpretation of Types

Definition 6.2 [[Θ ⊢ τ]] : p̆K ^{| Θ |} → p̆K.

• [[Θ ⊢ Θ_{i}]] = Π_{i} (1 ≤ i ≤ | Θ |).

• [[Θ ⊢ τ_{1} + τ_{2}]] = (+ ∘ ⟨Π_{2}[[Θ ⊢ τ_{1}]], Π_{2}[[Θ ⊢ τ_{2}]]⟩)^{}˘ .

• [[Θ ⊢ τ_{1} × τ_{2}]] = (⊗ ∘ ⟨Π_{2}[[Θ ⊢ τ_{1}]], Π_{2}[[Θ ⊢ τ_{2}]]⟩)^{}˘ .

• [[Θ ⊢ τ_{1}⇀ ⇀τ_{2}]] = (⇀ ⇀ ∘ ⟨Π_{1}[[Θ ⊢ τ_{1}]], Π_{2}[[Θ ⊢ τ_{2}]]⟩)^{}˘ .

• [[Θ ⊢ μT.τ]] = [[Θ, T ⊢ τ]]^{‡}. □

Remark. The parameterisation ( )^{‡} on p̆K appearing in the last item of the above definition is the one obtained, by Corollary 5.6 (2) and Theorem 5.7, from the given parameterisation on pK.

By construction and because of Theorem 5.7, [[Θ ⊢ τ]] is a symmetric V-functor. The interpretation of types respects a substitution lemma (Lemma 6.3), establishing that evaluation is the semantic counterpart of syntactic substitution. This is needed to interpret expressions.

Lemma 6.3 (Substitution Lemma) There exists a canonical natural isomorphism

β : [[Θ ⊢ τ_{1}[T ↦ τ_{2}]]] ≅ [[Θ, T ⊢ τ_{1}]]⟨Id, [[Θ ⊢ τ_{2}]]⟩

such that β_{A}^{§} = β_{A}^{−1} for every symmetric A. □

6.4.2 Interpretation of Expression Contexts

Definition 6.4 [[Θ ⊢ Γ]] : p̆K ^{| Θ |} → p̆K.

• [[Θ ⊢ ⟨⟩]] = K_{(1,1)} (the constantly (1, 1) functor).

• [[Θ ⊢ Γ, x : τ]] = (⊗ ∘ ⟨Π_{2}[[Θ ⊢ Γ]], Π_{2}[[Θ ⊢ τ]]⟩)^{}˘ . □

Remark. [[Θ ⊢ Γ]] is a symmetric V-functor.

6.4.3 Interpretation of Expressions

The interpretation of expressions is defined in the standard way. Variables correspond to projections, inl/inr to coproduct injections, case to coproduct selection, ⟨ , ⟩ to partial pairing, fst/snd to projections, λx. to currying, ( ) to evaluation and intro/elim to folding/unfolding a recursive type.

Definition 6.5 For symmetric A ∈ | p̆K | ^{| Θ |} we define [[Θ, Γ ⊢ e : τ]]_{A} as follows:

• [[Θ, Γ ⊢ Γ_{i}]]_{A} = π_{i} (1 ≤ i ≤ | Γ |).

• [[Θ, Γ ⊢ inl(e) : τ_{1} + τ_{2}]]_{A} = ⨿_{1} ∘ [[Θ, Γ ⊢ e : τ_{1}]]_{A}.

• [[Θ, Γ ⊢ inr(e) : τ_{1} + τ_{2}]]_{A} = ⨿_{2} ∘ [[Θ, Γ ⊢ e : τ_{2}]]_{A}.

• [[Θ, Γ ⊢ case e of inl(x_{1}).e_{1} or inr(x_{2}).e_{2} : τ]]_{A}

= [[[Θ, ⟨Γ, x_{1} : τ_{1}⟩ ⊢ e_{1} : τ]]_{A}, [[Θ, ⟨Γ, x_{2} : τ_{2}⟩ ⊢ e_{2} : τ]]_{A}]

∘ δ_{A} ∘ ⟨⟨id, [[Θ, Γ ⊢ e : τ_{1} + τ_{2}]]_{A}⟩⟩

where δ_{A} is the canonical natural isomorphism

[[Θ ⊢ Γ]](A)_{2} ⊗ ([[Θ ⊢ τ_{1}]](A)_{2} + [[Θ ⊢ τ_{2}]](A)_{2}) ≅

([[Θ ⊢ Γ]](A)_{2} ⊗ [[Θ ⊢ τ_{1}]](A)_{2}) +

([[Θ ⊢ Γ]](A)_{2} ⊗ [[Θ ⊢ τ_{1}]](A)_{2}).

• [[Θ, Γ ⊢ ⟨e_{1}, e_{2}⟩ : τ_{1} × τ_{2}]]_{A}

= ⟨⟨[[Θ, Γ ⊢ e_{1} : τ_{1}]]_{A}, [[Θ, Γ ⊢ e_{2} : τ_{2}]]_{A}⟩⟩.

• [[Θ, Γ ⊢ fst(e) : τ_{1}]]_{A} = π_{1} ∘ [[Θ, Γ ⊢ e : τ_{1} × τ_{2}]]_{A}.

• [[Θ, Γ ⊢ snd(e) : τ_{2}]]_{A} = π_{2} ∘ [[Θ, Γ ⊢ e : τ_{1} × τ_{2}]]_{A}.

• [[Θ, Γ ⊢ λ : τ_{1}x.e : τ_{1}⇀ ⇀τ_{2}]]_{A}

= pλ([[Θ, ⟨Γ, x : τ_{1}⟩ ⊢ e : τ_{2}]]_{A}).

• [[Θ, Γ ⊢ e(e_{1}) : τ_{2}]]_{A}

= ε ∘ ⟨⟨[[Θ, Γ ⊢ e : τ_{1}⇀ ⇀τ_{2}]]_{A}, [[Θ, Γ ⊢ e_{1} : τ_{1}]]_{A}⟩⟩.

• [[Θ, Γ ⊢ intro(e) : μT.τ]]_{A}

= I_{A} ∘ [[Θ, Γ ⊢ e : τ[T ↦ μT.τ]]]_{A}
where I_{A} = (φ_{A}^{[[Θ, T ⊢τ]]} ∘ β_{A})_{2}.

• [[Θ, Γ ⊢ elim(e) : τ[T ↦ μT.τ]]]_{A}

= E_{A} ∘ [[Θ, Γ ⊢ e : μT.τ]]_{A}
where E_{A} = (φ_{A}^{[[Θ, T ⊢τ]]} ∘ β_{A})_{1}. □

Remark. By Theorem 5.7 and Lemma 6.3, I_{A} and E_{A} are mutual inverses.

The interpretation of expressions is well-defined:

Proposition 6.6 For A ∈ | p̆K | ^{| Θ |} symmetric,

[[Θ, Γ ⊢ e : τ]]_{A} : [[Θ ⊢ Γ]](A)_{2} ⇀ [[Θ ⊢ τ]](A)_{2}. □

Remark. It can be shown [Fio94] that the interpretation of expressions in Poset-models induced by domain structures with a Poset-category of total maps is parametric with respect to representations [Rey74].

6.5 Domain-theoretic models

In this subsection, the results of Sections 4 and 5 are combined to produce Cpo-models of FPC. Domaintheoretic models correspond to uniform domain structures with a Cpo-category of total maps whose category of partial maps is a Cpo-model with respect to the induced order (Definition 3.3) and where algebraic compactness arises from the limit/colimit coincidence.

Definition 6.7 A domain-theoretic model of FPC is specified by a uniform domain structure (K, D) and a Cpo-enrichment ⊑ for K satisfying:

DTM1. (K, ⊑) has chosen binary Poset-coproducts.

DTM2. (K, ⊑) has chosen binary Poset-products.

DTM3. (pK, ⊏ ∼ ) is a Poset-category with chosen Poset-partial-exponentials.

DTM4. pK has a chosen zero object.

DTM5. K has chosen colimits of ω-chains of embeddings. □

Theorem 6.8 [Fio94] If (K, D, ⊑) is a domaintheoretic model of FPC then (p(K, D), ⊏ ∼ ) is a Cpomodel of FPC. □

Example 6.9 For W a small Cpo-category, let ([W, Cpo], ⊑) be the Cpo-functor-category of Cpo-functors W → Cpo and natural transformations ordered pointwise, and let ΣC_{[W,Cpo]} be the subcategory of [W, Cpo] of all pointwiseadmissible and cartesian natural transformations. Then, ([W, Cpo], ΣC_{[W,Cpo]}, ⊑) specifies a domaintheoretic model. □

7 Computational adequacy

The relationship between the operational notion of termination and the denotational notion of totality is examined. It is shown that in any model of FPC the interpretation of expressions is computationally sound, meaning that if the evaluation of a program terminates then it has a total interpretation. Further, certain absolute domain-theoretic models are shown to be computationally adequate, meaning that if a program has a total interpretation then its evaluation terminates.

7.1 Computational Soundness

The strategy for proving computational soundness is as usual: observe that values have total interpretations and that the interpretation of programs is preserved under evaluation:

Lemma 7.1 In any V-model of FPC,

1. [[Θ, Γ ⊢ v : τ]]_{A} ↓ for every value v.

2. if Θ, Γ ⊢ e ⇝ v : τ then [[Θ, Γ ⊢ e : τ]]_{A} = [[Θ, Γ ⊢ v : τ]]_{A}. □

Theorem 7.2 (Computational Soundness) In any V-model of FPC, if Θ, Γ ⊢ e ✓ : τ then [[Θ, Γ ⊢ e : τ]]_{A} ↓. □

7.2 Adequacy

Convention. We write [[⊢ τ]] for [[⊢ τ]]() and [[⊢ p : τ]] for [[⊢ p : τ]]_{()}.

Definition 7.3 A V-model of FPC is computationally adequate if, for every p ∈ Programs(τ),

[[⊢ p : τ]] ↓ implies ⊢ p ✓ : τ. □

Fix a domain-theoretic model of FPC. Computational adequacy cannot be proved directly by induction. To establish it (see Lemma 7.13), we inductively prove the following stronger version

[[⊢ p : τ]] ↓ ⇒ ∃ v. p ⇝ v ∧ [[⊢ p : τ]] ⪯_{τ} v

where { ⪯_{τ} ⊆ K(1, [[⊢ τ]]_{2}) × Values(τ)} is a family of formal-approximation relations with the following closure properties:

R1. x ⪯_{σ+τ} inl(v) ⟺ ∃ x′ ⪯_{σ} v. x = ⨿_{1} ∘ x′

x ⪯_{σ+τ} inr(v) ⟺ ∃ x′ ⪯_{τ} v. x = ⨿_{2} ∘ x′

R2. x ⪯_{σ×τ} ⟨v_{1}, v_{2}⟩

⟺

(π_{1} ∘ x ⪯_{σ} v_{1}) ∧ (π_{2} ∘ x ⪯_{τ} v_{2})

R3. f ⪯_{σ⇀ ⇀τ} λx : σ. e

⟺

(∀ x ∈ K(1, [[⊢ σ]]_{2}). ∀ v ∈ Values(σ).
x ⪯_{σ} v ⇒ ε ∘ ⟨⟨f, x⟩⟩ ≾_{τ} e[x ↦ v])

where u ≾ p ⟺ (u ↓ ⇒ ∃ v. p ⇝ v ∧ u ⪯ v).

R4. x ⪯_{μT. τ} intro(v) ⟺ E ∘ x ⪯_{τ[T ↦ μT. τ]} v.

We now embark on the major task of establishing the existence of the formal-approximation relations. The difficulty is that they are defined recursively and one should guarantee that this definition makes sense. This is better discussed with the aid of some definitions.

For closed τ, generalising from the formalapproximation relations, we set

| R(τ) | = {(A, ⪯) | A ∈ | K | ∧ ⪯ ⊆ K(1, A) × Values(τ)}

and given ⪯ ⊆ K(1, A) × Values(τ), we define its extension to partial maps and programs ≾ ⊆ pK(1, A) × Programs(τ), by

u ≾ p ⟺ (u ↓ ⇒ ∃ v. p ⇝ v ∧ u ⪯ v).

Now, to provide an equational description of the closure properties of ⪯_{σ⋆τ} (⋆ ∈ {+, ×, ⇀ ⇀}) and to clarify the closure property of ⪯_{μT.τ}, the type constructors are logically extended to relations following (R1)–(R3):

Definition 7.4 For closed σ and τ,

1. Let +_{σ,τ} : | R(σ) | × | R(τ) | → | R(σ + τ) | be the function mapping ((A, ⪯_{A}), (B, ⪯_{B})) to (A + B, ⪯_{A} + ⪯_{B}) where

x (⪯_{A} + ⪯_{B}) inl(v) ⟺ (∃ x′ ⪯_{A} v. x = ⨿_{1} ∘ x′) and x (⪯_{A} + ⪯_{B}) inr(v) ⟺ (∃ x′ ⪯_{B} v. x = ⨿_{2} ∘ x′).

2. Let ⊗_{σ,τ} : | R(σ) | × | R(τ) | → | R(σ × τ) | be the function mapping ((A, ⪯_{A}), (B, ⪯_{B})) to (A ⊗ B, ⪯_{A} ⊗ ⪯_{B}) where

x (⪯_{A} ⊗ ⪯_{B}) ⟨v_{1}, v_{2}⟩ ⟺

(π_{1} ∘ x ⪯_{A} v_{1}) ∧ (π_{2} ∘ x ⪯_{B} v_{2}).

3. Let ⇀ ⇀_{σ,τ} : | R(σ) | × | R(τ) | → | R(σ⇀ ⇀τ) | be the function mapping ((A, ⪯_{A}), (B, ⪯_{B})) to (A⇀ ⇀B, ⪯_{A} ⇀ ⇀ ⪯_{B}) where

f (⪯_{A} ⇀ ⇀ ⪯_{B}) λx : σ. e ⟺

(∀ x ∈ K(1, A). ∀ v ∈ Values(σ). x ⪯_{A} v ⇒ ε ∘ ⟨⟨f, x⟩⟩ ≾_{B} e[x ↦ v]). □

Then, (R1)–(R3) can be written as

⪯_{σ+τ} = ⪯_{σ} + ⪯_{τ} ,
⪯_{σ×τ} = ⪯_{σ} ⊗ ⪯_{τ} ,
⪯_{σ⇀ ⇀τ} = ⪯_{σ} ⇀ ⇀ ⪯_{τ} .

In the case of recursive types (R4) we intuitively have that

E : ⪯_{μT.τ} ≅ 𝕀 (⪯_{τ[T ↦ μT.τ]})  (1)

where x (𝕀 ⪯) intro(v) ⟺ x ⪯ v. And this is exactly where the difficulty in constructing ⪯_{μT. τ} resides as we have to solve a recursive equation between relations!

We make | R(τ) | into the objects of a category; the notion of morphism is suggested by (1):

Definition 7.5 The category R(τ) has objects | R(τ) | and morphisms u : (A, ⪯_{A}) ⇀ (B, ⪯_{B}) where u : A ⇀ B is such that for every x ∈ K(1, A) and every v ∈ Values(τ), if x ⪯_{A} v then u∘x ≾_{B} v. Composition and identities are as in pK. □

Proposition 7.6 The functions +_{σ,τ}, ⊗_{σ,τ} and ⇀ ⇀_{σ,τ} extend to functors satisfying

U_{σ+τ} ∘ +_{σ,τ} = + ∘ (U_{σ} × U_{τ}),
U_{σ×τ} ∘ ⊗_{σ,τ} = ⊗ ∘ (U_{σ} × U_{τ}),
U_{σ⇀ ⇀τ} ∘ ⇀ ⇀_{σ,τ} = ⇀ ⇀ ∘ (U_{σ}^{op} × U_{τ})

where U_{τ} : R(τ) → pK is the evident forgetful functor. □

The type constructors on pK have been extended to the R(τ)’s but there are too many relations in them to be able to find recursive types. The way out is to find subcategories pK(τ) of R(τ) in which this is possible.

Definition 7.7 Let pK(τ) be the full subcategory of R(τ) consisting of all those objects (A, ⪯) such that for every v ∈ Values(τ), ⪯^{−1} (v) is closed under lubs of ω-chains in pK(1, A). □

In order that the notion of approximation on the pK(τ)’s be inherited from pK (i.e. that the forgetful functor pK(τ) → pK be a Cpo-functor) we restrict attention to absolute models:

Definition 7.8 A Cpo-model of FPC is absolute if for every A ∈ | K |, K(1, A) is inaccessible by lubs of ω-chains in pK(1, A). □

In domain-theoretic models absoluteness has a simple characterisation:

Proposition 7.9 A domain-theoretic model of FPC is absolute iff [id_{1}] is inaccessible by lubs of ω-chains in D(1). □

Remark. The above could have been stated as: the D-classifier 1 ↣ Σ (i.e. the counit of the representation K( , Σ) ≅ pK( , 1) ≅ D( ) : K^{op} → Set) is inaccessible by lubs of ω-chains in K(1, Σ).

Example 7.10 For a small Cpo-category W, the domain-theoretic model ([W, Cpo], ΣC_{[W,Cpo]}) is absolute iff W has a finite number of connected components. □

From now on let our fixed domain-theoretic model of FPC be non-trivial and absolute. Then, we have the following lemma which displays the essential categorical structure needed to prove the existence of the formal-approximation relations.

Lemma 7.11

A1. (pK(τ), ⊏ ∼ ) is a Cpo-category and the forgetful functor pK(τ) → pK Cpo-enriches.

A2. (pK(τ), ⊏ ∼ ) is parameterised Cpo-algebraically compact.

A3. For ⋆ = +, ⊗ (resp. ⇀ ⇀), the functor ⋆_{σ,τ} restricts to a Cpo-functor pK(σ) × pK(τ) → pK(σ ⋆ τ) (resp. pK(σ)^{op} × pK(τ) → pK(σ⇀ ⇀τ)).

A4. 𝕀_{μT. τ} : pK(τ[T ↦ μT. τ]) ≅ pK(μT. τ) : 𝔼_{μT. τ} where

𝕀_{μT. τ} : (A, ⪯) ↦ (A, 𝕀 ⪯)

with x (𝕀 ⪯) intro(v) ⟺ x ⪯ v

and

𝔼_{μT. τ} : (A, ⪯) ↦ (A, 𝔼 ⪯)

with x (𝔼 ⪯) v ⟺ x ⪯ intro(v).

A5. [Strict Uniformity] For every pair of symmetric Cpo-functors F and G, if

pK(σ)^{}˘p̆K pK(σ_{1})^{}˘ × … × pK(σ_{m})^{}˘ × pK(σ)^{}˘p̆K × … × p̆K × p̆K  F G

commutes then for every initial parameterised G-algebra (G^{†}, ι^{G}) there exists an initial parameterised F -algebra (F^{†}, ι^{F}) such that

pK(σ_{1})^{}˘ × … × pK(σ_{m})^{}˘  pK(σ)^{}˘≅^{ι^{F}} F ⟨Id, F^{†}⟩ F^{†} p̆K × … × p̆K  p̆K ≅^{ι^{G}} G⟨Id, G^{†}⟩ G^{†}

commutes. □

Once the Properties (A1)–(A5) are known to hold, the formal-approximation relations are constructed by providing a non-standard interpretation of types in the pK(τ)’s (Proposition 7.12) which extends the interpretation of types (Definition 6.2) respecting the folding and unfolding of recursive types and the substitution of types.

Convention. Given Θ ≡ T_{1}, …, T_{m} and closed σ_{i} (1 ≤ i ≤ m) we write σ⃗ for σ_{1}, …, σ_{m} and [Θ ↦ σ⃗] for [T_{1} ↦ σ_{1}, …, T_{m} ↦ σ_{m}].

Proposition 7.12 There exists an interpretation

⟨[Θ ⊢ τ]⟩(σ⃗) : pK(σ_{1})^{}˘ × … × pK(σ_{|Θ|})^{}˘ → pK(τ[Θ ↦ σ⃗])^{}˘ such that ⟨[Θ ⊢ τ]⟩(σ⃗) is a symmetric Cpo-functor and

pK(σ_{1})^{}˘ × … × pK(σ_{|Θ|})^{}˘p̆K × … × p̆K  ⟨[Θ ⊢ τ]⟩(σ⃗) [[Θ ⊢ τ]] pK(τ[Θ ↦ σ⃗])^{}˘p̆K

commutes. □

From the non-standard interpretation of types, the formal-approximation relations are easily extracted as the second component of ⟨[⊢ τ]⟩()_{2}.

The following main lemma is now proved by induction on the structure of e:

Lemma 7.13 For Γ ≡ x_{1} : τ_{1}, …, x_{n} : τ_{n}, if x_{i} ⪯_{τ_{i}} v_{i} (1 ≤ i ≤ n) then

[[Γ ⊢ e : τ]] ∘ ⟨⟨x_{1}, …, x_{n}⟩⟩ ≾_{τ} e[x_{1} ↦ v_{1}, …, x_{n} ↦ v_{n}].□

Finally, since [[⊢ p : τ]] ≾_{τ} p, we conclude:

Theorem 7.14 (Computational Adequacy) Every absolute non-trivial domain-theoretic model of FPC is computationally adequate. □

Remark. Using (A3), domain structures with a Cpo-category of total maps satisfying the axioms (DTM1)–(DTM4) and absoluteness, and equipped with structure for interpreting natural numbers and booleans can be shown to be computationally adequate for call-by-value PCF with sums and products (c.f. [BCL85]).

Corollary 7.15 For every non-empty small Cpo-category W, the domain-theoretic model specified by ([W, Cpo], ΣC_{[W,Cpo]}) is computationally adequate. □

Remark. Thus there are computationally-adequate non-absolute domain-theoretic models.

Acknowledgements. We are grateful to Barry Jay and John Power for discussions on categorical matters.

References

[Abr90] S. Abramsky. The lazy λ-calculus. In Logical Foundations of Functional Programming. Addison-Wesley, 1990.

[Adá93] J. Adámek. Data types in algebraically ωcomplete categories. To appear in Information and Computation, 1993.

[Bar92] M. Barr. Algebraically compact functors. Journal of Pure and Applied Algebra, 82:211–231, 1992.

[BCL85] G. Berry, P.-L. Curien, and J.-J. Lévy. Full abstraction for sequential languages: the state of the art. In M. Nivat and J.C. Reynolds, editors, Algebraic methods in semantics, pages 89–132. Cambridge University Press, 1985.

[Fio93] M.P. Fiore. Cpo-categories of partial maps. In CTCS-5 (Category Theory and Computer Science Fifth Biennial Meeting), pages 45– 49. CWI, September 1993.

[Fio94] M.P. Fiore. Axiomatic domain theory in categories of partial maps. Forthcoming Ph.D. thesis, 1994.

[Fre90] P.J. Freyd. Recursive types reduced to inductive types. In 5^{th} LICS Conf., pages 498– 507. IEEE, Computer Society Press, 1990.

[Fre91] 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.

[Fre92] P.J. Freyd. Remarks on algebraically compact categories. In M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series, pages 95–106. Cambridge University Press, 1992.

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

[Kel82] G.M. Kelly. Basic Concepts of Enriched Category Theory. Cambridge University Press, 1982.

[LM84] G. Longo and E. Moggi. Cartesian closed categories of enumerations for effective typestructures. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Symposium on Semantics of Data Types, volume 173 of Lecture Notes in Computer Science. Springer-Verlag, 1984.

[MC88] A.R. Meyer and S.S. Cosmadakis. Semantical paradigms: Notes for an invited lecture. In 3^{rd} LICS Conf., pages 236–253. IEEE, Computer Society Press, 1988.

[Mog86] E. Moggi. Categories of partial morphisms and the partial lambda-calculus. In Proceedings Workshop on Category Theory and Computer Programming, Guildford 1985, volume 240 of Lecture Notes in Computer Science, pages 242–251. Springer-Verlag, 1986.

[Mog89] E. Moggi. Computational lambda-calculus and monads. In 4^{th} LICS Conf., pages 14– 23, 1989.

[Pit93] A.M. Pitts. Relational properties of domains. Technical Report 321, Cambridge Univ. Computer Laboratory, December 1993.

[Plo85] G.D. Plotkin. Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School, 1985.

[Plo93] G.D. Plotkin. Type theory and recursion (extended abstract). In 8^{th} LICS Conf., page 374. IEEE, Computer Society Press, 1993.

[Rey74] J. Reynolds. Towards a theory of type structure. In B. Robinet, editor, Programming Symposium ’74, volume 19 of Lecture Notes in Computer Science. Springer-Verlag, 1974.

[Ros86] G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986.

[RR88] E. Robinson and G. Rosolini. Categories of partial maps. Information and Computation, 79:95–130, 1988.

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

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