Sequentiality in an extensional framework^{∗}

Antonio Bucciarelli LIENS – DMI Ecole Normale Supérieure 45 rue d’Ulm 75230 Paris Cédex France

        e-mail: buccia@dmi.ens.fr

Thomas Ehrhard IGM Université de Marne-la-Vallée 2 rue de la Butte Verte 93166 Noisy-le-Grand Cédex France

                                    e-mail: ehrhard@dmi.ens.fr

Abstract

We present a cartesian closed category of dI-domains with coherence and strongly stable functions which provides a new model of PCF, where terms are interpreted by functions and where, at first order, all functions are sequential.

We show how this model can be refined in such a way that the theory it induces on the terms of PCF be strictly finer than the theory induced by the Scott model of continuous functions. Keywords: lambda-calculus, denotational semantics, continuity, stability, sequentiality.

∗This article is published in Information and Computation 110(1994), pp. 265-296.

Contents

1 dI-domains and stable functions 3

2 From sequentiality to strong stability 6

3 Strong stability 10

4 Extensionality 16

5 Extensionally Embedded dI-Domains with Coherence 18

6 About the theory induced by ESS on PCF 23

Introduction

One of the main goals of denotational semantics is to find models of purely functional programming languages like PCF (see [Plotkin, G. (1977)] and [Berry, G. and Curien, P.-L. and Levy, J.-J. (1985)]) as adapted as possible to the operational semantics of these languages. This consists in finding cartesian closed categories of domains where there are “as few points as possible”, aiming at a situation where any finite point is definable by a term of PCF. In that situation, the model is fully abstract (see [Milner, R. (1977)]).

Plotkin [Plotkin, G. (1977)] remarked that the presence of functions like “parallel or” in the Scott models prevents them from being fully abstract. Previously, Vuillemin [Vuillemin, J. (1974)] and Milner proposed the notion of sequentiality as a way to take determinism into account in the semantics of computations. Later on, Kahn and Plotkin [Kahn, G. and Plotkin, G. (1978)] extended this notion to the general framework of concrete data structures (CDSs). Since “parallel or” does not exist in the model of Kahn and Plotkin and since, more generally, computations in PCF are deterministic, it became natural to look for sequential models of PCF. Unfortunately, the general model proposed by Kahn and Plotkin cannot take functionality into account: the category of CDSs and sequential functions is not cartesian closed.

The attempt of harmonizing sequentiality with functionality led to two main developments. The first one consisted in weakening the notion of sequentiality in a property which still makes sense at higher orders, and this is what Berry [Berry, G. (1979)] did introducing stable semantics. The second one, carried out by Berry and Curien [Berry, G. and Curien, P.-L. (1982)], was to stick to the notion of sequentiality of Kahn and Plotkin, but the price to pay was the impossibility of keeping functions as morphisms; they were obliged to switch to sequential algorithms.

The model presented in the first part of this paper reminds the stable semantics for two reasons: first, the morphisms of our category are functions and second they are characterized by a preservation property similar to stability, this is why we call them “strongly stable”. Indeed, in this model, the domains are endowed with a certain notion of “coherence” which is a predicate on the set of their finite subsets. A function has then to preserve this coherence and to commute with the glbs of coherent sets. The interesting phenomenon is that Kahn-Plotkin sequentiality may be expressed in these terms. The main result is then the construction of a model dIC where all morphisms are functions and, at ground types, these functions are sequential.

Even if dIC is an extensional model (in the sense that all morphisms are functions), it does not reflect all the extensional properties of PCF. Actually, cartesian closure enforces the order between functions to be the stable one, which is strictly finer than the extensional order. For this reason, in a stably ordered model, there are functionals which are not PCF definable. Indeed, Jim and Meyer [Jim, T. and Meyer, A. (1991)] have shown that the stable model, the Berry’s bidomain model [Berry, G. (1979)], and the model of sequential algorithms are not better than the continuous one, as far as inclusion of theories is taken as criterion of comparison.

A natural approach to this problem consists in enriching the structure of domains by supplying information about the extensional (pointwise) ordering, and by imposing the continuity of morphisms w.r.t. this ordering. This is roughly what has been done by Berry with the definition of biordered structure (see [Berry, G. (1979)], section 4.7). However, this method is not completely satisfactory: as there are in general less stable morphisms between two ground types X and Y than continuous ones, in a function space (X → Y) → Z there are, even in the biordered case, functionals that would not exist in the extensional construction. Hence it is necessary to take into account in higher type domains information supplied by elements (arguments) that we want to discard from the semantics, like the “parallel or”. This is what we achieve by keeping not only two orders, but two domains, a “stable” domain embedded in a “continuous” one. The model obtained this way is called ESS. The relevance of this method is illustrated by the fact that the theory of ESS equates more terms than the theory of the continuous model.

In section 1, we recall some basic facts about the theory of stable functions and dIdomains. Section 2 shows that sequentiality can be expressed as a “stability” property and in section 3 we extend this notion of stability to higher order. This first part of the paper develops [Bucciarelli, A. and Ehrhard, T. (1991)A] in that strong stability is extended to the framework of dI-domains, whereas in the original article only qualitative domains were considered. In section 4, we explain how the lack of extensionality prevents the model previously defined from being fully abstract. In section 5 we provide a way to make the strongly stable model “extensional” and this leads to the definition of ESS. These two sections are borrowed from [Bucciarelli, A. and Ehrhard, T. (1991)B]. Section 6 presents a new result: we show that the model ESS has a finer theory than the one of the Scott model. However, ESS is not the fully abstract model.

1 dI-domains and stable functions

In this section we outline Berry’s theory of stable maps (see [Berry, G. (1978)] and [Berry, G. (1979)]).

The largest cartesian closed sub-category of Scott domains in which morphisms are stable turns out to be the category of dI-domains and stable maps. Hence dI-domains are the most general framework for dealing with stable functions and retaining properties like (ω-)algebraicity and bounded completeness, very appealing from a technical point of view and for the computational intuitions they support.

Definition 1 A dI-domain X is a Scott domain (i.e. an ω-algebraic bounded complete cpo) such that:

• Each compact element has finitely many lower bounds (property I).

• If x, y, z ∈ X are such that y and z are bounded, then

x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z) (property d).

The last condition is equivalent to a weaker form of distributivity:

Proposition 1 A Scott domain X satisfies property d if and only if for all x, y, z bounded in X

x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z) .

In the sequel “x ↑ y” stands for “x and y are bounded”.

An interesting characterization of dI-domains may be given in terms of prime elements.

Definition 2 Let X be a poset. A point x ∈ X is prime if

∀B ⊆ X (x ≤ ⋁ B) ⇒ (∃y ∈ B x ≤ y) .

X is prime algebraic if any element is the lub of its prime lower bounds.

The next proposition is due to Winskel [Winskel, G. (1988)]:

Proposition 2 An ω-algebraic bounded complete cpo satisfying the I property is a dIdomain if and only if it is prime algebraic.

Let |X|, K(X) stand for the set of prime and compact elements of X respectively.

Definition 3 A stable function between two dI-domain: X and Y is a Scott-continuous f : X → Y such that

∀x, y ∈ X x ↑ y ⇒ f(x ∧ y) = f(x) ∧ f(y) .

Actually the original definition of stable function (see [Berry, G. (1979)]), which makes sense in a class of complete partial orders larger then dI-domains, has been given in terms of the existence of minimal computations, as expressed by the next proposition:

Proposition 3 Let f be a continuous function between two dI-domains X and Y; f is stable if and only if

∀x ∈ X ∀b ∈ K(Y) b ≤ f(x) ⇒ ∃a ∈ K(X) \{ \begin{matrix}a ≤ x, b ≤ f(a) \\ ∀x′ ≤ x (b ≤ f(x′) ⇒ a ≤ x′) \end{matrix} .

The idea underlying the definition of stable function is that, when a given finite amount b of information is obtained at the output of a deterministic function applied to a given input, it is possible to find the part of this input which has actually been used by the function for the computation of b.

A stable function is fully described by its trace. Traces have been introduced by Girard in [Girard, J.-Y. (1986)], where the author reinvented the notion of stability and used stable functions between qualitative domains to construct a model of system F, a polymorphic λ-calculus. The notion of trace can be extended to general dI-domains as follows:

Definition 4 If f : X → Y is stable, its trace is defined by

tr(f) = {(a, q) | a ∈ K(X), q ∈ |Y | , and a minimal such that q ≤ f(a)} .

Let us now define the stable order on functions and see how it is related to traces.

Definition 5 Let f, g : X → Y be two monotone functions. One says that f is stably less than g, and writes f ≤ g, if

∀x, y ∈ X x ≤ y ⇒ f(x) = f(y) ∧ g(x) .

As for the notion of dI-domain it is important to stress that stable ordering is by no means arbitrary: actually it is the largest order included in the pointwise one which makes evaluation stable.

Proposition 4 If f, g : X → Y are stable, then:

• ∀x ∈ X f(x) = ⋁{q | ∃a ≤ x (a, q) ∈ tr(f)}

• f ≤ g if and only if tr(f) ⊆ tr(g).

Let us state some properties of the stably ordered poset of stable functions between two dI-domains.

Proposition 5 Let X and Y be two dI-domains. The poset Z of stable functions from X to Y, stably orderd, is a dI-domain. Furthermore:

• If F ⊆ Z is directed or bounded, then tr(⋁ F) = ⋃_{f∈F} tr(f).

• If f, g ∈ Z are bounded, then tr(f ∧ g) = tr(f) ∩ tr(g).

• A function f ∈ Z is compact iff tr(f) is a finite set.

The proofs of these results can be found for instance in [Zhang, G.Q. (1991)].

An easy consequence of this proposition is that any non-empty set F of stable functions has a stable glb (for the stable order). However, in general, the trace of this glb is not the intersection of the traces of the elements of F. This is due to the fact that a subset of a trace is not a trace in general. Actually, if t ⊆ K(X) × |Y | is the trace of a stable function, then

∀(a, q) ∈ t ∀q′ ∈ |Y | q′ ≤ q ⇒ ∃a′ ≤ a (a′, q′) ∈ t .  (1)

However, when a kind of “downward coherence” condition is satisfied by a non-empty set of stable functions, the trace of its glb is the intersection of traces. This is expressed in the next proposition, that will be useful in the sequel. Let us first mention that if t is a trace of a stable function, and if t′ ⊆ t satisfies the condition (1) above, then t′ is also the trace of a stable function.

Lemma 1 Let F be a family of stable functions from X to Y. If (a, q) ∈ ⋂_{f∈F} tr(f) is such that for all q′ ∈ |Y |, q′ ≤ q ⇒ ∃a′ ≤ a (a′, q′) ∈ ⋂_{f∈F} tr(f), then (a, q) ∈ tr(⋀ F).

Proof: With the notations of the lemma, the set t = {(a′, q′) ∈ ⋂_{f∈F} tr(f) | a′ ≤ a, q′ ≤ q} satisfies condition (1) and hence is the trace of a stable function and we have (a, q) ∈ t and t ⊆ tr(⋀ F).

Let dI be the category of dI-domains and stable functions.

Proposition 6 dI is cartesian closed.

2 From sequentiality to strong stability

In this section we give some mathematical motivations for our approach to sequentiality through a strong form of stability. Our basic intuition of sequentiality corresponds to the definition by Kahn and Plotkin. A key notion in the framework of CDSs is the one of cell. Cells are “boxes” in which values can be stored. The CDS representing the flat domain of integers, for instance, has {⋆} as set of cells and {0, 1, 2, …, n, …} as set of values. The integer n is obtained by filling ⋆ with n. Our starting point consists in replacing cells by linear functions. Cells are no longer part of the structure of domains but, given a dIdomain X, we can recover the information supplied by cells in CDSs (which is essentially intensional) from suitable sets of linear functions from X to the Sierpinsky domain O (the two point dI-domain ⊥ < ⊤). In the case of the flat domain of integers the function defined by tr(⋆) = {(0, ⊤), (1, ⊤), …, (n, ⊤), …} replaces the cell ⋆.

Definition 6 A linear function between two dI-domains X and Y is a stable function f such that:

• f(⊥) = ⊥

• for all x, y ∈ X, x ↑ y ⇒ f(x ∨ y) = f(x) ∨ f(y).

Fact 1 A stable function f : X → Y is linear if and only if, for all (a, q) ∈ tr(f), a ∈ |X|.

Given a dI-domain X, let X^{⊥} be the set of linear functions from X to O. By the fact above and the definition of traces, it is easy to see that, if α ∈ X^{⊥}, then tr(α) = {(p_{1}, ⊤), …, (p_{n}, ⊤), …} where the p_{i}’s are prime and pairwise unbounded elements of X. Conversely, if {p_{1}, …, p_{n}, …} is a set of pairwise unbounded prime elements of X, then the set {(p_{1}, ⊤), …, (p_{n}, ⊤), …} is the trace of a linear function from X to O. From now on we identify elements of X^{⊥} and sets of prime and pairwise unbounded elements of X. In the sequel p ∈ α means (p, ⊤) ∈ tr(α) and ↑ α is the set {x ∈ X | α(x) = ⊤}.

Elements of X^{⊥} will be called linear properties on X.

Definition 7 If X is a dI-domain, a subset Q of X^{⊥} separates X if

∀x, y ∈ X x ↑ y ⇒ (x = y ⇔ ∀α ∈ Q (x ∈ ↑ α ⇔ y ∈ ↑ α)) .

Actually X^{⊥} itself separates X in a stronger sense, namely

∀x, y ∈ X x = y ⇔ ∀α ∈ X^{⊥} (x ∈ ↑ α ⇔ y ∈ ↑ α) .

However we are interested in the weaker notion of separation expressed by definition 7, because linear properties play the role of questions (cells in the CDS framework) in our approach to sequentiality, and the set of all the linear properties on X is too rich in general. Consider for instance the flat domain of boolean values B: by definition B^{⊥} = {∅, {true}, {false}, {true, false}}, but there exist proper subsets of B^{⊥} that do separate B, e.g. B^{∗} = {∅, {true, false}} (this is the canonical choice of questions on booleans, which does not allow to separate true and false).

Fact 2 Let x, x′ ∈ X, α ∈ X^{⊥}; • ⊥∉↑ α.

• x ∨ x′ ∈ ↑ α ⇒ x ∈ ↑ α or x′ ∈ ↑ α.

• If x ↑ x′, x ∈ ↑ α and x′ ∈ ↑ α then x ∧ x′ ∈ ↑ α (this generalizes to finite, non-empty and bounded sets).

Definition 8 A sequential structure is a couple X = (X_{∗}, X^{∗}) where X_{∗} is a dI-domain and X^{∗} is a subset of X_{∗}^{⊥} which separates X_{∗} and contains the empty linear property ∅.

A sequential structure (X_{∗}, X^{∗}) is finitary if

∀a ∈ K(X_{∗}) ♯{α | a ∈ ↑ α} < ∞ .

In the sequel, given a sequential structure X = (X_{∗}, X^{∗}), we shall simply note X the underlying dI-domain X_{∗}.

Observe that in a stable CDS S (see [Curien, P.-L. (1993)]) a cell c may be viewed as a linear map from S to O, namely the one which maps a state x ∈ S to ⊤ if c is filled in x and to ⊥ otherwise. Observe also that, in a CDS, a compact state fills only a finite number of cells. This is why we consider that the notion of finitary sequential structure is a simple, but reasonably faithful abstraction of the notion of CDS. All the sequential structures considered in the sequel will be finitary, and we shall call them simply sequential structures.

We give now the definition of sequential functions between sequential structures, which is essentially the one of Kahn and Plotkin [Kahn, G. and Plotkin, G. (1978)].

Definition 9 Let (X, X^{∗}) and (Y, Y^{∗}) be sequential structures. A function f : X → Y is sequential if it is Scott-continuous and:

∀x ∈ X ∀β ∈ Y^{∗} f(x) ∉ ↑ β ⇒ ∃α ∈ X^{∗} \{ \begin{matrix}x ∉ ↑ α \\ ∀x′ ≥ x f(x′) ∈ ↑ β ⇒ x′ ∈ ↑ α \end{matrix} .

If we read “x ∈ ↑ α” as “the datum x answers to the question α”, then the previous definition says that if f(x) does not answer a given question β, then there exists a question α not answered by x that must be answered by any x′ greater than x such that f(x′) answers β. Such an α is called a sequentiality index of f at x for β.

Proposition 7 Any sequential function is stable.

Proof: Let (X, X^{∗}), (Y, Y^{∗}) be sequential structures and f : X → Y be sequential. If x ↑ x′ in X we have to show that f(x) ∧ f(x′) ≤ f(x ∧ x′), the symmetric inequality being granted by monotonicity of f. Let us suppose that f(x∧x′) < f(x)∧f(x′). By separation there exists a linear property β ∈ Y^{∗} such that f(x) ∧ f(x′) ∈ ↑ β and f(x ∧ x′) ∉ ↑ β. Let α be a sequentiality index of f at x ∧ x′ for β. Since f(x) ∈ ↑ β and f(x′) ∈ ↑ β we get by sequentiality x ∈ ↑ α and x′ ∈ ↑ α and, by fact 2, (x ∧ x′) ∈ ↑ α, which is absurd since α is a sequentiality index at x ∧ x′. The rest of this section is devoted to show how we can recover Kahn-Plotkin sequentiality as a generalized form of stability on sequential structures.

Definition 10 Let (X, X^{∗}) be a sequential structure. A subset A of X is linearly coherent if it is finite, non-empty and

∀α ∈ X^{∗} A ⊆ ↑ α ⇒ ⋀ A ∈ ↑ α .

We note C^{L}X the set of linearly coherent subsets of X.

A function f : X → Y is linearly stable if it is Scott-continuous and

∀A ∈ C^{L}X f(A) ∈ C^{L}Y and f(⋀ A) = ⋀ f(A) .

To start with, we observe that any linearly stable function is stable. It is a straightforward consequence of the following:

Proposition 8 If (X, X^{∗}) is a sequential structure and B ⊆ X is finite, non-empty and bounded, then B ∈ C^{L}X.

Proof: Let B ⊆ X be finite, non-empty and bounded. If α ∈ X^{∗} is such that B ⊆↑ α, then, by stability of α, ⋀ B ∈↑ α.

Actually, linear stability is much stronger than stability:

Proposition 9 Let (X, X^{∗}) and (Y, Y^{∗}) be sequential structures. A function f : X → Y is linearly stable if and only if it is sequential.

Proof: Let f : X → Y be sequential and let A ⊆ X be linearly coherent. We have to prove that f(A) is linearly coherent and that f(⋀ A) = ⋀ f(A).

Let β ∈ Y^{∗} be such that f(A) ⊆ ↑ β. If ⋀ f(A) ∉ ↑ β then f(⋀ A) ∉ ↑ β, since f(⋀ A) ≤ ⋀ f(A) by monotonicity of f. Hence by sequentiality of f at ⋀ A there exists α ∈ X^{∗} such that ⋀ A ∉ ↑ α and A ⊆ ↑ α, and this is absurd by linear coherence of A. If f(⋀ A) < ⋀ f(A) then by separation there exists β ∈ Y^{∗} such that ⋀ f(A) ∈ ↑ β and f(⋀ A) ∉ ↑ β and by sequentiality of f at ⋀ A we get a contradiction as above.

Conversely, let f : X → Y be linearly stable, Let x ∈ X and β ∈ Y^{∗} be such that f(x) ∉ ↑ β. Let C ⊆ X be the set of points c ∈ X compatible with x and minimal such that f(c) ∈ ↑ β. By stability of f, the elements of C are compact and pairwise unbounded. Moreover:

∀x′ ≥ x f(x′) ∈ ↑ β ⇔ ∃c ∈ C x′ ≥ c .

If C is empty, then ∅ is a sequentiality index for β at x (in this case there is no x′ ≥ x such that f(x′) ∈ ↑ β).

If C = {c} then f(x ∨ c) ∈ ↑ β, hence x ∨ c > x since f(x) ∉ ↑ β. By separation there exists α ∈ X^{∗} such that x ∨ c ∈ ↑ α and x ∉ ↑ α. Such a α is a sequentiality index for β at x.

If C contains at least two elements and is finite, it cannot be linearly coherent, since otherwise f(⋀ C) = ⋀ f(C) and ⋀ f(C) ∈ ↑ β, hence f(⋀ C) ∈ ↑ β, absurd by minimality of the elements of C. Since C is not linearly coherent, there exists α ∈ X^{∗} such that C ⊆ ↑ α and ⋀ C ∉ ↑ α. For keeping such a α as sequentiality index for β at x, it remains to show that x ∉ ↑ α. But if x ∈ ↑ α then by fact 2, for all c ∈ C, we have c ∧ x ∈ ↑ α and hence ⋀_{c∈C}(x ∧ c) ∈ ↑ α and a fortiori ⋀ C ∈ ↑ α; contradiction.

The last case we have to consider is ♯C = ∞. Any element of C is compact and any finite (non-singleton) subset of C is not linearly coherent (as above). Let (c_{i})_{i∈ω} be an enumeration of C, C_{i} = {c_{j} | j ≤ i + 1} and Γ_{i} = {α ∈ X^{∗} | C_{i} ⊆ ↑ α and ⋀ C_{i} ∉ ↑ α}. For each i ∈ ω, the set {Γ_{i}}_{i∈ω} is finite by definition 8, and it is non-empty because C_{i} is not linearly coherent. Since the sequence (⋀ C_{i})_{i∈ω} is a decreasing sequence of compact elements there exists by property I an integer n such that, for all i greater than n, ⋀ C_{i} = ⋀ C_{n}. Let us choose such an integer n. The sequence (Γ_{i+n})_{i∈ω} is a decreasing sequence of finite and non-empty sets so it has a non-empty intersection. Let α ∈ ⋂_{i∈ω} Γ_{i+n}. Then α is a sequentiality index for β at x, since it is easy to prove as above that x ∉ ↑ α.

As for Scott-continuous and stable function, there exists a natural notion of open set w.r.t. linearly stable functions:

Definition 11 A subset U of a dI-domain X is linearly stable open (linearly stable for short) if its characteristic map from D to O is linearly stable, or equivalently if for any A ∈ C^{L}X, A ⊆ U ⇒ ⋀ A ∈ U. We write O_{S}(X) for the set of linearly stable open subsets of X.

Not surprisingly linearly stable sets do not give rise to a topology over dI-domains (arbitrary unions fail to preserve linear stability, as in the stable case). Nevertheless linearly stable functions turn out to be exactly those which preserve linearly stable sets by inverse image. Moreover functions which map linear properties on linearly stable sets by inverse image are linearly stable as well (it is easy to see that linear properties are particular cases of linearly stable sets).

Then we have:

Proposition 10 A function f : X → Y is linearly stable iff one of the two following equivalent conditions holds:

i) For all V ∈ O_{S}Y, we have f^{−1}(V) ∈ O_{S}X.

ii) For all β ∈ Y^{∗}, we have f^{−1}(↑ β) ∈ O_{S}X.

Proof: If f is linearly stable, then it satisfies (i) since the composition of two linearly stable maps is linearly stable. If it satisfies (i), it satisfies (ii) because any linearly open subset (i.e. any linear property) of Y is linearly stable. We just have to prove that if f satisfies (ii), it is linearly stable. So assume that (ii) holds for f. Let A ∈ C^{L}X. Let β ∈ Y^{∗} be such that f(A) ⊆ ↑ β. We have A ⊆ f^{−1}(↑ β), and since f^{−1}(↑ β) ∈ O_{S}X, we have ⋀ A ∈ f^{−1}(↑ β), that is f(⋀ A) ∈↑ β, and this implies ⋀ f(A) ∈↑ β, so f(A) ∈ C^{L}Y. For the same reason (since Y^{∗} separates Y) we have ⋀ f(A) = f(⋀ A). Let us prove that f is continuous. Let D be a directed subset of X. We know that f(⋁ D) ≥ ⋁ f(D). Let β ∈ Y^{∗} be such that f(⋁ D) ∈ ↑ β. That is ⋁ D ∈ f^{−1}(↑ β), so there exists an x ∈ D such that x ∈ f^{−1}(↑ β), that is f(x) ∈↑ β, and hence ⋁ f(D) ∈↑ β.

To build a model of PCF, the most natural idea would be to take as morphisms linearly stable functions. Actually, this does not give rise to a cartesian closed category for evaluation is not linearly stable as shown by the following counterexample.

Let X and Y be two sequential structures. Then the canonical choice for (X × Y)^{∗} is X^{∗} + Y^{∗} (indeed, if we aim at a cartesian category, any acceptable choice must be a subset of that one). Take X = (B^{3} → O) and Y = B^{3}. Let b_{1} = (true, false, ⊥), b_{2} = (false, ⊥, true) and b_{3} = (⊥, true, false). For i = 1, 2, 3, let f_{i} be the element of X whose trace is {(b_{i}, ⊤)}. Then in X × Y, the set A = {(f_{i}, b_{i})}_{i=1,2,3} is linearly coherent, since {b_{i}}_{i=1,2,3} and {f_{i}}_{i=1,2,3} are. Indeed, no linear open set contains all the elements of the former, and the elements of the latter are pairwise bounded atoms. But evaluation maps all the elements of A to ⊤, and its glb to ⊥, so it is not linearly stable.

The function g = ⋁_{1≤i≤3} f_{i}, known as Gustave’s function in the literature, is an example due to Berry of a stable and non-sequential function (see [Berry, G. (1979)]).

3 Strong stability

In this section we generalize the previous situation to an abstract notion of domains endowed with “coherence”, and we get a cartesian closed category.

Observe that the usual notion of coherence (that is being upper-bounded) is preserved by subsets, that is if A is coherent and if B ⊆ A then B is coherent too. But linear coherence does not enjoy this property: consider in B^{3} the points b_{1} = (true, false, ⊥), b_{2} = (false, ⊥, true) and b_{3} = (⊥, true, false). It is easy to see that they are lineraly coherent (actually no linear property contains these three points). Nevertheless b_{1} and b_{2} are not linearly coherent since the linear property the trace of which is {(true, ⊥, ⊥), (false, ⊥, ⊥)} contains both but not their glb.

Anyway, it is clear that any singleton is linearly coherent. Furthermore, linear coherence is down-closed w.r.t. the Egli-Milner preorder between subsets.

Definition 12 If (D, ≤) is a poset and if A, B ⊆ D, we say that A is Egli-Milner smaller than B (we write A ⊑ B) if

∀x ∈ A ∃y ∈ B x ≤ y and ∀y ∈ B ∃x ∈ A x ≤ y .

Proposition 11 If A ∈ C^{L}X, B ⊑ A and B is finite then B ∈ C^{L}X.

Proof: Let α ∈ X^{∗} be such that B ⊆ ↑ α. Since every element of A has a lower bound in B, we have A ⊆ ↑ α and hence ⋀ A ∈ ↑ α. So there exists p ∈ tr(α) such that p ≤ ⋀ A. Let x ∈ B Since x ∈ α there exists p′ ∈ tr(α) such that p′ ≤ x. But x has an upper bound in A, which is consequently an upper bound of p and p′. Thus p′ = p, and this holds for any x ∈ B, so ⋀ B ∈ ↑ α. Furthermore, it is clear that B is non-empty (since A is), so B ∈ C^{L}X.

In the sequel, down-closure w.r.t. the Egli-Milner preorder and preservation by directed lub’s will be our only requirements about coherence.

If P is a set we note P_{fin}^{∗}(P) the set of its finite and non-empty subsets.

Definition 13 A dI-domain with coherence (dIC) is a dI-domain X endowed with a subset C(X) of P_{fin}^{∗}(X) which satisfies the following conditions:

• ∀x ∈ X {x} ∈ C(X).

• ∀A ∈ C(X) ∀B ∈ P_{fin}^{∗}(X) B ⊑ A ⇒ B ∈ C(X).

• If D_{1}, …, D_{n} are directed subsets of X such that for any family x_{1} ∈ D_{1}, …, x_{n} ∈ D_{n} we have {x_{1}, … x_{n}} ∈ C(X), then {⋁ D_{1}, …, ⋁ D_{n}} ∈ C(X).

Such a subset of P(X) will be called an acceptable coherence for X.

A strongly stable function from X to Y is a Scott-continuous function f such that for any A ∈ C(X) we have f(A) ∈ C(Y) and ⋀ f(A) = f(⋀ A).

Observe that a bounded, finite and non-empty subset of X is always in C(X) and thus any strongly stable function is stable.

The following is useful:

Proposition 12 If f, g : X → Y are continuous and f is strongly stable, and if g ≤ f, then g is strongly stable.

Proof: Let A ∈ C(X). We have g(A) ⊑ f(A) ∈ C(Y) and thus g(A) ∈ C(Y). Furthermore, if x ∈ A, we have g(⋀ A) = g(x)∧f(⋀ A). Thus g(⋀ A) = ⋀ g(A)∧⋀ f(A) = ⋀ g(A).

If P and Q are two sets and if E is a subset of P × Q, we note E_{P} (resp. E_{Q}) the projection of E on P (resp. the projection of E on Q). If A ⊆ P and B ⊆ Q, we call pairing of A and B any subset E of P × Q such that E_{P} = A and E_{Q} = B.

Proposition 13 If (X, C(X)) and (Y, C(Y)) are two dICs, the usual cartesian product X × Y endowed with the coherence

C(X × Y) = {C ⊆ X × Y | C_{X} ∈ C(X) and C_{Y} ∈ C(Y)}

is the cartesian product of X and Y in the category of dICs and strongly stable maps.

The proof is straightforward (one has essentially to prove that C(X × Y) satisfies the axioms of coherence). From now on we abbreviate (X, C(X)) by X, when no ambiguity is possible.

Proposition 14 Let X and Y be dICs. The domain of strongly stable functions from X to Y, endowed with the stable order, is a dI-domain. It will be noted [X → Y].

Proof: We already know that the space of stable functions from X to Y (stably ordered) is a dI-domain and that any subtrace of the trace of a strongly stable map is the trace of a strongly stable map (by proposition 12).

Let us prove first that [X → Y] enjoys the I-property. Let t ∈ [X → Y] be a compact trace (we consider here [X → Y] as a set of traces ordered by inclusion). Let D be a directed family of traces of stable maps from X to Y such that t ⊆ ⋃ D. We have

t = t ∩ ⋃ D = ⋃{t ∩ s | s ∈ D}

where all the t ∩ s (when s ∈ D) are traces of strongly stable maps (since t and s are bounded, t ∩ s is the trace of a stable map included in t, and so the corresponding map is strongly stable by proposition 12). But t is compact and the family {t ∩ s | s ∈ D} is directed, so there exists s ∈ D such that t ⊆ s, so t is compact in the dI-domain of stable maps from X to Y, so it is finite, and thus has finitely many lower bounds.

Distributivity and algebraicity follow easily from the fact that they hold for stable maps and from proposition 12.

Last, we have to show that any directed family D of strongly stable functions has a least upper bound in [X → Y]. Let D be such a family and let g : X → Y be defined by

g(x) = ⋁_{f∈D} f(x) .

We already know ([Berry, G. (1979)]) that g is the stable least upper bound of D. It remains to show that g is strongly stable. Let A ∈ C(X). We prove first that g(A) ∈ C(Y), using the third axiom of coherences (see definition 13). We know that for all x ∈ A the set D(x) = {f(x) | f ∈ D} is directed. Let B = (y_{x})_{x∈A} be a family of points of Y such that ∀x ∈ A y_{x} ∈ D(x). Since A is finite and D is directed, there exists a function f ∈ D such that B ⊑ f(A) and hence since f is strongly stable we have B ∈ C(Y). So g(A) ∈ C(Y). We show now that g(⋀ A) = ⋀_{x∈A} g(x).

g(⋀ A) = ⋁_{f∈D} f(⋀ A)
= ⋁_{f∈D} ⋀_{x∈A} f(x)
≤ ⋀_{x∈A} ⋁_{f∈D} f(x)
= ⋀_{x∈A} g(x) .

Take any prime element p ≤ ⋀_{x∈A} ⋁_{f∈D} f(x). For all x ∈ A we choose f_{x} ∈ D such that p ≤ f_{x}(x). Since A is finite and D is directed, we can find f ∈ D such that f ≥ f_{x} for any x ∈ A. So p ≤ f(x) for all x ∈ A and thus p ≤ ⋁_{f∈D} ⋀_{x∈A} f(x) = g(⋀ A).

Remark that all the axioms of coherences are used in the previous proof. We note Ev the evaluation map from [X → Y] × X to Y.

Definition 14 We say that F ⊆ [X → Y] is coherent if it is finite, non-empty and for all A ∈ C(X) and for all pairing E of F and A the set Ev(E) = {f(x) | (f, x) ∈ E} is in C(Y) and furthermore

(⋀ F)(⋀ A) = ⋀ Ev(E) .

The set of coherent subsets of [X → Y] is noted C([X → Y]).

In order to prove that C([X → Y]) is an acceptable coherence, we need a lemma:

Lemma 2 Let F and F′ be finite subsets of [X → Y] such that F ∈ C([X → Y]) and F′ ⊑ F. Let q be a prime element of Y and let x ∈ X be such that q ≤ ⋀_{f′∈F′} f′(x). Then there exists a compact a ∈ X such that a ≤ x and (a, q) ∈ ⋂_{f′∈F′} tr(f′).

Proof: For any f′ ∈ F′, we have f′(x) ≥ q. For f′ ∈ F′, let c(f′) be the unique compact of X such that c(f′) ≤ x and (c(f′), q) ∈ tr(f′). We have also

(⋀ F)(x) = ⋀_{f∈F} f(x) ≥ ⋀_{f′∈F′} f′(x) ≥ q

and thus there is a compact a in X such that a ≤ x and (a, q) ∈ tr(⋀ F), hence (a, q) ∈ tr(f) for all f ∈ F. Now, for any f′ ∈ F′, there exists f ∈ F such that tr(f′) ⊆ tr(f). For such a f, we have (c(f′), q) ∈ tr(f) and (a, q) ∈ tr(f). But c(f′) and a are both bounded by x and hence they must be equal. So, for any f′ ∈ F′ we have (a, q) ∈ tr(f′) and this concludes the proof of the lemma.

Proposition 15 The set C([X → Y]) is an acceptable coherence for [X → Y].

Proof: First, if f ∈ [X → Y], then {f} ∈ C([X → Y]) since f is strongly stable. Next, let F and F′ be finite subsets of [X → Y] such that F ∈ C([X → Y]) and F′ ⊑ F. Let A ∈ C(X) and E′ be any pairing of F′ and A. Let E be given by

E = {(f, x) ∈ F × A | ∃f′ ∈ F′ f′ ≤ f and (f′, x) ∈ E′} .

Since F′ ⊑ F, this is a pairing of F and A. We have Ev(E) ∈ C(Y) and Ev(E′) ⊑ Ev(E) and thus Ev(E′) ∈ C(Y).

Let us prove now that, for any x ∈ X we have (⋀ F′)(x) = ⋀_{f′∈F′} f′(x). The direction ≤ is clear. Consider a prime element q of Y such that ⋀_{f′∈F′} f′(x) ≥ q. By lemma 2 we know that there is a compact a ≤ x such that (a, q) ∈ tr(f′) for all f′ ∈ F′. Let q′ ≤ q be prime in Y. Since for all f′ ∈ F′ we have f′(a) ≥ q, we have ⋀_{f′∈F′} f′(a) ≥ q′, so applying again lemma 2, there exists a′ ≤ a such that (a′, q′) ∈ tr(f′) for all f′ ∈ F′. Now, by lemma 1, we know that (a, q) ∈ tr(⋀ F′), and thus (⋀ F′)(x) ≥ q, and we conclude.

Let us prove that (⋀ F′)(⋀ A) = ⋀_{(f′,x)∈E′} f′(x).

We already know that

(⋀ F′)(⋀ A) = ⋀_{f′∈F′} f′(⋀ A) .

But, for any (f′, x) ∈ E′ and any f ∈ F such that f′ ≤ f we have f′(⋀ A) = f(⋀ A)∧f′(x). Thus

⋀_{f′∈F′} f′(⋀ A) = ⋀_{f′∈F′} ⋀{f′(x) ∧ f(⋀ A) | f ∈ F, x ∈ A, f ≥ f′, (f′, x) ∈ E′}

= ⋀_{f′∈F′} (⋀{f′(x) | x ∈ A, (f′, x) ∈ E′} ∧ ⋀{f(⋀ A) | f ∈ F, f′ ≤ f})

= ⋀_{f′∈F′} ⋀{f′(x) | x ∈ A, (f′, x) ∈ E′} ∧ ⋀_{f′∈F′} ⋀{f(⋀ A) | f ∈ F, f′ ≤ f}

= ⋀_{(f′,x)∈E′} f′(x) ∧ ⋀_{f∈F} f(⋀ A)

since F′ ⊑ F. Now, since F is coherent

⋀_{f′∈F′} f′(⋀ A) = ⋀_{(f′,x)∈E′} f′(x) ∧ ⋀_{(f,x)∈E} f(x)
= ⋀_{(f′,x)∈E′} f′(x)

by definition of E.

Last, let D_{1}, …, D_{n} be directed subsets of [X → Y] such that, for any f_{1} ∈ D_{1}, …, f_{n} ∈ D_{n}, we have {f_{1}, …, f_{n}} ∈ C([X → Y]). For 1 ≤ i ≤ n, let g_{i} = ⋁ D_{i}. We prove that G = {g_{1}, …, g_{n}} ∈ C([X → Y]). For A ∈ C(X), we take a pairing of G and A that we define as a pairing E of {1, …, n} and A. First, {g_{i}(x)}_{(i,x)∈E} ∈ C(Y). Actually, for any (i, x) ∈ E, let D_{i,x} = D_{i}(x). Take any family (f_{i,x}(x))_{(i,x)∈E} in these sets. Since A is finite, we may find functions f_{1} ∈ D_{1}, …, f_{n} ∈ D_{n} such that, for all x ∈ A, f_{i} ≥ f_{i,x}, and thus {f_{i,x}(x)}_{(i,x)∈E} ⊑ {f_{i}(x)}_{(i,x)∈E}. But the latter set is in C(Y) since {f_{i}}_{i=1,...,n} ∈ C([X → Y]). Next, we prove that (⋀ G)(⋀ A) = ⋀_{(i,x)∈E} g_{i}(x). On one hand

⋀_{(i,x)∈E} g_{i}(x) = ⋀_{(i,x)∈E} ⋁_{f∈D_{i}} f(x)

call this point u. On the other hand,

(⋀ G)(⋀ A) = ⋁_{f⃗∈D}( ⋀_{i=1}^{n} f_{i})(⋀ A)

by distributivity, where D = D_{1} × … × D_{n}. So

(⋀ G)(⋀ A) = ⋁_{f⃗∈D}( ⋀_{(i,x)∈E} f_{i}(x))

call this point v. It is clear that v ≤ u. Take any prime q of Y such that q ≤ u, that is

∀(i, x) ∈ E ∃f_{i,x} ∈ D_{i} f_{i,x}(x) ≥ q .

Take such a family (f_{i,x})_{(i,x)∈E}. Since A is finite, we may find some family f⃗ ∈ D such that ∀(i, x) ∈ E f_{i} ≥ f_{i,x}, and so

∃f⃗ ∈ D ∀(i, x) ∈ E f_{i}(x) ≥ q

that is v ≥ q.

From proposition 15, it results that Ev is a strongly stable map. In fact we have taken the greatest possible coherence on [X → Y] making Ev strongly stable. To conclude that the category is cartesian closed, it remains to prove that “curryfication” is strongly stable.

Proposition 16 If f : Z × X → Y is a strongly stable function, then for all z ∈ Z the function f^{z} : X → Y defined by f^{z}(x) = f(z, x) is strongly stable. Moreover the function g : Z → [X → Y] defined by g(z) = f^{z} is strongly stable.

Proof: Actually, we already know the corresponding result for stable functions, and in that case, for all z ∈ Z,

tr(f^{z}) = {(a, q) | ∃d ≤ z ((d, a), q) ∈ tr(f)} .

The fact that, for any z ∈ Z, the function f^{z} is strongly stable is clear, since {z} ∈ C(Z). We prove now that, for any C ∈ C(Z), the following holds:

f^{⋀ C} = ⋀_{z∈C} f^{z} .

The direction ≤ is clear. Let us prove the converse. Take any (a, q) ∈ tr(⋀_{z∈C} f^{z}) ⊆ ⋂_{z∈C} tr(f^{z}). Let C′ = {d | ∃z ∈ C d ≤ z and ((d, a), q) ∈ tr(f)}. We have C′ ⊑ C and we know that C′ is finite, indeed its cardinality is bounded by the cardinality of C. Actually, if d, d′ ∈ C′ are bounded by the same element of C, they must be equal. Thus C′ ∈ C(Z) and hence we must have f(⋀ C′, a) ≥ q. But this implies that C′ is a singleton {d_{0}} because the elements of C′ are pairwise unbounded and are minimal points d ∈ Z such that f(d, a) ≥ q. Hence we conclude

∃d∀z ∈ C d ≤ z and ((d, a), q) ∈ tr(f)

and thus (a, q) ∈ tr(f^{⋀ C}).

Take any C ∈ C(Z). We prove that g(C) ∈ C([X → Y]). We take a pairing of g(C) with a set A ∈ C(X), that is a pairing E of C with A. The fact that {f^{z}(x) | (z, x) ∈ E} ∈ C(Y) results from the fact that f is strongly stable, because E ∈ C(Z × X). Next, we compute

⋀_{(z,x)∈C} f^{z}(x) = ⋀_{(z,x)∈C} f(z, x)
= f(⋀ C, ⋀ A)
= f^{⋀ C}(⋀ A)
= ( ⋀_{z∈C} f^{z})(⋀ A)

and this is what we wanted. But we have proven above precisely that g(⋀ C) = ⋀ g(C) so g is a strongly stable function.

To summarize:

Theorem 1 The category dIC of dICs with strongly stable functions as morphisms is cartesian closed.

Using previous propositions, it is routine to prove this fact. See [MacLane, S. (1971)] for categorical details. Actually dIC is a Λ-category in the sense of [Berry, G. (1979)], section 3.3.5. There exists a standard method for getting a model of PCF out of a Λcategory, once ground types are interpreted (the flat domains of integers and booleans are canonically chosen) and this model satisfies the finite approximations theorem. Let us see for instance how recursion operators are interpreted. Let X be a dIC. By cartesian closure, each functional Y_{n} : [X → X] → X defined by Y_{n}(f) = f^{n}(⊥) is strongly stable. Furthermore the sequence (Y_{n})_{n∈ω} is increasing with respect to the stable order (it is already true in the stable case). Its limit is the least fixpoint operator.

In [Bucciarelli, A. and Ehrhard, T. (1991)A], we have presented a similar theory of strong stability, but we considered qualitative domains instead of general dIdomains. We have been obliged to shift to dI-domains because of the construction of section 5 (extensional embeddings). However, the category of qualitative domains with coherence is cartesian closed as well.

Definition 15 A qualitative domain with coherence (qDC for short) is a dI-domain with coherence, which is atomic as a dI-domain (that is, any lower bound of a prime element p is either ⊥ or p). The category of qDCs and strongly stable functions is noted qDC.

Proposition 17 The category qDC is a full sub-CCC of the category dIC.

The proof consists in observing that, when X and Y are atomic dICs, then X × Y and [X → Y] are atomic as well. One can consult [Bucciarelli, A. and Ehrhard, T. (1991)A] for more details, and for a direct proof of cartesian closedness (it is slightly simpler than the one we have given here for dICs).

The notion of coherence previously defined for function spaces makes the property expressed in proposition 10 false in general. To be precise, in a dIC X we may define in the usual way the set O_{S}X of strongly stable open sets, and it is false in general that if a function f : X → Y preserves these open sets by inverse image it is strongly stable. Actually, take X = B^{3} and Y = [X → O], and consider the function f : X → Y the trace of which is {(b_{i}, (b_{i}, ⊤))}_{i=1,2,3}. This function is not strongly stable. Actually the image of the coherent set {b_{i}}_{i=1,2,3} is {(b_{i}, ⊤)}_{i=1,2,3} which is not coherent, because of the pairing {((b_{i}, ⊤), b_{i})}_{i=1,2,3}. But any strongly stable open subset of Y which contains two different elements of the image of f is Y itself, because the (b_{i}, ⊤)’s are pairwise bounded in Y, and of course f^{−1}(Y) ∈ O_{S}X. So a strongly stable open subset of Y different from Y contains either none of the (b_{i}, ⊤)’s and then its inverse image by f is empty, or it contains just one of them, say (b_{1}, ⊤), and its inverse image by f is the set of upper bounds of b_{1}. Hence f preserves strongly stable open sets under inverse image. However there is a weakening of proposition 10 which remains true.

Proposition 18 Let X and Y be two dICs, the latter being endowed with a linear coherence. Then f : X → Y is strongly stable iff one of the two following equivalent conditions holds:

i) For all V ∈ O_{S}Y, we have f^{−1}(V) ∈ O_{S}X.

ii) For all β ∈ Y^{∗}, we have f^{−1}(↑ β) ∈ O_{S}X.

The proof is essentially the same as the one of proposition 10.

This proposition is interesting because, up to uncurryfication, the codomain of any term of PCF is a ground type, and so may be endowed with a linear coherence in a strongly stable semantics of the language.

4 Extensionality

In the previous model, we have been obliged to order the functions stablewise, but this induces some problems with respect to full abstraction. We can summarize these problems by saying that the higher order functionals do not reflect the “extensional” behaviour of lambda-calculus.

Let us begin by stating rather informally two extensionality properties that are satisfied by any PCF-definable functional. Let X, Y, Z be non-arrow types, M : (X → Y) → Z a definable functional and f, g : X → Y be two functions. Then

(p1) (∀x ∈ X f(x) ≤ g(x)) ⇒ M(f) ≤ M(g)

(p2) (∀x ∈ X f(x) ↑ g(x)) ⇒ M(f) ↑ M(g)

(see [Curien, P.-L. (1993)], page 359 for proofs). These properties state that definable functionals behave well w.r.t. the extensional (i.e. pointwise) order between functions. As soon as one deals with categories of stable functions, in order to define more adequate models, it is necessary to adopt stable ordering, because evaluation has to be stable.

The first problem caused by stable ordering at higher types, as shown in [Berry, G. (1979)], section 4.72, lies in the possibility of defining stable functionals which are not increasing w.r.t. the extensional order, and hence which do not satisfy (p1).

Let us consider an example borrowed from [Berry, G. (1979)], section 4.7.1. The set O → O = {λx. ⊥, λx.x, λx.⊤} is linearly ordered by pointwise order (λx. ⊥≤ λx.x ≤ λx.⊤), but λx.x and λx.⊤ are not upper bounded w.r.t. the stable order. Consider now the functional T : (O → O) → B defined by

T (λx. ⊥) =⊥, T (λx.x) = true, T (λx.⊤) = false .

T is clearly a stable functional, but it does not satisfy (p1).

Berry’s idea in order to eliminate elements like T from the model consists in enriching the structure of domains, by keeping at the same time a stable and an extensional order and by requiring continuity of morphisms w.r.t. the two orders, and stability w.r.t. the stable one. We do not go into the details of Berry’s definition of biordered structure (see [Berry, G. (1979)], section 4.7), but rather we show that this approach does not take into account property (p2) of definable functionals, by means of an example ([Curien, P.-L. (1993)], page 357): let f, g : B^{2} → B be the “left or” and the “right or” functions respectively, defined by

tr(f) = {((true, ⊥), true), ((false, true), true), ((false, false), false)}

and

tr(g) = {((⊥, true), true), ((true, false), true), ((false, false), false)}

and let S : (B^{2} → B) → B be the functional defined by tr(S) = {(f, true), (g, false)}.

In an extensional framework S does not exist, because f and g are bounded by the “parallel or” function, and hence an increasing functional cannot take incoherent (i.e. not upper bounded) values on f and g respectively. As “parallel or” does not exist in the stable framework, S is a stable functional which is not definable because of (p2).

But S is not eliminated by Berry’s construction of biordered structures: actually S is increasing w.r.t. the pointwise order on the space of stable functions from B^{2} to B, because the “parallel or” function does not exist in that space.

This suggests to “refine” Berry’s construction by keeping not only two orders, but also two domains: a stably ordered domain of stable functions embedded in a domain of continuous functions, ordered pointwise, in which non stable functions like “parallel or” do exist. Morphisms have then to be stable (actually strongly stable in our approach) functions which satisfy some extensionality constraints, expressed in terms of the extensional domains, which force properties like (p1) and (p2). This approach leads to the definition of a model which turns out to be “finer” than the continuous one, as we shall see in section 6.

5 Extensionally Embedded dI-Domains with Coherence

We turn now the ideas of the previous section into a formal framework, in order to define a category of “extensional” dICs. To make more readable the treatment of function spaces in the category we are going to define, we give the definition of extensionally embedded dI-domains with coherence (EdIs for short) in two steps.

Definition 16 An extensionally embedded pre-dI-domain with coherence (EPdI) is a triple (S, E, i) where S is a bounded complete and distributive cpo endowed with a coherence C(S) satisfying the axioms of definition 13, E is a Scott domain and i : S → E is a continuous injection which preserves arbitrary lubs and such that

∀a, b, c ∈ S (a ↑ b and i(c) ≤ i(a) ∧ i(b)) ⇒ i(c) ≤ i(a ∧ b) .

This last property will be called external stability. A map satisfying the properties required for i will be called an extensional embedding from S into E.

In this definition we do not require S to be algebraic. We can already define the notion of strongly stable and extensional morphism between EPdIs.

Definition 17 Let (S, E, i), (S′, E′, i′) be EPdIs. A function φ : S → S′ is an extensional strongly stable (ESS) function if it is strongly stable and:

(e1) ∀a, b ∈ S i(a) ≤ i(b) ⇒ i′(φ(a)) ≤ i′(φ(b)) .

(e2) If B ⊆ S is such that i(B) is bounded then the set i′(φ(B)) is bounded.

Conditions (e1) and (e2) are intended to insure that morphisms behave well w.r.t. the partial orders of E and E′, in the sense that, if φ : S → S′ satisfies conditions (e1) and (e2), one can define a function \overline{φ} : E → E′ by \overline{φ}(x) = ⋁\{i′(φ(a)) | a ∈ K(S) and i(a) ≤ x\}, and that this function is monotone. Observe also that \overline{φ} is continuous as soon as i preserves compactness; this further condition will be required in the definition of EdIs. Algebraicity of S is expressed in a form that makes it easy to prove the same property for function spaces.

Definition 18 An extensional embedded dI-domain with coherence (EdI) is a tuple (S, E, i, (ψ_{n})_{n∈ω}) such that (S, E, i) is an EPdI and:

• Each ψ_{i} is a strongly stable function from S to S which satisfies ψ_{i} ∘ ψ_{i} = ψ_{i}.

• For all i ∈ ω, the range of ψ_{i} is finite.

• For all i ∈ ω, ψ_{i} ≤ ψ_{i+1} w.r.t. the stable order.

• ⋁_{i∈ω} ψ_{i} = Id .

Moreover we require that i preserve compactness, that is if a is compact in S then i(a) is compact in E.

Proposition 19 If (S, E, i, (ψ_{n})_{n∈ω}) is an EdI then S is a dI-domain.

Proof: We know by definition that S is a bounded complete distributive cpo, hence we have just to prove that S is algebraic and satisfies the I property. The first remark is that any element in the range of a ψ_{i} is compact. Actually if ψ_{i}(a) ≤ ⋁ D where D is directed in S, then ψ_{i}(a) = ψ_{i}(ψ_{i}(a)) ≤ ψ_{i}(⋁ D) = ⋁{ψ_{i}(d) | d ∈ D}. Now {ψ_{i}(d) | d ∈ D} is a finite directed set, hence it contains its lub, and such a lub is the image by ψ_{i} of some element d ∈ D. Hence we obtain ψ_{i}(a) ≤ ψ_{i}(d) ≤ d ∈ D. Now for all a ∈ S we get by hypothesis a = ⋁_{i∈ω} ψ_{i}(a), and hence algebraicity of S. To show that S satisfies the I property, let a ∈ K(S). As a = ⋁_{i∈ω} ψ_{i}(a), there exists i_{0} such that ψ_{i_{0}}(a) = a. Now if b ≤ a we get ψ_{i_{0}}(b) = b ∧ ψ_{i_{0}}(a) = b ∧ a = b, as ψ_{i_{0}} ≤ Id. Hence {b ∈ S | b ≤ a} is a subset of the range of ψ_{i_{0}} which is finite. The definition of extensional strongly stable functions between EdIs is exactly the same as before, that is we require φ : S → S′ to be strongly stable and to satisfy (e1) and (e2)

Proposition 20 If φ : S → S′ is an extensional strongly stable function, then \overline{φ} : E → E′ defined by \overline{φ}(x) = ⋁\{i′(φ(a)) | a ∈ K(S) and i(a) ≤ x\} is continuous, and i ∘ \overline{φ} = φ ∘ i′.

Proof: We just outline the proof. The fact that \overline{φ} is well defined follows from property (e2) of φ and from bounded completeness of E′ and \overline{φ} is monotone by property (e1) of φ. Continuity follows from the fact that i preserves compactness. Finally the stated equation is an easy consequence of (e1) (actually algebraicity of S is also needed).

So the following diagram commutes:

\begin{matrix}E & ⟶^{\overline{φ}} & E′ \\ ^{i}↑ & & _{i′}↑ \\ S & ⟶^{φ} & S′ \end{matrix}

It is easy to see that composition of ESS functions is ESS, and that the identity is ESS. We are interested in proving that the category of EdIs and ESS functions (ESS for short) is cartesian closed.

The cartesian product is essentially trivial.

Proposition 21 Let X = (S, E, i) and X′ = (S′, E′, i′) be two EdIs. Then (S × S′, E × E′, i × i′) is an EdI and it is the cartesian product of X and X′ in ESS.

We do not give the proof which is straightforward.

The existence of function spaces is less easy to prove. We proceed in several steps. From now on, X = (S, E, i) and X′ = (S′, E′, i′) will be two fixed EdIs.

Proposition 22 Let T be the set of all extensional strongly stable functions from X to X′. Then T endowed with the stable ordering is a bounded complete and distributive cpo.

Proof: We have to prove directed completeness, bounded completeness and distributivity.

• Directed completeness. Let D be a directed family of extensional stable functions from X to X′. Let ψ : S → S′ be defined by ψ(a) = ⋁_{φ∈D} φ(a). We check that it is a strongly stable function and that it is the stable lub of D like in the proof of proposition 14. We have to prove that it satisfies the two axioms of extensionality for functions. Let first a, b ∈ S be two points such that i(a) ≤ i(b). Since i′ is continuous, i′ψ(a) = ⋁_{φ∈D} i′φ(a), so since each φ ∈ D is extensional i′ψ(a) ≤ ⋁_{φ∈D} i′φ(b) = i′ψ(b). Let B ⊆ S be such that i(B) is bounded. For each φ ∈ D, we know that i′φ(B) is bounded, let y_{φ} be the lub of this set in E′. The set {y_{φ} | φ ∈ D} is directed since D is. The lub y of this set is an upper bound of each i′ψ(b) when b ∈ B. Actually, i′ψ(b) = ⋁_{φ∈D} i′φ(b) and each i′φ(b) is smaller than y_{φ} and hence than y.

• Bounded completeness. We know that the lub of a bounded family of extensional strongly stable functions is a strongly stable function (actually, it is stably bounded by a strongly stable function). We prove that it is extensional as before, using the fact that i′ preserves bounded lubs.

• Distributivity. It is enough to prove that if φ and φ′ are two bounded extensional stable functions, their stable glb ψ given by ψ(a) = φ(a) ∧ φ′(a) is extensional, for we know that distributivity holds for strongly stable maps. So let φ and φ′ be two such functions. Let a, b ∈ S be such that i(a) ≤ i(b). We have i′φ(a) ≤ i′φ(b) and i′φ′(a) ≤ i′φ′(b), hence i′(φ(a) ∧ φ′(a)) ≤ i′φ(b) ∧ i′φ′(b) and we get i′(φ(a) ∧ φ′(a)) ≤ i′(φ(b) ∧ φ′(b)) by external stability of i′. Next let B ⊆ S be such that i(B) is bounded. Then i′(φ ∧ φ′)(B) is bounded e.g. by the lub of i′φ(B) which we know to exist.

Now, let F be the Scott domain of continuous functions from E to E′. Let I : T → F be defined by I(φ) = \overline{φ}. Then

Proposition 23 The map I is an extensional embedding.

Proof: Continuity of I follows easily from continuity of i′. Actually, if D is directed we get:

I(⋁ D)(x) = ⋁_{i(a)≤x} i′((⋁ D)(a))
= ⋁_{i(a)≤x} i′( ⋁_{φ∈D} φ(a))
= ⋁_{i(a)≤x} ⋁_{φ∈D} i′(φ(a))
= ⋁_{φ∈D} ⋁_{i(a)≤x} i′(φ(a))
= ⋁_{φ∈D} I(φ)(x)

the variable a in these expressions ranging over compact elements of S. The proof that I commutes with arbitrary lubs is exactly the same as before, as that property holds for i′. It remains to prove that if φ and ψ are bounded in T and θ ∈ T is such that I(θ) ≤ I(φ)∧I(ψ) then I(θ) ≤ I(φ ∧ ψ). Note that for all a ∈ S, (φ ∧ ψ)(a) = φ(a) ∧ ψ(a), φ and ψ being bounded, hence, as i′ enjoys external stability, for all a ∈ S we get i′(θ(a)) ≤ i′(φ ∧ ψ)(a).

The last step for showing that (T, F, I) is an EPdI consists in endowing T with a coherence C(T). We use the canonical definition given in section 3. Hence we can state the following

Proposition 24 (T, F, I) is an EPdI.

To show that (T, F, I) is actually an EdI we have to define a chain (Ψ_{n})_{n∈ω} of functions from T to T as in definition 18. We know by definition that S and S′ are endowed respectively with (ψ_{n})_{n∈ω} and (ψ′_{n})_{n∈ω}, hence it is quite natural to define Ψ_{n}(φ) = ψ′_{n} ∘ φ ∘ ψ_{n}.

If f is a function, let us note rg(f) its range.

Proposition 25 The sequence (Ψ_{n})_{n∈ω} defined by Ψ_{n}(φ) = ψ′_{n} ∘ φ ∘ ψ_{n} satisfies the properties expressed in definition 18.

Proof: We have to prove that for all n, Ψ_{n} is an extensional strongly stable function with finite range such that Ψ_{n} ∘ Ψ_{n} = Ψ_{n}, that Ψ_{n} ≤ Ψ_{n+1} w.r.t. the stable order, and last that ⋁_{n∈ω} Ψ_{n} = Id_{T →T}.

• extensional strong stability. As usual we prove only extensionality, strong stability being insured by cartesian closedness of dIC. Let φ, φ′ ∈ T be such that \overline{φ} ≤ \overline{φ′}, and let n ∈ ω. For all a ∈ S we get \overline{φ}(iψ_{n}(a)) ≤ \overline{φ′}(iψ_{n}(a)) that is i′φ(ψ_{n}(a)) ≤ i′φ′(ψ_{n}(a)) and thus since ψ′_{n} is extensional i′(ψ′_{n}(φ(ψ_{n}(a)))) ≤ i′(ψ′_{n}(φ′(ψ_{n}(a)))) and hence \overline{Ψ}_{n}(φ) ≤ \overline{Ψ}_{n}(φ′). If B is a subset of T such that I(B) is bounded by h, it is easy to see that \overline{Ψ}_{n}(B) is bounded by h.

• Ψ_{n} has finite range. Let E be the equivalence relation over S′ defined by: b E b′ iff ψ′_{n}(b) = ψ′_{n}(b′). As rg(ψ′_{n}) is finite, E has finitely many equivalence classes. Now let E be the equivalence relation over T defined by: φ E φ′ iff ∀x ∈ rg(ψ_{n}) φ(x) E φ′(x). The equivalence relation E has finitely many classes (actually less then ♯E^{♯rg(ψ_{n})}, where ♯E stands for the number of classes of E), hence it is enough to show that if φ E φ′ then Ψ_{n}(φ) = Ψ_{n}(φ′). If φ E φ′ and a ∈ S, we get by definition φ(ψ_{n}(a)) E φ′(ψ_{n}(a)) and hence Ψ_{n}(φ)(a) = Ψ_{n}(φ′)(a), and we are done.

The fact that (Ψ_{n})_{n∈ω} is an increasing chain which converges to the identity and that, for all n ∈ ω, Ψ_{n} ∘ Ψ_{n} = Ψ_{n} is standard in stability theory, see e.g. [Berry, G. (1979)], section 4.7.

The last thing to prove in order to show that (T, F, I) is actually an EdI is that I preserves compactness.

Proposition 26 If φ ∈ T is compact, then I(φ) = \overline{φ} is compact.

Proof: We know that, for any compact element φ of T, there exists an integer n such that φ = Ψ_{n}(φ). Hence it is enough to show that for any φ ∈ T and for any n ∈ ω, the function I(Ψ_{n}(φ)) is compact. By definition we have

I(Ψ_{n}(φ))(x) = ⋁{i′(ψ′_{n}(φ(ψ_{n}(a)))) | i(a) ≤ x and a ∈ K(S)}
= ⋁{i′(ψ′_{n}(φ(a))) | i(a) ≤ x and a ∈ rg(ψ_{n})}

hence we get I(Ψ_{n}(φ)) = ⋁{[i(a), i′(ψ′_{n}(φ(a)))] | a ∈ rg(ψ_{n})}, where [x, y] is the function that maps z on y if x ≤ z and on ⊥ otherwise (step function). Hence I(Ψ_{n}(φ)) is compact, being the lub of a finite set of compact step functions. We can now state the following

Proposition 27 (T, F, I) is an EdI.

In order to show that with this choice of function spaces we get a cartesian closed category, we have to prove that evaluation and abstraction are extensional strongly stable morphisms. As usually we shall just prove extensionality, strong stability being a consequence of the general case treated in section 3.

Proposition 28 The function Ev : T × S → S′ defined by Ev(φ, a) = φ(a) is ESS.

Proof: Let φ, φ′ ∈ T be such that \overline{φ} ≤ \overline{φ′} and a, a′ ∈ S such that i(a) ≤ i(a′). We have

i′(Ev(φ, a)) = i′(φ(a)) = \overline{φ}(i(a)) ≤ \overline{φ}(i(a′)) ≤ \overline{φ′}(i(a′)) = i′(Ev(φ′, a′)) .

If B ⊆ T × S is such that (I × i)(B) is bounded by (g, z), we get i′(Ev(B)) = {i′(φ(a)) | (φ, a) ∈ B\} = \{\overline{φ}(i(a)) | (φ, a) ∈ B\}, and this set is bounded by g(z) by hypothesis. Let us show now that abstraction is ESS.

Proposition 29 Let (U, H, j) be an EdI, and φ : U × S → S′ be an extensional strongly stable function. Let Φ : U → (S → S′)) be defined by Φ(c) = φ^{c} : S → S′ where φ^{c}(a) = φ(c, a). Then, for all c ∈ U, φ^{c} is ESS and furthermore the function Φ is ESS.

Proof: We just prove extensionality.

• φ^{c} is ESS. Let a, a′ ∈ S be such that i(a) ≤ i(a′). We get i′(φ^{c}(a)) = i′(φ(c, a)) ≤ i′(φ(c, a′)) = i′(φ^{c}(a′)). If B ⊆ S is such that i(B) is bounded than i′(φ^{c}(B)) = {i′(φ(c, a)) | a ∈ B} is bounded by extensionality of φ.

• Φ is ESS. Let c, c′ ∈ U be such that j(c) ≤ j(c′). For proving that \overline{Φ(c)} ≤ \overline{Φ(c′)} it is enough to show that, for all a ∈ S, i′(Φ(c)(a)) ≤ i′(Φ(c′)(a)). Just remark

i′(Φ(c)(a)) = i′(φ(c, a)) ≤ i′(φ(c′, a)) = i′(Φ(c′)(a)) ,

the central inequality coming from extensionality of φ. Last, if B ⊆ U is such that j(B) is bounded by z, let us define h : E → E′ by h(x) = \overline{φ}(z, x). We get, for all c ∈ B and for all x ∈ E,

\overline{Φ(c)}(x) = \overline{φ}(i(c), x) ≤ \overline{φ}(z, x) = h(x)

hence h is an upper bound for \overline{Φ}(B).

We can now summarize:

Theorem 2 The category ESS is cartesian closed.

Moreover it is easy to see that ESS is a Λ-category, and hence that it provides a model of PCF (see [Berry, G. (1979)], section 3.3)

In the sequel, we shall note [X → Y] the previously described exponential of two EdI’s X and Y.

6 About the theory induced by ESS on PCF

In this section we compare the theories of the models ESS and CONT, the latter being the standard Scott model. The result that we obtain (theorem 3) is an a posteriori justification of the construction performed in section 5.

In order to make the following proofs more readable, we shall note, if X is an EdI, S^{X} its intensional part (the dI-domain), E^{X} its extensional part (the Scott domain) and i^{X} the embedding, so that X = (S^{X}, E^{X}, i^{X}). The finite projections ψ_{n} that are part of the structure will be kept implicit (indeed, they do not play any role in the following). We shall generally note the injection i^{X} simply i when there is no ambiguity about the object of the category ESS we are dealing with.

We work with a version of PCF which has ι, the type of integers, as unique ground type. We shall often write σ_{1}, …, σ_{n} → σ a type σ_{1} → (… (σ_{n} → σ) …), so that any type can be written σ_{1}, …, σ_{n} → ι. (The only type constructor is “→”; there is no cartesian product in the syntax.)

The language is based on a certain number of basic “constants” which are given with an integer arity. If c is a constant of arity k, then its type is ι → … → ι (with k arrows) that we also write ι^{k} → ι. If the arity of c is 0, then c is simply a constant of type ι.

In the semantics, the type ι will always be interpreted as the usual flat domain ι_{⊥}. In the model ESS, ι is interpreted as the triple (ι_{⊥}, ι_{⊥}, Id) which trivially satisfies the required axioms, the coherence of ι_{⊥} being the linear one: a subset A of ι_{⊥} is coherent if it is a singleton or if it is finite and contains ⊥.

The notion of model of PCF we shall consider here is the one used by Berry in his thesis (see [Berry, G. (1979)], section 3.5). Indeed, ESS is a model in this sense; we have already said that it is a Λ-category, and we have chosen an interpretation for the type of integers.

If M is a model of PCF, we shall use the following notations :

• If σ is a type of PCF, [σ]^{M} will be the object of M which interprets σ in the model.

• If M is a term of PCF of type σ with free variables x_{1}, …, x_{n} of respective types σ_{1}, …, σ_{n} and if ρ is an environment (so that ρ(x_{k}) ∈ [σ_{k}]^{M}), then the semantics of M in this environment will be written [M]_{ρ}^{M}, and it will be an element of the object [σ]^{M} of M.

We prove first a technical lemma about the model ESS which will be the key result for what follows.

Lemma 3 Let X_{1}, …, X_{k}, Y_{1}, …, Y_{n} be EdIs, and let

Φ : [X_{1} → ι_{⊥}] × … × [X_{k} → ι_{⊥}] × Y_{1} × … × Y_{n} → ι_{⊥}

be an ESS function. Let φ_{l} : S^{X_{l}} → ι_{⊥} for 1 ≤ l ≤ k be ESS functions, f_{l} : E^{X_{l}} → ι_{⊥} for 1 ≤ l ≤ k be continuous functions such that, for all l and for all a ∈ S^{X_{l}} we have φ_{l}(a) = f_{l}(i(a)) (in ι_{⊥}). Last let b_{j} ∈ S^{Y_{j}} for 1 ≤ j ≤ n. Then we have

i(Φ)(f_{1}, …, f_{k}, i(b_{1}), …, i(b_{n})) = Φ(φ_{1}, …, φ_{k}, b_{1} …, b_{n})

in ι_{⊥}.

Proof: Since clearly we have i(φ_{l}) ≤ f_{l} (in the extensional ordering, of course) the inequality

i(Φ)(f_{1}, …, f_{k}, i(b_{1}), …, i(b_{n})) ≥ Φ(φ_{1}, …, φ_{k}, b_{1} …, b_{n})

holds, for Φ(φ_{1}, …, φ_{k}, b_{1} …, b_{n}) = i(Φ)(i(φ_{1}), … i(φ_{k}), i(b_{1}), …, i(b_{n})).

Now assume that i(Φ)(f_{1}, …, f_{k}, i(b_{1}), …, i(b_{n})) is equal to a non-bottom element p of ι_{⊥}. By the very definition of i(Φ) which is \overline{Φ}, we can find, for all l ∈ \{1, …, k\}, a map ψ_{l} : S^{X_{l}} → ι_{⊥} in ESS such that i(ψ_{l}) ≤ f_{l} and Φ(ψ_{1}, …, ψ_{k}, b_{1}, …, b_{n}) = p. Let l ∈ {1, …, k} and let x ∈ E^{X_{l}}. We have :

i(ψ_{l})(x) = ⋁{ψ_{l}(a) | a ∈ K(S^{X_{l}}) and i(a) ≤ x}
= ⋁{i(ψ_{l})(i(a)) | a ∈ K(S^{X_{l}}) and i(a) ≤ x}
≤ ⋁{f_{l}(i(a)) | a ∈ K(S^{X_{l}}) and i(a) ≤ x}
= ⋁{φ_{l}(a) | a ∈ K(S^{X_{l}}) and i(a) ≤ x}
= i(φ_{l})(x) .

(We have used the hypothesis about the φ_{l}’s and the f_{l}’s.) So we have i(ψ_{l}) ≤ i(φ_{l}) for all l. We know that Φ satisfies the extensionality requirement (e1) of definition 17, and thus

Φ(φ_{1}, …, φ_{k}, b_{1}, …, b_{n}) ≥ Φ(ψ_{1}, …, ψ_{k}, b_{1}, …, b_{n}) = p

and we conclude since ι_{⊥} is flat.

CONT is the standard Scott model of PCF, with ι still interpreted as ι_{⊥}. If ρ is an environment in the model ESS, we note i(ρ) the environment in the model CONT defined by i(ρ)(x) = i(ρ(x)) for any variable x of PCF. Observe that, for any type σ of PCF, we have [σ]^{CONT} = E^{[σ]ESS}.

Proposition 30 Let M be a term of PCF of type σ_{1}, …, σ_{n} → ι. Let ρ be an environment in ESS, and let a_{l} ∈ S^{[σ_{l}]ESS} (for 1 ≤ l ≤ n). Then

[M]CONT_{i(ρ)}(i(a_{1})) … (i(a_{n})) = [M]ESS_{ρ}(a_{1}) … (a_{n})

(this equality holds in ι_{⊥}).

Proof: For both models CONT and ESS are models of η-conversion and enjoy the finite approximations theorem (they are Λ-categories, see [Berry, G. (1979)]), we just have to prove the result for completely η-expanded finite Böhm-trees (that is, the η-expanded normal forms of PCF enriched with the constant Ω of type ι). The syntax (and the typing) of these Böhm-trees can be described as follows (types of terms and variables are written as superscripts when necessary) :

M^{ι} = c^{ι^{k}→ι}M_{1}^{ι} … M_{k}^{ι} | x^{σ_{1},...,σ_{n}→ι}M_{1}^{σ_{1}} … M_{n}^{σ_{n}} | Ω

and

M^{σ_{1},...,σ_{n}→ι} = λx_{1}^{σ_{1}} … x_{n}^{σ_{n}}.M^{ι} .

Observe in particular that the fixpoint combinator Y, which is indeed an essential part of the syntax of PCF, does not appear in this recursive definition. This is because, when one considers η-expanded terms of PCF, Y is always applied to some argument, and so the term cannot be normal. For instance, Y^{ι→ι→ι} is approximated by the following sequence of η-expanded Böhm trees :

λx^{ι→ι}.Ω, λx^{ι→ι}.xΩ, λx^{ι→ι}.x(xΩ), …

We prove the result by induction on the structure of Böhm-trees, assuming that the constants are interpreted in the same way in both models. (This implies that a constant of arity ≥ 2 is interpreted as a sequential function, but this is always the case in standard PCF).

If M is a constant of type ι or a variable of type ι, or if M is Ω, the result is obvious since i^{ι_{⊥}} is the identity.

Assume that M = cM_{1} … M_{k} with c a constant of arity k, and call γ the interpretation of c in both models. We have

[M]CONT_{i(ρ)} = γ([M_{1}]CONT_{i(ρ)}, …, [M_{k}]CONT_{i(ρ)})

but by inductive hypothesis, for l ∈ {1, …, k}, we have [M_{l}]CONT_{i(ρ)} = [M_{l}]ESS_{ρ} and we conclude.

Now assume that

M = x^{σ_{1},...,σ_{n}→ι}M_{1}^{σ_{1}} … M_{n}^{σ_{n}} .

Without loss of generality we can assume that there is an integer 1 ≤ k ≤ n such that, for 1 ≤ l ≤ k, the type σ_{l} be functional, say σ_{l} = τ_{1}^{l}, …, τ_{m_{l}}^{l} → ι, and that, for k < l ≤ n, we have σ_{l} = ι. For 1 ≤ l ≤ k, let X_{l} = [τ_{1}^{l}]^{ESS} × … × [τ_{m_{l}}^{l}]^{ESS} and let φ_{l} = [M_{l}]ESS_{ρ}, that we consider as a morphism (in ESS) S^{X_{l}} → ι_{⊥}, and let f_{l} = [M_{l}]CONT_{i(ρ)}, that we consider as a morphism (continuous function) E^{X_{l}} → ι_{⊥}. For k < l ≤ n, let b_{l} = [M_{l}]ESS_{ρ} ∈ ι_{⊥}, which is equal, by inductive hypothesis, to [M_{l}]CONT_{i(ρ)}. If a ∈ S^{X_{l}}, we know by inductive hypothesis that φ_{l}(a) = f_{l}(i(a)). Let Φ = ρ(x). Applying lemma 3, we get

i(Φ)(f_{1}, …, f_{k}, b_{k+1}, …, b_{n}) = Φ(φ_{1}, …, φ_{k}, b_{k+1}, …, b_{n})

since i(b_{l}) = b_{l} for k < l ≤ n. But the left hand side of this equation is [M]CONT_{i(ρ)} and the right hand side is [M]ESS_{ρ}.

Last, assume that M = λx_{1} … x_{k}.N^{ι} with x_{l} of type σ_{l} for 1 ≤ l ≤ k. Let a_{l} ∈ S^{[σ_{l}]ESS} for 1 ≤ l ≤ k. Let ρ be an environment in ESS and let ρ′ be the environment ρ modified by setting ρ′(x_{l}) = a_{l} for 1 ≤ l ≤ k. Then we have [M]CONT_{i(ρ)}(i(a_{1})) … (i(a_{k})) = [N]CONT_{i(ρ′)} and now, by inductive hypothesis, [N]CONT_{i(ρ′)} = [N]ESS_{ρ′} and finally [N]ESS_{ρ′} = [M]ESS_{ρ}(a_{1}) … (a_{k}). This concludes the proof.

The result we just proved is the main tool for comparing the theory of the extensional strongly stable model of PCF with the theory of the continuous model.

We need now to introduce a few notations.

Definition 19 Let M be a model of PCF, and let M and N be to terms of PCF with the same type. We say that M equates M and N and we write M ⊧ M = N if, for any environment ρ in M, we have [M]_{ρ}^{M} = [N]_{ρ}^{M}.

The (equational) theory T(M) of the model M is the set of all equations which are valid in M.

Theorem 3 The theory of ESS is finer than the one of CONT in the sense that T(CONT) ⊆ T(ESS), and this inclusion is strict.

Proof: Let M, N be two terms of type σ of PCF such that CONT ⊧ M = N. Let ρ be an environment in ESS. We must prove that [M]ESS_{ρ} = [N]ESS_{ρ}. Assume that σ = σ_{1}, …, σ_{n} → ι (with possibly n = 0). What we have to prove, since ESS is an extensional model of PCF, is that, for any a_{1} ∈ S^{[σ_{1}]ESS}, …, a_{n} ∈ S^{[σ_{n}]ESS}, we have [M]ESS_{ρ}(a_{1}) … (a_{n}) = [N]ESS_{ρ}(a_{1}) … (a_{n}). But

[M]ESS_{ρ}(a_{1}) … (a_{n}) = [M]CONT_{i(ρ)}(i(a_{1})) … (i(a_{n}))

by proposition 30.

Since CONT ⊧ M = N, we know that [M]CONT_{i(ρ)}(i(a_{1})) … (i(a_{n})) = [N]CONT_{i(ρ)}(i(a_{1})) … (i(a_{n})) and we conclude by applying proposition 30 to N.

The fact that the inclusion T(CONT) ⊆ T(ESS) is strict can simply be justified by the fact that the “parallel or” does not exist in ESS, and hence the two functionals M_{0} and M_{1} introduced by Plotkin in [Plotkin, G. (1977)], p. 234, have the same semantics in our model, but not in the Scott model. A natural question is whether the previous result may be extended to inequational theories. The first thing to do is to define the extensional inequational theory of the model ESS:

ESS ⊧ M ≤ N iff ∀ρ i([M]ESS_{ρ}) ≤ i([N]ESS_{ρ}) .

Then one checks that the continuous inequational theory is included in that one.

References

[Berry, G. (1978)] Stable models of typed lambda-calculi. Proceedings, 5th International Colloquium on Automata, Languages and Programming, Udine, Lecure Notes in Computer Science 62, pp. 72-89, Springer.

[Berry, G. (1979)] Modèles complètement adéquats et stables des lambda-calculs typés. Thèse de Doctorat d’Etat, Université Paris 7.

[Berry, G. and Curien, P.-L. (1982)] Sequential algorithms on concrete data structures. Theoretical Computer Science 20, pp. 265-321.

[Berry, G. and Curien, P.-L. and Levy, J.-J. (1985)] Full abstraction for sequential languages: the state of the art. Proceedings, French-US Seminar on the Applications of Algebra to Language Definition and Compilation, Fontainebleau, june 1982, pp. 89-132, Cambridge University Press.

[Bucciarelli, A. and Ehrhard, T. (1991)A] Sequentiality and strong stability. Proceedings, Logic in Computer Science 1991, Amsterdam, pp. 138-145.

[Bucciarelli, A. and Ehrhard, T. (1991)B] Extensional embedding of a strongly stable model of PCF. Proceedings, 18th International Colloquium on Automata, Languages and Programming, Madrid, Lecure Notes in Computer Science 510, pp. 35-47, Springer.

[Curien, P.-L. (1993)] Categorical Combinators, Sequential Algorithms and Functional Programming. Progress in Theoretical Computer Science, Birkhäuser.

[Girard, J.-Y. (1986)] The system F of variable types, fifteen years later. Theoretical Computer Science 45, pp. 159-192.

[Jim, T. and Meyer, A. (1991)] Full Abstraction and the Context Lemma. Proceedings, Theoretical Aspects of Computer Software, Sendai, Lecture Notes in Computer Science 526, pp. 131-151, Springer.

[Kahn, G. and Plotkin, G. (1978)] Domaines Concrets. Rapport IRIA-LABORIA 336.

[MacLane, S. (1971)] Categories for the Working Mathematician. Graduate Texts in Mathematics 5, Springer.

[Milner, R. (1977)] Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4, pp. 1-23.

[Plotkin, G. (1977)] LCF considered as a programming language. Theoretical Computer Science 5, pp. 223-256.

[Winskel, G. (1988)] An introduction to Event Structures. Lecture Notes in Computer Science 354, pp. 364-397, Springer.

[Vuillemin, J. (1974)] Syntaxe, sémantique et axiomatique d’un langage de programmation simple. Thèse de Doctorat d’Etat, Université Paris 7.

[Zhang, G.Q. (1991)] Logical Domains. Progress in Theoretical Computer Science, Birkhäuser.