Projecting sequential algorithms on strongly stable functions^{∗}

Thomas Ehrhard Laboratoire de Mathématiques Discrètes UPR 9016 du CNRS, 163 avenue de Luminy, case 930 F 13288 MARSEILLE CEDEX 9 ehrhard@lmd.univ-mrs.fr

Abstract

We relate two sequential models of PCF: the sequential algorithm model due to Berry and Curien and the strongly stable model due to Bucciarelli and the author. More precisely, we show that all the morphisms araising in the strongly stable model of PCF are sequential in the sense that they are the “extensional projections” of some sequential algorithms. We define a model of PCF where morphisms are “extensional” sequential algorithms and prove that any equation between PCF terms which holds in this model also holds in the strongly stable model.

Introduction

In previous works ([BE1, BE2, BE4, E]), we introduced the notion of strong stability as an alternative way to deal with sequentiality. Our first observation was that the definition of sequentiality that Kahn and Plotkin have proposed in [KP] could be expressed as a preservation property. To express sequentiality of functions, one needs domains equipped with a suitable notion of “cell”. The domain is then equipped with a “filling relation” between states (elements of the domain) and cells. The intuition is that, if a pair (x, α) is in this relation, then the cell α which should be considered as a “place” (typically, an index in a cartesian product) is filled in the datum x by some “value”. Several values may fill the same cell, but in a given datum, a cell can be filled only by one value. Typically, in a cartesian product of two domains corresponding to ground types (natural numbers, booleans…), there are two cells corresponding to the two components of the product. We observed that a fundamental property of cells which always holds in the frameworks where Kahn-Plotkin sequentiality makes sense is linearity. This means first that, if two bounded states fill the same cell, then their greatest lower bound (glb) also fills this cell (because, in that case, the cell is filled by the same value in both states) and second that, if the least upper bound (lub) of two states fills a cell, then one of the two states must fill that cell. This fundamental property has an important corollary: the set of cells of a cartesian product of two domains equipped with cells must be a subset of the disjoint union of their sets of cells. Actually, in a cartesian product, any element is of the shape (x, y), and one has (x, y) = (x, ⊥)∨(⊥, y) and so if (x, y) fills a cell, it must be the case that (x, ⊥) or (⊥, y) fill that cell (but not both since ⊥ does never fill any cell). This property means that the cells always perform a suitable decomposition of objects, at least when they are built up out of “ground domains” by terms of first order operations like products. (For higher types, which are built using “function spaces”, things become more complicated, and the goal of this paper is precisely to give a new insight on what happens.) For practical reasons, we add an empty cell ⊥ to any set of cells associated with a domain. This cell is filled by no element of the domain.

∗To appear in Annals of Pure and Applied Logic

In that framework, we can formulate the Kahn-Plotkin definition as follows: a function f : X → Y between two domains equipped with cells is sequential if, for any state x of X and any cell β of Y such that f(x) does not fill β, there exists a cell α of X, not filled by x and which is filled by any x′, state of X greater than x such that f(x′) be filled. This can be easily understood if the function f is seen as a deterministic process. Let us assume, in order to simplify a bit, that the target domain Y has only one cell different from ⊥. Now for f(x), there are only two possibilities: either it is undefined (the only cell is empty) or it is defined (the only cell is filled). Assume that we are in the first case. Then there are two possibilities: Either, whatever additional information we give to its input, the process f is unable to fill its output. This situation is described by the Kahn-Plotkin definition: take α = ⊥, the empty cell. Or the process is stuck somewhere in its computation because, in its input datum x, it has found a hole (unfilled cell) α. Since the process is deterministic, it cannot decide that, after all, this lacking information could be replaced by something else: it really needs α to be filled in x in order to fill its output cell. This is precisely what the Kahn-Plotkin definition says: if we increase the information x to a greater piece of data x′ in such a way that the only cell of Y be filled in f(x′), then the cell α where the computational process was stuck in x must be filled in x′.

In order to use this idea of sequentiality for building a model of a functional language like PCF, we need to define a suitable notion of “function space”. The most natural idea is the following: if X and Y are domains equipped with cells, take as space of functions from X to Y the set Z of all Kahn-Plotkin sequential functions from X to Y equipped with a suitable order and a suitable set of cells. The problem is that, until now, all the natural attempts in that direction have failed; it seems impossible to find a set of cells on Z such that the evaluation function (which takes a function, an argument and applies the function to the argument) be Kahn-Plotkin sequential.

In order to get out of this difficulty, there are two kinds of approaches up to now. The first one consists in changing the notion of sequential morphisms: this is the

“sequential algorithms” approach. A sequential algorithm is roughly a sequential function equipped with a Skolem function for the ∀∃ sequence of quantifiers in the Kahn-Plotkin definition of sequentiality. In a sequential algorithm, the sequential function will sometimes be called “extensional component” and the Skolem function “intensional component”. For the set Z of sequential algorithms from X to Y, it is possible to find an order and a notion of cell such that Z be the exponentiation of X and Y, but both these notions use in a very strong way the intensional components of sequential algorithms. This approach has been developed by Berry and Curien [C1] and has now interesting developments in the direction of models of linear logic [L, C2, AJ] which have strong analogies with the game-theoretic model proposed by Blass [Bl]. This approach has been very successful since it has allowed for a new characterization of the fully abstract model of PCF [AJM, HO]. With Bucciarelli, we also developed an abstract theory of sequential algorithms [BE3].

The other approach consists in reformulating the Kahn-Plotkin condition. The first result in this direction is the cartesian closedness of the category of dI-domains and stable functions, discovered by Berry. A stable function is a continuous function which commutes to the glb’s of finite and bounded sets of data. However, stability only captures “local sequentiality”, that is sequentiality restricted to bounded subsets of domains. Actually, there are stable functions which are not sequential. In the same spirit, we observed with Bucciarelli that Kahn-Plotkin sequentiality could be expressed as a glb’s-preservation property, for some sets of data which are not necessarily bounded. Let us be a bit more specific. In a domain X equipped with a suitable set of cells, let us call “linearly coherent set” any finite and non-empty subset A of X which has the following property: for any cell α, if all the elements of A fill the cell α, then the glb of A fills the cell α. Intuitively, this can be reformulated as follows: if all the elements of A fill a given cell α, then they all fill α with the same value. We observed that a function from X to Y is Kahn-Plotkin sequential if and only if it sends any linearly coherent set to a linearly coherent set and commutes to the glb’s of linearly coherent sets. Obviously, any finite and bounded subset of X is linearly coherent (and so, as it is well known, any sequential function is stable), but the converse is false. For instance, any finite set which contains ⊥ (the minimum of X, the datum which does not fill any cell) is linearly coherent, since it is impossible to find a cell which is filled by all the elements of such a set of data. So, rather than considering domains equipped with cells, it became natural to consider domains equipped with a “coherence”, that is, a suitable subset of the set of finite and non-empty subsets of the domain, which are called “coherent”. We have studied this notion in the framework of qualitative domains and dI-domains, and in both cases, we could prove cartesian closedness. A morphism between two domains equipped with a coherence is a continuous function which sends coherent sets on coherent sets and commutes to the glb’s of coherent sets. More recently, we have found a simplified framework for dealing with strong stability, namely the framework of hypercoherences [E] which also gives rise to a new model of linear logic, and we shall use this theory of strongly stable functions in the sequel. A hypercoherence is a very simple structure (a hypergraph) which naturally gives rise to a qualitative domain equipped with a coherence. All the constructions that we performed on general qualitative domains with coherence (cartesian product and function space), when restricted to qualitative domains with coherence induced by hypercoherences, give rise to qualitative domains with coherence induced by hypercoherences. Furthermore, these constructions are more easily expressed directly in terms of hypercoherences than in terms of qualitative domains with coherence.

Between two domains equipped with linear coherences, we know that strong stability corresponds exactly to Kahn-Plotkin sequentiality (typically, ground types and products of them will be interpreted as domains equipped with linear coherences). But the coherence induced on the exponentiation (function space) of two such domains equipped with linear coherences is generally not linear. So a very natural question arises: are strongly stable functionals Kahn-Plotkin sequential? Unfortunately, as it is stated, this question does not make any sense. Actually, there is in general no notion of cell on the space of strongly stable functions from a domain to another domain which makes the evaluation sequential. (Remember that there is a notion of cell for function spaces only in the framework of sequential algorithms). What we present here is a construction which shows that “any strongly stable function” (not exactly any, but at least those which arise in the strongly stable model of PCF) is the “extensional component” (in a generalized sense) of a sequential algorithm. More precisely, we construct a CCC where objects are triples (E, X, π). In such a triple, E is a “sequential structure”, that is a domain E_{∗} equipped with a set of cells E^{∗} and an additional structure called “accessibility relation”, X is a hypercoherence, and π is a function from E_{∗} to qD (X) (the qualitative domain induced by X). The function π has to be linear, strongly stable (w.r.t. the linear coherence induced by E^{∗} on E_{∗} and the coherence induced by the hypercoherence X on qD (X)) and onto. This last requirement is absolutely essential for our purpose; the intuition behind such a triple (E, X, π) is the following: E_{∗} is a space of sequential algorithms, qD (X) is a space of strongly stable functions, and π is the “forgetful” operation which sends any sequential algorithm on its (generalized) extensional component. Then, saying that π is onto means that any strongly stable function is in some sense the extensional component of a sequential algorithm.

When one tries to perform this construction, two main problems arise:

• First of all, not all sequential algorithms can be “projected” on strongly stable functions, but only the “extensional” ones. Consider the following well known counter-example. From Bool^{2} to Bool (where Bool is the type of booleans), one can define a “strict and” program, that is a program which computes the “and” of its two arguments in such a way that both of these arguments are used, even when one of them is “false”. More precisely, one can define two essentially different such silly “and” programs: the first one uses first its first argument, and the second one uses first its second argument. These programs are called respectively “left strict and” and “right strict and”. In the strongly stable model of PCF, these two programs have exactly the same semantics, but their interpretations as sequential algorithms are different, and even unbounded. However, the extensional components of these sequential algorithms are equal to the unique strongly stable interpretation of the two programs. It is possible to define a sequential algorithm of type (Bool^{2} → Bool) → Bool which sends the “left strict and” on “true” and the “right strict and” on “false”. Now this sequential algorithm cannot be projected on a strongly stable functional, since that functional should send on different values one and the same strongly stable function.

We solve this problem by adding an extensionality constraint on sequential algorithms. This constraint is naturally expressed using the “projections” π.

• Secondly, the requirement that π should be onto is not sufficient for building the exponentiation in our category in general. We need a kind of “uniform surjectivity” which is expressed as a lifting property. Surprisingly enough, proving the lifting property for the extensional projection of the exponentiation becomes then a simple abstract categorical calculation.

In that way, we build a category where the objects are the triples (E, X, π) previously described (with π satisfying the lifting condition), and a morphism between two such objects (E, X, π) and (F, Y, π′) is a sequential algorithm from E to F which is extensional with respect to π and π′. We prove that this category is cartesian closed. When we define the exponentiation (G, Z, Π) of two objects (E, X, π) and (F, Y, π′) we take of course for Z the hypercoherence which is the exponentiation of X and Y in the category of hypercoherences and general strongly stable functions. Then the surjectivity of Π states that any strongly stable function from X to Y is the extensional component of some sequential algorithm.

The model of PCF constructed in this way can be considered as a model of “extensional sequential algorithms”. We can define a functor from this model to the model of hypercoherences and strongly stable functions, using the extensional projections π. This functor is full and commutes to the cartesian product and exponentiation. Then it is easy to see that any equation (or inequation) on PCF which holds in the model of extensional sequential algorithms also holds in the model of hypercoherences and strongly stable functions. In this technical sense, we can say that the model of hypercoherences and strongly stable functions is “sequential”. We consider this result as very important because it establishes a strong connection between the “explicit” approach to sequentiality (sequential algorithms) and the “implicit” one (strongly stable functions). This means that strong stability has a computational interpretation, and this fact was not obvious at first sight.

The paper consists of three sections. In the first section, we recall some basics of domain theory, and the ground definitions and results of the theory of strongly stable functions. We also describe briefly the model of hypercoherences. In the second section, we give an abstract theory of sequential algorithms. This theory is analogous to the one presented in [BE3], but the objects we consider here satisfy an additional requirement (internal sequentiality) which is essential for relating strong stability to sequentiality. We had to perform again all the constructions of [BE3] in this modified framework. The last section contains the construction of our model of extensional sequential algorithms, and the proof of the syntactic result mentioned above. A very short appendix outlines the syntax of PCF and the notion of model considered here.

Contents

1 Preliminaries 7 1.1 Preliminaries about sets and relations . . . . . . . . . . . . . . . . . . . 7 1.2 Preliminaries in domain theory . . . . . . . . . . . . . . . . . . . . . . . 7 1.3 Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4 Qualitative domains and coherence spaces . . . . . . . . . . . . . . . . . 11 1.5 dI-domains with coherence . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.6 Hypercoherences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

2 An abstract theory of sequential algorithms 14 2.1 Sequential structures and sequential algorithms . . . . . . . . . . . . . . 15 2.2 Strongly stable functions and sequential algorithms on sequential struc-

tures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3 Properties of the stable order . . . . . . . . . . . . . . . . . . . . . . . . 20 2.4 Finite retractions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.5 Substructures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.6 The category of sequential structures and sequential algorithms . . . . . 25

3 Extensional projections 33 3.1 Two particular sequential structures . . . . . . . . . . . . . . . . . . . . 34 3.2 Extensionally projected sequential structures . . . . . . . . . . . . . . . 35 3.3 Comparison with the model of hypercoherences . . . . . . . . . . . . . . 41

1 Preliminaries

1.1 Preliminaries about sets and relations

Let E and F be two sets. If C ⊆ E × F, we denote by C_{1} or C_{E} the first projection of C and by C_{2} or C_{F} its second projection. We say that C is a pairing of E and F if C_{1} = E and C_{2} = F.

The disjoint union of E and F will be denoted by E + F and represented by G = (E × {1}) ∪ (F × {2}). If C ⊆ G, we denote by C_{1} = {a ∈ E | (a, 1) ∈ C} its first component and by C_{2} = {b ∈ F | (b, 2) ∈ C} its second component.

Definition 1 Let E and F be sets. Let R ⊆ E × F be a binary relation. Let A ⊆ E and B ⊆ F. We say that A and B are paired under R if (A × B) ∩ R is a pairing of A and B.

Assume that A ⊆ E and B ⊆ F are paired under R ⊆ E × F. If R is the relation “∈”, we say that A is a multisection of B and we write A < B. If F = E is an ordered set, and if the relation R is the order relation on E, we say that A is Egli-Milner less than B w.r.t. this order relation and we write A ⊑ B (usually there will not be any possible confusion about the order involved).

So A < B means that A ⊆ ⋃ B and that A ∩ b is non empty for all b ∈ B. And A ⊑ B means that any element of A is less than an element of B and any element of B is greater than an element of A (this corresponds to the Egli-Milner relation in power-domains theory).

Obviously, the relation ⊑ is a preorder on E.

If E is a set, we denote by P_{fin}^{∗} (E) the set of its finite and non-empty subsets. We write x ⊆_{fin}^{∗} E when x is a finite and non-empty subset of E.

If E and F are sets, if F is a set of functions from E to F and if x ∈ E, we denote by F(x) the set {f(x) | f ∈ F}.

1.2 Preliminaries in domain theory

If D is a poset and x, x′ ∈ D, the notation x ↑ x′ means that x and x′ are bounded in D.

We shall use the abbreviations “lub” for “least upper bound” and “glb” for “greatest lower bound”.

A complete partial order (cpo for short) is a poset where any directed family has a lub.

Definition 2 A cpo D is bounded complete iff any bounded subset of D has a lub.

We shall use the abbreviation bccpo for “bounded-complete cpo”.

Observe that a bccpo has always a least element (the lub of ∅) which will be denoted by ⊥.

In a bccpo, any non-empty subset has a glb. Actually, one can define equivalently a bccpo as a cpo which has a least element and where any non-empty subset has a glb.

Definition 3 Let D be a bccpo and let D′ ⊆ D, that we consider as a poset with the order induced by D. One says that D′ is a sub-bccpo of D if for any A ⊆ D′, if A is bounded in D, then its lub (in D) belongs to D′. We say that such a D′ is a multiplicative sub-bccpo of D if furthermore, for any x, x′ ∈ D′, if x and x′ are bounded (in D, or equivalently in D′), their glb (in D) belongs to D′.

Obviously, a sub-bccpo D′ of a bccpo D is a bccpo, and the inclusion map preserves all the existing lub’s. If D′ is a multiplicative sub-bccpo, then the inclusion map commutes furthermore to binary bounded meets.

Definition 4 Let D be a bccpo. One says that D is distributive if, for x, x′, y ∈ D such that x and x′ are bounded, one has

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

The notion of linear open subset of a bccpo will play an important role in this work, because it will modelize the intuitive notion of question or cell over a datatype. They are those subsets of the domain whose characteristic map (taking its values in the two points Sierpinsky domain {⊥ < ⊤}) is linear. Here is a direct definition:

Definition 5 Let D be a bccpo. A subset α of D is called linear open if:

• α is upper-closed (that is, if x ∈ α and x′ ≥ x then x′ ∈ α).

• α is closed under non-empty, finite and bounded glb’s (equivalently, if x, x′ ∈ α are bounded, then x ∧ x′ ∈ α).

• α is completely prime, that is, if A ⊆ D is bounded and if ⋁ A ∈ α, then A ∩ α is non-empty.

In particular, ⊥ ∉ α. The empty linear subset of D will often be noted ⊥. One denotes by D^{⊥} the set of all linear open subsets of D.

Definition 6 Let D be a bccpo and let Q be a subset of D^{⊥}. One says that Q separates D locally if, whenever x, x′ ∈ D are bounded and satisfy

∀α ∈ Q x ∈ α ⇔ x′ ∈ α

one has x = x′.

Lemma 1 Let D be a bccpo such that there exists a subset of D^{⊥} which separates D locally. Then D is distributive.

Proof: Let Q be a subset of D^{⊥} which separates D locally. Let x, x′, y ∈ D be such that x and x′ are bounded. We have to prove that (x∨x′)∧y = (x∧y)∨(x′ ∧y) and for this we can assume that x, x′ and y are bounded (otherwise, replace y by (x ∨ x′) ∧ y). We clearly have (x∨x′)∧y ≥ (x∧y)∨(x′∧y). So let α ∈ Q be such that (x∨x′)∧y ∈ α. Then one has y ∈ α and x ∨ x′ ∈ α, that is x ∈ α or x′ ∈ α. Assume for instance that x ∈ α. Then, since x and y are bounded, one has x ∧ y ∈ α, and we conclude.

Definition 7 Let D and D′ be bccpo’s. A function f : D → D′ is continuous if it commutes to directed lub’s. It is stable if it is continuous and commutes to finite and bounded glb’s. It is linear if it is stable and commutes to all existing finite lub’s.

Observe that a linear open subset of a bccpo D can alternatively be viewed as a linear map D → O, where O is the two point domain {⊥, ⊤} with ⊥ < ⊤.

Observe also that if D is a bccpo and if D′ is a multiplicative sub-bccpo of D, then the inclusion map from D′ to D is linear, so that any element of D^{⊥}, when restricted to D′, defines an element of D′^{⊥}.

Definition 8 Let D and D′ be two bccpo’s, and let f, g : D → D′ be two continuous functions. One says that f is extensionally less than g if, for all x ∈ D, one has f(x) ≤ g(x). One says that f is stably less than g if for all x, y ∈ D such that x ≤ y one has f(x) = f(y) ∧ g(x).

Definition 9 Let D be a bccpo. One says that an element x of D is compact (or isolated) if, for all A ⊆ D directed, if ⋁ A ≥ x, there exists y ∈ A such that y ≥ x. The element x of D is said to be prime if the same property holds for any A ⊆ D bounded.

One says that D is algebraic if any element of D is the lub of its compact lower bounds, and one says that D is ω-algebraic if it is algebraic and if the set of its isolated points is enumerable.

One says that D is prime-algebraic if any element of D is the lub of its prime lower bounds.

One says that D has the I-property if any compact element of D has only finitely many lower bounds.

Observe that ⊥ is always compact, but never prime (since ⊥ = ⋁ ∅).

In a partial order, one calls ω-chain an ω-indexed increasing chain of elements. In a cpo, any ω-chain has a lub, because an ω-chain is a particular case of directed set.

Lemma 2 Let D and D′ be two ω-algebraic bccpo’s. A function from D to D′ is continuous iff it commutes to the lubs of all ω-chains.

Of course, bounded completeness does not play any role in the previous lemma, which holds for arbitrary ω-algebraic cpo’s. But we do not need this generality here.

Definition 10 A Scott-domain is an ω-algebraic bccpo.

Definition 11 A dI-domain is a distributive bccpo which is ω-algebraic and has the I-property.

The following is due to Winskel (see [W]), and is proved by induction on isolated elements.

Proposition 1 If D is dI-domain, then D is prime-algebraic.

If D is dI-domain, we denote by K(D) the set of its compact elements and by |D| the set of its prime elements.

It is well known that the category dI of dI-domains and stable functions is cartesian closed. We recall briefly how the product and the exponentiation are defined in this category.

Proposition 2 Let D and D′ be two dI-domains. The set D × D′, endowed with the product order, is a dI-domain which is the product of D and D′ in the category dI.

Proposition 3 Let D and D′ be two dI-domains. The set [D → D′]_{S} of all stable functions from D to D′ endowed with the stable ordering is a dI-domain which is the exponentiation of D and D′ in the category dI. Furthermore:

• If F ⊆ [D → D′]_{S} is bounded or directed, and if x ∈ D, then

(⋁ F)(x) = ⋁_{f∈F} f(x) .

• If F ⊆ [D → D′]_{S} is non-empty, finite and bounded, and if x ∈ D, then

(⋀ F)(x) = ⋀_{f∈F} f(x) .

1.3 Traces

We define the notion of trace of a stable function, which allows for a “concrete” representation of these functions and simplifies the study of the function spaces in the stable case.

In this section, D and D′ are two fixed dI-domains.

Definition 12 Let f : D → D′ be a stable function. The trace of f is the subset tr (f) of K(D) × |D′| defined by:

tr (f) = {(a, q) ∈ K(D) × |D′| | q ≤ f(a) and a minimal with this property}

The stable functions are completely characterized by their traces.

Proposition 4 Let f : D → D′ be a stable function, and let x be any element of D. Then

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

Furthermore, traces behave very nicely with respect to the stable ordering.

Proposition 5 Let f, g : D → D′ be stable functions. Then f is less than g (w.r.t. the stable ordering) iff tr (f) is a subset of tr (g).

Linear functions have a very simple characterization in terms of traces.

Proposition 6 Let f : D → D′ be a stable function. f is linear iff tr (f)_{1} is a subset of |D|.

One defines also traces for the linear open subsets of a dI-domain.

Definition 13 Let α ∈ D^{⊥}. The trace of α is the set

tr (α) = {p ∈ |D| | p ∈ α and p minimal} .

Then one has:

Proposition 7 Let α ∈ D^{⊥} and let x ∈ D. Then x ∈ α iff there exists p ∈ tr (α) such that p ≤ x.

The characterizations of linear open subsets’ traces is very simple: if u ⊆ |D|, then u is the trace of an element of D^{⊥} iff the elements of u are pairwise unbounded.

1.4 Qualitative domains and coherence spaces

We are now interested in a special kind of dI-domains.

Definition 14 Let (V, ≤) be a poset with a least element ⊥. An atom in V is an element of V which is different from ⊥ and which has no other lower bounds than ⊥ and itself.

Definition 15 A dI-domain D is said to be atomic if all its prime element are atoms.

Now we define a “concrete” representation of atomic dI-domains based on [G1].

Definition 16 A qualitative domain (qD for short) is a set E such that:

• If e ∈ E and e′ ⊆ e, then e′ ∈ E.

• E is closed under directed unions.

The elements of E are sometimes called states of the qD E.

If E is a qualitative domain, then E (ordered by ⊆) is an atomic dI-domain, where the isolated elements are the finite elements of E and the prime elements are the elements of E which are singletons. Conversely, if D is an atomic dI-domain, then the set of all subsets of |D| which are bounded in D is a qualitative domain.

This establishes a one-to-one correspondence between atomic dI-domains and qualitative domains.

If E is a qualitative domain, the set |E| = {a | {a} ∈ E} is called web of E (so the web of E is the set of prime elements of E, if we consider E as a dI-domain).

The interesting property of qualitative domains is the following:

Proposition 8 The category of qualitative domains and stable functions is a full sub-CCC of the category of dI-domains and stable functions.

There is a sub-class of the class of qualitative domains which is also of interest in the theory of stable functions:

Definition 17 A qualitative domain E is said to be a coherence space if it has the following property: for any x ⊆ |E|, if

∀a, a′ ∈ x {a, a′} ∈ E

then x ∈ E.

So a coherence space E is completely defined by a reflexive and symmetric relation on |E|. Observe that a coherence space can also be viewed as a dI-domain which is atomic and where a family of points is bounded as soon as it is pairwise bounded (this property is sometimes called coherence in the literature).

Proposition 9 The category of coherence spaces and stable functions is a full sub-CCC of the category of qualitative domains and stable functions.

If E is a qualitative domain, we define the coherence space E^{⊥} as follows: |E^{⊥}| = |E| and {a, a′} ∈ E^{⊥} iff a = a′ or {a, a′} ∉ E. Then we consider E^{⊥} as a set of questions on E and we say that a data x ∈ E answers a question α ∈ E^{⊥} iff x ∩ α ≠ ∅. If x answers α then it is easily checked that x ∩ α is a singleton. Observe that E^{⊥} is the space of traces (in the sense of definition 13) of all linear open subsets (see definition 5) of E, considered as a dI-domain, so our notations are consistent.

1.5 dI-domains with coherence

In [BE4], we have developed a theory of strongly stable functions in the framework of dI-domains with coherence. Let us give the main definitions and results of this theory.

Definition 18 A dI-domain with coherence (dIC for short) is a pair (E, C (E)) where E is a dI-domain and C (E) is a subset of P_{fin}^{∗} (E) satisfying the following properties:

• For any u ∈ E, the singleton {u} is in C (E).

• If A ∈ C (E) and if B ∈ P_{fin}^{∗} (E) satisfy B ⊑ A, then B ∈ C (E).

• If D_{1}, …, D_{n} (with n ≥ 1) is a family of directed subsets of E such that, for any u_{1} ∈ D_{1}, …, u_{n} ∈ D_{n} one has {u_{1}, …, u_{n}} ∈ C (E), then {⋁ D_{1}, …, ⋁ D_{n}} ∈ C (E).

By abuse of notation, we shall sometimes denote a dIC (E, C (E)) simply by E. If E is a dIC, the elements of C (E) will be called the coherent subsets of E.

And now we define a notion of morphism between two such objects:

Definition 19 Let E and F be two dIC’s. A strongly stable function f : E → F is a function f : E → F which is Scott-continuous and such that, for any A ∈ C (E),

f(A) ∈ C (F) and ⋀ f(A) = f(⋀ A) .

Observe that any strongly stable function is stable, because any non-empty, finite and bounded subset of a dIC is coherent. The category of dIC’s and strongly stable functions will be denoted by dIC.

Proposition 10 The category dIC is cartesian closed.

We do not give the proof which can be found in [BE4]. We just describe the cartesian product and the exponentiation in that category. So, let E and F we two dIC’s.

The cartesian product of E and F is the dI-domain E × F equipped with the following coherence:

C (E × F) = {C ∈ P_{fin}^{∗} (E × F) | C_{1} ∈ C (E) and C_{2} ∈ C (F)} .

The projections and the pairing of two functions are defined are usual.

The exponentiation is more difficult to describe. First of all, the set of all strongly stable functions from E to F, equipped with the stable order, is a dI-domain G. Now on G we want to define a coherence C (G) such that, at least, the evaluation morphism Ev : G × E → F defined by Ev(f, u) = f(u) be strongly stable. We simply take the greatest (with respect to inclusion) coherence satisfying this last requirement. That is:

C (G) = {F ∈ P_{fin}^{∗} (G) | ∀E ⊆ G × E

(E_{1} = F and E_{2} ∈ C (E)) ⇒ \{ \begin{matrix}Ev(E) ∈ C (F) \\ Ev(⋀ E) = ⋀ Ev(E) \end{matrix} \} .

We denote by E → F this exponentiation (G, C (G)), which lies in the category dIC and satisfies the required conditions.

1.6 Hypercoherences

In [E], we have introduced the notion of hypercoherence as a simplified framework where strong stability makes sense. We recall here the basic definitions and the properties of this model of PCF that we use in the sequel.

Definition 20 A hypercoherence X is a pair (|X| , Γ (X)) where |X| is an enumerable set (the web) and Γ (X) is a subset of P_{fin}^{∗} (|X|) (the atomic coherence) such that, for any a ∈ |X|, one has {a} ∈ Γ (X).

If X is a hypercoherence, we denote by Γ^{∗} (X) and call strict atomic coherence of X the set of all elements of Γ (X) which are not singletons (observe that X can be described by Γ^{∗} (X) as well as by Γ (X)).

Out of a hypercoherence, we define a qualitative domain with coherence, that is a dI-domain with coherence where the underlying dI-domain is a qualitative domain.

Definition 21 Let X be a hypercoherence. We define qD (X) and C (X) as follows :

qD (X) = {x ⊆ |X| | ∀u ⊆_{fin}^{∗} |X| u ⊆ x ⇒ u ∈ Γ (X)}

and

C (X) = {A ⊆_{fin}^{∗} qD (X) | ∀u ⊆_{fin}^{∗} |X| u < A ⇒ u ∈ Γ (X)} .

qD (X) will be called the qualitative domain generated by X and its elements will be called the states of qD (X), and C (X) will be called the state coherence generated by X. The couple (qD (X) , C (X)) will be denoted by qDC (X). The set of finite states of qD (X) will be denoted by qD_{fin} (X). The set of elements of C (X) which have at least two elements will be denoted by C^{∗} (X).

It is clear that qD (X) is always a qualitative domain, and its web is |X| by our only requirement about hypercoherences. Observe also that qDC (X) is a dIC.

The morphisms between hypercoherences that we shall consider in this paper are the strongly stable functions. There is also a notion of linear morphisms between hypercoherences; their theory is developed in [E]. If X and Y are hypercoherences, a strongly stable function from X to Y is a strongly stable function from the dIC qDC (X) to the dIC qDC (Y).

We denote by HCohFS the category of hypercoherences and strongly stable functions.

Let X and Y be hypercoherences. Let X × Y be the hypercoherence defined by |X × Y | = |X| + |Y | and w ∈ Γ (X × Y) if w ⊆_{fin}^{∗} |X × Y | and

(w_{2} = ∅ ⇒ w_{1} ∈ Γ (X)) and (w_{1} = ∅ ⇒ w_{2} ∈ Γ (Y)) .

Let X → Y be the hypercoherence Z whose web is the set of all (x, b) where x ∈ qD (X) is finite and b ∈ |Y |, and whose atomic coherence is given by: w ∈ Γ (Z) if w ∈ P_{fin}^{∗} (|Z|) and

w_{1} ∈ C (X) ⇒ (w_{2} ∈ Γ (Y) and (#w_{2} = 1 ⇒ #w_{1} = 1))

or equivalently

w_{1} ∈ C (X) ⇒ w_{2} ∈ Γ (Y) and w_{1} ∈ C^{∗} (X) ⇒ w_{2} ∈ Γ^{∗} (Y)

Then we have the following result:

Proposition 11 If X and Y are hypercoherences, then

qDC (X × Y) = qDC (X) × qDC (Y) and qDC (X → Y) = qDC (X) → qDC (Y) .

In that proposition, the exponentiation qDC (X) → qDC (Y) is of course taken in the category dIC (and similarly for the cartesian product), and its domain component is the set of traces of all strongly stable functions from qDC (X) to qDC (Y) ordered by inclusion, which is isomorphic to the set of all strongly stable functions from qDC (X) to qDC (Y) stably ordered; this domain is a qualitative domain.

So the category of hypercoherences and strongly stable functions is equivalent to a full sub-CCC of dIC.

2 An abstract theory of sequential algorithms

As already mentioned in the introduction, Concrete Data Structures (CDS’s) provide a semantics of PCF where all terms are interpreted by sequential algorithms, that is, basically, sequential functions equipped with an explicit “evaluation strategy” which specifies how the function explores its input. An exhaustive account of sequential algorithms on CDS’s can be found in [C1]. Let us just say that a CDS is a structure out of which one can define a domain (the domains definable in this way are called “concrete domains”) which is naturally equipped with a set of “cells”. An element of the domain is then obtained by filling some cells with values. An important component of a CDS is its “accessibility relation”: given an element x of the associated domain, there are some cells which are said to be accessible from x. This means that we are allowed to increase x by filling some of these cells by values. Among all CDS’s, Curien pointed out in [C1] that the subclass of sequential CDS’s has good closure properties. A CDS is sequential if its accessibility relation satisfies a condition which means intuitively that, given a cell and an element x of the associated domain, there is a “deterministic” way of making this cell accessible from x. This condition is called “internal sequentiality”.

In [BE3], we have developed a theory of sequential algorithms where, instead of considering CDS’s, we axiomatize directly a notion of domain equipped with “cells” or “questions”, which are described as linear open subsets of the domain. We called these objects “sequential structures”. In this work, we observed that sequential structures had to be equipped with an accessibility relation in order to make the category of sequential structures and sequential algorithms cartesian closed.

The object of this section is to give a precise account of the theory of sequential structures. In contrast with [BE3], the sequential structures presented here will have to satisfy a further axiom which corresponds to the internal sequentiality of sequential CDS’s.

The sequential structures presented here are probably slightly more general than sequential CDS’s, but this is not the real technical reason why we introduce them. The point is that, for the purpose of section 3, sequential structures seem easier to handle than CDS’s.

2.1 Sequential structures and sequential algorithms

Since ω-algebraicity and I-property in the “extensional” sequential structures that we shall introduce in section 3 will be a bit problematic, we introduce the notion of sequential structure in two steps.

Definition 22 A pre-sequential structure (PSS for short) is a tuple E = (E_{∗}, E^{∗}, ⊢_{E}) where E_{∗} is a bounded complete cpo, E^{∗} is an enumerable subset^{1} of E^{⊥} containing ⊥ and locally separating E_{∗}, and ⊢_{E}⊆ E_{∗} ×E^{∗} is a binary relation satisfying the following axioms:

(PSS1) For any u ∈ E_{∗}, u ⊢_{E} ⊥. For any u ∈ E_{∗} and α ∈ E^{∗}, if u ∈ α then u ⊬_{E} α.

(PSS2) If u ∈ E_{∗} and α ∈ E^{∗} satisfy u ∈ α, then there exists u′ ≤ u such that u′ ⊢_{E} α.

(PSS3) If u ∈ E_{∗} and α ∈ E^{∗} satisfy u ⊢_{E} α, and if u′ ≥ u satisfies u′ ∉ α, then u′ ⊢_{E} α.

(PSS4) If D ⊆ E is directed and satisfies ⋁ D ⊢_{E} α for α ∈ E^{∗}, then there exists u ∈ D such that u ⊢_{E} α. (This condition will be called internal continuity in the sequel.)

(PSS5) If u ∈ E_{∗} and α ∈ E^{∗} satisfy u ∉ α and u ⊬_{E} α, then there exists α′ ∈ E^{∗} such that u ⊢_{E} α′ and for any u′ ≥ u, if u′ ⊢_{E} α, then u′ ∈ α′. (This condition will be called internal sequentiality in the sequel, and α′ will be called internal sequentiality index for α at u.)

1More precisely, E^{∗} is a set of formal objects with a distinguished element ⊥, and “∈” should be considered as a relation, called filling relation, on E_{∗} × E^{∗} which is linear in its first component and such that x ∈ ⊥ never holds.

If E is a PSS, if u ∈ E_{∗}, we denote by E_{u}^{∗} the set {α ∈ E_{∗} | u ⊢_{E} α}. The elements of E^{∗} are sometimes called cells of E. If x ∈ α, one says that the cell α is filled in x. If x ⊢_{E} α, one says that the cell α is accessible from x.

Definition 23 A PSS E is a sequential structure if it enjoys furthermore the two following properties:

• E_{∗} is ω-algebraic.

• If u ∈ E_{∗} is compact, then there are only finitely many α ∈ E^{∗} such that u ∈ α.

Lemma 3 If E is a sequential structure, then E_{∗} is a dI-domain.

Proof: We already know that E_{∗} is distributive by lemma 1. So we just have to prove that E_{∗} enjoys the I-property.

For u ∈ E_{∗}, let |u| be the set {α ∈ E_{∗} | u ∈ α}. If u′ ≤ u, we know that if |u′| = |u| then u = u′ by local separation. But if u is compact, then |u| is finite, since E is a sequential structure. So if u is compact, u has finitely many lower bounds.

Lemma 4 Let E be a PSS, and let u, u′ ∈ E_{∗} be bounded. Let α ∈ E^{∗}. If u ⊢_{E} α and u′ ⊢_{E} α, then u ∧ u′ ⊢_{E} α. This property will be called internal stability.

Proof: Let u, u′ ∈ E_{∗} be bounded, and let α ∈ E^{∗} be such that u ⊢_{E} α and u′ ⊢_{E} α. Assume that u ∧ u′ ⊬_{E} α. Let α′ ∈ E^{∗} be an internal sequentiality index for α at u ∧ u′. By internal sequentiality, we have u ∈ α′ and u′ ∈ α′, whence the contradiction, by stability of α′.

Now we introduce the notion of sequential algorithm which, as already mentioned, is reminiscent of the notion of abstract algorithm defined in [C1].

Definition 24 Let E and F be PSS’s. A sequential algorithm from E to F is a pair (f, φ) where f : E_{∗} → F_{∗} is a Scott-continuous function, and for all u ∈ E_{∗}, φ_{u} is a function F_{f(u)}^{∗} → E_{u}^{∗} satisfying the following axioms:

• φ_{u}(⊥) = ⊥

• If u ≤ u′ and if β ∈ F_{f(u)}^{∗}, then

f(u′) ∈ β ⇒ u′ ∈ φ_{u}(β)

This condition is called sequentiality.

• If u ≤ u′ and if β ∈ F_{f(u)}^{∗}, then

u′ ∉ φ_{u}(β) ⇒ φ_{u′}(β) = φ_{u}(β)

This condition is called permanence.

• If D ⊆ E is directed and if β ∈ F_{f(⋁ D)}^{∗} is such that φ_{⋁ D}(β) ≠ ⊥, then there exists u ∈ D such that f(u) ⊢_{E} β and φ_{u}(β) = φ_{⋁ D}(β). This condition is called continuity (of φ).

Lemma 5 If (f, φ) is a sequential algorithm, then f is a stable function.

The proof is easy, it is similar to the proof of lemma 4.

Definition 25 Let E and F be PSS’s. Let (f, φ), (g, ψ) : E → F be sequential algorithms. One says that (f, φ) is stably less than (g, ψ) and writes (f, φ) ≤ (g, ψ) iff f is extensionally less than g and, for any u ∈ E_{∗} and β ∈ F_{f(u)}^{∗}, if φ_{u}(β) ≠ ⊥, then g(u) ∉ β and ψ_{u}(β) = φ_{u}(β).

Definition 26 Let E,F and G be PSS’s. The identity algorithm E → E is the pair (Id, ι) where Id is the identity and ι_{u} is the identity for all u ∈ E_{∗}. It will often be simply denoted by Id.

If (f, φ) : E → F and (g, ψ) : F → G are two sequential algorithms, their composition (h, θ) : E → G is given by

h(u) = g(f(u)) and θ_{u}(γ) = φ_{u}(ψ_{f(u)}(γ))

and will be denoted by (g, ψ) ∘ (f, φ).

One should check that (g, ψ) ∘ (f, φ) is actually a sequential algorithm. We leave this verification to the reader (the proof can also be found in [BE3]).

And so we define a category where the objects are sequential structures and the morphisms are sequential algorithms. Let us call SeqSt this category.

2.2 Strongly stable functions and sequential algorithms on sequential structures

The goal of this section is to relate formally the notion of “sequential function” (ie. continuous function having an “evaluation strategy”) to the notion of “sequential algorithm” (ie. continuous function equipped with an “evaluation strategy”). More precisely, we want to relate sequential algorithms to strongly stable functions (w.r.t. the linear coherence on a sequential structure, see below the precise definition). The internal sequentiality condition will be essential in order to relate sequential functions to strongly stable functions.

We first define a notion of sequential functions between sequential structures.

Definition 27 Let E and F be sequential structures and let f : E_{∗} → F_{∗} be a Scottcontinuous function. One says that f is sequential if for all u ∈ E_{∗}, for all β ∈ F_{f(u)}^{∗}, there exists α ∈ E_{u}^{∗} such that, for all u′ ≥ u, if f(u′) ∈ β then u′ ∈ α. Such an α is called sequentiality index of f for β at u.

Here we can notice a slight difference between our notion of sequentiality and the Kahn and Plotkin’s notion. They would have said:

“One says that f is sequential if, for all u ∈ E_{∗}, for all β ∈ F_{f(u)}^{∗}

• either there is no u′ ≥ u such that f(u′) ∈ β

• or there exists α ∈ E_{u}^{∗} such that, for all u′ ≥ u, if f(u′) ∈ β then u′ ∈ α.”

Actually, in our framework, Kahn and Plotkin’s definition is equivalent to ours, because we have added in the sets of questions the empty question ⊥.

Now we prove that a sequential function can be endowed with an “evaluation strategy”, giving rise to a sequential algorithm in the sense of definition 24. This proof does not use the internal sequentiality axiom.

Proposition 12 Let E and F be sequential structures. If (f, φ) : E → F is a sequential algorithm, then f is a sequential function. Conversely, if f : E_{∗} → F_{∗} is a sequential function, there exists φ such that (f, φ) is a sequential algorithm E → F.

Proof: The first part of the proposition is obvious (by the definition of sequential algorithms).

Now let f : E_{∗} → F_{∗} be a sequential function. We define the family (φ_{u}) by well founded induction on the finite elements of E_{∗} (which is a dI-domain).

Let u_{0}, u_{1}, … be an enumeration of all finite elements of E_{∗} such that, if u < u_{n}, then the index i of u in the enumeration is such that i < n. (Such an enumeration is easy to build from a given enumeration, because there are only finitely many elements below a finite element.) We define φ_{u_{n}} by induction on n.

Let n ∈ ω. We assume (inductive hypothesis) that φ_{u_{i}} is defined for all i < n and that, for i, j < n,

(1) For any u ∈ E_{∗}, if u_{i} ≤ u, if β ∈ F_{f(u_{i})}^{∗} and if f(u) ∈ β, then u ∈ φ_{u_{i}}(β). This means that φ_{u_{i}}(β) is a sequentiality index of f for β at u_{i}.

(2) If u_{i} and u_{j} are bounded, if β ∈ F_{f(u_{i})}^{∗}∩F_{f(u_{j})}^{∗}, and if u_{i} ∉ φ_{u_{j}}(β) and u_{j} ∉ φ_{u_{i}}(β), then φ_{u_{i}}(β) = φ_{u_{j}}(β). This coherence condition corresponds to the permanence condition. Observe that when we assume that u_{i} ≤ u_{j}, that condition is exactly the permanence of the sequentiality index between u_{i} and u_{j}.

Now, let β ∈ F_{f(u_{n})}^{∗}. There are two cases:

(a) Either there exists i < n such that u_{i} ≤ u_{n}, β ∈ F_{f(u_{i})}^{∗} and u_{n} ∉ φ_{u_{i}}(β). In that case, we choose such an index i and we set φ_{u_{n}}(β) = φ_{u_{i}}(β). This cell does not depend on the choice of i. Actually, if j < n is another index satisfying the same condition, then u_{i} and u_{j} are bounded by u_{n}, and we have u_{i} ∉ φ_{u_{j}}(β) and u_{j} ∉ φ_{u_{i}}(β), because u_{n} ∉ φ_{u_{j}}(β) and u_{n} ∉ φ_{u_{i}}(β). So, by inductive hypothesis, φ_{u_{i}}(β) = φ_{u_{j}}(β).

(b) Or, for all i < n, if u_{i} ≤ u_{n} and β ∈ F_{f(u_{i})}^{∗}, then u_{n} ∈ φ_{u_{i}}(β). Then, we choose a sequentiality index α of f for β at u_{n}. We set φ_{u_{n}}(β) = α.

Let u ≥ u_{n} and let β ∈ F_{f(u_{n})}^{∗} be such that f(u) ∈ β. If there exists i < n such that u_{i} ≤ u_{n}, β ∈ F_{f(u_{i})}^{∗} and u_{n} ∉ φ_{u_{i}}(β) = α, then φ_{u_{n}}(β) = α (case (a)). But we have u ≥ u_{i} and f(u) ∈ β, so by inductive hypothesis, we conclude that u ∈ α. If there is no such i (case (b)), we have chosen for α = φ_{u_{n}}(β) a sequentiality index of f for β at u_{n}, so we conclude directly that u ∈ α. So condition (1) holds for u_{n} in both cases.

Now let us check condition (2). So let j < n be such that u_{j} and u_{n} are bounded, let β ∈ F_{f(u_{j})}^{∗} ∩ F_{f(u_{n})}^{∗} be such that u_{j} ∉ φ_{u_{n}}(β). There are two cases:

• Either (a) holds, then we have taken φ_{u_{n}}(β) = φ_{u_{i}}(β) where i < n is such that u_{i} ≤ u_{n}, β ∈ F_{f(u_{i})}^{∗} and u_{n} ∉ φ_{u_{i}}(β). Assume that u_{n} ∉ φ_{u_{j}}(β). Then we have u_{i} ∉ φ_{u_{j}}(β) since u_{i} ≤ u_{n}, and so, by inductive hypothesis (2), we have φ_{u_{i}}(β) = φ_{u_{j}}(β).

• Or (b) holds. We prove that u_{n} ∈ φ_{u_{j}}(β) and that will prove that our second hypothesis holds for the sequence u_{1}, …, u_{n}. Let k < n be such that u_{k} = u_{j} ∧u_{n}. Then we know that β ∈ F_{f(u_{k})}^{∗} (because f is stable), and we have u_{n} ∈ φ_{u_{k}}(β) by our hypothesis about u_{n}. So, since u_{j} and u_{n} are bounded, we must have u_{j} ∉ φ_{u_{k}}(β), and thus, by inductive hypothesis, φ_{u_{j}}(β) = φ_{u_{k}}(β) and we conclude.

This achieves the construction of φ_{u} for all u ∈ E_{∗} finite. If u ∈ E_{∗} is not finite and if β ∈ F_{f(u)}^{∗}, there are two cases:

• Either there exists u′ ≤ u finite such that β ∈ F_{f(u′)}^{∗} and u ∉ φ_{u′}(β) and then we take φ_{u}(β) = φ_{u′}(β). This does not depend on the choice of u′ because of condition (2).

• Or there is no such u′. Then we take φ_{u}(β) = ⊥.

And now φ_{u} is defined for all u ∈ E_{∗}. Proving that (f, φ) is a sequential algorithm is easy, using conditions (1) and (2).

Lemma 6 A function f : E_{∗} → F_{∗} is sequential iff it satisfies the following condition: For all u ∈ E_{∗} and all β ∈ F^{∗}, if f(u) ∉ β, there exists α ∈ E^{∗} such that u ∉ α, and, for all u′ ≥ u, if f(u′) ∈ β, then u′ ∈ α.

This condition will be called global sequentiality.

Proof: We use in an essential way the internal sequentiality of E and F.

First, let f be sequential, and let us prove that f is globally sequential. Let β ∈ F^{∗} be such that f(u) ∉ β. If β ∈ F_{f(u)}^{∗}, then a sequentiality index α of f for β at u satisfies the required condition. Otherwise, by internal sequentiality, we can find β′ ∈ F^{∗} such that β′ ∈ F_{f(u)}^{∗} and, if v ≥ f(u) and β ∈ F_{v}^{∗}, then v ∈ β′. Now let α be a sequentiality index of f for β′ at u. Let u′ ≥ u be such that f(u′) ∈ β. Then there exists v ≤ f(u′) such that β ∈ F_{v}^{∗}, and thus such that v ∈ β′. So we have f(u′) ∈ β′, and thus u′ ∈ α.

If f is globally sequential, the proof that f is sequential is similar to the previous one. One must use internal sequentiality in E.

Definition 28 Let E be a sequential structure. A subset A of E_{∗} is linearly coherent if it is finite and satisfies the following condition: for all α ∈ E^{∗}, if for all u ∈ A one has u ∈ α, then ⋀ A ∈ α. We denote by C^{L} (E) the set of all linearly coherent subsets of E.

Let E and F be sequential structures. A function f : E_{∗} → F_{∗} is strongly stable if it is Scott-continuous and, for all A ∈ C^{L} (E), one has f(A) ∈ C^{L} (F) and f(⋀ A) = ⋀ f(A).

The proof of the following result can be found in [BE4].

Proposition 13 A function f : E_{∗} → F_{∗} is globally sequential iff it is strongly stable.

We can summarize the content of this section as follows:

Proposition 14 If (f, φ) : E → F is a sequential algorithm, then f is strongly stable.

Conversely, if f : E_{∗} → F_{∗} is strongly stable, one can find φ such that (f, φ) is a sequential algorithm from E to F.

2.3 Properties of the stable order

We establish now some properties of the poset of sequential algorithms from one PSS to another. More precisely, we prove that this poset is a bccpo and that composition of sequential algorithms is a continuous operation. This result will be essential when we shall deal with finite retractions for function spaces.

Lemma 7 Let E and F be two PSS’s, and let (f, φ), (g, ψ) : E → F be two sequential algorithms. If (f, φ) ≤ (g, ψ), then f is stably less than g.

Proof: Let u ≤ u′. We have f(u) ≤ f(u′) ∧ g(u). Let β ∈ F^{∗} be such that f(u′) ∧ g(u) ∈ β, and assume that f(u) ∉ β. By internal sequentiality, we can assume that f(u) ⊢_{F} β. By sequentiality, we have u′ ∈ φ_{u}(β). Hence φ_{u}(β) ≠ ⊥, and hence by stable ordering g(u) ∉ β, and this is a contradiction.

Definition 29 Let E and F be PSS’s. We denote by AS(E, F) the poset of sequential algorithms from E to F (stably ordered).

Lemma 8 Let E and F be PSS’s. The poset AS(E, F) is a cpo.

Proof: Let D be a directed family of sequential algorithms E → F. Its lub (g, ψ) is defined as follows:

• g(u) = ⋁_{(f,φ)∈D} f(u).

• Let β ∈ F_{g(u)}^{∗}. If there exists (f, φ) ∈ D such that β ∈ F_{f(u)}^{∗} and φ_{u}(β) ≠ ⊥, then ψ_{u}(β) = φ_{u}(β) and otherwise, ψ_{u}(β) = ⊥. This does not depend on the choice of (f, φ) because D is directed for the stable order of sequential algorithms.

Let us prove that (g, ψ) is indeed a sequential algorithm. Let u, u′ ∈ E_{∗} be such that u ≤ u′, and let β ∈ F_{g(u)}^{∗}. By internal continuity, we can find (f, φ) ∈ D such that f(u) ⊢_{F} β. Since D is directed, we can assume that all its elements have that property.

• Assume that g(u′) ∈ β. Let (f, φ) ∈ D be such that f(u′) ∈ β. By sequentiality, we have u′ ∈ φ_{u}(β), hence φ_{u}(β) ≠ ⊥, hence ψ_{u}(β) = φ_{u}(β) and thus u′ ∈ ψ_{u}(β).

• Assume that u′ ∉ ψ_{u}(β). Then for all (f, φ) ∈ D, we have u′ ∉ φ_{u}(β) and we conclude.

• Let D ⊆ E^{∗} be directed, let β ∈ F_{g(⋁ D)}^{∗} be such that ψ_{⋁ D}(β) ≠ ⊥. Let (f, φ) ∈ D be such that β ∈ F_{f(⋁ D)}^{∗} and ψ_{⋁ D}(β) = φ_{⋁ D}(β). By continuity of φ we can find u ∈ D such that f(u) ⊢_{F} β and φ_{⋁ D}(β) = φ_{u}(β). Since φ_{u}(β) ≠ ⊥, we have g(u) ⊢_{F} β and ψ_{u}(β) = φ_{u}(β) = ψ_{⋁ D}(β).

Proving that (g, ψ) is actually the lub of D is easy.

Lemma 9 The poset AS(E, F) is bounded complete.

Proof: Let (f, φ), (g, ψ) ∈ AS(E, F) be two sequential algorithms bounded by (h, η) ∈ AS(E, F). We define (l, λ) as follows

• l(u) = f(u) ∨ g(u)

• Let β ∈ F_{l(u)}^{∗}. If f(u) ⊢_{F} β and φ_{u}(β) ≠ ⊥, then λ_{u}(β) = φ_{u}(β). Similarly if g(u) ⊢_{F} β and ψ_{u}(β) ≠ ⊥. If neither of these conditions hold, set λ_{u}(β) = ⊥. This definition makes sense because (f, φ) and (g, ψ) are bounded. Actually, if f(u) ⊢_{F} β, g(u) ⊢_{F} β, φ_{u}(β) ≠ ⊥ and ψ_{u}(β) ≠ ⊥, then we know that φ_{u}(β) = ψ_{u}(β) = η_{u}(β).

Let us prove that (l, λ) is a sequential algorithm. Let u, u′ ∈ E_{∗} be such that u ≤ u′, and let β ∈ F_{l(u)}^{∗}.

• Assume that l(u′) ∈ β. Then f(u′) ∈ β or g(u′) ∈ β. Assume that f(u′) ∈ β. We know that f(u) = f(u′) ∧ l(u) (since f is stably less than l) and hence f(u) ⊢_{F} β, by internal stability. By sequentiality of (f, φ), we conclude.

• Assume that u′ ∉ λ_{u}(β). We can assume that f(u′) ⊢_{F} β or g(u′) ⊢_{F} β, otherwise the result is obvious. Assume for instance that f(u′) ⊢_{F} β. Since f(u) = f(u′) ∧ l(u), we get by internal stability f(u) ⊢_{F} β. We can assume that λ_{u}(β) = φ_{u}(β) (if this is not the case, make the same reasonment with (g, ψ)). We conclude using permanence of (f, φ).

• Continuity of λ is easy to check.

Again, we omit the proof that (l, λ) is actually the lub of (f, φ) and (g, ψ).

Since AS(E, F) is bounded complete, it has glb’s for all non-empty subsets. These glb’s are hard to characterize in general, but the case of two bounded algorithms is easy and important for what follows.

Lemma 10 Let (f, φ), (g, ψ) ∈ AS(E, F) be two sequential algorithms which are bounded. Then their glb (l, λ) is defined by

l(u) = f(u) ∧ g(u)
λ_{u}(β) = \{ \begin{matrix}φ_{u}(β) = ψ_{u}(β) & if f(u) ⊢_{F} β, g(u) ⊢_{F} β, \\ & φ_{u}(β) ≠ ⊥ and ψ_{u}(β) ≠ ⊥ \\ ⊥ & otherwise \end{matrix}

This characterization makes sense precisely because (f, φ) and (g, ψ) are bounded. Actually, this forces φ_{u}(β) and ψ_{u}(β) to have the same value when they are both defined and different from ⊥.

We omit the verification that (l, λ) is actually a sequential algorithm, and that it is the glb of (f, φ) and (g, ψ) in AS(E, F).

Lemma 11 Composition is a Scott-continuous function from AS(E, F) × AS(F, G) (equipped with the product order) to AS(E, G).

Proof: We prove first that composition is monotone. Let (f, φ), (f′, φ′) ∈ AS(E, F) and (g, ψ), (g′, ψ′) ∈ AS(F, G) be such that (f, φ) ≤ (f′, φ′) and (g, ψ) ≤ (g′, ψ′). Let (h, η) = (g, ψ) ∘ (f, φ) and (h′, η′) = (g′, ψ′) ∘ (f′, φ′). Obviously, h ≤ h′ extensionally. Let u ∈ E_{∗} and γ ∈ G_{h(u)}^{∗}, and assume that α = η_{u}(γ) ≠ ⊥. Let β = ψ_{f(u)}(γ), we have α = φ_{u}(β). Since (f, φ) ≤ (f′, φ′), we have f′(u) ⊢_{F} β and φ′_{u}(β) = φ_{u}(β).

Since α ≠ ⊥, we have also β ≠ ⊥, and hence, since (g, ψ) ≤ (g′, ψ′), we have g′(f(u)) ⊢_{G} γ and ψ′_{f(u)}(γ) = β. By sequentiality and permanence of (g′, ψ′) we have ψ′_{f′(u)}(γ) = ψ′_{f(u)}(γ) because f′(u) ∉ β. So we conclude.

Let D ⊆ AS(E, F) × AS(F, G) be directed. The two projections D_{1} ⊆ AS(E, F) and D_{2} ⊆ AS(E, F) of D are directed. Let (l, λ) = ⋁ D_{1} and (m, μ) = ⋁ D_{2}. Let (k, κ) = (m, μ) ∘ (l, λ) and (k′, κ′) = ⋁{(g, ψ) ∘ (f, φ) | ((f, φ), (g, ψ)) ∈ D}. We have (k′, κ′) ≤ (k, κ) because composition is monotone. So let us prove the converse inequality. Let u ∈ E_{∗} and γ ∈ G_{k(u)}^{∗} be such that κ_{u}(γ) ≠ ⊥. Using the fact that D is directed, we can find a couple ((f, φ), (g, ψ)) ∈ D such that g(f(u)) ⊢_{G} γ and κ_{u}(γ) = φ_{u}(ψ_{f(u)}(γ)). By definition of (k′, κ′) we have also k′(u) ⊢_{G} γ and κ′_{u}(γ) = φ_{u}(ψ_{f(u)}(γ)), and we conclude.

2.4 Finite retractions

The object of this section is to define the finite retractions, which are a tool for specifying in a “uniform” way algebraicity for PSS’s. This tool is very useful for proving algebraicity for the spaces of “extensional” sequential algorithms that we shall define in section 3. We have used the same tool in [BE2] for a similar reason. Let us stress that our terminology is non-standard: what we call here “retraction” is usually called “projection” in the litterature of denotational semantics. We prefer to avoid the use of the word “projection” here because it will be used with a completely different meaning in the sequel.

We have here to deal with a stupid problem: in a PSS E, there may exist elements α of E^{∗} different from ⊥ which are not filled by any element of E_{∗}. Obviously, these elements do not play any role in the structure of E, but we are obliged either to reject them by a specific axiom, but this would complicate all the theory of PSS’s, or to take them carefully under consideration when defining the finite retractions which have to generate in a finite way the whole structure of E, including these dummy questions α. For the sake of simplicity, we have chosen this second solution.

Definition 30 Let E be a PSS. A dummy question of E is an element α of E^{∗} such that for any u ∈ E_{∗} one has u ∉ α. A dummy set of E is a subset V of E^{∗} any element of which is a dummy question of E.

Definition 31 Let E be a PSS. A retraction on E is a continuous function r : E_{∗} → E_{∗} such that r ≤ Id for the stable order.

If r is a retraction on E, we denote by |r| the set

|r| = {α ∈ E^{∗} | ∃u ∈ E_{∗} r(u) ∈ α}

Observe that a retraction r is stable and satisfies r ∘ r = r. This is due to the fact that r ≤ Id for the stable order.

Let r be a retraction on a PSS E and let V be a dummy set of E. We define a family of functions ρ_{u}^{r,V} : E_{r(u)}^{∗} → E_{u}^{∗} (for u ∈ E_{∗}) as follows:

ρ_{u}^{r,V} (α) = \{ \begin{matrix}α & if α ∈ |r| ∪ V and u ∉ α \\ ⊥ & otherwise \end{matrix}

Lemma 12 If r is a retraction on a PSS E and V is a dummy set of E, then (r, ρ^{r,V}) is a sequential algorithm on E such that (r, ρ^{r,V}) ≤ Id.

Proof: We first prove that (r, ρ^{r,V}) is a sequential algorithm. Let α ∈ E_{r(u)}^{∗} and let v ∈ E_{∗} be such that v ≥ u.

• Assume first that r(v) ∈ α. Then obviously α ∈ |r|. Furthermore, since r(u) = r(v) ∧ u, we have u ∉ α. Hence ρ_{u}^{r,V} (α) = α and v ∈ ρ_{u}^{r,V} (α) since v ≥ r(v).

• Assume now that v ∉ ρ_{u}^{r,V} (α). If ρ_{u}^{r,V} (α) = ⊥, we obviously have also ρ_{v}^{r,V} (α) = ⊥. Otherwise, we know that α ∈ |r| ∪ V, that ρ_{u}^{r,V} (α) = α and hence that v ∉ α. So we conclude that ρ_{v}^{r,V} (α) = α.

The continuity of ρ^{r,V} is left to the reader.

Now we check that (r, ρ^{r,V}) ≤ Id. So let u ∈ E_{∗} and α ∈ E_{r(u)}^{∗} be such that ρ_{u}^{r,V} (α) ≠ ⊥. This implies that u ∉ α, and hence ι_{u}(α) = α and this concludes the proof.

Lemma 13 Let E be a PSS.

• Let r and s be two retractions on E and let V and W be two dummy sets of E such that V ⊆ W. If, for all u ∈ E_{∗} one has r(u) ≤ s(u), then (r, ρ^{r,V}) ≤ (s, ρ^{s,W}).

• Let (r_{n})_{n∈ω} is a family of retractions of E such that r_{n}(u) ≤ r_{n+1}(u) for all n ∈ ω and u ∈ E_{∗} and ⋁_{n∈ω} r_{n}(u) = u. Let (V_{n})_{n∈ω} be a family of dummy sets of E such that V_{n} ⊆ V_{n+1} for all n ∈ ω and such that ⋃_{n∈ω} V_{n} is the set of all dummy questions of E. Then

⋁_{n∈ω}(r_{n}, ρ^{r_{n},V_{n}}) = (Id, ι) .

Proof: We keep the notations of the lemma.

• Let u ∈ E_{∗} and α ∈ E_{r(u)}^{∗}, and assume that ρ_{u}^{r,V} (α) ≠ ⊥. This means that α ∈ |r| ∪ V and that u ∉ α. Since |r| ⊆ |s| and V ⊆ W, we have α ∈ |s| ∪ W, and since s(u) ≤ u, we have s(u) ∉ α and we conclude.

• Let (r, ρ) = ⋁_{n∈ω}(r_{n}, ρ^{r_{n},V_{n}}). Then obviously r = Id. Let u ∈ E_{∗} and let α ∈ E_{u}^{∗}. Let n be such that r_{n}(u) ⊢_{E} α (we can find such an index n by internal continuity). If α is not dummy, we can assume that α ∈ |r_{n}|. If α is dummy, we can assume that α ∈ V_{n}. In both cases, we have ρ_{u}^{r_{n},V_{n}}(α) = α, and thus ρ_{u}(α) = α.

Definition 32 Let E be a PSS. A finite retraction on E is a retraction r on E such that:

• The set r(E_{∗}) is finite.

• The set |r| is finite.

Definition 33 Let E be a PSS. A generating system of finite retractions (GSFR for short) on E is a family of finite retractions (r_{n})_{n∈ω} on E such that:

• For all n ∈ ω and u ∈ E_{∗}, r_{n}(u) ≤ r_{n+1}(u).

• For all u ∈ E_{∗}, ⋁_{n∈ω} r_{n}(u) = u.

Observe that if (r_{n})_{n∈ω} is a GSFR on E, one actually has r_{n} ≤ r_{n+1} for the stable order, and not only for the extensional order. This is due to the fact that r_{n} ≤ Id and r_{n+1} ≤ Id in the stable order.

Proposition 15 Let E be a PSS. If E admits a GSFR, then E is a sequential structure.

Proof: Let (r_{n})_{n∈ω} be a GSFR on E.

First, since (r_{n})_{n∈ω} is a stably increasing family of stable functions with finite images and having Id as lub, we know by standard considerations that E_{∗} is a dI-domain (see for instance [B1]). So we only have to prove that any isolated element of E_{∗} answers only to a finite number of questions of E^{∗}. So let u ∈ E_{∗} be isolated and let n ∈ ω be such that r_{n}(u) = u. Let α ∈ E^{∗} be such that u ∈ α. Then obviously α ∈ |r_{n}|, which is finite by hypothesis, and we are done.

From now on, we call sequential structure only a PSS equipped with a GSFR.

2.5 Substructures

The notion of sub-PSS that we introduce now is essential for the theory of extensional sequential algorithms presented in section 3. Actually, roughly speaking, the space of extensional sequential algorithms will be a sub-PSS of the space of all sequential algorithms.

Definition 34 Let E be a PSS and let S ⊆ E_{∗}. One says that S defines a sub-PSS of E if:

(1) S is a multiplicative sub-bccpo of E_{∗}.

(2) For any u ∈ S and any α ∈ E^{∗}, if u ∈ α, then there exists u′ ∈ S such that u′ ≤ u and u′ ⊢_{E} α.

Let E be a PSS, and let S defining a sub-PSS of E. We know that S is a bccpo, since E_{∗} is. Observe first that any element of E^{∗} can be seen as a linear open subset of S. So we consider E^{∗} as a set of linear open subsets of S which obviously separates S locally. Now if we set F_{∗} = S, F^{∗} = E^{∗} and if we take for ⊢_{F} the restriction of ⊢_{E} to S (that is, if u ∈ S and α ∈ E^{∗}, we say that u ⊢_{F} α iff u ⊢_{E} α), then the tuple (F_{∗}, F^{∗}, ⊢_{F}) becomes a PSS, because of condition (2) in the previous definition. The PSS defined in this way from S will be called the “sub-PSS of E defined by S”.

Lemma 14 Let E and E′ be PSS’s. Let S ⊆ E_{∗} and S′ ⊆ E′_{∗} which define the sub-PSS’s F and F′ of E and E′ respectively. Let (f, φ) : E → F be a sequential algorithm such that, for any u ∈ S one has f(u) ∈ S′. Then, by restriction to S, (f, φ) defines a sequential algorithm from F to F′.

The proof is completely straightforward.

One of the main interests of finite retractions is that they are easily transferred to substructures:

Lemma 15 Let E be a sequential structure, and let (r_{n}) be its associated sequence of finite retractions. Let S ⊆ E_{∗} be a sub-bccpo of E_{∗} defining a sub-PSS F of E. If, for any n ∈ ω and for any u ∈ S one has r_{n}(u) ∈ S, then the family (r_{n}) defines a GSFR for F.

Again, the proof is completely straightforward.

In the situation described by the previous lemma, we shall say that S defines a sequential substructure of E, or that the sub-PSS of E defined by S is a sequential substructure of E.

2.6 The category of sequential structures and sequential algorithms

The main goal of this section is to prove that the category of sequential structures and sequential algorithms is cartesian closed.

The first step is to define the cartesian product. This is essentially trivial.

Let E and F be two sequential structures. Let G be defined by: the dI-domain G_{∗} is the product of the dI-domains E_{∗} and F_{∗}, and G^{∗} is the disjoint sum of E^{∗} and F^{∗}, with bottoms collapsed, that is G^{∗} = ({1} × E^{∗}) ∪ ({2} × F^{∗}) and (1, ⊥) = (2, ⊥) = ⊥. Then we define (u, v) ∈ γ, for (u, v) ∈ G and γ ∈ G^{∗} as follows: (u, v) ∈ (1, α) iff u ∈ α and (u, v) ∈ (2, β) iff v ∈ β. The accessibility relation is defined similarly: (u, v) ⊢_{G} (1, α) iff u ⊢_{E} α, and (u, v) ⊢_{G} (2, β) iff v ⊢_{F} β.

Proposition 16 G is a sequential structure, and it is the cartesian product E × F of E and F in the category SeqSt.

Proof: It is easy to prove that all the required conditions are fulfilled by G. Let us just check internal sequentiality and build a GSFR for this product.

Let us first check internal sequentiality. Let (u, v) ∈ G and γ ∈ G^{∗} be such that (u, v) ∉ γ and (u, v) ⊬_{G} γ. Assume that γ is of the shape (1, α). Then u ∉ α and u ⊬_{E} α, and thus, since E enjoys internal sequentiality, there exists α′ ∈ E_{u}^{∗} such that, for any u′ ≥ u, if u′ ⊢_{E} α, then u′ ∈ α. Now, it is clear that (1, α′) is an index of internal sequentiality in G for γ at (u, v). So G has a structure of PSS.

Next, if (r_{n}) is the GSFR of E and if (s_{n}) is the GSFR of F, it is clear that the family (t_{n})_{n∈ω} defined by t_{n}(u, v) = (r_{n}(u), s_{n}(v)) is a GSFR for G.

To finish, let us just say that the first projection (p^{1}, π^{1}) : G → E is defined by

p^{1}(u, v) = u and π_{(u,v)}^{1}(α) = (1, α) ,

that the second one is defined similarly, and that, if (f, φ) : H → E and (g, ψ) : H → F are sequential algorithms, their pairing (h, η) : H → G is defined by:

h(w) = (f(w), g(w))
η_{w}(1, α) = φ_{w}(α)
η_{w}(2, β) = ψ_{w}(β) .

Now we describe the exponentiation in the category SeqSt. Let E and F be two sequential structures. We stepwise define a sequential structure K which is the exponentiation of E and F in SeqSt.

First, K_{∗} is AS(E, F), the poset of sequential algorithms from E to F. We know that it is a bounded complete cpo. We define now K^{∗}, the set of cells for sequential algorithms.

Definition 35 An element of K^{∗} is a pair (u_{0}, β) where u_{0} ∈ E_{∗} is finite, and β ∈ F^{∗}. We collapse all the cells of the shape (u_{0}, ⊥) on ⊥ ∈ K^{∗}.

Observe that K^{∗} is an enumerable set, since E is ω-algebraic and F^{∗} is enumerable. Now we define the filling and accessibility relations of K.

Definition 36 Let (f, φ) ∈ K_{∗} and (u_{0}, β) ∈ K^{∗}.

• (f, φ) ∈ (u_{0}, β) iff f(u_{0}) ∈ β and u_{0} minimal with that property (and then one says that (f, φ) fills (u_{0}, β) extensionally), or f(u_{0}) ⊢_{F} β, φ_{u_{0}}(β) ≠ ⊥ and if u < u_{0} and f(u) ⊢_{F} β, then u_{0} ∈ φ_{u}(β) (and then one says that (f, φ) fills (u_{0}, β) intensionally). Furthermore, one never has (f, φ) ∈ ⊥.

• (f, φ) ⊢_{K} (u_{0}, β) iff f(u_{0}) ⊢_{F} β, φ_{u_{0}}(β) = ⊥ and, if u < u_{0} and f(u) ⊢_{F} β, then u_{0} ∈ φ_{u}(β). Furthermore, (f, φ) ⊢_{K} ⊥ always holds.

Lemma 16 The filling relation of K is linear in its first component.

Proof:

• Let D ⊆ K_{∗} be a directed family of sequential algorithms and let (u_{0}, β) ∈ K^{∗}. Let (g, ψ) = ⋁ D. Assume that (g, ψ) ∈ (u_{0}, β). There are two cases:

– g(u_{0}) ∈ β and u_{0} is minimal with that property. Since g(u_{0}) = ⋁_{(f,φ)∈D} f(u_{0}), there exists (f, φ) ∈ D such that f(u_{0}) ∈ β. The minimality of u_{0} for this (f, φ) is obvious, since (f, φ) ≤ (g, ψ).

– g(u_{0}) ⊢_{F} β, ψ_{u_{0}}(β) ≠ ⊥, and if u < u_{0} and g(u) ⊢_{F} β, then u_{0} ∈ ψ_{u}(β). Let (f, φ) ∈ D be such that f(u_{0}) ⊢_{F} β and ψ_{u_{0}}(β) = φ_{u_{0}}(β). Let u < u_{0} be such that f(u) ⊢_{F} β. By permanence for (f, φ), we have φ_{u}(β) ≠ ⊥, so φ_{u}(β) = ψ_{u}(β). Hence u_{0} ∈ φ_{u}(β), and thus (f, φ) ∈ (u_{0}, β).

• Let (f^{1}, φ^{1}), (f^{2}, φ^{2}) ∈ K_{∗} be bounded. Let (g, ψ) be their lub. Checking that if (g, ψ) ∈ (u_{0}, β) then (f^{i}, φ^{i}) ∈ (u_{0}, β) for i = 1 or i = 2 is similar to what we did in the case of directed families of algorithms.

• Let (f^{1}, φ^{1}), (f^{2}, φ^{2}) ∈ K_{∗} be bounded. Let (g, ψ) be their glb. We know that g(u) = f^{1}(u) ∧ f^{2}(u). Furthermore, if g(u) ⊢_{F} β, there are two cases:

– Either we have f^{i}(u) ⊢_{F} β and φ_{u}^{i}(β) ≠ ⊥ for i = 1 and for i = 2. Then we know that φ_{u}^{1}(β) = φ_{u}^{2}(β) and we have ψ_{u}(β) = φ_{u}^{1}(β).

– Or this is not the case, and then ψ_{u}(β) = ⊥.

Assume that (f^{i}, φ^{i}) ∈ (u_{0}, β) for i = 1, 2. In fact, since (f^{1}, φ^{1}) and (f^{2}, φ^{2}) are bounded, there are only two cases:

– Either f^{i}(u_{0}) ∈ β and u_{0} minimal, for i = 1 and for i = 2. In that case, we have g(u_{0}) ∈ β and the minimality of u_{0} is obvious.

– Or, for both values of i, we have f^{i}(u_{0}) ⊢_{F} β, φ_{u_{0}}^{i}(β) ≠ ⊥, and if u < u_{0} is such that f^{i}(u) ⊢_{F} β, then u_{0} ∈ φ_{u}^{i}(β). By internal stability, we have g(u_{0}) ⊢_{F} β. Furthermore, we know that φ_{u_{0}}^{1}(β) = φ_{u_{0}}^{2}(β), and ψ_{u_{0}}(β) is the common value of these two expressions. So we have ψ_{u_{0}}(β) ≠ ⊥. The minimality of u_{0} is easily checked.

We shall often use the following “minimization principle”:

Lemma 17 Let (f, φ) ∈ K_{∗}, let u ∈ E_{∗} and let β ∈ F_{f(u)}^{∗}. Let us denote by A(f, φ, u, β) the set of all finite lower bounds u_{0} of u such that f(u_{0}) ⊢_{F} β and u ∉ φ_{u_{0}}(β). Then

• either A(f, φ, u, β) is empty

• or it has a least element u_{1}, and one has φ_{u_{1}}(β) = φ_{u}(β).

Furthermore, if φ_{u}(β) ≠ ⊥, then A(f, φ, u, β) is not empty, and one has (f, φ) ∈ (⋀ A(f, φ, u, β), β). And, if φ_{u}(β) = ⊥ and A(f, φ, u, β) ≠ ∅, then (f, φ) ⊢_{K} (⋀ A(f, φ, u, β), β).

The proof of this fact is left to the reader.

Lemma 18 K^{∗} separates K_{∗} locally.

Proof: Let (f, φ), (g, ψ) ∈ K_{∗} be such that (f, φ) ≤ (g, ψ) and |(f, φ)| = |(g, ψ)|. We have to prove that (g, ψ) ≤ (f, φ). Let u ∈ E_{∗}, we prove that g(u) ≤ f(u). Let β ∈ |g(u)|. Then by stability of g and β, we can find u_{0} ≤ u finite and minimal such that g(u_{0}) ∈ β. Then we have (u_{0}, β) ∈ |(g, ψ)| = |(f, φ)|. But since (f, φ) ≤ (g, ψ), we cannot have f(u_{0}) ⊢_{F} β and φ_{u_{0}}(β) ≠ ⊥, so in fact f(u_{0}) ∈ β, and hence f(u) ∈ β, thus by local separation in F we have f(u) ≥ g(u).

Now let u and β be such that g(u) ⊢_{F} β and ψ_{u}(β) ≠ ⊥. Using the minimization principle, we can find u_{0} ≤ u finite such that (g, ψ) ∈ (u_{0}, β), and this filling is intensional, because g(u_{0}) ⊢_{F} β and ψ_{u_{0}}(β) = ψ_{u}(β). We know that (f, φ) ∈ (u_{0}, β), and since we have f(u_{0}) ∉ β (because f(u_{0}) ≤ g(u_{0})), we must have f(u_{0}) ⊢_{F} β and φ_{u_{0}}(β) ≠ ⊥, and hence, since (f, φ) ≤ (g, ψ), we have φ_{u_{0}}(β) = ψ_{u_{0}}(β) = ψ_{u}(β), so by sequentiality and permanence of (f, φ) we get f(u) ⊢_{F} β and φ_{u}(β) = ψ_{u}(β) and we conclude.

Lemma 19 Let (f, φ) and (u_{0}, β) be such that (f, φ) ∈ (u_{0}, β). Then there exists (g, ψ) ∈ K_{∗} such that (g, ψ) ≤ (f, φ) and (g, ψ) ⊢_{K} (u_{0}, β).

Proof: We have f(u_{0}) ∈ β or f(u_{0}) ⊢_{F} β. So we can choose v ≤ f(u_{0}) such that v ⊢_{F} β. We define (g, ψ) as follows:

• If u ∈ E_{∗}, then g(u) = f(u ∧ u_{0}) ∧ v.

• If γ ∈ F_{g(u)}^{∗}, then

ψ_{u}(γ) = \{ \begin{matrix}φ_{u∧u_{0}}(γ) & if f(u ∧ u_{0}) ⊢_{F} γ, u ∉ φ_{u∧u_{0}}(γ) and u ≥ u_{0} ⇒ γ ≠ β \\ ⊥ & otherwise . \end{matrix}

We prove first that (g, ψ) is a sequential algorithm. Let u, u′ ∈ E_{∗} be such that u ≤ u′, and let γ ∈ F_{g(u)}^{∗}.

• Assume that g(u′) ∈ γ, that is f(u′ ∧ u_{0}) ∧ v ∈ γ. Thus one has f(u ∧ u_{0}) ⊢_{F} γ, otherwise one would have f(u ∧ u_{0}) ∈ γ (since g(u) ⊢_{F} γ), and this would lead to a contradiction, since f(u ∧ u_{0}) and f(u′ ∧ u_{0}) ∧ v are bounded. So, by sequentiality of (f, φ), we get u′ ∧ u_{0} ∈ φ_{u∧u_{0}}(γ). From that, we can also deduce that u ∉ φ_{u∧u_{0}}(γ) (since u and u′ ∧ u_{0} are bounded). Last, one has γ ≠ β, since v ∉ β and v ∈ γ. So we conclude that u′ ∈ ψ_{u}(γ).

• Assume that u′ ∉ ψ_{u}(γ). We prove that ψ_{u′}(γ) = ψ_{u}(γ), considering several cases:

– If f(u ∧ u_{0}) ⊬_{F} γ, this means that f(u ∧ u_{0}) ∈ γ, and the same will hold for u′ since u′ ≥ u. So ψ_{u′}(γ) = ⊥.

– If f(u ∧ u_{0}) ⊢_{F} γ and u ∈ φ_{u∧u_{0}}(γ), assume that f(u′ ∧ u_{0}) ⊢_{F} γ and u′ ∉ φ_{u′∧u_{0}}(γ). We have u′ ∈ φ_{u∧u_{0}}(γ) (since u′ ≥ u), and thus φ_{u∧u_{0}}(γ) ≠ φ_{u′∧u_{0}}(γ) (since u′ ∉ φ_{u′∧u_{0}}(γ)), hence u′ ∧ u_{0} ∈ φ_{u∧u_{0}}(γ) (by permanence), and this is a contradiction, since u and u′ ∧ u_{0} are bounded. So once again we get ψ_{u′}(γ) = ⊥.

– If f(u ∧ u_{0}) ⊢_{F} γ and u ∉ φ_{u∧u_{0}}(γ), but u ≥ u_{0} and γ = β, then we also have u′ ≥ u_{0}, and thus ψ_{u′}(γ) = ⊥.

– Assume now that we are in the interesting case, that is: f(u ∧ u_{0}) ⊢_{F} γ, u ∉ φ_{u∧u_{0}}(γ) and u ≥ u_{0} ⇒ γ ≠ β. Then we know that u′ ∉ φ_{u∧u_{0}}(γ) (this is our hypothesis) hence u′ ∧ u_{0} ∉ φ_{u∧u_{0}}(γ), hence f(u′ ∧ u_{0}) ⊢_{F} γ and φ_{u∧u_{0}}(γ) = φ_{u′∧u_{0}}(γ), and thus u′ ∉ φ_{u′∧u_{0}}(γ). Assume that u′ ≥ u_{0} and γ = β. Then we certainly have u ≱ u_{0}, that is u ∧ u_{0} < u_{0}. Thus, since (f, φ) ∈ (u_{0}, β), we have u_{0} ∈ φ_{u∧u_{0}}(β), that is u_{0} ∈ ψ_{u}(β) and this is contradictory because u′ ≥ u_{0}. So u′ ≥ u_{0} ⇒ γ ≠ β, and thus ψ_{u′}(γ) = ψ_{u}(γ).

• The continuity property is easy.

Now, we check that (g, ψ) ≤ (f, φ). The fact that, for all u ∈ E_{∗}, g(u) ≤ f(u) is obvious. Let u and γ be such that g(u) ⊢_{F} γ and ψ_{u}(γ) ≠ ⊥. Then we know that f(u ∧ u_{0}) ⊢_{F} γ and u ∉ φ_{u∧u_{0}}(γ). Thus f(u) ⊢_{F} γ and φ_{u}(γ) = φ_{u∧u_{0}}(γ) = ψ_{u}(γ) and we conclude.

Last we check that (g, ψ) ⊢_{K} (u_{0}, β). First, we have g(u_{0}) = v ⊢_{F} β and ψ_{u_{0}}(β) = ⊥. Next, let u < u_{0} be such that g(u) ⊢_{F} β. Remember that (f, φ) ∈ (u_{0}, β). We have f(u) ∉ β by the minimality property of u_{0}, and thus f(u) ⊢_{F} β and u_{0} ∈ φ_{u}(β). But we have ψ_{u}(β) = φ_{u}(β) because u ∧ u_{0} = u and u ≱ u_{0} and we conclude.

Lemma 20 K enjoys the internal continuity property.

Proof: Let (u_{0}, β) ∈ K^{∗} and let D ⊆ K_{∗} be directed and such that ⋁ D ⊢_{K} (u_{0}, β). Let (g, ψ) = ⋁ D. One has g(u_{0}) ⊢_{F} β, and since g(u_{0}) = ⋁_{(f,φ)∈D} f(u_{0}), one can find, by internal continuity of F, an algorithm (f^{0}, φ^{0}) ∈ D such that f^{0}(u_{0}) ⊢_{F} β. Furthermore, for any u ∈ E_{∗} such that u < u_{0} and g(u) ⊢_{F} β, one has u_{0} ∈ ψ_{u}(β). Hence, for any such u, one can find (f^{u}, φ^{u}) ∈ D such that f^{u}(u) ⊢_{F} β and φ_{u}^{u}(β) = ψ_{u}(β) (by the characterization of (g, ψ) = ⋁ D given in the proof of lemma 8). Since D is directed, and since there are only finitely many u ∈ E_{∗} such that u ≤ u_{0}, we can find (f, φ) ∈ D which is greater than (f^{0}, φ^{0}) and all the (f^{u}, φ^{u})’s. It is clear now that (f, φ) satisfies (f, φ) ⊢_{K} (u_{0}, β).

Lemma 21 K enjoys the internal sequentiality property.

Proof: Let (f, φ) ∈ K_{∗} and (u_{0}, β) ∈ K^{∗} be such that (f, φ) ∉ (u_{0}, β) and (f, φ) ⊬_{K} (u_{0}, β). We distinguish two cases:

• Assume first that f(u_{0}) ⊢_{F} β. Then we can also assume that φ_{u_{0}}(β) = ⊥, otherwise there is no (g, ψ) ≥ (f, φ) such that (g, ψ) ⊢_{K} (u_{0}, β) and we can take ⊥ as internal sequentiality index. We have A(f, φ, u_{0}, β) ≠ ∅ (this set contains u_{0}); let u_{1} be the glb of this set. We know that (f, φ) ⊢_{K} (u_{1}, β), let us check that (u_{1}, β) is an internal sequentiality index. Let (g, ψ) ≥ (f, φ) be such that (g, ψ) ⊢_{K} (u_{0}, β). Then we have g(u_{0}) ⊢_{F} β, and also g(u_{1}) ⊢_{F} β, since f(u_{1}) ≤ g(u_{1}) ≤ g(u_{0}). But u_{1} < u_{0} (because (f, φ) ⊬_{K} (u_{0}, β), (f, φ) ⊢_{K} (u_{1}, β) and u_{1} ≤ u_{0}), so u_{0} ∈ ψ_{u_{1}}(β) (because (g, ψ) ⊢_{K} (u_{0}, β)), and thus ψ_{u_{1}}(β) ≠ ⊥. Let now u ∈ E_{∗} be such that u < u_{1} and g(u) ⊢_{F} β. Then we have f(u) ⊢_{F} β, because f(u) = g(u) ∧ f(u_{1}). Thus, by the minimality property of u_{1}, we have u_{1} ∈ φ_{u}(β), thus φ_{u}(β) ≠ ⊥, hence ψ_{u}(β) = φ_{u}(β), so u_{1} ∈ ψ_{u}(β) and we conclude.

• Assume now that f(u_{0}) ⊬_{F} β. Then we can assume that f(u_{0}) ∉ β. Let β′ be an internal sequentiality index for β at f(u_{0}). Let u_{1} = ⋀ A(f, φ, u_{0}, β′). We distinguish two subcases:

– Assume first that φ_{u_{1}}(β′) ≠ ⊥. Let (g, ψ) be such that (g, ψ) ≥ (f, φ), and assume that (g, ψ) ⊢_{F} (u_{0}, β). Since (f, φ) ≤ (g, ψ) and φ_{u_{1}}(β′) ≠ ⊥, we have g(u_{1}) ⊢_{F} β′ and ψ_{u_{1}}(β′) = φ_{u_{1}}(β′). But we have g(u_{0}) ⊢_{F} β, and thus g(u_{0}) ∈ β′ (since β′ is an internal sequentiality index), hence by sequentiality, u_{0} ∈ ψ_{u_{1}}(β′), that is u_{0} ∈ φ_{u_{1}}(β′) and this is a contradiction. So there is no such (g, ψ), and we can take ⊥ as internal sequentiality index.

– Assume now that φ_{u_{1}}(β′) = ⊥. Then we have (f, φ) ⊢_{K} (u_{1}, β′). Let (g, ψ) be such that (g, ψ) ≥ (f, φ) and (g, ψ) ⊢_{K} (u_{0}, β). Then we have g(u_{0}) ⊢_{F} β and thus g(u_{0}) ∈ β′, hence u_{0} ∈ ψ_{u_{1}}(β′) and ψ_{u_{1}}(β′) ≠ ⊥. If u < u_{1} is such that g(u) ⊢_{F} β′, we have f(u) ⊢_{F} β′ because f(u) = g(u) ∧ f(u_{1}), and thus u_{1} ∈ φ_{u}(β′), so ψ_{u}(β′) = φ_{u}(β′). Thus (g, ψ) ∈ (u_{1}, β′) and hence (u_{1}, β′) is an internal sequentiality index for (u_{0}, β) at (f, φ).

Proposition 17 K is a PSS.

It is a consequence of the previous lemmas. The only properties that we have not proved are PSS1 and PSS3. The corresponding verifications are easy and left to the reader.

We want now to build a GSFR for K, so that K equipped with this GSFR will be a sequential structure.

Lemma 22 Let r and s be finite retractions on E and F respectively. Let V and W be finite dummy sets of E and F respectively. Then the map S_{r,V,s,W} (that we simply note S here) which is defined by

\begin{aligned}S : & K_{∗} & → & K_{∗} \\ & (f, φ) & ↦ & (s, ρ^{s,W}) ∘ (f, φ) ∘ (r, ρ^{r,V}) \end{aligned}

is a finite retraction on K.

Proof: First, we know that S is well defined and continuous (by lemma 11). Let (f, φ) ∈ K_{∗}. Then the algorithm (g, ψ) = S(f, φ) is defined by:

• For u ∈ E_{∗}, g(u) = s(f(r(u))).

• For u ∈ E_{∗} and β ∈ F_{g(u)}^{∗},

ψ_{u}(β) = \{ \begin{matrix}α = φ_{r(u)}(β) & if β ∈ |s| ∪ W and f(r(u)) ∉ β and α ∈ |r| ∪ V and u ∉ α. \\ ⊥ & otherwise \end{matrix}

We prove first that S ≤ Id for the stable ordering. The fact that this inequation holds in the extensional ordering is a consequence of lemmas 11 and 12. So let (f, φ), (f′, φ′) ∈ K_{∗} be such that (f, φ) ≤ (f′, φ′). Let (g, ψ) = S(f, φ) and let (g′, ψ′) = S(f′, φ′). We just have to prove that (h, θ) ≤ (g, ψ) where (h, θ) = (g′, ψ′) ∧ (f, φ).

Using the stable inequalities r ≤ Id, s ≤ Id and f ≤ f′, we get:

g(u) = s(f′(r(u)) ∧ f(u))
= g′(u) ∧ s(f(u))
= g′(u) ∧ f(u) ∧ s(f′(u))
= h(u) since g′(u) ≤ s(f′(u)).

Now let u ∈ E_{∗} and β ∈ F_{h(u)}^{∗} be such that α = θ_{u}(β) ≠ ⊥. This implies that f(u) ⊢_{F} β and φ_{u}(β) = α, and also that β ∈ |s| ∪ W, α ∈ |r| ∪ V, s(f′(r(u))) ⊢_{F} β, f′(r(u)) ∉ β and φ′_{r(u)}(β) = α. The only thing we have to check is that φ_{r(u)}(β) = α. But if this were not the case we would have by permanence u ∈ φ_{r(u)}(β), hence α′ = φ_{r(u)}(β) ≠ ⊥, and hence, since (f, φ) ≤ (f′, φ′), we would conclude that φ′_{r(u)} = α′ ≠ α which is contradictory.

Now let u_{0} be a finite element of E_{∗} and β be an element of F^{∗}, and assume that (g, ψ) ∈ (u_{0}, β). By the minimality condition on u_{0}, it is clear that r(u_{0}) = u_{0} since r(u_{0}) ≤ u_{0}. So u_{0} ∈ r(E_{∗}). Furthermore, we must have s(f(u_{0})) ∈ β or β ∈ |s| ∪ W. So in both cases β ∈ |s| ∪ W. But both sets r(E_{∗}) and |s| ∪ W are finite. So there are only finitely many (u_{0}, β) such that (g, ψ) ∈ (u_{0}, β).

To conclude the proof, we just have to check that S takes only a finite amount of different values. But, for (f, φ) ∈ K_{∗}, observe that (g, ψ) = S(f, φ) has the following properties :

• The function g takes its values in s(F_{∗}) and is completely known when its values on r(E_{∗}) are known. Since both these sets are finite, there are only finitely many possible such g’s.

• Let u ∈ E_{∗}. If β ∈ F_{g(u)}^{∗} and if ψ_{u}(β) ≠ ⊥, then certainly β ∈ |s| ∪ W and ψ_{u}(β) ∈ |r| ∪ V. Since both these sets are finite, there are only finitely many possible ψ_{u}’s. Observe furthermore that ψ_{u} is completely determined by ψ_{r(u)}. Since there are only finitely many possible values for r(u), we conclude that there are only finitely many possible ψ’s.

Now let (r_{n})_{n∈ω} and (s_{n})_{n∈ω} be GSFR’s for E and F respectively. Let (V_{n})_{n∈ω} and (W_{n})_{n∈ω} be increasing families of finite dummy sets of E and F respectively such that ⋃_{n∈ω} V_{n} contains all the dummy questions of E and similarly for ⋃_{n∈ω} W_{n}. Such families of dummy sets exist because E^{∗} and F^{∗} are enumerable. For n ∈ ω, let us simply denote by S_{n} the finite retraction S_{r_{n},V_{n},s_{n},W_{n}}.

Lemma 23 The family (S_{n})_{n∈ω} is a GSFR for K.

This is a consequence of lemmas 11 and 13.

So now K can be considered as a sequential structure, equipped with its GSFR (S_{n})_{n∈ω}.

To complete the proof that the category SeqSt is cartesian closed, we give the evaluation map and we describe the exponential transposition.

Lemma 24 Let (Ev, ε) : K × E → F be defined by:

Ev(f, φ, u) = f(u)

and, when f(u) ⊢_{F} β,

ε_{f,φ,u}(β) = \{ \begin{matrix}(2, φ_{u}(β)) & if φ_{u}(β) ≠ ⊥ \\ (1, (⋀ A(f, φ, u, β), β)) & if φ_{u}(β) = ⊥ and A(f, φ, u, β) ≠ ⊥ \\ ⊥ & otherwise \end{matrix}

Then (Ev, ε) is a sequential algorithm.

Proof: Let (f, φ) ∈ K_{∗}, u ∈ E_{∗} and β ∈ F_{f(u)}^{∗}. The proof that (f, φ, u) ⊢_{K×E} ε_{(f,φ,u)}(β) is straightforward. We prove sequentiality and permanence for (Ev, ε). Continuity is left to the reader. Let (g, ψ) ∈ K_{∗} be such that (g, ψ) ≥ (f, φ) and v ∈ E_{∗} be such that v ≥ u.

• We prove first sequentiality. Assume that g(v) ∈ β. We have to prove that (g, ψ, v) ∈ ε_{(f,φ,u)}(β). We distinguish several cases.

– First, if φ_{u}(β) ≠ ⊥, then we know that g(u) ⊢_{F} β and ψ_{u}(β) = φ_{u}(β). By sequentiality of (g, ψ), we have v ∈ ψ_{u}(β) and we conclude.

– Assume now that φ_{u}(β) = ⊥ and that A(f, φ, u, β) is non-empty, and let u_{0} be its glb. We have to prove that (g, ψ) ∈ (u_{0}, β). If g(u_{0}) ∈ β, then u_{0} is minimal with that property since, if u < u_{0} satisfies g(u) ∈ β, then f(u) = g(u) ∧ f(u_{0}), thus f(u) ⊢_{F} β, thus φ_{u}(β) ≠ ⊥ by minimality of u_{0}. So assume that g(u_{0}) ⊢_{F} β. Since g(v) ∈ β we have v ∈ ψ_{u_{0}}(β) and thus ψ_{u_{0}}(β) ≠ ⊥. If u_{1} < u_{0} satisfies g(u_{1}) ⊢_{F} β then we also have f(u_{1}) ⊢_{F} β (since f(u_{1}) = f(u_{0}) ∧ g(u_{1})), and then by minimality of u_{0} we get u_{0} ∈ φ_{u_{1}}(β) = ψ_{u_{1}}(β) and we conclude.

– Last assume that φ_{u}(β) = ⊥ and that A(f, φ, u, β) = ∅. Then we know that for any u_{0} ≤ u finite such that f(u_{0}) ⊢_{F} β we have u ∈ φ_{u_{0}}(β) (and thus u is not finite). Let v_{0} ≤ v be finite such that g(v_{0}) ∈ β (such a v_{0} can be found since g is continuous). Let u_{0} = v_{0} ∧ u. We have f(u_{0}) = f(v_{0}) ∧ f(u) = g(v_{0}) ∧ f(v) ∧ f(u) = g(v_{0}) ∧ f(u) and hence f(u_{0}) ⊢_{F} β, and hence we get u ∈ φ_{u_{0}}(β) so φ_{u_{0}}(β) ≠ ⊥, hence, since (f, φ) ≤ (g, ψ), we have g(u_{0}) ⊢_{F} β and ψ_{u_{0}}(β) = φ_{u_{0}}(β). Then, since g(v_{0}) ∈ β, we get by sequentiality v_{0} ∈ φ_{u_{0}}(β). On the other hand we have seen that u ∈ φ_{u_{0}}(β), hence u_{0} = u ∧ v_{0} ∈ φ_{u_{0}}(β) and this is a contradiction, so that case is impossible.

• Now we prove permanence, so assume that (g, ψ, v) ∉ ε_{(f,φ,u)}(β). Again we have to distinguish cases.

– First, assume that φ_{u}(β) ≠ ⊥. Then we have g(u) ⊢_{F} β and ψ_{u}(β) = φ_{u}(β), hence v ∉ ψ_{u}(β) and we conclude by permanence of (g, ψ).

– Assume now that φ_{u}(β) = ⊥ and that A(f, φ, u, β) ≠ ∅. Let u_{0} be the glb of that set. Then f(u_{0}) ⊢_{F} β, φ_{u_{0}}(β) = ⊥ and u_{0} is minimal with this property. If we had g(u_{0}) ∈ β then u_{0} would be minimal with this property, and this is impossible, since by hypothesis (g, ψ) ∉ (u_{0}, β). Actually, assume that there exists u < u_{0} such that g(u) ∈ β. Then we have f(u) ⊢_{F} β (since f(u) = f(u_{0}) ∧ g(u)) and thus φ_{u}(β) ≠ ⊥ (since u_{0} is minimal such that φ_{u_{0}}(β) = ⊥), whence the contradiction because (f, φ) ≤ (g, ψ). So g(u_{0}) ⊢_{F} β. Similarly we get ψ_{u_{0}}(β) = ⊥ (and thus g(v) ⊢_{F} β and ψ_{v}(β) = ⊥). The minimality of u_{0} with respect to that property is clear (use again the fact that (f, φ) ≤ (g, ψ)), so ε_{(g,ψ,v)}(β) = (u_{0}, β) (since u ≤ v), and we conclude.

– Last, assume that φ_{u}(β) = ⊥ and that A(f, φ, u, β) = ∅. We check first that g(v) ⊢_{F} β. If this were not the case we would have g(v) ∈ β, thus we could find v_{0} ≤ v finite such that g(v_{0}) ∈ β. Setting u_{0} = v_{0} ∧ u, we would get f(u_{0}) = f(v_{0}) ∧ f(u) = g(v_{0}) ∧ f(v) ∧ f(u), so f(u_{0}) ⊢_{F} β, so u ∈ φ_{u_{0}}(β), hence also g(u_{0}) ⊢_{F} β and ψ_{u_{0}}(β) = φ_{u_{0}}(β). By sequentiality of (g, ψ), one would also get v_{0} ∈ ψ_{u_{0}}(β), and so v_{0} ∧ u ∈ ψ_{u_{0}}(β) and this would be a contradiction. One checks similarly that ψ_{v}(β) = ⊥. Last we prove that A(g, ψ, v, β) = ∅. So let v_{0} ∈ A(g, ψ, v, β). Let u_{0} = v_{0} ∧ u. As above, one checks that f(u_{0}) ⊢_{F} β, and u ∈ φ_{u_{0}}(β). So g(u_{0}) ⊢_{F} β and ψ_{u_{0}}(β) = φ_{u_{0}}(β). Hence v_{0} ∉ ψ_{u_{0}}(β) (since u ∈ ψ_{u_{0}}(β)), hence ψ_{v_{0}}(β) = φ_{u_{0}}(β) ≠ ⊥ and this is in contradiction with our hypothesis that v_{0} ∈ A(g, ψ, v, β).

The sequential algorithm (Ev, ε) will be our evaluation morphism.

Lemma 25 Let G be a sequential structure and let (f, φ) : G × E → F be a sequential algorithm. Then one defines a sequential algorithm (g, ψ) : G → K by setting:

• g(w) = (f^{w}, φ^{w}) where (f^{w}, φ^{w}) : E → F is the sequential algorithm defined by f^{w}(u) = f(w, u) and, if β ∈ F_{f(w,u)}^{∗}

φ_{u}^{w}(β) = \{ \begin{matrix}α & if φ_{(w,u)}(β) = (2, α) \\ ⊥ & otherwise \end{matrix}

• if (f^{w}, φ^{w}) ⊢_{K} (u_{0}, β), then

ψ_{w}(u_{0}, β) = \{ \begin{matrix}γ & if φ_{(w,u_{0})}(β) = (1, γ) \\ ⊥ & otherwise \end{matrix}

Proof: One has to prove the following things :

• (f^{w}, φ^{w}) is a sequential algorithm from E to F for all w.

• The map g is Scott-continuous.

• If (f^{w}, φ^{w}) ⊢_{K} (u_{0}, β), then w ⊢_{G} ψ_{w}(u_{0}, β).

• And last: (g, ψ) enjoys sequentiality and permanence.

All these verifications are rather easy and we leave them to the reader (see also [BE3] for more details).

To prove that K is the exponentiation of E and F in the category SeqSt, it remains to check that some categorical equations relating evaluation and exponential transpose hold. For these verifications, we refer to [BE3]. The exponentiation K of E and F will be denoted by AS(E, F) in the sequel.

So now we conclude:

Proposition 18 The category SeqSt is cartesian closed.

3 Extensional projections

We have now enough material about sequential algorithms for the construction of the category of “extensionally projected sequential structures” we aim at.

3.1 Two particular sequential structures

We first define a sequential structure which corresponds to the “vertical” domain of natural numbers. This sequential structure will be useful for proving continuity for the projections of sequential algorithms. Let \overline{ω} be the sequential structure defined by:

• \overline{ω}_{∗} is the total order of natural numbers, completed by a top ⊤. (⊥ = 0 < 1 < … < ⊤)

• \overline{ω}^{∗} is the set of all questions (n) (for n ∈ ω), plus an empty question ⊥, where

(n) is defined by:

k ∈ (n) iff k > n .

• The accessibility relation is defined by:

k ⊢\overline{ω} (n) iff k = n .

Next we define a family of sequential structures which will be useful for proving strong stability of the projections of sequential algorithms. More precisely, we shall show that any coherent set in a hypercoherence can be seen as the image by a strongly stable function of a coherent set in a cartesian product of “flat hypercoherences”.

Let n > 0 be an integer. We denote by I_{n} the sequential structure defined by:

• I_{n}_{∗} is the flat domain with non-bottom elements 1, …, n and a bottom ⊥.

• I_{n}^{∗} is the set {⊥, ∗} where ∗ is defined by u ∈ ∗ iff u ≠ ⊥.

• One has u ⊢_{I_{n}} ∗ iff u = ⊥.

Define also a hypercoherence J_{n} by |J_{n}| = {1, …, n} and Γ (J_{n}) = {{i} | i ∈ |J_{n}|}.

Let n ≥ 1. We denote by e_{i} the element (n − i + 1, …, n − 1, ⊥, 1, …, n − i) of (I_{n−1}^{n})_{∗} (for i = 1, …, n), so that

e_{1} = (⊥, 1, 2, …, n − 1)
e_{2} = (n − 1, ⊥, 1, …, n − 2)
⋮
e_{n} = (1, 2, …, n − 1, ⊥)

Then observe that {e_{1}, …, e_{n}} ∈ C^{L} (I_{n−1}^{n}) but that no proper subset (with cardinality ≥ 2) of {e_{1}, …, e_{n}} is in C^{L} (I_{n−1}^{n}). Actually, if A is such a subset of {e_{1}, …, e_{n}}, there exists clearly an index j ∈ {1, …, n} such that, for any x ∈ A, the j-th component of x is different from ⊥ (take a j such that e_{j} ∉ A). Then since A is not a singleton, these j-th components have different values because we have defined the e_{i}’s as circular permutations of e_{1}. It follows that A is not linearly coherent. Of course, there are many other ways of defining the e_{i}’s in such a way that the family {e_{1}, …, e_{n}} be “minimal” coherent.

Observe also that, up to a canonical isomorphism, ((I_{n−1}^{n})_{∗}, C^{L} (I_{n−1}^{n})) is simply qDC (J_{n−1}^{n}), and e_{i}, considered as an element of qD (J_{n−1}^{n}), is the state {(1, n − i + 1), …, (i − 1, n − 1), (i + 1, 1), …, (n, n − i)}. We shall use this identification freely in the sequel. The family {e_{1}, …, e_{n}} constitutes a generalization of the Berry’s family, which will play an important role in the sequel for the following reason:

Lemma 26 Let X be a hypercoherence. Let x_{1}, …, x_{n} ∈ qD (X) be such that A = {x_{1}, …, x_{n}} ∈ C (X). Let x = ⋂_{i=1}^{n} x_{i} and

t = {(⊥, a) | a ∈ x} ∪ {(e_{i}, a_{i}) | i ∈ {1, …, n}, a_{i} ∈ x_{i} \ x} .

Then t is the trace of a strongly stable function f^{A} from I_{n−1}^{n} to X which satisfies f^{A}(e_{i}) = x_{i} for all i.

Proof: This amounts to showing that

t = {(∅, a) | a ∈ x} ∪ {(e_{i}, a_{i}) | i ∈ {1, …, n}, a_{i} ∈ x_{i} \ x}

is in qD (J_{n−1}^{n} → X). Let w ⊆ t be non-empty and such that w_{1} ∈ C (J_{n−1}^{n}). There are two cases:

• Either ∅ ∈ w_{1}. Then there exists a ∈ w_{2} such that a ∈ x, and thus w_{2} < A, so w_{2} ∈ Γ (X). Furthermore, if w_{2} is a singleton {a}, then we must have (∅, a) ∈ t, hence a ∈ x. This clearly implies that w_{1} = {∅}.

• Or w_{1} ⊆ {e_{1}, …, e_{n}}. If w_{1} is a singleton {e_{i}} then we have w_{2} ⊆ x_{i}, so w_{2} ∈ Γ (X). Otherwise, we know that w_{1} = {e_{1}, …, e_{n}} because w_{1} ∈ C^{L} (I_{n−1}^{n}), and so w_{2} < A, thus w_{2} ∈ Γ (X). Furthermore, in that case, w_{2} cannot be a singleton. Actually, if w_{2} were {a}, we would have a ∈ x_{i} \ x for any i ∈ {1, …, n}, that is a ∈ ⋂_{i=1}^{n}(x_{i} \ x) = ∅.

So t is the trace of the strongly stable morphism f^{t} : J_{n−1}^{n} → X. We denote by f^{A} the corresponding strongly stable function (I_{n−1}^{n})_{∗} → qD (X) which is given by:

f^{A}(e) = {a | ∃e′ ≤ e (e′, a) ∈ t} .

We have f^{A}(e_{i}) = x ∪ (x_{i} \ x) = x_{i} and this concludes the proof.

3.2 Extensionally projected sequential structures

We define our category of extensionally projected sequential structures, and we prove its cartesian closedness.

We give first the definition of the objects of this category:

Definition 37 An extensionally projected sequential structure (ESS) is a triple (E, X, π) where E is a sequential structure, X is a hypercoherence and π : (E_{∗}, C^{L}E) → qDC (X) is a strongly stable linear function satisfying the following lifting property:

For any sequential structure F and for any strongly stable function f : (F_{∗}, C^{L} (F)) → qDC (X), there exists a strongly stable (and thus sequential) function f′ : F_{∗} → E_{∗} such that π ∘ f′ = f.

Furthermore, the GSFR (r_{n})_{n∈ω} of E is assumed to be π-extensional, that is: for all u, u′ ∈ E_{∗}, if π(u) = π(u′) then π(r_{n}(u)) = π(r_{n}(u′)).

Last, the relation ⊢_{E} must satisfy the following requirement: if u ⊢_{E} α, then there exists u′ ≤ u such that u′ ⊢_{E} α and π(u′) = ∅ (we say that the relation ⊢_{E} is π-flat).

The lifting property is the basic requirement about ESS’s. It insures that π is onto, and in an uniform way. Specifically, as we shall see, it insures that for any state coherent subset A of qD (X), on can find a linearly coherent subset of E_{∗} which is projected by π on A.

Strong stability and linearity of π are essential technical requirements for the construction of the exponentiation in the category of ESS’s we are defining.

The π-flatness condition is technically essential, as it will become clear in the following proofs. It has also an intuitive meaning: the accessibility structure of E is purely intensional; it has no extensional counterpart in X.

The morphisms are simply sequential algorithms satisfying an extensionality requirement expressed in terms of π:

Definition 38 Let P = (E, X, π) and Q = (F, Y, π′) be two ESS’s.

An extensional sequential algorithm (or simply sequential algorithm) from P to Q is a sequential algorithm (f, φ) : E → F which is π-extensional, that is: if u, u′ ∈ E_{∗} satisfy π(u) = π(u′), then π′(f(u)) = π′(f(u′)).

Definition 39 The category ESS is the category whose objects are the ESS’s and whose morphisms are the (extensional) sequential algorithms between ESS’s.

Let us now state and prove the lemma which is the key of our construction:

Lemma 27 Let P = (E, X, π) be an ESS.

• If x_{0} ≤ x_{1} ≤ … is an increasing ω-chain in X, then there exists and increasing ω-chain u_{0} ≤ u_{1} ≤ … in E_{∗} such that π(u_{i}) = x_{i} for all i.

• If x_{1}, …, x_{n} ∈ qD (X) are such that {x_{1}, …, x_{n}} ∈ C (X), then there exist u_{1}, …, u_{n} ∈ E_{∗} such that {u_{1}, …, u_{n}} ∈ C^{L} (E) and π(u_{i}) = x_{i} for all i.

Proof: Let x_{0} ≤ x_{1} ≤ … be an increasing ω-chain in qD (X). Let f : \overline{ω}_{∗} → qD (X) be defined by f(n) = x_{n} and f(⊤) = ⋁_{n∈ω} x_{n}. Then f is obviously Scott-continuous. Furthermore, f is strongly stable because any non-empty and finite subset of {x_{i}} is bounded and thus coherent, and the preservation of non empty (linearly coherent) glb’s is obvious since \overline{ω}_{∗} is totally ordered. So, by the lifting property of π, there exists a sequential function f′ : \overline{ω}_{∗} → E_{∗} such that π ∘ f′ = f. Let u_{i} = f′(i) (for i ∈ ω). Then u_{0} ≤ u_{1} ≤ … is an increasing ω-chain such that π(u_{i}) = x_{i} for all i.

Let A = {x_{1}, …, x_{n}} ∈ C (X). We consider the function f^{A} : (I_{n−1}^{n})_{∗} → qD (X) introduced in lemma 26. This function is strongly stable and satisfies f^{A}(e_{i}) = x_{i} for all i. By the lifting property, we can find a sequential function f′ : (I_{n−1}^{n})_{∗} → E_{∗} such that f^{A} = π ∘ f′. Let u_{i} = f′(e_{i}). Since f′ is strongly stable, we have {u_{1}, …, u_{n}} ∈ C^{L} (E) and we conclude, since for all i we have π(u_{i}) = π(f′(e_{i})) = f^{A}(e_{i}) = x_{i}.

As an easy consequence of this lemma, it appears that, in an ESS (E, X, π), the function π is surjective (onto).

Proposition 19 Let P = (E, X, π) and Q = (F, Y, π′) be ESS’s. Then R = (E × F, X × Y, π × π′) is an ESS, and it is the cartesian product of P and Q in the category ESS.

The proof is a straightforward verification.

Now, let P = (E, X, π) and Q = (F, Y, π′) be two fixed ESS’s. We want to define their exponentiation, an ESS (H, Z, Π).

For Z, we have no choice: we take X → Y, the exponentiation of X and Y in the category HCohFS.

Now we define H as a sub-PSS of AS(E, F). Let L be the poset of extensional sequential algorithms from P to Q, ordered by the stable ordering of sequential algorithms.

Lemma 28 The poset L is a multiplicative sub-bccpo of AS(E, F).

Proof: Let B ⊆ L be bounded in AS(E, F). Let (g, ψ) be its lub in AS(E, F). It will be sufficient to prove that (g, ψ) ∈ L, i.e. to prove that (g, ψ) satisfies the extensionality requirement. Let u, u′ ∈ E_{∗} be such that π(u) = π(u′). Then we have

π′(g(u′)) = π′( ⋁_{(f,φ)∈B} f(u′))
= ⋁_{(f,φ)∈B} π′(f(u′)) since π′ is linear
= ⋁_{(f,φ)∈B} π′(f(u))
= π′(g(u)) .

For bounded binary meets, we proceed similarly, using the stability of π′.

Lemma 29 The poset L defines a sub-PSS of AS(E, F).

Proof: Let (f, φ) ∈ L and let (u_{0}, β) be such that (f, φ) ∈ (u_{0}, β). We have to prove that there exists (g, ψ) ∈ L such that (g, ψ) ≤ (f, φ) and (g, ψ) ⊢_{AS(E,F)} (u_{0}, β).

We construct (g, ψ) as in the proof of lemma 19, but we use furthermore the fact that we can choose our v such that π′(v) = ∅. This insures that, for any u ∈ E_{∗}, we have π′(g(u)) = ∅, and thus (g, ψ) is extensional for a trivial reason.

Now let H be the sub-PSS of AS(E, F) defined by L.

We know that E is equipped with an extensional GSFR (r_{n})_{n∈ω}, and that F is equipped with an extensional GSFR (s_{n})_{n∈ω}. From these, we build a GSFR (S_{n})_{n∈ω} for AS(E, F) as we did when we stated and proved lemma 23. It is easily checked that, if (f, φ) ∈ L, then one has S^{n}(f, φ) ∈ L for any n ∈ ω. Then by lemma 15, we can state the following

Lemma 30 H is a sequential substructure of AS(E, F).

Definition 40 Let (f, φ) ∈ H_{∗}. We call extension of (f, φ) and denote by Π(f, φ) the function g : qD (X) → qD (Y) defined by:

g(x) = π′(f(u)) where u ∈ E_{∗} is such that π(u) = x .

This definition makes sense, because π is surjective, and because (f, φ) is extensional.

Lemma 31 If (f, φ) ∈ H_{∗}, then Π(f, φ) is a strongly stable function X → Y.

Proof: Let g = Π(f, φ).

• We check first that g is Scott-continuous. Let x_{0} ≤ x_{1} ≤ … be an ω-chain in qD (X). Applying lemma 27, we can find an ω-chain u_{0} ≤ u_{1} ≤ … in E_{∗} such that π(u_{i}) = x_{i} for all i. Since π is continuous, we have π(⋁ u_{i}) = ⋁ π(u_{i}) = ⋁ x_{i}, thus g(⋁ x_{i}) = π′(f(⋁ u_{i})). Hence, since π′ and f are continuous, we conclude.

• Let x_{1}, …, x_{n} ∈ qD (X) be such that {x_{1}, …, x_{n}} ∈ C (X). By lemma 27, we can find a family u_{1}, …, u_{n} ∈ E_{∗} such that {u_{1}, …, u_{n}} ∈ C^{L} (E) and π(u_{i}) = x_{i} for i = 1, …, n. We have {g(x_{i})}_{i=1,...,n} = {π′(f(u_{i}))}_{i=1,...,n}, thus {g(x_{i})}_{i=1,...,n} ∈ C (Y), since f and π′ are strongly stable. Furthermore, since π is strongly stable, we have π(⋀ u_{i}) = ⋀ π(u_{i}) = ⋀ x_{i}, hence g(⋀ x_{i}) = π′(f(⋀ u_{i})) = ⋀ π′(f(u_{i})) = ⋀ g(x_{i}) since f and π′ are strongly stable.

So now we can consider Π as a function H_{∗} → qD (Z).

Lemma 32 The function Π is linear and strongly stable.

Proof:

• Let us check first that Π is monotone. Let (f, φ) ∈ E_{∗} and (f′, φ′) ∈ E_{∗} be such that (f, φ) ≤ (f′, φ′), let g = Π(f, φ) and g′ = Π(f′, φ′). Let x, x′ ∈ qD (X) be such that x ≤ x′, and let u, u′ ∈ E_{∗} be such that u ≤ u′, and π(u) = x and π(u′) = x′ (such u and u′ can be found, by lemma 27). We have

g(x) = π′(f(u))
= π′(f(u′) ∧ f′(u))
= π′(f(u′)) ∧ π′(f′(u))
= g(x′) ∧ g′(x)

because f ≤ f′ (for the stable ordering), and because π′ is stable (for it is strongly stable).

• Let B ⊆ H_{∗} be a bounded family of extensional sequential algorithms, and let (h, θ) be its lub. By monotonicity of Π, the set Π(B) is bounded. We know that for u ∈ E_{∗}, h(u) = ⋁_{(f,φ)∈B} f(u). Let g = Π(h, θ). We have to prove that g = ⋁ Π(B). Let x ∈ qD (X) and let u ∈ E_{∗} be such that π(u) = x. We have

g(x) = π′(h(u))
= π′ ( ⋁_{(f,φ)∈B} f(u))

= ⋁_{(f,φ)∈B} π′(f(u)) since π′ is linear
= ⋁_{(f,φ)∈B} Π(f, φ)(x)
= (⋁ Π(B))(x) .

• Let (f^{1}, φ^{1}), …, (f^{n}, φ^{n}) be a family of elements of H_{∗} such that {(f^{1}, φ^{1}), …, (f^{n}, φ^{n})} ∈ C^{L} (H). For i = 1, …, n, let g^{i} = Π(f^{i}, φ^{i}).

– First, we prove that ⋀ g^{i} = Π(f, φ) where (f, φ) = ⋀_{i=1}^{n}(f^{i}, φ^{i}). Let g = Π(f, φ). Since Π is monotone, we certainly have g ≤ ⋀ g^{i}. Let x ∈ qD (X) and let u ∈ E_{∗} be such that π(u) = x. The set E = {((f^{i}, φ^{i}), u) | i = 1, …, n} is in C^{L} (H × E) (for E_{1} ∈ C^{L} (H) and E_{2} ∈ C^{L} (E)), and since Ev is sequential and thus strongly stable, we have Ev(⋀ E) = ⋀ Ev(E), that is f(u) = ⋀ f^{i}(u). So g(x) = π′(⋀ f^{i}(u)). But Ev(E) ∈ C^{L} (F) and π′ is strongly stable, thus g(x) = ⋀(g^{i}(x)). Since (⋀ g^{i})(x) ≤ ⋀(g^{i}(x)) (because the stable ordering is contained in the extensional ordering), we conclude that indeed g = ⋀ g^{i}.

– We prove next that {g^{i}}_{i=1,...,n} ∈ C (Z). So let x_{1}, …, x_{m} ∈ qD (X) be such that {x_{1}, …, x_{m}} ∈ C (X). Let I be a pairing of {1, …, n} and {1, …, m}. Let u_{1}, …, u_{n} ∈ E_{∗} be such that {u_{1}, …, u_{n}} ∈ C^{L} (E) and π(u_{i}) = x_{i} for all i. We know that the set I = {((f^{i}, φ^{i}), u^{j}) | (i, j) ∈ I} is in C^{L} (H × E) (for I_{1} ∈ C^{L} (H) and I_{2} ∈ C^{L} (F)) and hence Ev(I) ∈ C^{L} (F) (because Ev is sequential, and thus strongly stable). Since π′ is strongly stable, we get π′(Ev(I)) ∈ C (Y), that is {g^{i}(x_{j}) | (i, j) ∈ I} ∈ C (Y). Now we have to show that (⋀ g^{i})(⋀ x_{j}) = ⋀_{(i,j)∈I}(g^{i}(x_{j})). But we have seen above that ⋀ g^{i} = g where g = Π(⋀(f^{i}, φ^{i})), so (⋀ g^{i})(⋀ x_{j}) = g(⋀ x_{j}). But g(⋀ x_{j}) = π′(f(⋀ u_{j})), where (f, φ) = ⋀(f^{i}, φ^{i}) (since π(⋀ u_{j}) = ⋀ x_{j}, and by definition of g). Since Ev is strongly stable, we have ⋀(Ev(I)) = Ev(⋀ I), that is ⋀(Ev(I)) = f(⋀ u_{j}). So we get, applying π′ to both members of this last equation, and using the strong stability of π′, ⋀_{(i,j)∈I}(g^{i}(x_{j})) = g(⋀ x_{j}) and we conclude.

So Π is strongly stable, and this achieves the proof of the lemma.

Lemma 33 The function Π has the lifting property.

Proof: Let G be a sequential structure, and let h : G_{∗} → qD (Z) be a strongly stable function. We consider h as a morphism in the category dIC, which is cartesian closed (see section 1.5). In that category, we can transpose h in h′ : G_{∗} × qD (X) → qD (Y) which is strongly stable. But π : E_{∗} → qD (X) is also a morphism in that category, so, in dIC, we can construct l = h′ ∘ (Id × π) : G_{∗} × E_{∗} → qD (Y), which is strongly stable. But π′ enjoys the lifting property, so we can find a strongly stable m : G_{∗}×E_{∗} → F_{∗} such that π′∘m = l. Since m is strongly stable, we can find a μ such that (m, μ) : G×E → F is a sequential algorithm. Now, let (k, κ) : G → AS(E, F) be the exponential transpose of (m, μ) in the category SeqSt of sequential structures and sequential algorithms.

• In fact, (k, κ) is a sequential algorithm G → H. We just have to prove that, if w ∈ G_{∗}, then k(w) ∈ H_{∗}. Let (f, φ) = k(w). We have to prove that this sequential algorithm is extensional. But if u ∈ E_{∗}, we have f(u) = m(w, u), so π′(f(u)) = l(w, u) = h′(w, π(u)), and the extensionality is obvious and we can apply lemma 14.

• Now we check that Π ∘ k = h. Let w ∈ G_{∗}. The function g = Π(k(w)) is defined by g(x) = π′(m(w, u)), where u ∈ E_{∗} is such that π(u) = x (for x ∈ qD (X)). So g(x) = h′(w, x) = h(w)(x), by definition of the exponentiation in dIC, and we conclude.

Lemma 34 The triple (H, Z, Π) is an ESS.

Proof: There remain only a few things to prove.

• For all n ∈ ω, the finite retraction S^{n} is Π-extensional. Let (f, φ), (f′, φ′) ∈ H_{∗} be such that Π(f, φ) = Π(f′, φ′). Let (g, φ) = S^{n}(f, φ) and (g′, φ′) = S^{n}(f′, φ′). Let x ∈ qD (X), and let u ∈ E_{∗} be such that π(u) = x. We have

Π(g, φ)(x) = π′(g(u))
= π′(s^{n}(f(r^{n}(u))))
= π′(s^{n}(f′(r^{n}(u))))

because π′(f(r^{n}(u))) = π′(f′(r^{n}(u))) since Π(f, φ) = Π(f′, φ′), and because (s^{n}, σ^{n}) is extensional. And we conclude.

• If (f, φ) ⊢_{H} (u_{0}, β), then we have seen in the proof of lemma 29 how to build an algorithm (g, ψ) ∈ H_{∗} such that (g, ψ) ≤ (f, φ) and (g, ψ) ⊢_{H} (u_{0}, β). Furthermore, we constructed (g, ψ) in such a way that, for any u ∈ E_{∗}, one has π′(g(u)) = ∅. This clearly means that Π(g, ψ) = ∅ and we conclude that ⊢_{H} is Π-flat.

And this achieves the proof.

Lemma 35 The ESS (H, Z, Π) is the exponentiation of P and Q in the category ESS.

Proof: We define evaluation and abstraction using lemmas 24 and 25 and the fact that H is a sub-PSS of AS(E, F). Let us prove for instance that (Ev, ε) is indeed an extensional sequential algorithm H × E → F. We just have to prove extensionality.

Let (f, φ), (f′, φ′) ∈ H_{∗} be such that Π(f, φ) = Π(f′, φ′), and let u, u′ ∈ E_{∗} be such that π(u) = π(u′). We have

π′(Ev(f, φ, u)) = π′(f(u))
= Π(f, φ)(π(u)) by definition of Π
= Π(f′, φ′)(π(u′)) by hypothesis
= π′(Ev(f′, φ′, u′)) .

The remainder is left to the reader. The exponentiation of P and Q in ESS will be denoted by [P → Q].

Theorem 1 The category ESS is cartesian closed.

In fact, it is a λ-category and thus a model of PCF.

3.3 Comparison with the model of hypercoherences

If P = (E, X, π) is an ESS, let us denote by Π(P) the hypercoherence X and if Q = (F, Y, π′) is another ESS and (f, φ) : P → Q a sequential algorithm, let us denote by Π(f, φ) = Π(f, φ) : X → Y its extension (which is a morphism in HCohFS, as we have seen).

Proposition 20 The operation Π is a functor ESS → HCohFS which commutes to cartesian product and exponentiation.

Proof: Let P = (E, X, π), Q = (F, Y, π′) and R = (G, Z, π′′) be ESS’s. First, let us check that Π is functorial. If x ∈ qD (X) and u ∈ E_{∗} is such that π(u) = x, we have Π(Id)(x) = π(u) = x. Then, let (f, φ) : P → Q and (g, ψ) : Q → R be sequential algorithms. We have

(Π(g, ψ) ∘ Π(f, φ))(x) = Π(g, ψ)(π′(f(u)))
= π′′(g(f(u))
= Π((g, ψ) ∘ (f, φ))(x)

Next, by definition of product and exponentiation in ESS we have Π(P × Q) = Π(P)×Π(Q) and Π([P → Q]) = [Π(P) → Π(Q)]. It remains simply to check that the projections (of the cartesian product) and the evaluation morphism (of the exponentiation) are preserved by the functor Π. Let us check this property for the evaluation. So let g ∈ qD ([X → Y]), and let x ∈ qD (X). Let u ∈ E be such that π(u) = x, and let (f, φ) : P → Q be a sequential algorithm such that Π(f, φ) = g. We have

Π(Ev, ε)(g, x) = π′(Ev((f, φ), u))
= π′(f(u))
= g(x)

and we conclude.

Observe also that both ESS and HCohFS are λ-categories and that Π is a functor of λ-categories (typically, Π is monotone w.r.t. the cpo structure of hom-sets). We consider now these categories as models of PCF (see a description of the syntax in the appendix), interpreting the basic type ι in the usual way (flat domain). To be more precise, this means:

• [ι]^{ESS} = (ι_{⊥}, I, Id) where ι_{⊥} is the sequential structure whose dI-domain is the flat domain of natural numbers, and whose set of linear properties is {⊥, ∗} (filling and accessibility relations defined like in section 3.1 for I_{n}) and I is the hypercoherence defined by |I| = ω and Γ (I) = {{n} | n ∈ ω}. Of course, one has qD (I) = (ι_{⊥})_{∗} up to a trivial isomorphism.

• And [ι]^{HCohFS} = I.

If M^{σ} is a term of PCF with free variables among the list x_{1}^{σ_{1}}, …, x_{k}^{σ_{k}}, we consider its semantics in the model M as a morphism

[M]^{M} : ∏_{i=1}^{k}[σ_{i}]^{M} → [σ]^{M} .

Lemma 36 If σ is a type of PCF, one has

Π([σ]^{ESS}) = [σ]^{HCohFS}

and if M^{σ} is a term of PCF with free variables x_{1}^{σ_{1}}, …, x_{k}^{σ_{k}}, then

Π([M]^{ESS}) = [M]^{HCohFS} .

This is a direct consequence of proposition 20, using the categorical computation of semantics (see [C1]).

As an immediate corollary, we get:

Theorem 2 Let M and N be two terms of PCF with the same type. Then

ESS ⊧ M = N ⇒ HCohFS ⊧ M = N .

And this means that the model of hypercoherences is at least as good as the model of (extensional) sequential algorithms. This implication is not an equivalence since for instance the “left strict and” and the “right strict and” are equal in HCohFS and different in ESS.

A similar result could as well be proved for inequational theories instead of equational ones (for the functor Π preserves also the order between morphisms).

Appendix: syntax and semantics of PCF

We work with a version of PCF which has ι, the type of natural numbers as single ground type. We shall denote by σ_{1}, …, σ_{n} → σ the type σ_{1} → (… → σ), 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 ι. The terms are then constructed using application, λ-abstraction and fix-point combinators (for any type σ, we have a fix-point combinator Y^{(σ→σ)→σ} of type (σ → σ) → σ). Terms must be typable in Curry’s system of simple types based on the only ground type ι.

The notion of model of PCF we consider here is the one used by Berry in his thesis (see [B1], chapter 3.5). A model M consists essentially of a cartesian closed category (in fact, a λ-category) also denoted by M, of the choice of an object [ι]^{M} of M interpreting the type ι in the model, and of morphisms of M interpreting the basic constants of the language; if c is a constant of arity k, its interpretation [c]^{M} must be a morphism from ([ι]^{M})^{k} to [ι]^{M} in the category M. The interpretations of terms are then defined using standard categorical constructions (see [C1, LS] for example).

If M is a model of PCF, we 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 among x_{1}, …, x_{n} of respective types σ_{1}, …, σ_{n}, then the semantics of M is a morphism [M]^{M} from Π_{i=1}^{n}[σ_{i}]^{M} to [σ]^{M} in M.

References

[AJ] S. Abramsky and R. Jagadeesan. Games and Full Completeness for Multiplicative Linear Logic. Journal of Symbolic Logic 59(1994), pp. 543-574.

[AJM] S. Abramsky, R. Jagadeesan and P. Malacaria. Full abstraction for PCF. In Proc. Theoretical Aspects of Computer Science 1994, Sendai, Japan.

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

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

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

[Bl] A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic 56(1992), pp. 183-220.

[BE1] A. Bucciarelli and T. Ehrhard. Sequentiality and strong stability. In Proc. Logic in Computer Science 1991, Amsterdam, pp. 138-145.

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

[BE3] A. Bucciarelli and T. Ehrhard. A theory of sequentiality. Theoretical Computer Science 113(1993), pp. 273-291.

[BE4] A. Bucciarelli and T. Ehrhard. Sequentiality in an extensional framework. Information and Computation 110(1994), pp. 265-296.

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

[C2] P.-L. Curien. On the symmetry of sequentiality. In Proc. Mathematical Foundations of Programming Semantics 1993, New Orleans, Lecture Notes in Computer Science 802, Springer.

[E] T. Ehrhard. Hypercoherences: a strongly stable model of linear logic. Mathematical Structures in Computer Science 3(1993), pp. 365-385.

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

[HO] M. Hyland and L. Ong. On full abstraction for PCF. Manuscript, 1994.

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

[L] F. Lamarche. Sequentiality, Games and Linear Logic (abstract). In G. Winskel, ed., Proceedings of the CLICS Workshop, 23-27 March 1992, Part II. Publications of the Computer Science department of Aarhus university, DAIMI PB 397-II May 1992, pp. 599-607. A complete version is accessible on the ftp server theory.doc.ic.ac.uk at Imperial College.

[LS] J. Lambek and P. Scott. Introduction to Higher Order Categorical Logic. Cambridge studies in advanced mathematics 7, Cambridge University Press, 1986.

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

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

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

[V] J. Vuillemin. Syntaxe, Sémantique et Axiomatique d’un Langage de Programmation Simple. Thèse de Doctorat d’Etat, Université Paris 7, 1974.

[W] G. Winskel. Events in Computation. PhD Thesis, Edinburgh, 1981.