The sequentially realizable functionals^{∗}

John Longley^{†}

Abstract

We consider a notion of sequential functional of finite type, more generous than the familiar notion embodied in Plotkin’s language PCF. We study both the “full” and “effective” partial type structures arising from this notion of sequentiality. The full type structure coincides with that given by the strongly stable model of Bucciarelli and Ehrhard; it has also been characterized by van Oosten in terms of realizability over a certain combinatory algebra.

We survey and relate several known characterizations of these type structures, and obtain some new ones. We show that (in both the full and effective scenarios) every finite type can be obtained as a retract of the pure type \overline{2}, and hence that all elements of the effective type structure are definable in PCF extended by a certain universal functional H. We also consider the relationship between our notion of sequentially computable functional and other known notions of higher-type computability.

Contents

1 Introduction 3 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Outline of the paper . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2 A combinatory algebra for sequential computation 7 2.1 Construction of B and B_{eff}. . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Combinatory completeness . . . . . . . . . . . . . . . . . . . . . . 10 2.3 Irredundant realizers . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.4 A fixed point combinator . . . . . . . . . . . . . . . . . . . . . . . 14

3 Realizability models 15 3.1 Realizability models over B and B_{eff} . . . . . . . . . . . . . . . . . 15 3.2 The SR functionals . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.3 Modified realizability . . . . . . . . . . . . . . . . . . . . . . . . . 18 4 Concrete data structures 19

∗LFCS Report ECS-LFCS-98-402. Submitted to Annals of Pure and Applied Logic.

†LFCS, Division of Informatics, University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ. Email: jrl@dcs.ed.ac.uk.

4.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.2 B as a universal object . . . . . . . . . . . . . . . . . . . . . . . . 22 4.3 Sequential DCDSs and realizability . . . . . . . . . . . . . . . . . 25

5 The hypercoherence model 27 5.1 An extensional collapse construction . . . . . . . . . . . . . . . . 27 5.2 Sequential algorithms and hypercoherences . . . . . . . . . . . . . 30 5.3 Effectivity in hypercoherences . . . . . . . . . . . . . . . . . . . . 32 5.4 The stable order . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

6 A presheaf model 35 6.1 The Colson-Ehrhard characterization . . . . . . . . . . . . . . . . 35 6.2 A presheaf presentation . . . . . . . . . . . . . . . . . . . . . . . . 36

7 A universal type 39 7.1 Call-by-value types . . . . . . . . . . . . . . . . . . . . . . . . . . 39 7.2 Construction of H . . . . . . . . . . . . . . . . . . . . . . . . . . 41 7.3 Properties of H . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

8 Applications of universality 48 8.1 Hypercoherences revisited . . . . . . . . . . . . . . . . . . . . . . 48 8.2 The category of retracts of type \overline{2} . . . . . . . . . . . . . . . . . . 51

9 PCF and universal functionals 53 9.1 Call-by-value PCF . . . . . . . . . . . . . . . . . . . . . . . . . . 53 9.2 The language PCF+H . . . . . . . . . . . . . . . . . . . . . . . . 56 9.3 Degrees of expressivity . . . . . . . . . . . . . . . . . . . . . . . . 59 9.4 Types and universal functionals . . . . . . . . . . . . . . . . . . . 61

10 Synthetic domain theory 66 10.1 Well-complete and replete objects . . . . . . . . . . . . . . . . . . 66 10.2 The Σ-order . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68

11 Notions of higher-type computability 70 11.1 General definitions . . . . . . . . . . . . . . . . . . . . . . . . . . 70 11.2 Three notions of computability . . . . . . . . . . . . . . . . . . . 72

12 Conclusions and further directions 76 12.1 Review of results . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 12.2 The meaning of “sequentiality” . . . . . . . . . . . . . . . . . . . 77 12.3 Game-theoretic models . . . . . . . . . . . . . . . . . . . . . . . . 78 12.4 A programming language for SR functionals . . . . . . . . . . . . 80

1 Introduction

1.1 Background

The classic papers of Scott [51] and Plotkin [45] introduced the language for finitetype computable functionals now widely known as PCF. These authors gave a denotational semantics for this language using complete partial orders, and also pointed out a certain mismatch between the language and its denotational model: because of the “sequential” character of computations in PCF, there are elements of the model (such as “parallel or”) that are in some sense computable but are not definable by terms of PCF.

These early papers initiated a search for other denotational models that more precisely clarified the nature of sequential computation, and in particular gave a semantic characterization of a fully abstract model of PCF. This generated an extensive body of research (see e.g. [6]), which culminated around 1993, when several solutions to the full abstraction problem were announced [2, 21, 40, 41].

The general problem of understanding sequentiality is of both conceptual and practical importance, given that most widely used deterministic programming languages are sequential in character. Much of the study of sequentiality to date has centred around PCF—indeed, it is sometimes implicitly assumed that “sequential” computability is synonymous with PCF-computability, at least for functionals of finite type. However, in their paper on game semantics for PCF [21], Hyland and Ong make the following penetrating remarks:^{1}

‘Persisting in the background of these developments is a deeper, more philosophical question of whether there is such a thing as a canonical notion of sequential computation at higher type. Clearly, the kind of computation defined by PCF is at least a contender for such a standard. But it seems to us that there is no compelling evidence (yet) that PCF-style computation is the only acceptable notion of higher-type sequentiality.’

‘In fact it is unclear whether there are various inequivalent notions of higher-type sequentiality, all of them equally appealing; or whether … there is just one notion under different guises.’

The purpose of the present paper is to investigate an alternative notion of higher-type sequentiality, more generous than the PCF one. We will show that this alternative notion is both mathematically compelling, in that it admits a large number of prima facie independent characterizations, and computationally appealing, in that it arises from a natural and intuitive concept of sequential algorithm.

The class of functionals that we consider is not new. Its discovery is due in essence to Bucciarelli and Ehrhard [9], who constructed a model of PCF involving a category of domains and strongly stable functions. Ehrhard later showed that the relevant part of this model could be more simply presented within the framework of hypercoherences [15]. The strongly stable model was originally conceived as a line of attack on the PCF full abstraction problem, and as a step towards a more denotational understanding of certain features of the Berry-Curien sequential algorithms model [5]. However, it has since turned out to be of considerable interest in its own right. A crucial step was taken by Ehrhard [16], who showed that the notion of strong stability admits a computational interpretation: every morphism in the strongly stable model of PCF is “sequential” in the sense that it can be computed by a Berry-Curien sequential algorithm. This line of investigation was continued in [17], where Ehrhard showed that the strongly stable model is the extensional collapse of the sequential algorithms model. Next, in the autumn of 1996, van Oosten [43] discovered a combinatory algebra embodying an appealing notion of sequential computation, and showed that it yields a realizability model that coincides with the strongly stable model at the finite types. Exactly the same combinatory algebra was rediscovered independently by the present author early in 1997, which gave rise to the investigation reported in the present paper.

1See [21], pages 18–19, 15.

A simple example may be helpful at this point. Let Σ = 1_{⊥} be the twoelement poset with ⊥ ⊑ ⊤, and let Σ^{Σ} be the set of monotone functions Σ → Σ. Consider the function F : Σ^{Σ} → 2_{⊥} defined by

F g = \{ \begin{matrix}true & if g⊥ = ⊤ \\ false & if g⊥ = ⊥ but g⊤ = ⊤ \\ ⊥ & otherwise. \end{matrix}

Intuitively, F tells us whether a function g is able to return a result without looking at its argument. The function F is strongly stable, and it is in some sense sequentially computable. Indeed, the reader familiar with Standard ML [38] (a sequential programming language!) may enjoy verifying that F can be implemented as a function of type ((unit->unit)->unit)->bool, using either exceptions or references. Likewise, one can implement F using control features such the call/cc operator of Scheme [53], or the catch operator considered by Cartwright and Felleisen [12]. Although these implementations make internal use of non-functional features, in terms of their external behaviour they are perfectly “functional”, in the sense that given equal inputs they yield equal outputs (provided these inputs are themselves functional). However, it is easily seen that F is not sequentially computable in the PCF sense, since it is not monotone with respect to the pointwise order. Thus F, although in some sense a functional program, cannot be implemented within the functional fragment of ML.

In this paper the higher-type functionals in question will be called the sequentially realizable (or SR) functionals, as distinguished from the PCF-sequential functionals. In some sense, the SR functionals include all PCF-sequential functionals, together with the above function F and “all things like it”. Indeed, the SR functionals provide an answer to the question of how far one can travel in a language such as PCF+catch without sacrificing the functional nature (i.e. extensionality) of programs.

As with other classes of higher-type functionals, one may consider either the full (continuous) partial type structure of SR functionals, or the effective type structure that arises as its recursive analogue. These two finite type structures will be our main objects of study. The full type structure coincides exactly with that arising from Bucciarelli and Ehrhard’s strongly stable model; however, for our present purposes we prefer the name sequentially realizable to strongly stable, since (a) we wish to emphasize the computational aspect of these functionals; and (b) the effective version of sequential realizability unfortunately does not coincide with the effective version of strong stability (this point will be explained in Section 5.3). The word realizable here should be understood in a rather loose informal sense: the “realizers” in question might be either intensional objects in a realizability model à la Hyland, sequential algorithms in the sense of Berry-Curien, strategies in a game model, or programs in a language such as PCF+catch or Standard ML.

1.2 Outline of the paper

The aims of the present paper are threefold. Firstly, we hope to provide evidence that the notion of SR functional is in some sense a fundamental one. To this end, we collect together a wide variety of characterizations of the (full and effective) SR functionals, surveying various known descriptions and obtaining some new ones. Secondly, we review some of the known results in a more conceptual light, and point out some of the abstract relationships between existing constructions. Thirdly, we study some intrinsic properties of the type structure of SR functionals: for example, that every finite type is a retract of the pure type \overline{2}, and that every element of the effective type structure is PCF-definable from a certain universal functional H.

The rest of the paper is arranged as follows. In Section 2 we introduce van Oosten’s combinatory algebra B, and its effective subalgebra B_{eff}. We prove that these are indeed combinatory algebras, and obtain some basic properties of them. In Section 3 we construct realizability models from these combinatory algebras, in particular the categories of modest sets over B and B_{eff}. These categories give rise to the full and effective SR functionals respectively, and will play a central role in the rest of the paper.

In Sections 4–6 we survey several other characterizations of the SR functionals, and examine the connections between them. In Section 4 we study the relationship between B and the concrete data structures (CDSs) considered by Berry and Curien. We show that B can be seen as a universal (sequential) CDS, and that a good category of CDSs and sequential functions embeds fully in Mod(B). We also show that sequential algorithms are essentially equivalent to realizers in Mod(B). In Section 5 we study the hypercoherence model, and give a new proof of van Oosten’s theorem that the partial type structure in Mod(B) coincides with that in Bucciarelli and Ehrhard’s strongly stable model. Our proof exploits the connection with sequential algorithms, and invokes Ehrhard’s result [17] relating sequential algorithms to the strongly stable model. In Section 6 we consider another characterization of the strongly stable model due to Colson and Ehrhard [13], and recast this as a presheaf construction of the SR functionals.

Section 7 contains the central new result of the paper. In the type structure of (full or effective) SR functionals, every finite type arises as a retract of the pure type \overline{2}. The key to this result is the construction of a retraction \overline{3} ⊲ \overline{2}, which is inspired directly by the combinatory algebra B. The next two sections present some applications of this result. In Section 8 we use it to give a fairly simple (and more self-contained) alternative proof of van Oosten’s theorem, and to show how one can obtain recursive types as retracts of \overline{2}. In Section 9 we show that every effective SR functional is definable in the language PCF extended with a single universal functional H of type level 3. The language PCF+H gives us yet another handle on the SR functionals, yielding various new results. We also prove a technical fact: there is no universal SR functional of an essentially simpler type than that of H. Sections 7–9 are mostly independent of 4–6, except that Sections 8.1 and 9.4 refer to the material on hypercoherences.

We then point out some of the connections between our results and other ideas in semantics. In Section 10 we review our results from the standpoint of synthetic domain theory. In Section 11 we consider the relationship between sequential realizability and other possible notions of higher-type computability. We show that, in a suitable precise sense, there can be no “ultimate” notion of higher-type computability that subsumes all reasonable such notions. One may interpret this latter fact as a kind of “anti-Church’s Thesis” for higher types.

We end the paper with a discussion of the significance of our results, and of the claim that they embody a natural notion of “sequential” higher-type functional. We also mention some avenues for further research, including the possible applications of the SR functionals to programming language design.

In the present paper we study the SR functionals mainly from a “denotational” point of view, touching only intermittently on the issue of how they might be implemented operationally. This latter question could cover both the design of particular syntactic systems (programming languages) for implementing the SR functionals, and the use of games as an intensional-semantical setting for modelling various operational paradigms. We will survey some of this territory briefly in Section 12.3; a more detailed study of the SR functionals from an operational perspective may appear in a subsequent paper.

1.3 Acknowledgements

I have benefited from discussions and correspondence with very many people, including Samson Abramsky, Thomas Ehrhard, Martín Escardó, Martin Hyland, Jim Laird, Hanno Nickau, Luke Ong, Jaap van Oosten, Gordon Plotkin, Alex Simpson and Thomas Streicher. I also thank Gail Kemp for moral support. This research was funded by the EPSRC Research Grants GR/L89532 “Notions of computability for general datatypes” and GR/J84205 “Frameworks for programming language semantics and logic”.

2 A combinatory algebra for sequential computation

2.1 Construction of B and B_{eff}.

We begin by describing the combinatory algebra B introduced by van Oosten in [43]. We will follow van Oosten’s notation in certain respects.

Let N be the set of natural numbers (including 0), and let N_{⊥} = N ⊔ {⊥}. We will identify partial functions N ⇀ N with total functions N → N_{⊥}; we write N_{⊥}^{N} for the set of such functions.

As a first step, let us consider informally the possible behaviours of a “sequential” algorithm or strategy σ for computing a partial function F : N_{⊥}^{N} ⇀ N. Suppose σ is presented with a function g : N → N_{⊥} as an argument. There are three possibilities: Firstly, σ might simply diverge, in which case F is the everywhere undefined function. Secondly, σ might return a natural number straightaway, in which case F is a constant function. Thirdly, σ might ask for the value of g on some argument n, say. If g(n) is undefined, then σ can do nothing; however, if g(n) returns an answer m, then the subsequent behaviour of σ may be conditional on m. Indeed, for each value of m we have again the above three possibilities for the behaviour of σ, and so on.

We may represent the behaviour of such a strategy σ as a (finite or infinite) decision tree. This consists of a set of nodes, each carrying a label which may be either a question ?n or an answer !n (n ∈ N). At each node, the children are indexed by (a subset of the) natural numbers. The way in which such a decision tree represents a strategy should be clear from Figure 1, which shows part of a decision tree together with pseudocode for the corresponding part of the strategy. (Decision trees of this kind will be very familiar to readers of e.g. [5, 12].)

Formally, we may identify the nodes of a decision tree with finite sequences of natural numbers: the root node is the empty sequence ϵ, and the child m of the node [m_{1}, …, m_{k}] (if it exists) is the node [m_{1}, …, m_{k}, m]. (This is the notation we shall use for displaying finite sequences.) We write Seq(N) for the set of finite sequences of natural numbers (including ϵ), and use α, β, … to range over Seq(N). (Note that Roman letters will stand for natural numbers and Greek letters for sequences.) We write m; α or α; m for the result of adjoining a new element at the beginning or end of a sequence, and α; β for concatenation of sequences.

Likewise, we may identify the labels in a decision tree with elements of N+N, where the left and right summands correspond to the tags ? and ! respectively. This leads us to the following definition:

Definition 2.1 A decision tree is formally a partial function σ : Seq(N) → N + N. The domain of σ is the set of nodes in the tree.

One might ask whether one ought also to impose hygiene conditions on σ: for example, that the set of nodes of the tree is prefix-closed, and that labels !n may appear only on leaves of the tree. In fact such conditions will not be necessary, although trees that do not satisfy them will contain “dead” nodes that will never be reached in any play of the strategy. Note also that the same question may

[figure]

           ?5

[figure]

 !4

[figure]

           ?3

[figure]

                    ?1

                         ...

[figure]

      !7

[figure]

                ?0

                    ...

      0

            2

[figure]

                 3

        0

[figure]

               1

[figure]

              .....

                                  fn g =>
                                    case g(5) of
                                      0 => output 4
                                    | 1 => diverge
                                    | 2 => (case g(3) of
                                         0 => output 7
                                       | 1 => (case g(0) of ...)
                                         ...)
                                    | 3 => (case g(1) of
                                           => diverge)
                                      ...

Figure 1: Part of a decision tree for a sequential strategy

be asked twice on the same path through the tree, and this too may give rise to inaccessible nodes.

The key observation in the construction of B is that nodes and labels can themselves be coded as natural numbers—that is, both Seq(N) and N + N admit injections into N. Let ⟨⋯⟩ : Seq(N) ↣ N be some effective coding for nodes: for example, take

⟨ϵ⟩ = 0, ⟨m_{1}, …, m_{k}⟩ = 2^{m_{1}}3^{m_{2}} … p_{k}^{m_{k}+1} − 1,

where ⟨m_{1}, …, m_{k}⟩ abbreviates ⟨[m_{1}, …, m_{k}]⟩. Likewise, let [?,!] : N + N ↣ N be some effective coding for labels, for example:

?(n) = 2n, !(n) = 2n + 1.

In general, we will require simply that these encoding operations are effective. It is automatic that the images of these encodings are semidecidable subsets of N, and that the corresponding decoding operations are effective. (The particular codings given above are of course bijective, but this is not a necessary property and we will not assume it below.)

Using these codings, we can represent a decision tree σ : Seq(N) ⇀ N + N simply by a partial function f : N ⇀ N (i.e. by an element f ∈ N_{⊥}^{N}). Explicitly, we say f represents σ if for all α ∈ Seq(N) and l ∈ N + N we have

f(⟨α⟩) = [?,!](l) iff σα = l.

Clearly, every partial function f ∈ N_{⊥}^{N} represents a unique decision tree σ_{f}, and for every decision tree σ there is a least partial function f_{σ} that represents it.

If f represents σ, a play of σ against a function g may be viewed as a “dialogue” between f and g. Thus, the procedure for playing a strategy against an argument gives rise to an operation |: N_{⊥}^{N} × N_{⊥}^{N} → N_{⊥}. This operation is intuitively sequentially computable; the following informal ML-style recursive definition gives the idea. (A more formal definition in call-by-value PCF will be given in Section 9.1.)

fun play f g α =
case f⟨α⟩ of
!n ⇒ n
|?n ⇒ (case g(n) of m ⇒ play f g (α; m))
fun | f g = play f g ϵ

A minor modification of this gives us an operation • : N_{⊥}^{N} × N_{⊥}^{N} → N_{⊥}^{N}: in effect, we use f to represent an infinite forest of decision trees rather than just a single one.

fun • f g = (fn n ⇒ play f g [n])

These ideas may be expressed more formally as follows:

Definition 2.2 (i) Let play : N_{⊥}^{N} × N_{⊥}^{N} × Seq(N) → N_{⊥} be the smallest partial function such that, for all f, g ∈ N_{⊥}^{N}, α ∈ Seq(N) and n, m ∈ N,

• if f⟨α⟩ = !n then play(f, g, α) = n,

• if f⟨α⟩ = ?n and g(n) = m then play(f, g, α) = play(f, g, (α; m)).

(ii) Let |, • be the operations defined by

f | g = play(f, g, ϵ), f • g = λn.play(f, g, [n]).

Let B be the applicative structure (N_{⊥}^{N}, •).

Clearly the function play can be constructed by an iteration up to ω. As usual, we take • to be left-associative in expressions such as f • g • h. By abuse of notation, we sometimes write B for the underlying set N_{⊥}^{N}.

As is observed in [43], the construction of B is reminiscent of Kleene’s second model K_{2}, the partial combinatory algebra for “function realizability” (see [25]). In both cases, the elements are functions from N to N, and at each stage in the application of f to g, f either returns a result or requests further information about g. However, B differs from K_{2} in two respects: firstly, we use partial rather than total functions on N; and secondly, at each stage f is allowed to specify the particular piece of further information about g that it would like to see.

We will write ⊑ for the pointwise ordering on B. It is clear that (B, ⊑) is a CPO and that the functions play, | and • are monotone and continuous.

It is easy to check that if f, g ∈ N_{⊥}^{N} are partial recursive then so is f • g. This justifies the following definition:

Definition 2.3 Let N_{⊥}^{N}_{eff} be the subset of N_{⊥}^{N} consisting of the partial recursive functions, and let B_{eff} be the applicative structure (N_{⊥}^{N}_{eff}, •). The elements of B_{eff} are called effective elements of B.

2.2 Combinatory completeness

The main result of this section is that B and B_{eff} are both combinatory algebras: in fact, there are elements k, s ∈ B_{eff} such that for all x, y, z ∈ B we have

k • x • y = x, s • x • y • z = (x • z) • (y • z).

(The fact that B is a combinatory algebra was stated without proof in [43].)

Although the definition of application in B is fairly simple, the proof that it is a combinatory algebra seems to require a significant effort, however it is tackled. This is perhaps surprising: intuitively it seems fairly clear that for both k and s there are sequential algorithms that mediate the appropriate interactions between x, y, z. However, a direct definition of s in particular would be very cumbersome, and it seems more illuminating to obtain k, s indirectly via Curry’s combinatory completeness property. We use the following standard notions from the theory of combinatory algebras (cf. [3, chapter 5]).

Definition 2.4 (i) Let V be an infinite supply of formal variables, and suppose we also have a formal constant c for each element c ∈ B. The formal expressions over B are freely constructed from variables and constants via formal juxtaposition (a binary operation). If x_{0}, …, x_{r} are distinct variables, we write x_{0}, …, x_{r} ⊢ e to mean that e is a formal expression whose variables are among x_{0}, …, x_{r}.

(ii) A valuation ν for x_{0}, …, x_{r} associates to each x_{i} an element a_{i} = ν(x_{i}) of B. Formally, a valuation is an ordered list (x_{0} ↦ a_{0}, …, x_{r} ↦ a_{r}). If x_{0}, …, x_{r} ⊢ e and ν is a valuation for x_{0}, …, x_{r}, we define the interpretation [[ e]]_{ν} of e relative to ν inductively as follows:

• If c is a constant then [[ c]]_{ν} = c.

• If x is a variable then [[ x]]_{ν} = ν(x).

• If e_{1}e_{2} is a juxtaposition then [[ e_{1}e_{2} ]]_{ν} = [[ e_{1} ]]_{ν} • [[ e_{2} ]]_{ν}.

Our goal is to show the following: if x_{0}, …, x_{r} ⊢ e then there exists f ∈ B such that for all valuations ν = (x_{0} ↦ a_{0}, …, x_{r} ↦ a_{r}) we have f •a_{0} •⋯•a_{r} = [[ e]]_{ν}. As a first step, we prove an “uncurried” version of this, in which f takes the arguments a_{0}, …, a_{r} all together rather than separately. As a means of lumping arguments together, let us say that an element b ∈ B represents a valuation (x_{0} ↦ a_{0}, …, x_{r} ↦ a_{r}) if b⟨i, n⟩ = a_{i}(n) whenever 0 ≤ i ≤ r and n ∈ N.

Proposition 2.5 Suppose x⃗ ⊢ e, where x⃗ abbreviates x_{0}, …, x_{r}. Then there is a (canonical) element (Λx⃗.e) ∈ B such that whenever ν is a valuation for x⃗ and b represents ν, we have (Λx⃗.e) • b = [[ e]]_{ν}. Moreover, if all the constants occurring in e are effective then so is (Λx⃗.e).

Proof By induction on the structure of e.

• For constants c ∈ B, let (Λx⃗.c) be the (least) partial function f such that for all n, m, c(n) = m implies f⟨n⟩ =!m. Clearly (Λx⃗.c)•b = c for all b ∈ B. Moreover, if c is effective then so is (Λx⃗.c).

• For variables x_{i}, let (Λx⃗.x_{i}) be the partial function f given by

f⟨n⟩ =?⟨i, n⟩, f⟨n, m⟩ =!m.

Clearly, if b represents (x_{0} ↦ a_{0}, …, x_{r} ↦ a_{r}) then (Λx⃗.x_{i}) • b = a_{i}. Moreover, (Λx⃗.x_{i}) is always effective.

• For juxtapositions e_{1}e_{2}, suppose f_{1} = (Λx⃗.e_{1}) and f_{2} = (Λx⃗.e_{2}). We will construct f ∈ B such that for all b we have f • b = (f_{1} • b) • (f_{2} • b). Let play_{1} : N × Seq(N) → N_{⊥} and play_{2} : N × N × Seq(N) → N_{⊥} be the smallest partial functions satisfying the following conditions for all m, p, q, α, β, γ:

– If f_{1}⟨α⟩ =?q then play_{1}(⟨α⟩, ϵ) =?q and play_{1}(⟨α⟩, (m, γ)) = play_{1}(⟨α, m⟩, γ).

– If f_{1}⟨α⟩ =!(!p) then play_{1}(⟨α⟩, ϵ) =!p.

– If f_{1}⟨α⟩ =!(?q) then play_{1}(⟨α⟩, γ) = play_{2}(⟨α⟩, ⟨q⟩, γ).

– If f_{2}⟨β⟩ =?q then play_{2}(⟨α⟩, ⟨β⟩, ϵ) =?q and play_{2}(⟨α⟩, ⟨β⟩, (m, γ)) = play_{2}(⟨α⟩, ⟨β, m⟩, γ).

– If f_{2}⟨β⟩ =!p then play_{2}(⟨α⟩, ⟨β⟩, γ) = play_{1}(⟨α, p⟩, γ).

(Clearly play_{1}, play_{2} can be constructed by simultaneous iteration.) Now define f by f⟨n; α⟩ = play_{1}(⟨n⟩, α). By some tedious inductions, it is straightforward to verify that f has the desired property.

Set (Λx⃗.e_{1}e_{2}) = f; then (Λx⃗.e_{1}e_{2})•b = [[ e_{1}e_{2} ]]_{ν} provided both (Λx⃗.e_{1})•b = [[ e_{1} ]]_{ν} and (Λx⃗.e_{2}) • b = [[ e_{2} ]]_{ν}. Moreover, it is easy to see that if both (Λx⃗.e_{1}) and (Λx⃗.e_{2}) are effective then so is (Λx⃗.e_{1}e_{2}). □

The next step is to show that (Λx⃗.e) can be transformed into a representation of e that takes its arguments one at a time. Some further notation will be helpful. If b, c ∈ B and i ∈ N, define b[c/x_{i}] ∈ B as follows: if m = ⟨i, n⟩ for some n then b[c/x_{i}](m) = c(n); otherwise b[c/x_{i}](m) = b(m). Note that if b represents (x_{0} ↦ a_{0}, …, x_{r} ↦ a_{r}) and 0 ≤ i ≤ r, then b[c/x_{i}] represents (x_{0} ↦ a_{0}, …, x_{i} ↦ c, …, x_{r} ↦ a_{r}).

Proposition 2.6 Given any f ∈ B and i ∈ N, there is a (canonical) element curry_{i}(f) ∈ B such that for all b, c ∈ B we have curry_{i}(f) • b • c = f • b[c/x_{i}]. Moreover, if f is effective then so is curry_{i}(f).

Proof Let play′ : N × Seq(N) × Seq(N) → N_{⊥} be the smallest partial function satisfying the following conditions for all m, n, p, q, α, β, γ:

– If f⟨α⟩ =!p then play′(⟨α⟩, ϵ, ϵ) =!(!p).

– If f⟨α⟩ =?⟨i, n⟩ then play′(⟨α⟩, ϵ, ϵ) =!(?n)

and play′(⟨α⟩, (m, β), γ) = play′(⟨α, m⟩, β, γ).

– If f⟨α⟩ =?q where ¬∃n. q = ⟨i, n⟩, then play′(⟨α⟩, β, ϵ) =?q and play′(⟨α⟩, β, (m, γ)) = play′(⟨α, m⟩, β, γ).

Now define curry_{i}(f) by curry_{i}(f)⟨⟨n, β⟩, γ⟩ = play′(⟨n⟩, β, γ). It is straightforward to show that curry_{i}(f) has the required property, and the effectivity condition is obvious. □

It now follows readily that B, B_{eff} are combinatory algebras.

Theorem 2.7 (Combinatory completeness) (i) Suppose that x_{0}, …, x_{r} ⊢ e. Then there is an element (λ^{∗}x⃗.e) ∈ B such that for all valuations ν = (x⃗ ↦ a⃗) we have (λ^{∗}x⃗.e) • a_{0} • ⋯ • a_{r} = [[ e]]_{ν}. Moreover, if all constants appearing in e are effective then so is (λ^{∗}x⃗.e).

(ii) There exist k, s ∈ B_{eff} such that for all x, y, z ∈ B we have k • x • y = x, s • x • y • z = (x • z) • (y • z).

Proof (i) Define (λ^{∗}x⃗.e) = (curry_{0}(… (curry_{r}(Λx⃗.e)) …)) • (λn.⊥). Note that for any ν = (x⃗ ↦ a⃗), the element (λn.⊥)[a_{0}/x_{0}] … [a_{r}/x_{r}] represents ν. So by Propositions 2.6 and 2.5 we have

(λ^{∗}x⃗.e) • a_{0} • ⋯ • a_{r} = (Λx⃗.e) • (λn.⊥)[a_{0}/x_{0}] … [a_{r}/x_{r}] = [[ e]]_{ν}.

The effectivity condition follows from those in Propositions 2.6 and 2.5. (ii) Take k = (λ^{∗}xy.x), s = (λ^{∗}xyz.(xz)(yz)). □

Remarks 2.8 (i) The construction of B can be carried out more generally starting from any infinite set X equipped with injective coding functions Seq(X) ↣ X and X + X ↣ X.

(ii) A combinatory algebra A closely related to B has recently been constructed by Samson Abramsky, using ideas from Girard’s Geometry of Interaction and the history-free games model of [2]. The construction of A makes use of coding operations [L, R] : N + N ↣ N and pair : N × N → N. The underlying set of A is N_{⊥}^{N}, and application is defined by the formula

f • g = L^{−1} ∘ ⋃_{r≥0} h^{r} ∘ f ∘ L,

where h = f ∘ R ∘!g ∘ R^{−1} and !g = pair ∘ (id × g) ∘ pair^{−1}. Further details and motivation are given in [32].

It turns out that A and B are equivalent in the sense of [31]. More particularly, they have the same underlying set, and application in each is representable in the other. It follows that A, B give rise to exactly the same category of modest sets (see Section 3). However, the construction of A seems to be of independent interest for several reasons—for instance, subject to some conditions on the coding operations, one can identify a subalgebra A_{wb} of well-bracketed strategies, which yields a realizability model embodying the PCF notion of sequentiality (see [32]).

We will see in Section 4 that B and B_{eff} are λ-algebras, though they are not λ-models. An interesting question, suggested to us by Luke Ong, is whether one can find a good syntactic calculus (such as an untyped λ-calculus with control features or a suitable extension of combinatory logic) in which all the effective elements of B are definable.

In the remainder of this section we establish some technical facts about B and B_{eff} which give further insight into their nature.

2.3 Irredundant realizers

We have already mentioned that our decision trees may contain redundancy in that the same question may be asked more than once along a single path, and may also contain inaccessible nodes for other reasons. We show here that any decision tree may be “pruned” to yield an equivalent tree not suffering from any of these kinds of redundancy, and that moreover this pruning operation may be performed within B itself.

In fact we will consider two notions of irredundant element, according to whether we are thinking of single decision trees or infinite forests.

Definition 2.9 (Irredundant elements) Let f be an element of B. (i) f is |-irredundant if, for all α, β ∈ Seq(N),

• if f⟨α⟩ is defined then it is a question or an answer;

• if f⟨α⟩ is defined and β is a proper prefix of α then f⟨β⟩ is a question;

• if f⟨α⟩ is defined and β is a proper prefix of α then f⟨β⟩ ≠ f⟨α⟩.

(ii) f is •-irredundant if f⟨ϵ⟩ = ⊥ and f_{n} is |-irredundant for each n, where f_{n}⟨α⟩ = f⟨n; α⟩.

The important facts about irredundant elements are given by the following:

Proposition 2.10 (i) To each f ∈ B we may associate a |-irredundant element irr_{|}(f) such that irr_{|}(f) | g = f | g for all g, and if f is already |-irredundant then irr_{|}(f) = f. Moreover, there is an element irr_{|} ∈ B_{eff} such that irr_{|} • f = irr_{|}(f) for all f.

(ii) Likewise, to each f ∈ B we may associate a •-irredundant irr_{•}(f) such that irr_{•}(g) • g = f • g for all g, and if f is •-irredundant then irr_{•}(f) = f. Moreover, there is an element irr_{•} ∈ B_{eff} such that irr_{•} • f = irr_{•}(f) for all f.

Proof (i) The informal idea behind the construction of irr_{|}(f) from f is clear: we simply drop all inaccessible nodes of f, and omit all repetitions of previously asked questions, knowing that they must receive the same answer as before. Thus, to find out what irr_{|}(f)⟨m_{1}, …, m_{l}⟩ should be, we may engage in a dialogue with f, using m_{1}, …, m_{l} as a “script” giving the answers to the first l distinct questions asked by f. Formally, we define irr_{|}(f) to be the smallest partial function f_{0} such that f_{0}⟨m_{1}, …, m_{l}⟩ = f⟨t_{1}, …, t_{j}⟩ whenever the following conditions hold for some q_{1}, …, q_{j}, r_{1}, …, r_{l}:

• f⟨t_{1}, …, t_{i−1}⟩ =?q_{i} for 1 ≤ i ≤ j;

• r_{1}, …, r_{l} are the distinct elements of the sequence q_{1}, …, q_{j} in order of

appearance, and whenever q_{i} = r_{h} we have t_{i} = m_{h};
• f⟨t_{1}, …, t_{j}⟩ is of the form !p or ?q where q ∉ {q_{1}, …, q_{j}}.

It is routine to verify that irr_{|}(f) | g = n iff f | g = n, that irr_{|}(f) is |-irredundant, and that if f is |-irredundant then irr_{|}(f) = f.

It remains to show that there exists irr_{|} ∈ B_{eff} that computes irr_{|}(f) from f. Formally, let irr_{|} be the least partial function satisfying the following for all α = m_{1}, …, m_{l} and β:

• If β =?q_{1}, …,?q_{j} and r_{1}, …, r_{k} are the distinct elements of q_{1}, …, q_{j} in order of appearance, where k ≤ l, then irr_{|}⟨⟨α⟩, β⟩ =?⟨m_{h(1)}, …, m_{h(j)}⟩, where each h(i) is determined by q_{i} = r_{h(i)}.

• If β =?q_{1}, …,?q_{j} contains exactly l distinct questions and u is of the form !p or ?q where q ∉ {q_{1}, …, q_{j}}, then irr_{|}⟨⟨α⟩, β, u⟩ =!u.

Clearly irr_{|} is effective, and it is easy to verify that irr_{|} • f = irr_{|}(f) for any f. (ii) We may now define irr_{•} ∈ B_{eff} as the least partial function such that

• if irr_{|}⟨⟨α⟩, β⟩ =?⟨γ⟩ then irr_{•}⟨n, α, β⟩ =?⟨n, γ⟩;

• if irr_{|}⟨⟨α⟩, β⟩ =!u, then irr_{•}⟨n, α, β⟩ =!u,

and take irr_{•}(f) = irr_{•} • f. It is easy to see that irr_{•}(f) has the required properties. □

There is an analogy here with the Scott graph model Pω [50]. In both B and Pω we may identify a class of “canonical” realizers we may associate to each element x a canonical element that represents the same endofunction, and moreover this canonical element can be computed from x within the combinatory algebra itself. However, there is an important difference: in Pω there is a unique canonical element representing any given continuous function (namely its graph), but in B there are usually many irredundant elements that represent a given sequential function, corresponding to different sequential algorithms (cf. Section 4).

2.4 A fixed point combinator

In any combinatory algebra (A, ·), we say that an element y is a fixed point combinator if y·x = x·(y·x) for every x. It is well known that every combinatory algebra has a fixed point combinator: for instance, we may define one by Curry’s formula

y = (λ^{∗}xy.y(xxy))(λ^{∗}xy.y(xxy)).

On the other hand, for every x ∈ B we know that the function α_{x} : y ↦ x • y is continuous with respect to the CPO structure of B, so it has a least fixed point.

Perhaps surprisingly, there are fixed point combinators in B that do not always compute the least fixed point. Our aim here is to show that there is one that does. The combinator defined above would probably suffice, but it is easier to show the required property for a more concretely defined element y.

Lemma 2.11 There is an element y ∈ B_{eff} such that for all x ∈ B, y • x is the least fixed point of α_{x}.

Proof Let i = s • k • k, so that i • x = x for all x. Let y_{0} be the element ⊥ ∈ B (i.e. the function λm.⊥), and define inductively y_{k+1} = s • i • y_{k}. Since y_{0} ⊆ y_{1}, by induction we have y_{k} ⊆ y_{k} + 1 for every k. So take y = ⨆ y_{k}. Since the y_{k} are effective uniformly in k, clearly y is effective.

Now take any x ∈ B. We have y_{0} • x = ⊥, and so by induction we have y_{k} • x = α_{x}^{k}(⊥) for each k. Since application is continuous, we have y • x = ⨆ α_{x}^{k}(⊥), and this is the least fixed point of α_{x}. □

It follows immediately that if x ∈ B_{eff} then the least fixed point of α_{x} is also an element of B_{eff}. For the rest of the paper, y will denote the element of B_{eff} given by the above proof.

3 Realizability models

3.1 Realizability models over B and B_{eff}

We now review the construction of the standard realizability models corresponding to B and B_{eff}. We will focus almost entirely on the categories of modest sets over these combinatory algebras; these are full subcategories of the corresponding realizability toposes, but in this paper we shall only occasionally refer to the latter. We will use the notation and terminology of [31], where further information on realizability models may be found.

The following definition makes sense for any combinatory algebra (A, ·):

Definition 3.1 (Modest sets) (i) A modest set X over A consists of a set |X| (called the underlying set of X) together with a function assigning to each x ∈ |X| a non-empty set ∥x∥ ⊆ A (called the set of realizers for x), such that

a ∈ ∥x∥ ∧ a ∈ ∥x′∥ ⟹ x = x′.

We sometimes write ∥x∥_{X} for ∥x∥ to avoid ambiguity.

(ii) Suppose X, Y are two modest sets over A. A function f : |X| → |Y | is said to be tracked by r ∈ A if for all x ∈ |X| and a ∈ ∥x∥_{X} we have r · a ∈ ∥fx∥_{Y}. A morphism f : X → Y is a function f : |X| → |Y | that is tracked by some r ∈ A. We write Mod(A) for the category of modest sets over A and morphisms between them.

Remarks 3.2 (i) The fact that Mod(A) is a category follows easily from the combinatory completeness of (A, ·). It is easy to see that Mod(A) is equivalent to the category PER(A) of partial equivalence relations on A.

(ii) Typically we are only interested in properties of modest sets up to isomorphism, and we will often switch freely between different representatives of the same isomorphism class, using whichever is most convenient. We may think of isomorphic modest sets as different presentations of essentially the same object.

One can think of a modest set X as a “datatype”, where for each value x ∈ |X| we have a set ∥x∥ of “intensional representations” of x. The category of modest sets turns out to have very good properties (for more details see [31]):

Proposition 3.3 The category Mod(A) is cartesian closed and regular, and it has finite sums and a natural number object. □

We recall the construction of exponentials in Mod(A). If X and Y are modest sets, then Y^{X} is defined as follows: |Y^{X}| is the set of morphisms f : X → Y, and ∥f∥_{Y^{X}} is the set of elements r ∈ A that track f. It is easy to check that Y^{X} is indeed a modest set. The evaluation morphism Y^{X} × X → Y is the obvious function |Y^{X}| × |X| → |Y |.

We now identify some important structure in Mod(B) and Mod(B_{eff}). (Note at once that Mod(B_{eff}) is a non-full subcategory of Mod(B).) For the terminal object 1 in both categories, we may take |1| = {∗}, ∥ ∗ ∥ = {λm.⊥}. For the natural number object N, we take |N| = N, ∥n∥ = \{\overline{n}\}, where \overline{(}n) : 0 ↦ n, m + 1 ↦ ⊥. It is easy to check that N (equipped with the obvious zero and successor morphisms) is indeed a natural number object in both Mod(B) and Mod(B_{eff}).

Next we define a lift operation −_{⊥} on objects of Mod(B). Let up : B → B be the function defined by

up(r)(0) = 0, up(r)(n + 1) = r(n),

and for any object X, let X_{⊥} be the object given by

|X_{⊥}| = |X| ⊔ {⊥}, ∥x∥_{X_{⊥}} = {up(r) | r ∈ ∥x∥_{X}}, ∥⊥∥_{X_{⊥}} = {λn.⊥}.

The operation −_{⊥} clearly extends to a functor, and indeed a monad, on Mod(B), which restricts well to a monad on Mod(B). In the case of N_{⊥}, we will usually work with the following simpler presentation: |N_{⊥}| = N_{⊥}, ∥x∥ = \{\overline{x}\} (where \overline{⊥} = λm.⊥). It is easy to check that this is isomorphic to the object given by the definition of −_{⊥}.

In both categories, the object N_{⊥}^{N} has a particularly simple presentation. This will be very useful in Section 7 when we consider call-by-value PCF and various extensions of it.

Proposition 3.4 (i) Let B be the “object of realizers” in Mod(B), defined by |B| = N_{⊥}^{N}, ∥f∥ = {f}. Then B ≅ N_{⊥}^{N} in Mod(B).

(ii) Let B_{eff} be the object of realizers in Mod(B_{eff}): |B_{eff}| = N_{⊥}^{N}_{eff}, ∥f∥ = {f}. Then B_{eff} ≅ N_{⊥}^{N} in Mod(B_{eff}). □

Note that the operation • is representable in B_{eff} by the element λ^{∗}xy.xy. Hence it is easy to see that the operation | is also representable in B_{eff} in the following sense: there is an element bar ∈ B_{eff} such that for all f, g ∈ B and x ∈ N_{⊥}, bar • f • g = \overline{x} iff f | g = x. It follows that in both Mod(B) and Mod(B_{eff}) there are morphisms dot : N_{⊥}^{N} ×N_{⊥}^{N} → N_{⊥}^{N} and bar : N_{⊥}^{N} ×N_{⊥}^{N} → N_{⊥} corresponding to • and | respectively.

3.2 The SR functionals

We are now ready to interpret the simple types in Mod(B). This will lead to our definition of the sequentially realizable functionals, which are the primary objects of study in this paper.

Definition 3.5 (Simple types) (i) The simple types (or finite types) are freely generated from a single ground type \overline{0} via the binary type constructor →:

σ := \overline{0} | σ_{1} → σ_{2}.

The pure types \overline{0}, \overline{1}, \overline{2}, … are defined by \overline{k + 1} = \overline{k} → \overline{0}.

(ii) For each type σ, its interpretation in Mod(B) is the object [[ σ]] given by

[[ \overline{0} ]] = N_{⊥}, [[ σ_{1} → σ_{2} ]] = [[ σ_{2} ]]^{[[ σ_{1} ]]}.

The interpretation [[ σ]]_{eff} in Mod(B_{eff}) is defined analogously.

Note that the above gives the “call-by-name” interpretation of the simple types, i.e. the one used for modelling the call-by-name version of PCF, as in [45]. We will content ourselves with this for the time being, but in Section 7 we shall also consider the call-by-value interpretation.

The sequentially realizable functionals themselves are introduced via a general notion of (abstract) type structure. For now, we choose a definition of type structure that matches our call-by-name interpretation of types.

Definition 3.6 (i) A (call-by-name, partial) type structure T consists of the following:

• a set T^{σ} for each type σ, where T \overline{0} = N_{⊥},

• for each σ, τ a total “application” function ·_{στ} : T^{σ→τ} × T^{σ} → T^{τ}.

(ii) The type structures R, R_{eff} are defined by R^{σ} = |[[ σ]]|, R_{eff}^{σ} = |[[ σ]]_{eff}|, with the application functions given by the evaluation morphisms. We call the elements of R the sequentially realizable (SR) functionals, and the elements of R_{eff} the effective SR functionals.

Clearly the type structures R, R_{eff} are both extensional, in the sense that if f · x = g · x for all x then f = g.

Remarks 3.7 (i) It should be clear already that both R and R_{eff} are in some sense models of PCF. One can easily exhibit realizers for the basic arithmetical operations; application and abstraction are given by the CCC structure of the category of modest sets; and for each type σ one can verify that the element y ∈ B_{eff} realizes fixed point operators Y ∈ R^{(σ→σ)→σ} and Y_{eff} ∈ R_{eff}^{(σ→σ)→σ}. One could prove directly at this stage that this gives adequate interpretations of PCF in R and R_{eff}, but we will defer a formal discussion of PCF until Section 9.

(ii) The reader may enjoy verifying that R\overline{2} and R\overline{2} eff also contain a non-PCF-definable element F with the following specification (this is essentially the example given in the Introduction):

F g = \{ \begin{matrix}0 & if g⊥ = 0 \\ 1 & if g⊥ = ⊥ but g0 = 0 \\ ⊥ & otherwise. \end{matrix}

Unfortunately, many of the basic properties of R and R_{eff} are difficult to prove directly from the above definitions. For instance, it will turn out that R_{eff} can be identified with a substructure of R (that is, there are inclusions R_{eff}^{σ} ↣ R^{σ} commuting with application), and that each R^{σ} is CPO with the ordering defined by

f ⊑ g ⇔ ∃q ∈ ∥f∥, r ∈ ∥g∥. q ⊑ r,

We will defer the proofs of these facts until we have gathered more information about these type structures.

3.3 Modified realizability

The construction given above will be the central one used in this paper. However, we now briefly consider another realizability construction that also gives rise to the SR functionals: the modified realizability model over B. The notion of modified realizability is due in essence to Kreisel [26]; modified realizability toposes have been extensively studied e.g. in [20, 44]. For our purposes, it suffices to consider a much smaller category, analogous to the category of modest sets.

In the following definition, A is any total combinatory algebra, and we suppose moreover that we have an element 0 ∈ A such that 0 · a = 0 for all a ∈ A. (The element 0 plays a technical role in the construction of modified realizability toposes; it is not too important for the purposes of this paper.)

Definition 3.8 (Modified modest sets) (i) A modified modest set^{2} X over a combinatory algebra A consists of a modest set X over A in the usual sense, together with a subset P_{X} ⊆ A (called the set of potential realizers for X) such that 0 ∈ P_{X} and ∥x∥ ⊆ P_{X} for all x ∈ |X|.

(ii) Suppose X, Y are modified modest sets over A. A function f : |X| → |Y | is said to be tracked in the modified sense by r ∈ A if r tracks f in the usual sense, and furthermore for all a ∈ P_{X} we have r·a ∈ P_{Y}. A morphism f : X → Y is a function f : |X| → |Y | that is tracked in the modified sense by some r ∈ A. We write mMod(A) for the category of modified modest sets.

Modified modest sets may be thought of as modest sets with some extra “type information” built in: we may think of P_{X} as giving a “type” for realizers of elements of X. It is easy to show that mMod(A) is a cartesian closed category. The exponential Y^{X} is defined as follows: |Y^{X}| is the set of morphisms X → Y in mMod(A); ∥f∥_{Y^{X}} is the set of elements r that track f in the modified sense; and P_{Y^{X}} is the set (P_{X} ⇒ P_{Y}) (in general we write (A ⇒ B) for the set {r | ∀a ∈ A. r • a ∈ B}).

In the case A = B or B_{eff}, we may take 0 = λm.⊥. Both mMod(B) and mMod(B_{eff}) have a natural number object N which may be described as follows: the underlying modest set of N is the object N described in Section 3.1, and P_{N} = \{\overline{⊥}, \overline{0}, \overline{1}, …\}. Likewise, there is an obvious candidate for N_{⊥} in these categories: the underlying modest set is N_{⊥}, and P_{N_{⊥}} = P_{N}. This means that as before we can give interpretations [[ −]]_{m}, [[ −]]_{m,eff} of the simple types in these categories, and hence obtain type structures R_{m}, R_{m,eff} from them.

Proposition 3.9 For A = B or B_{eff}, the interpretation of the simple types in mMod(A) agrees with that in Mod(A). That is, for each type σ we have U[[ σ]]_{m} = [[ σ]] and U[[ σ]]_{m,eff} = [[ σ]]_{eff}. Hence R_{m} = R and R_{m,eff} = R_{eff}.

Proof For simplicity, we just consider the case A = B; the effective case is similar. First observe that the object N_{⊥} in mMod(B) is isomorphic to the object N′_{⊥} described as follows: the underlying modest set of N′_{⊥} is again N_{⊥}, but P_{N′_{⊥}} is the whole of B. We can define an interpretation [[ −]]′_{m} of the simple types using N′_{⊥} instead of N′, and hence obtain a type structure R′_{m}; it is easy to show by induction on types that R′_{m} = R_{m}.

2Jaap van Oosten has pointed out to me that, in terms of the categorical properties of these objects within the modified realizability topos, the term “discrete” is perhaps more appropriate than “modest” in this context. However, here we will stick with the term “modest” to maintain a sense of analogy with Section 3.1.

We now show by induction on σ that U[[ σ]]′_{m} = [[ σ]] and P_{[[ σ]]′_{m}} = B. The base case is trivial by definition of N′_{⊥}. So suppose the hypotheses hold for σ and τ. By the definition of exponentials we have P_{[[ σ→τ ]]′_{m}} = {r | ∀a ∈ B. r · a ∈ B} = B, since B is total. It is now clear that U[[ σ → τ ]]′_{m} = [[ σ → τ ]]. □

Remark 3.10 Our category mMod(A) is restricted enough that it embeds fully in both the modified realizability topos mRT(A) and Streicher’s category MAss(A) of modified assemblies over A (see [54]). Both these embeddings preserve the cartesian closed structure, but unfortunately (in the case A = B or B_{eff}) neither of them preserves the natural number object.

One reason for being particularly interested in our object N_{⊥} will become apparent in Section 5. But we would also expect that in both mRT(B) and MAss(B), the finite types over the true natural number object yield the SR functionals.

4 Concrete data structures

In this section we consider the concrete data structures (CDSs) of Kahn and Plotkin [22], together with the sequential algorithms and sequential functions studied by Berry and Curien [5]. We will see that B itself be regarded as a universal object for a certain class of CDSs. It follows that a certain category of CDSs and sequential functions can be identified with a full subcategory of Mod(B), and that moreover there is a strong connection between sequential algorithms of cds and realizers in Mod(B).

4.1 Basic definitions

We begin by recalling some definitions from [5]. We refer the reader to this paper or to the book [14] for further details and motivation.

Definition 4.1 A concrete data structure (CDS) M consists of the following:

• a countable set C_{M} of cells;

• a countable set of V_{M} of values;

• a set E_{M} ⊆ C_{M} × V_{M} of events, such that for all c ∈ C_{M} there is at least one v such that (c, v) ∈ E_{M};

• an enabling relation ⊢_{M} between finite subsets of E_{M} and elements of C_{M}, which is well-founded in the following sense: there is no infinite sequence c_{0}, c_{1}, … of cells such that for each i there is a finite set t ⊆ E_{M} such that t ⊢_{M} c_{i} and t contains some element (c_{i+1}, v).

A state x of M is a subset of E_{M} such that • if (c, v) ∈ x and (c, v′) ∈ x then v = v′;

• if (c, v) ∈ x then there exists a finite set t ⊆ x such that t ⊢ c.

We write (D_{M}, ⊑) for the set of states of M ordered by inclusion. We also write D_{M}^{0} for the set of finite states of M.

If t ⊢ c we say that t is an enabling of c. We say that c is filled in a state x if (c, v) ∈ x for some v, and that c is accessible from x if c is not filled in x but x contains an enabling of c.

The well-foundedness condition implies that any non-empty CDS has at least one cell c such that ∅ ⊢ c; such a cell is called initial. The second condition in the definition of state ensures that every state is in some sense reachable. Note that the poset of states is always a CPO.

We will restrict our attention mainly to CDSs with the following property:

Definition 4.2 A CDS is deterministic, or is a DCDS, if for any state x and cell c, x contains at most one enabling of c.

Two different notions of morphism between DCDSs are of interest: the “extensional” notion of sequential function, and the more “intensional” notion of sequential algorithm. Sequential functions are simply certain functions between the relevant sets of states:

Definition 4.3 A sequential function f : M → M′ between DCDSs is a monotone and continuous function f : D_{M} → D_{M′} such that, for any x ∈ D_{M} and any c′ ∈ C_{M′} accessible from f(x), if there exists a state y ⊒ x such that c′ is filled in f(y), then there is a cell c ∈ C_{M} accessible from x such that c is filled in all such states y. Such a cell c is called a sequentiality index of f for c′ at x.

Note that the sequentiality index c need not be unique: indeed, a sequential algorithm can be regarded as telling us at each stage which cell c is to be filled next. Several equivalent definitions of sequential algorithm can be given; the following definition (adapted from [14]) is in some sense intermediate between the “concrete” and “abstract” definitions given in [5].

Definition 4.4 If M, M′ are DCDSs, the DCDS N = M^{′M} is defined as follows:

• C_{N} = D_{M}^{0} × C_{M′} (we will write the cell (x, c′) just as xc′).

• V_{N} = C_{M} +V_{M′} (we denote the left and right inclusions by ?,! respectively).

• Events of N are of two kinds:

– (xc′,?c) ∈ E_{N} iff c is accessible from x in M;

– (xc′,!v′) ∈ E_{N} iff (c′, v′) ∈ E_{M′}.

• Instances of the enabling relation of N are of two kinds:

– (yc′,?c) ⊢_{N} xc′ iff x = y ⊔ {(c, v)} for some v;

– (x_{1}c′_{1},!v′_{1}), …, (x_{n}c′_{n},!v′_{n}) ⊢_{N} xc′ iff x = x_{1} ∪ ⋯ ∪ x_{n}
and (c′_{1}, v′_{1}), …, (c′_{n}, v′_{n}) ⊢_{M′} c′.

A sequential algorithm a : M → M′ is simply a state of M^{′M}. The application operation · : D_{M^{′M}} × D_{M} → D_{M′} is defined by

a · x = {(c′, v′) | ∃y ⊑ x. (yc′,!v′) ∈ a}.

It is shown in [14] that if M and M′ are CDSs [resp. DCDSs] then so is M^{′M}. Moreover, for any sequential algorithm a : M → M′ between DCDSs, the mapping a_{∗} : x ↦ a · x : D_{M} → D′_{M} is a sequential function M → M′. Conversely, every sequential function between DCDSs is represented by at least one sequential algorithm in this way. (Accordingly, we will sometimes say things like “Let a_{∗} : M → M′ be a sequential function”.)

Given sequential algorithms a : M → M′ and b : M′ → M′′, their composition ba : M → M′′ may be defined directly (if somewhat opaquely) as follows.

– (xc′′,!v′′) ∈ ba iff for some y′ = {(c′_{1}, v′_{1}), …, (c′_{n}, v′_{n})} and x_{1}, …, x_{n} ∈ D_{M}^{0} with x = x_{1} ∪ ⋯ ∪ x_{n}, we have (x_{i}c′_{i},!v_{i}) ∈ a for each i, and (y′c′′,!v′′) ∈ b.

– (xc′′,?c) ∈ ba iff for some y′ = {(c′_{1}, v′_{1}), …, (c′_{n}, v′_{n})}, x_{0}, x_{1}, …, x_{n} ∈ D_{M}^{0} with x = x_{0} ∪ x_{1} ∪ ⋯ ∪ x_{n}, and c′ ∈ C_{M′}, we have (x_{i}c′_{i},!v_{i}) ∈ a for each i ≥ 1, (y′c′′,?c′) ∈ b and (x_{0}c′,?c) ∈ a.

This agrees with the indirect definition of composition given in [14, Section 2.6]. One can check that ba·x = b·(a·x), so composition for sequential algorithms agrees with composition for sequential functions. We write SeqAlg for the category of DCDSs and sequential algorithms. A major result of [5] is that SeqAlg is a cartesian closed category, with the exponential M^{′M} defined as above. However, it is well known that the category SeqFun of DCDSs and sequential functions is not cartesian closed.

The following condition was recognized by Curien as defining an interesting class of CDSs (see [14, Def. 2.1.10]):

Definition 4.5 A CDS M is called sequential if, for any cell d and any state x such that d is not filled in x, if there exists a state y ⊒ x such that d is filled in y, there is a cell c accessible from x such that c is filled in all such states y. Such a cell c is called a sequentiality index of M for d at x. We write SSeqFun for the category of sequential DCDSs with sequential functions, and SSeqAlg for the category of sequential DCDSs with sequential algorithms.

We will sometimes implicitly assume that a sequential CDS M comes equipped with a choice of sequentiality index c_{d,x} for each d and x to which the above conditions apply. Curien pointed out that sequential DCDSs are closed under finite products and exponentials—that is, SSeqAlg is a sub-CCC of SeqAlg. In fact, one can show that every sequential CDS is isomorphic to a sequential DCDS, and so the categories of sequential CDSs and sequential DCDSs are equivalent.

Remark 4.6 The above definitions all have a fairly evident effective analogue. For this, we need to work with CDSs M equipped with enumerations of C_{M} and V_{M}—that is, identifications of C_{M} and V_{M} with (not necessarily r.e.) subsets of N. An effective state of M is one that is given by a partial recursive function C_{M} ⇀ V_{M} (more precisely, by a partial recursive function N ⇀ V_{M} whose domain is contained in C_{M}). If M, M′ are DCDSs, a sequential function f : M → M′ is effective if, for all effective states x ∈ D_{M} and c′ ∈ C_{M′} satisfying the conditions of Definition 4.3, a sequentiality index of f for c′ at x can be recursively computed from c′ and a recursive index for x (one need not assume that different indices for x yield the same sequentiality index). An effective sequential algorithm M → M′ is just an effective state of M^{′M} (note that enumerations for M, M′ induce an enumeration for M^{′M} in a standard way). One may then check, by a routine effectivization of the standard proofs, that the effective sequential functions are precisely the maps induced by effective sequential algorithms. Such functions clearly map effective states to effective states.

We write SeqAlg_{eff} [resp. SeqFun_{eff}] for the category of enumerated DCDSs and effective sequential algorithms [resp. functions]. It is clear that SeqAlg_{eff} is cartesian closed, with the same exponentials as SeqAlg.

We say an enumerated DCDS M is effectively sequential for all cells d and effective states x satisfying the requirements in Definition 4.5, a sequentiality index for d at x can be recursively computed from d and an index for x (again, we need not assume extensionality). We write SSeqFun_{eff} and SSeqAlg_{eff} for the respective full subcategories of SeqFun_{eff} and SeqAlg_{eff} consisting of effectively sequential DCDSs.

4.2 B as a universal object

The key observation of this section is that the combinatory algebra B can be viewed as (the set of states of) a concrete data structure. The cells of this CDS are just the natural numbers; the values are also the natural numbers; every pair (c, v) is an event; and the enabling relation is given by ∅ ⊢ c for all c (all cells are initial). The states are then precisely the partial functions from cells to values, that is, elements of N_{⊥}^{N}. We will denote this CDS also by B.

It is easy to see that B is a sequential DCDS. Note that B can also be described as a countably infinite product (in either SeqFun or SeqAlg) of copies of a single-cell CDS N whose values are the natural numbers.

Any CDS M can be “embedded” in B in such a way that the states of M are identified with a subset of the states of B. Specifically, we pick some identifications of C_{M}, V_{M} with subsets of N (or we suppose such identifications are given by the hypothesis that C_{M}, V_{M} are countable). States of M are then identified with certain partial functions N ⇀ N, i.e. states of B. (We take these partial functions to be undefined outside the subset of N corresponding to C_{M}.) This gives us a continuous inclusion ι_{M} : D_{M} ↪ B between CPOs.

For convenience, we will assume henceforth that C_{M}, V_{M} actually are subsets of N for every M that we consider. Furthermore, in Definition 4.4, we identify V_{N} = C_{M} + V_{M′} with the set {?c | c ∈ C_{M}} ∪ {!v′ | v′ ∈ V_{M′}} where ?,! : N → N are the coding functions introduced in Section 2.

The following tells us when the embedding ι_{M} is well-behaved.

Proposition 4.7 For a DCDS M, the following conditions are equivalent: (i) M is sequential. (ii) ι_{M} is a sequential function i_{∗} : M → B. (iii) M is a retract of B in SeqFun. (iv) M is a retract of B in SeqAlg.

Proof (i) ⇒ (ii): Any sequentiality index of M for c at x is also a sequentiality index of ι_{M} for c at x. (Note that if c ∉ C_{M} then a sequentiality index of ι_{M} for n at x is not needed.) So ι_{M} = i_{∗} for some sequential algorithm i.

(ii) ⇒ (iii): It suffices to construct a sequential function j_{∗} : B → M such that j_{∗}i_{∗} = id_{M}. Let us say that a cell d is supported in a state y of B if there is a state x of M such that i_{∗}(x) ⊑ y and d is filled in i_{∗}(x). Write Σ_{y} for the set of cells supported in y, and define j_{∗}(y) to be the restriction of y to Σ_{y}. Clearly j_{∗} is monotone and continuous, and j_{∗}i_{∗} = id_{M}. Moreover, it is routine to check that j_{∗} is sequential.

(iii) ⇒ (i): Assume M →^{f_{∗}} B →^{g_{∗}} M is any retraction in SeqFun, and suppose we are given x ∈ D(M) and d not filled in x such that d is filled in some y ⊒ x. Since g_{∗}f_{∗}(x) = x, we may take c′ to be a sequentiality index of g_{∗} for d at f_{∗}(x); note that c′ is filled in f_{∗}(y). We can now take c a sequentiality index of f_{∗} for c′ at x, and check that c is a sequentiality index of M for d at x.

(iii) ⇒ (iv): It suffices to show that the only sequential algorithm representing the sequential function id_{M} is the identity. Clearly, for any cell c and state x, the only sequentiality index of id_{M} for c at x (if one exists) is c itself; and by the relationship between sequential algorithms and abstract algorithms established in [14, Section 2.6], this is enough.

(iv) ⇒ (iii) is trivial. □

The above proposition shows that B is a universal object in the categories SSeqFun and SSeqAlg. We henceforth suppose that each sequential DCDS M comes equipped with some choice of sequential algorithms i_{M}, j_{M} representing i_{∗}, j_{∗} respectively.

Since SSeqAlg is cartesian closed, we have that B^{B} is a retract of B—that is, B is a reflexive object in SSeqAlg. In fact, one can choose a retraction B^{B} ⊲ B that gives rise in the standard way to precisely the applicative structure (B, •). This is not the case for the particular retraction given by Proposition 4.7, but the following proposition establishes the relevant retraction. The essential force of this proposition is that irredundant realizers are sequential algorithms. (Throughout this section, “irredundant” will mean •-irredundant.)

Proposition 4.8 (i) To any sequential algorithm a : B → B there corresponds an irredundant element r_{a} ∈ B such that r • b = a · b for all b ∈ B.

(ii) The map I_{∗} : a ↦ r_{a} constitutes a sequential function B^{B} → B.

(iii) The map I_{∗} is a bijection between sequential algorithms B → B and irredundant elements of B.

(iv) The map J_{∗} : r ↦ I_{∗}^{−1}(irr_{•}(r)) constitutes a sequential function B → B^{B}.

Proof (i) Given a sequential algorithm a, we may construct a realizer r = r_{a} as follows. For each n ∈ N, let ρ_{n} : Seq(N) ⇀ B^{0} be the (unique) smallest partial function with the following properties:

• ρ_{n}(ϵ) = ∅.
• If ρ_{n}(α) = x and (xn,?m) ∈ a, then ρ_{n}(α, v) = x ∪ {m ↦ v}.

We now take r to be the smallest partial function such that, for all n, α, if ρ_{n}(α) = x and (xn, l) ∈ a (where l may be ?c or !v) then r⟨n, α⟩ = l.

We first check that r is irredundant. If r⟨n, α⟩ = l then from the definition l is a question or an answer. If moreover β is a proper prefix of α then ρ_{n}(β, v) is defined for some v, so if y = ρ_{n}(β) then (yn,?m) ∈ a for some m, whence r⟨n, β⟩ =?m. Finally, we have (m, v) ∈ ρ_{n}(β_{v}) ⊑ ρ_{n}(α), and so if x = ρ_{n}(α) then (xn,?m) ∉ a, so r⟨n, α⟩ ≠?m.

Next we show that r realizes b ↦ a · b, that is, (r • b)(n) = v iff ∃x ⊑ b. (xn,!v) ∈ a. By definition, (r•b)(n) = v iff there is a sequence c_{1}v_{1} … c_{k}v_{k} such that (c_{i}, v_{i}) ∈ b for 1 ≤ i < k, and if x_{i} denotes ρ_{n}⟨v_{1}, …, v_{i}⟩ then (x_{i}n,?c_{i+1}) ∈ a for 0 ≤ i < k and (x_{k}n,!v) ∈ a. So for the implication ⇒ above we may take y = x_{n}, since x_{n} ⊆ x. Conversely, given x ⊆ b with (xn,!v) ∈ a, let y_{0} = x, and while y_{i} ≠ ∅ let (y_{i+1}n,?d_{i}) be the unique enabling of y_{i}n in a (recall that B^{B} is a DCDS), where y_{i} = y_{i+1} ⊔ {(d_{i}, w_{i})}. By the well-foundedness of the enabling relation we have y_{k} = ∅ for some k. But then the sequence d_{k−1}w_{k−1} … d_{0}w_{0} satisfies the above requirements for c_{1}v_{1} … c_{k}v_{k}.

(ii) Suppose given a : B → B and c accessible from r_{a} such that c is filled in r_{b} for some b ⊒ a. Since r_{b} is irredundant, c must have the form ⟨n, α⟩. Let β = m_{1}, …, m_{k} be the shortest prefix of α such that ⟨n, β⟩ is not filled in r_{a}; then r_{a}⟨n, γ⟩ is a question for any proper prefix γ of β. So let x = ρ_{n}(β) as above. It is easy to check that xn is a sequentiality index of I_{∗} for c at a.

(iii) If r ∈ B is irredundant, then for each n and α = m_{1}, …, m_{k} such that r⟨n, α⟩ is defined, let σ_{n,α} be the (least) finite partial function such that for 0 ≤ i < k, if r⟨n, m_{1}, …, m_{i}⟩ =?q_{i} then σ_{n,α}(q_{i}) = m_{i+1}. Now define

a_{r} = {(σ_{n,α}n, l) | n ∈ N, α ∈ Seq(N), l = r⟨n, α⟩}

(here l may be either a question or an answer). Clearly a_{r} is a sequential algorithm B → B, and it is straightforward to check that a = a_{r} iff r = r_{a}.

(iv) Suppose given r ∈ B, and xn accessible from a = a_{r^{•}} such that xn is filled in a_{s^{•}} for some s ⊒ r. Let {(yn,?c)} be an enabling of xn in a, where x = y ∪ {(c, v)} and y = σ_{n,α} as above. Then for any s as above, we have that ⟨n, α, v⟩ is accessible from irr_{•}(r) and filled in irr_{•}(s). Next, one can see by applying (iii) above to the realizer irr_{•}(irr_{•}) that the map irr_{•} is a sequential function B → B. So take d a sequentiality index of this map for ⟨n, α, v⟩ at r. Then d is clearly a sequentiality index of J_{∗} for xn at r. □

Since J_{∗}I_{∗} = id, by the proof of Proposition 4.7 we have that JI = id.

Clearly, morphisms 1 → B in SeqAlg correspond precisely to elements (or states) of B. So by the above proposition, applying the functor Hom(1, −) to the composite

B × B ⟶^{J×id} B^{B} × B ⟶^{ev} B

gives precisely the function • : B × B → B.

Remarks 4.9 (i) By standard facts about reflexive objects in CCCs (see [3]), the above gives an alternative proof that (B, •) is a combinatory algebra. In fact it proves more: namely, that B is a λ-algebra. That is, if M, N are formal metaexpressions over B (possibly involving λ^{∗}) and M =_{β} N, then [[ M ]]_{ν} = [[ N ]]_{ν} for all valuations ν. It would be interesting to know what λ-theory is induced by the interpretation of pure λ-terms in B.

It is clear, however, that B is not a λ-model, since different irredundant elements can realize the same function B → B.

(ii) An alternative way of viewing the above results is the following: given the monoid M of realizable endofunctions on B (i.e. sequential endofunctions on N_{⊥}^{N}), one can obtain SSeqFun as a full subcategory of its Karoubi envelope K(M). This is interesting because the definition of M is much less cumbersome than that of SSeqFun. However, K(M) is strictly larger than SSeqFun, as it is easy to find realizable idempotents on B (and even projections) whose kernel is not a concrete domain (see [22]).

Remark 4.10 One can easily obtain an effective analogue of Proposition 4.7, showing that B is a universal object in both SSeqFun_{eff} and SSeqAlg_{eff}. One can also show that the retraction (I, J) : B^{B} ⊲ B described by Proposition 4.8 lives in SeqAlg_{eff}, and induces a bijection between effective sequential algorithms B → B and irredundant elements of B_{eff}. Clearly, morphisms 1 → B in SeqAlg_{eff} correspond to elements of B_{eff}, and so the retraction (I, J) gives rise to exactly the combinatory algebra B_{eff}.

4.3 Sequential DCDSs and realizability

Armed with the above results, we can formulate a precise connection between CDSs and modest sets over B: specifically, SSeqFun can be fully embedded in Mod(B).

We define a functor E : SSeqFun → Mod(B) as follows. Given M a sequential DCDS, we take |EM| to be the set D_{M} of states of M, and for each x ∈ D_{M} let ∥x∥_{EM} be the singleton set {i_{M∗}(x)}. Given f : M → M′ a sequential function, take Ef = f : D_{M} → D_{M′}. Note that if a : M → M′ is any sequential algorithm representing f then r_{a} ≡ I(i_{M′} ∘ a ∘ j_{M}) is a realizer for Ef.

Likewise, we have a functor E_{eff} : SSeqFun_{eff} → Mod(B_{eff}) given as follows: |E_{eff}M| is the set of effective states of M, and ∥x∥_{EeffM} = {i_{M∗}(x)} (note that if x is an effective state then i_{M∗}(x) ∈ B_{eff}). If f : M → M′ is an effective sequential function then E_{eff}f is the restriction of f to effective states. Note that if a is an effective sequential algorithm representing f then the realizer r_{a} defined as above is effective, since (we may assume) i_{M′} and j_{M} are effective.

Proposition 4.11 The functors E and E_{eff} are full and faithful.

Proof The faithfulness of E is trivial; the faithfulness of E_{eff} follows from the fact that any continuous map D_{M} → D_{M′} is determined by its action on effective states. To see that E is full, let g be any morphism EM → EM′, realized by r ∈ B say. Then j_{M′} ∘ J_{∗}(r) ∘ i_{M} is a sequential algorithm M → M′, representing a sequential function g^{∗} such that Eg^{∗} = g. Similarly for E_{eff}. □

Remarks 4.12 (i) Note that if f : M → M′ is effective then the realizers for E_{eff}f are precisely the effective realizers for Ef. This is because an arbitrary state of M, M′ is a least upper bound of effective states, and so any realizer that takes effective states of M to effective states of M′ also does the same for arbitrary states.

(ii) The above is an instance of a general piece of folklore about realizability models: given a category C with a universal and reflexive object X, giving rise to a combinatory algebra A_{X}, there is a full functor E : C → Mod(A_{X}) such that Ef = Eg iff Hom(1, f) = Hom(1, g).

(iii) All the modest sets in the image of either E or E_{eff} have the special property that every element has just one realizer. Such objects are (up to isomorphism) precisely the projective modest sets (see e.g. [31]).

(iv) It is immediate from Propositions 4.7 and 4.11 that the object B ≅ N_{⊥}^{N} is a universal object in the subcategory of Mod(B) corresponding to SSeqFun; similarly for B_{eff} in Mod(B_{eff}).

The above results establish the correspondence between sequential functions M → M′ and morphisms EM → EM′. There is also a close relationship between sequential algorithms and realizers in B. The correspondence is not a perfect bijection—intuitively there are more realizers than sequential algorithms—but it is fairly strong:

Proposition 4.13 Let M, M′ be sequential DCDS. Then there are sequential algorithms V : M^{′M} → B and W : B → M^{′M} such that

• if a : M → M′ is a sequential algorithm representing a sequential function f, then V · a tracks Ef;

• if r ∈ B tracks Ef, then W · r is a sequential algorithm representing f;

• W ∘ V = id;

• V ∘ W is realized by an element of B.

If moreover M, M′ are effectively sequential, then V, W are effective and induce a similar correspondence between effective sequential algorithms and realizers in B_{eff}; furthermore, V ∘ W is realized by an element of B_{eff}.

Proof Since SeqAlg is cartesian closed, composition and application of sequential algorithms are themselves given by sequential algorithms. So there are sequential algorithms V, W defined by

V = λa. I · (i_{M′} ∘ a ∘ j_{M}), W = λr. j_{M′} ∘ (J · r) ∘ i_{M}.

The first two conditions are then clear (cf. the proof that E is a functor and is full). The third condition holds because JI = id, j_{M}i_{M} = id and j_{M′}i_{M′} = id.

The fourth condition is immediate since, by Proposition 4.8(i), every sequential algorithm B → B is realized by an element of B. The effective versions of these conditions are straightforward given that i_{M}, j_{M}, i_{M′}, j_{M′} are effective (an appeal to Remark 4.12(i) is needed for the second condition.) □

This gives us a particular retraction (V, W) : M^{′M} ⊲ B in SSeqAlg. In general this is not identical to the chosen retraction (i, j) for M^{′M}, although the “translations” i ∘ W and V ∘ j are of course realizable by elements of B. We thus have the following relationship between EM^{′EM} and E(M^{′M}):

Proposition 4.14 The exponential EM^{′EM} in Mod(B) is isomorphic to an obvious quotient Q of E(M^{′M}), where |Q| is the set of sequential functions M → M′; and ∥f∥_{Q} is the union of the (singleton) sets ∥a∥_{E(M^{′M})} for a a sequential algorithm representing f. Similarly in the effective case. □

Since in general there is no canonical sequential algorithm representing a sequential function, the object Q (and hence EM^{′EM}) is not usually projective. We therefore have some kind of an explanation for why SSeqFun fails to be cartesian closed: the desired exponentials do live naturally in Mod(B), but they take us outside the subcategory corresponding to SSeqFun. This is an example of a common phenomenon: by passing from some category of objects to a category of partial equivalence relations on them, we often obtain a much richer structure. An abstract account of this phenomenon is given in [7].

5 The hypercoherence model

In the last section we explored the connections between the realizability model over B and the sequential algorithms model. In this section we relate both of these to the strongly stable model due to Bucciarelli and Ehrhard, as embodied in Ehrhard’s category of hypercoherences. In [43], van Oosten gave a direct proof that the SR functionals coincide exactly with the strongly stable functionals of finite type. Here we follow a more scenic route to this result via the modified realizability model and the sequential algorithms model. Our proof invokes a theorem of Ehrhard [17] which states that the hypercoherence model may be obtained as an extensional collapse of the sequential algorithms model. (We will give our own proof of Ehrhard’s theorem in Section 7.)

We discuss some of the insights that the hypercoherence model provides, particularly with regard to the stable order on the SR functionals. We also point out a curiosity, namely the failure of the effective analogue of Ehrhard’s result.

5.1 An extensional collapse construction

We start by considering the extensional collapse of the sequential algorithms model, as studied by Ehrhard in [17]. We give a cheap proof that this construction yields precisely the SR functionals, by relating it to the modified realizability model described in Section 3.3.

It will be convenient to recast the definitions of Section 3.3 in terms of partial equivalence relations (PERs). By a modified PER X on B we will mean a set P_{X} ⊆ B with 0 ∈ P_{X}, together with a partial equivalence relation ∼_{X} on P_{X} (that is, a symmetric, transitive relation on P_{X}). We say that r ∈ B realizes a morphism X → Y of modified PERs if for all a, b ∈ B we have

a ∈ P_{X} ⟹ r • a ∈ P_{Y} , a ∼_{X} b ⟹ r • a ∼_{Y} r • b.

A morphism of modified PERs is an equivalence class of such realizers, under the equivalence relation

q ∼ r ⟺ ∀a ∈ B. q • a ∼_{Y} r • a.

The category MPER(B) of modified PERs on B is clearly equivalent to mMod(B). The modified modest sets [[ σ]]_{m} thus correspond to the modified PERs M_{σ} = (P_{σ}, ∼_{σ}) defined as follows:

\begin{aligned}P\overline{0} & = & \{\overline{⊥}, \overline{0}, \overline{1}, …\}, \\ x ∼\overline{0} y & ⟺ & x = y, \\ P_{σ→τ} & = & (P_{σ} ⇒ P_{τ}), \\ q ∼_{σ→τ} r & ⟺ & ∀x, y. x ∼_{σ} y ⟹ q • x ∼_{τ} r • y. \end{aligned}

Next we consider the obvious interpretation [[ −]]_{s} of types in SSeqAlg:

[[ \overline{0} ]]_{s} = N, [[ σ → τ ]]_{s} = [[ τ ]]_{s}^{[[ σ]]_{s}},

where N is the CDS with a single cell which may be filled by any natural number. Define a partial equivalence relation ≈_{σ} on the states of [[ σ]]_{s} inductively as follows:

x ≈\overline{0} y ⟺ x = y, a ≈_{σ→τ} b ⟺ ∀x, y ∈ D([[ σ]]_{s}). x ≈_{σ} y ⟹ a·x ≈_{τ} b·y.

Remark 5.1 The structures (D([[ σ]]_{s}), ≈_{σ}) are exactly the structures ([σ]_{∗}^{SEQ}, ≈ ) defined in Section 6 of [17]. The interpretation [σ]^{SEQ} was there defined within the category of sequential structures, a larger category than SeqAlg. However, we have already seen that SSeqAlg is a full sub-CCC of SeqAlg, and it is shown in [8, Chapter 5] that SeqAlg is a full sub-CCC of the category of sequential structures. Thus, all the sequential structures [σ]^{SEQ} lie within the sub-CCC corresponding to SSeqAlg.

One can view each structure (D([[ σ]]_{s}), ≈_{σ}) as a modified modest set N_{σ} = (Q_{σ}, ≈_{σ}): we take Q_{σ} to be the set of realizers for elements of E([[ σ]]_{s})—these are in bijective correspondence with states of [[ σ]]_{s}—and just transport ≈_{σ} along this bijection. By Proposition 4.13 it is clear that there are application morphisms N_{σ→τ} × N_{σ} → N_{τ} realized essentially by •.

The definitions of M_{σ} and N_{σ} look very similar, and indeed they turn out to be isomorphic:

Proposition 5.2 For each type σ, we have M_{σ} ≅ N_{σ} in MPER(B); moreover, these isomorphisms commute with the evident application morphisms M_{σ→τ} × M_{σ} → M_{τ} and N_{σ→τ} × N_{σ} → N_{τ}.

Proof By induction on σ. The isomorphism M\overline{0} ≅ N\overline{0} is easy. So suppose c_{σ}, d_{σ} realize an isomorphism M_{σ} → N_{σ} and its inverse respectively, and likewise for τ. Let V : [[ τ ]]_{s}^{[[ σ]]_{s}} → B and W : B → [[ τ ]]_{s}^{[[ σ]]_{s}} be the sequential algorithms given by Proposition 4.13, and suppose v, w ∈ B are the corresponding realizers for morphisms E([[ σ → τ ]]_{s})\overleftarrow{→}B. By Proposition 4.13 we have that if r ∈ Q_{σ→τ} then v • r ∈ (Q_{σ} ⇒ Q_{τ}). We therefore have the following diagram of subsets of B and realizable functions between them (we label each arrow with an appropriate realizer):

[figure: P_{σ→τ} ≡; (P_{σ} ⇒ P_{τ}); λ^{∗}xy.c_{τ}(x(d_{σ}y)); \underline{λ^{∗}xy.d_{τ}(x(c_{σ}y))}; (Q_{σ} ⇒ Q_{τ}); w; \underline{v}; Q_{σ→τ}]

Hence we obtain realizers c_{σ→τ}, d_{σ→τ} for the composite functions P_{σ→τ} \overleftarrow{→}Q_{σ→τ}. It is routine to verify (using the induction hypothesis) that c_{σ→τ} and d_{σ→τ} realize morphisms M_{σ→τ} → N_{σ→τ} and N_{σ→τ} → M_{σ→τ} respectively; that these morphism commute with application; and hence that they are mutually inverse. □

Now consider the type structure E, where E^{σ} is the subquotient of Q_{σ} by ≈_{σ}, and the application operations are induced by •. This type structure is known as the extensional collapse of the sequential algorithms model. The following is now immediate from the above and Proposition 3.9:

Corollary 5.3 The type structure E is isomorphic to the type structure R of SR functionals. □

Remarks 5.4 (i) The effective analogue of this result also goes through: the extensional collapse E_{eff} of the evident interpretation [[ −]]_{s,eff} in the effective sequential algorithms model SSeqFun_{eff} is isomorphic to the type structure of effective SR functionals. Note that the sets P_{eff,σ} are defined by working entirely within B_{eff}, whereas the sets Q_{eff,σ} are defined via the interpretation of σ in the “full” sequential algorithms model. But this does not matter since it is easily shown that P_{eff,σ} = P_{σ} ∩ B_{eff} (cf. Remark 4.12(i)).

(ii) It is shown by Laird in [28] that the effective sequential algorithms model coincides exactly with the observational quotient of the language μPCF , an idealized functional language with control. From this and the above results, it follows directly that R_{eff} is the extensional collapse of the language μPCF. More precisely, R_{eff} is isomorphic to the subquotient of the type structure of closed μPCF terms by the logical relation induced by observational equivalence at ground type. Informally, this means that every effective SR functional can be written in μPCF.

One also obtains a similar result for the programming language PCF+catch studied by Cartwright, Curien and Felleisen in [11]. (The relationship between μPCF and PCF+catch is discussed in [28].) In [11] it is shown that PCF+catch has a fully abstract interpretation in the effective sequential algorithms model; a universality result for such an interpretation is proved by Kanneganti, Cartwright and Felleisen in [23].^{3} It follows from this that R_{eff} is the extensional collapse of PCF+catch. We would expect that many other programming languages should give rise to R_{eff} in this way—see Section 12.3.

5.2 Sequential algorithms and hypercoherences

We now recall some definitions concerning hypercoherences, and state the main theorem of Ehrhard [17]. For more background on hypercoherences, see this paper or [15].

Definition 5.5 (Hypercoherences) (i) A hypercoherence X is a countable set |X| together with a set Γ_{X} of non-empty finite subsets of |X|, such that {a} ∈ Γ_{X} for each a ∈ |X|. We call |X| the underlying set and Γ_{X} the atomic coherence of X.

(ii) The domain D(X) generated by a hypercoherence X is the set of all subsets x ⊆ |X| such that for all non-empty finite u ⊆ x we have u ∈ Γ_{X}. We will refer to the elements x ∈ D(X) as states of X.

(iii) The coherence C(X) generated by X is the set of non-empty finite subsets A ⊆ D(X) such that, for all non-empty finite u ⊆ |X|, u ⊲ A implies u ∈ Γ_{X}, where u ⊲ A means

∀a ∈ u. ∃x ∈ A. a ∈ x ∧ ∀x ∈ A. ∃a ∈ u. a ∈ x.

The intuition here is that |X| is some set of “atoms of information”, and Γ_{X} specifies which finite combinations of atoms are “consistent”. The domain D(X) can then be seen as the set of consistent “states” of X, where consistency is determined by looking at finite subsets. In fact D(X) (ordered by inclusion) is always a qualitative domain. The coherent subsets A of D(X) are, roughly speaking, those such that any finite “cross-section” u of A looks consistent. The coherent subsets are meant to generalize the notion of consistent pair of states in the theory of stable domains: they are those subsets for which we require morphisms to preserve the meets. This is reflected in the next definition:

Definition 5.6 (Strong stability) Let X, Y be hypercoherences. A strongly stable function X → Y is a continuous function f : D(X) → D(Y) such that for any A ∈ C(X) we have f(A) ∈ C(Y) and f(⋂ A) = ⋂ f(A). We write HC for the category of hypercoherences and strongly stable functions.

It is shown in [15, 16] that HC is a cartesian closed category, indeed a sub-CCC of the category of dI-domains with coherence. Given hypercoherences X, Y, the exponential Z = Y^{X} may be defined explicitly as follows: |Z| is the set of pairs (x, b) where x ∈ D(X) is finite and y ∈ |Y |; and for non-empty finite w ⊆ |Z| we have w ∈ Γ(Z) iff

π_{1}(w) ∈ C(X) ⟹ (π_{2}(w) ∈ Γ(Y) ∧ (π_{2}(w) a singleton ⟹ π_{1}(w) a singleton)).

3Actually in [23] the proof is worked out for a variant of PCF+catch including error values, but the same technique works for the error-free version.

In addition, we have a hypercoherence N of natural numbers, defined by

|N| = N, Γ_{N} = {{n} | n ∈ N}.

The associated domain D(N) is the familiar domain N_{⊥}. This means that we have an interpretation [[ −]]_{HC} of the simple types in HC, giving rise to a type structure H in the sense of Definition 3.6 (take H^{σ} = D([[ σ]]_{HC}) ≅ Hom(1, [[ σ]]_{HC})). We call H the type structure of strongly stable functionals.

The following result appears as Theorem 5 of [17]:

Theorem 5.7 (Ehrhard) The type structures E and H are isomorphic. □

From this and Corollary 5.3 above, we may immediately recover the main result of [43]:

Corollary 5.8 (van Oosten) The type structures H and R are isomorphic. □

Remarks 5.9 (i) The proof of Theorem 5.7 is non-constructive: an appeal to König’s Lemma is needed to show that every infinite element of H is represented by a sequential algorithm (see [17, Section 6]). The failure of the effective analogue of the theorem (see below) shows that the non-constructivity is essential.

(ii) If preferred, one could invoke van Oosten’s result and deduce Ehrhard’s theorem as a corollary. We give an alternative proof of Theorem 5.8, not dependent on either [17] or [43], in Section 7 below.

(iii) It is interesting to compare Ehrhard’s result in in [17], which we have invoked above, with his earlier construction of the hypercoherence model as the extensional collapse of the extensional sequential algorithms model (see [16]). Roughly speaking, in [17] we first define an interpretation of all types without regard to extensionality, and then pick out a type structure by the extensional collapse construction, whereas in [16] we carve out the subset of extensionally well-behaved algorithms at each type level, and use only this in defining the interpretation of the next type level. Intuitively, this corresponds exactly to the difference between exponentials in modified and standard realizability models.

The connection between the construction of [17] and modified realizability is made precise above. One might hope to make a similar precise link between the construction of [16] and standard realizability, yielding yet another proof of van Oosten’s result, and indeed we initially tried to do this. The precise connection seems elusive, but for an interesting reason. In both [16, 17] Ehrhard works in the category of sequential structures (cf. Remark 5.1), and it turns out that in [16] this extra generality is quite essential: even the sequential structure used to interpret the type (\overline{0}^{2} → \overline{0}) → \overline{0} falls outside the class of CDSs. We are thus unable to transfer the results of [16] to the realizability model.

The hypercoherence presentation of R shows a remarkable fact: the “computational” notion of sequential realizability can be captured exactly by a preservation property with a finitary character.

Many properties of the SR functionals that are hard to prove from the definition of R are relatively easy for H. One such property concerns the effective presentability of the finite elements (other examples appear in Section 5.4). Specifically, let H_{0}^{σ} be the poset of finite elements of (H^{σ}, ⊆). In view of the finitary nature of the construction of exponentials in HC, the following fact is clear (we omit the detailed proof):

Proposition 5.10 There are bijections β_{σ} : N → H_{0}^{σ} for each type σ, with respect to which

• the ordering and (pairwise) consistency relations on H_{0}^{σ} are decidable;

• the (binary) meet operations H_{0}^{σ} × H_{0}^{σ} → H_{0}^{σ} are recursive;

• the application operations H_{0}^{σ→τ} × H_{0}^{σ} → H_{0}^{τ} are recursive.

Moreover, codes for these operations may be obtained recursively from codes for σ and τ. □

It follows that the evident finitary analogue R_{fin} of R (in which we take 2_{⊥} instead of N_{⊥} as the ground type) is decidable. That is, the set R_{fin}^{σ} and the application functions ·_{στ} can be computed recursively from σ, τ (so that, for example, the size of R_{fin}^{σ} is recursive in σ. An important result of Loader [29] shows that the corresponding statement fails for PCF-sequentiality.

5.3 Effectivity in hypercoherences

Next we draw attention to a surprising anomaly. The effective analogue of Theorem 5.7 fails: that is, the extensional collapse of the effective sequential algorithms model does not coincide with the r.e. submodel of the hypercoherence model. We give an example to show that, even at first order types, there are r.e. strongly stable functions that are not represented by any effective sequential algorithm. This is somewhat analogous to the result due to M.B. Trakhtenbrot [56] that there exist r.e. elements of the Milner model that are not PCF-definable. However, the two situations are in fact quite distinct, so we cannot simply re-use known examples of the Trakhtenbrot phenomenon in our setting.

We should clarify what we mean by an r.e. element of the hypercoherence model. By an enumerated hypercoherence we shall mean a hypercoherence X together with a bijection between |X| and a subset of N; the r.e. states of X are then those x ∈ D(X) that correspond under this bijection to r.e. subsets of N. It is easy to give a standard enumeration for each of the hypercoherences [[ σ]]_{HC}: for [[ \overline{0} ]]_{HC} = N we may take the identity enumeration; and given enumerations for X, Y we may obtain an enumeration for Z = Y^{X} using some standard effective codings for pairs and finite sets. We shall always consider each [[ σ]]_{HC} as being equipped with this standard enumeration; it is worth remarking that the atomic coherence Γ_{[[ σ]]_{HC}} then corresponds to a decidable set of finite subsets of N. The effective states of these hypercoherences are of course closed under application, and so they constitute a substructure H_{eff} of H.

For convenience, we will identify states of the CDS N, and states of the hypercoherence N, with elements of N_{⊥}. In the following proposition we write σ = \overline{0} → \overline{0} → \overline{0} and τ = \overline{0} → \overline{0} → \overline{0} → \overline{0}.

Proposition 5.11 There exists an r.e. element t ∈ D([[ τ ]]_{HC}) such that there is no effective sequential algorithm a ∈ [[ τ ]]_{s,eff} with a · x · y · z = txyz for all x, y, z ∈ N_{⊥}.

Proof Let X be the hypercoherence [[ τ ]]_{HC}. We may identify |X| with the set of tuples (x, y, z, w) where x, y, z ∈ N_{⊥} and w ∈ N. Let A, B be disjoint but recursively inseparable r.e. subsets of N: for example, take

A = {e | φ_{e}(0) = 0}, B = {e | φ_{e}(0) = 1},

where φ_{e} is the eth partial recursive function. Now let t ⊆ |X| be the set

{(x, 1, 1, 1) | x ∈ N} ∪ {(x, 0, ⊥, 0) | x ∈ A} ∪ {(x, ⊥, 0, 0) | x ∈ B}.

Then t is r.e. since both A, B are r.e. To see that t ∈ D(X), first let Y = [[ σ]]_{HC}, and for each x ∈ N let t_{x} = {(y, z, w) | (x, y, z, w) ∈ t} considered as a subset of |Y |. It is easy to check that t_{x} ∈ D(Y) for each x (there are just three possibilities for t_{x}). But now since X = Y^{N}, we can see from the definition of exponentials in HC that if u is any non-empty finite subset of t then u ∈ Γ_{X}. Thus t ∈ D(X).

Now suppose, for contradiction, that a is an effective sequential algorithm representing t. Then for x ∈ N we have that a · x is an effective sequential algorithm representing t_{x}, recursive in x. If M is the CDS [[ σ]]_{s}, we may identify C_{M} with the set of pairs (y, z) with y, z ∈ N_{⊥}, and V_{M} with the set {?_{y},?_{z}}∪{!w | w ∈ N}, where ?_{y},?_{z} correspond to requests for the first and second arguments respectively. Now for each x ∈ N we have a · x ∈ D(M), and it is easy to see that ((1, 1),!1) ∈ a · x. Using the sequentiality of a · x, we can deduce that the cell (⊥, ⊥) is filled with either ?_{y} or ?_{z} in a · x. Furthermore, since a · x is recursive in x, there is a recursive function of x telling us which of these is the case. But such a function clearly separates A and B, giving us a contradiction. □

By Remark 5.4, the above proposition suffices to show that the type structure R_{eff} is not isomorphic to H_{eff}. We will see in Section 7 that R_{eff} is a proper substructure of H_{eff}. It appears that R_{eff} is the “right” effective analogue of the SR functionals, while H_{eff} seems to be something of a curiosity.

5.4 The stable order

The set of states of any hypercoherence are naturally ordered by inclusion. It is known e.g. from [15] that for a function space Y^{X}, this ordering coincides with Berry’s stable order on functions. The stable order also plays an important role in the theory of sequential functions. Here we briefly consider how the stable order fits into the picture described in this section and the last.

We first recall some standard notions. A poset (X, ≤) is called stable if whenever x, y ∈ X have a common upper bound, they have a greatest lower bound x ∧ y. A function f : X → Y between such posets is stable if whenever x, y ∈ X have an upper bound we have f(x ∧ y) = f(x) ∧ f(y). It is well known that the states of a DCDS [resp. hypercoherence] form a stable poset, and moreover that sequential functions [resp. strongly stable functions] are stable.

If X, Y are stable posets, the stable order ≤_{s} on stable functions X → Y is defined as follows:

f ≤_{s} g ⟺ ∀x, y ∈ X. x ≤ y ⟹ f(x) = f(y) ∧ g(x).

The category of stable posets and stable functions is cartesian closed: the exponential [X ⇒_{s} Y] is the set of stable functions X → Y ordered by ≤_{s}.

For DCDSs, the stable order admits alternative characterizations:

Proposition 5.12 Suppose f, g : M → M′ are sequential functions between DCDSs. Then the following are equivalent:

(i) f ≤_{s} g.

(ii) There exist sequential algorithms a, b with a_{∗} = f, b_{∗} = g such that a ⊑ b. (iii) There exist realizers q ∈ ∥Ef∥, r ∈ ∥Eg∥ such that q ⊑ r.

Proof (i) ⇒ (ii): Given f ≤_{s} g, take any b such that b_{∗} = g, and define

a = {(xc′,?c) ∈ b | true} ∪ {(xc′,!v′) ∈ b | (c′, v′) ∈ f(x)}.

It is routine to verify that a is a sequential algorithm and that a_{∗} = f.

(ii) ⇒ (i): The evaluation morphism D(M^{′M})×D(M) → D(M′) is stable, and so we obtain a stable function D(M^{′M}) → [D(M) ⇒_{s} D(M′)] mapping a ↦ a_{∗}. So if a ⊑ b then a_{∗} ≤_{s} b_{∗}.

(ii) ⇔ (iii) follows easily from Proposition 4.8. □

For hypercoherences, as we have already remarked, the stable order on morphisms X → Y coincides with the inclusion order on D(Y^{X}). Furthermore, this ordering on the type structure H can alternatively be characterized in terms of E or R:

Proposition 5.13 Suppose x ∈ H^{σ}, x′ ∈ E^{σ} and x′′ ∈ R^{σ} all correspond under the isomorphisms H ≅ E ≅ R, and similarly for y, y′, y′′. The following are equivalent:

(i) x ⊑ y in the inclusion order.

(ii) There exist sequential algorithms a ∈ x′, b ∈ y′ such that a ⊑ b.

(iii) There exist realizers q ∈ ∥x′′∥, r ∈ ∥y′′∥ such that q ⊑ r.

Proof (i) ⇒ (ii): For finite elements x, y this is Lemma 6 of [17]. One can extend the result to infinite elements by an application of König’s Lemma exactly as in [17, Theorem 5]. Let (r_{n}) be the standard increasing sequence of finite retractions on H^{σ}, and let (p_{n}) be the corresponding sequence of retractions on D^{σ} ≡ D([[ σ]]_{s}), as described in [17]. Each of these retractions has a finite image consisting entirely of finite elements, and the lub of each sequence is the identity. Suppose x ⊑ y, and for each n let x_{n} = r_{n}(x), y_{n} = r_{n}(y). Since these are finite elements, there exist a_{n} ⊑ b_{n} in the image of p_{n} that represent the corresponding elements x′_{n}, y′_{n} ∈ E^{σ}. In this case, we will say that c_{n} = (a_{n}, b_{n}) represents z_{n} = (x_{n}, y_{n}).

For each n there is a sequence c_{0} ⊑ … ⊑ c_{n} in D^{σ} × D^{σ}, where each c_{i} represents z_{i}: for instance, take (a_{n}, b_{n}) representing z_{n} and set c_{i} = (p_{i}(a_{n}), p_{i}(b_{n})).

Moreover, each z_{i} is represented by only finitely many pairs, since the image of p_{i} is finite. So by König’s Lemma, there exists an infinite sequence c_{0} ⊑ c_{1} ⊑ … where c_{i} represents z_{i}. By taking c = ⨆ c_{i} in D^{σ} ×D^{σ}, we obtain a, b representing x′, y′ as required.

(ii) ⇒ (i) is Lemma 7(i) of [17].

(ii) ⇔ (iii): By Proposition 5.12, (ii) holds iff there are realizers q′ ⊑ r′ for the elements corresponding to x, y respectively in the modified modest set N_{σ}. So by Proposition 5.2, (ii) holds iff the corresponding property holds for M_{σ}. But this is clearly equivalent to (iii), by inspection of the proof of Proposition 3.9. □

It follows immediately from Proposition 5.13 that the relation on each R^{σ} given by condition (iii) above is a complete partial order. What seems to be the analogous question for PCF-sequentiality is still open: for the games models of PCF (for example), it is not known whether the extensional collapse at each simple type is a CPO with the evident ordering.

6 A presheaf model

We now consider a characterization of the type structure R due to Colson and Ehrhard [13], inspired by the notion of reducibility from proof theory. As we shall see, it is a fairly short step from this to a description of R in terms of presheaves over the monoid of sequential endofunctions on N_{⊥}^{N}. For us, the interest of these results is twofold: firstly, they yield yet another mathematical characterization of R, quite different in flavour from those we have considered so far; and secondly, they reveal a sense in which sequential realizability may be seen as “canonically” extending the familiar notion of first-order sequentiality to higher types.

6.1 The Colson-Ehrhard characterization

We first summarize the crucial definitions and the main result from [13]. As before we write N_{⊥}^{N} for the set of all partial functions N ⇀ N, and we suppose we have a standard pairing function ⟨−, −⟩ : N_{⊥}^{N} × N_{⊥}^{N} → N_{⊥}^{N}, with corresponding projections fst, snd. For each type σ we define a set L^{σ}, and a set L_{ω}^{σ} of functions from N_{⊥}^{N} to L^{σ}, by simultaneous induction as follows:

• L\overline{0} = N_{⊥}.

• L\overline{0} ; ω is the set of sequential functions N_{⊥}^{N} → N_{⊥} in the sense of Milner [37] and Vuillemin [57] (equivalently, the functions N_{⊥}^{N} → N_{⊥} realizable by an element of B).

• L^{σ→τ} is the set of all functions f : L^{σ} → L^{τ} such that for all g ∈ L_{ω}^{σ} we have f ∘ g ∈ L_{ω}^{τ}.

• L_{ω}^{σ→τ} is the set of all functions f : N_{⊥}^{N} → L^{σ→τ} such that for all g ∈ L_{ω}^{σ} the function λr : N_{⊥}^{N}. f(fst r)(g(snd r)) is in L_{ω}^{τ}.

The sets L^{σ} constitute a type structure L, which can be seen as arising naturally from the set of sequential functions N_{⊥}^{N} → N_{⊥}.

The set N_{⊥}^{N} obviously plays an important role in the above definition. We shall also consider the hypercoherence N^{ω} that intuitively corresponds to N_{⊥}^{N}. We can define N^{ω} directly as follows: |N^{ω}| = N × N; and for non-empty finite w ⊆ |N^{ω}| we have w ∈ Γ(N^{ω}) iff

π_{1}(w) a singleton ⟹ π_{2}(w) a singleton.

One can check that D(N^{ω}) ≅ N_{⊥}^{N}, and that N^{ω} is indeed the ω-fold product of copies of N in HC.

We now import the main result of [13]. For the sake of completeness we give a summary of the proof.

Theorem 6.1 (Colson/Ehrhard) L ≅ H.

Proof (Outline.) The key lemma is the following: if X, Y are hypercoherences, a set-theoretic function D(X) → D(Y) is a strongly stable map X → Y provided for every strongly stable map g : N^{ω} → X, the function f ∘ g : N^{ω} → Y is strongly stable. This is proved as follows. Suppose f satisfies the proviso: we need to show that f is ω-continuous and preserves coherent sets and their meets. For continuity, one shows that every ω-chain in D(X) is the image of a “generic” chain in D(N^{ω}) via a strongly stable map g. The strong stability of f ∘ g then implies that f preserves the lub of this chain. For coherent sets, one shows that every coherent set in X is the image of a coherent set in N^{ω} via a strongly stable map g. Again, the strong stability of f ∘ g then gives us that f preserves this coherent set and its meet.

One then shows that at all types σ there are bijections L^{σ} ≅ D([[ σ]]_{HC}) and L_{ω}^{σ} ≅ D(N^{ω} ⇒ [[ σ]]_{HC}) that commute with the application maps. This is reasonably straightforward by simultaneous induction on σ, using the above lemma. □

6.2 A presheaf presentation

Next we relate L to a type structure arising from a certain category of presheaves. In the first instance, consider the two-object category C consisting of the sets 1 and N_{⊥}^{N} together with all Milner-Vuillemin sequential functions between them. (Equivalently, C may be described as the full subcategory of SeqFun consisting of the objects 1 and B.) For typographical convenience, we will write B for the object N_{⊥}^{N} of C.

The presheaf category over C is simply the category [C^{op}, Set] of functors C^{op} → Set and natural transformations between them. Given F, G : C^{op} → Set, we write Nat(F, G) for the set of natural transformations F → G. It is well known that the presheaf category over any small category is cartesian closed. In the case of our category C, if F, G : C^{op} → Set we may describe G^{F} explicitly as follows: G^{F} (1) = Nat(F, G); G^{F} (B) = Nat(h_{B} ×F, G), where h_{B} = Hom_{C}(−, B); and G^{F} (f) is induced by precomposition with Hom_{C}(−, f) × id_{F}.

We can obtain an interpretation of the simple types in [C^{op}, Set] by fixing on an interpretation of the type \overline{0}. Let M\overline{0} : C^{op} → Set be the functor defined as follows:

M\overline{0}(1) = L\overline{0} = N_{⊥}, M\overline{0}(B) = L\overline{0} ; ω, and the action of M\overline{0} on morphisms is given by precomposition. At higher types we then define M_{σ→τ} to be the exponential M_{τ}^{M_{σ}} in [C^{op}, Set]. The following proposition spells out the relationship between the functors M_{σ} and the sets L^{σ}, L_{ω}^{σ}:

Proposition 6.2 (i) For each type σ, there are bijections β^{σ} : M_{σ}(1) ≅ L^{σ} and β_{ω}^{σ} : M_{σ}(B) ≅ L_{ω}^{σ}, with respect to which the action of M_{σ} on functors corresponds to precomposition.

(ii) For each σ, τ, the function M_{σ→τ}(1) × M_{σ}(1) → M_{τ}(1), (α, x) ↦ α_{1}(x) corresponds under these bijections to the application function L^{σ→τ} × L^{σ} → L^{τ}.

Proof By simultaneous induction on σ. For type \overline{0}, (i) holds by definition of M\overline{0}. So suppose (i) holds for σ and τ. We first establish the bijection β^{σ→τ} : M_{σ→τ}(1) ≅ L^{σ→τ}. Suppose α ∈ M_{σ→τ}(1), and let f = β^{τ} ∘ α_{1} ∘ β^{σ−1} : L^{σ} → L^{τ}. By the naturality of α at each x : 1 → B, we have that

β_{ω}^{τ} ∘ α_{B} ∘ β_{ω}^{σ−1} = f ∘ − : L_{ω}^{σ} → L_{ω}^{τ}.

In particular, for any g ∈ L_{ω}^{σ} we have f ∘ g ∈ L_{ω}^{τ}; thus f ∈ L^{σ→τ}. Conversely, suppose f ∈ L^{σ→τ}; then f^{−} ≡ f ∘ − is a map from L_{ω}^{σ} to L_{ω}^{τ}. Set

α_{1} = β^{τ−1} ∘ f ∘ β^{σ}, α_{B} = β_{ω}^{τ−1} ∘ f^{−} ∘ β_{ω}^{σ}.

It is routine to check that this defines a natural transformation α ∈ M_{σ→τ}(1). Moreover, the above constructions are mutually inverse, since any α : M_{σ} → M_{τ} is uniquely determined by α_{1}, by naturality at each x : 1 → B. We thus have the required bijection β^{σ→τ}.

We now establish the bijection β_{ω}^{σ→τ} : M_{σ→τ}(B) ≅ L_{ω}^{σ→τ}. Suppose α ∈ M_{σ→τ}(B); then α is a natural transformation h_{B} × M_{σ} → M_{τ}, so in particular we have α_{1} : N_{⊥}^{N} × M_{σ}(1) → M_{τ}(1) and α_{B} : Hom(B, B) × M_{σ}(B) → M_{τ}(B). Let f : N_{⊥}^{N} → L^{τL^{σ}} be the function obtained from α_{1} by currying and composing with the given bijections. First note that for all x ∈ N_{⊥}^{N} and all g ∈ L_{ω}^{σ}, by the naturality of α at each y : 1 → B we have that α_{B}(k_{x}, g) = f(x) ∘ g ∈ L_{ω}^{τ}, where k_{x} is the constant morphism B → B corresponding to x. (Here, for clarity, we have omitted a few βs, as we shall generally do from now on.) Thus f(x) ∈ L^{σ→τ} for each x. Next, we wish to show that f ∈ L_{ω}^{σ→τ}. Given any g ∈ L_{ω}^{σ} and any e : B → B, by naturality of α at each y : 1 → B we have that α_{B}(e, g) = (λr. f(er)(gr)) ∈ L_{ω}^{τ}. Now note that fst, snd are sequential functions and so correspond to morphisms B → B. Note also that L_{ω}^{σ} is closed under precomposition with sequential functions N_{⊥}^{N} → N_{⊥}^{N} since this corresponds to the action of M_{σ} on morphisms B → B. Hence, given any g′ ∈ L_{ω}^{σ}, setting e = fst and g = g′ ∘ snd, we have that (λr. f(fst r)(g′(snd r))) ∈ L_{ω}^{τ}; thus f ∈ L_{ω}^{σ→τ}.

Conversely, suppose f ∈ L_{ω}^{σ→τ}. Reversing the above argument, given any g ∈ L_{ω}^{σ} and any e : B → B, there is a morphism d : B → B given by r ↦ ⟨er, r⟩. Since (λr. f(fst r)(g(snd r))) ∈ L_{ω}^{τ} and L_{ω}^{τ} is closed under precomposition with d, we have that (λr. f(er)(gr)) ∈ L_{ω}^{τ}. So define

α_{1}(x, a) = f(x)(a), α_{B}(e, g) = λr. f(er)(gr).

It is routine to check that this defines a natural transformation α ∈ M_{σ→τ}(B).

Once again, the above constructions are mutually inverse since α_{B} is uniquely determined by α_{1}. This gives us our bijection β_{ω}^{σ→τ}. The remaining clauses of the proposition are now immediate from the construction of β^{σ→τ} and β_{ω}^{σ→τ}. □

As usual, we can now obtain a type structure by taking global elements. For each σ let P^{σ} = Hom(1, M_{σ}), and consider the P^{σ} as equipped with the functions P^{σ→τ} × P^{σ} → P^{τ} induced by the evaluation morphisms in [C^{op}, Set]. Clearly we may identify P \overline{0} with N_{⊥}, so this defines a type structure P. From the above proposition we easily deduce the following:

Corollary 6.3 P ≅ R.

Proof The object 1 of [C^{op}, Set] is just the constant functor {∗}, which clearly coincides with the representable functor h_{1} = Hom(−, 1). So by the Yoneda Lemma, functors 1 → M_{σ} correspond naturally to elements of M_{σ}(1) ≅ L^{σ}. Moreover, it is easy to see that the bijections P^{σ} ≅ L^{σ} respect the application operations, so P ≅ L as type structures. Combining this with Theorem 6.1 and Corollary 5.8, we have that P ≅ R. □

The above characterization of the SR functionals using the category C was chosen to mesh well with the definition of L given in [13]. However, we can now dispense with the object 1 in C to obtain a more aesthetically pleasing description. Let M be the monoid of sequential endofunctions on N_{⊥}^{N}, as in Remark 4.9(ii), and let I be the full inclusion M ↪ C. It is easy to show the following:

Proposition 6.4 The categories [C^{op}, Set] and [M^{op}, Set] are equivalent.

Proof This follows trivially from the fact that 1 arises as an absolute coequalizer of two morphisms B\overrightarrow{→}B within C, and the Yoneda embedding exhibits [M^{op}, Set] as the free cocompletion of M (see e.g. [36, Section 1.5]). □

Under this equivalence, the object M\overline{0} corresponds to the right M-set X whose carrier is the set of sequential functions N_{⊥}^{N} → N_{⊥}, with right M-action given by precomposition. The type structure generated from X in [M^{op}, Set] thus gives a pleasing mathematical characterization of the SR functionals.

Remarks 6.5 (i) The object X bears very little relation to the natural number object in [M^{op}, Set], which is a much more boring M-set with a trivial M-action.

(ii) In the light of the universal property mentioned above, [M^{op}, Set] is in some sense a “canonical” extension of M to a cartesian closed category. The above result (and indeed the result of Colson and Ehrhard) therefore suggests that the SR functionals are in some way a canonical extension of the notion of infinitary first-order sequentiality (embodied by M) to higher types.

(iii) The infinite arity of the functions embodied by M is quite essential here. If we work with presheaves over the category of finitary Milner-Vuillemin sequential functions, there is nothing to impose continuity at higher types.

(iv) There seems to be some analogy between [M^{op}, Set] and its relation to the realizability model over B, and Mulry’s recursive topos [39] and its relation to the effective topos. However, we have not explored this connection.

7 A universal type

We now come to the main new result of the paper. We show that in R the type \overline{2} is a universal type, in the sense that every type σ is a retract of \overline{2}. More specifically, for every type σ there are SR functionals R^{σ}\overleftarrow{→}R\overline{2} that compose to give the identity on R\overline{2}; thus, R\overline{2} in some sense “contains” all higher types. The same also holds for R_{eff}. This gives us a very good grasp of these type structures, and numerous other results then follow fairly easily.

For ease of presentation, at this point in the paper we will shift the focus of our attention to the call-by-value SR functionals, rather than the call-by-name ones we have studied so far. Mathematically this does not make a big difference, and one can easily recover the call-by-name version of our results from the call-by-value version. In Section 7.1 we explain precisely the call-by-value interpretation of types that we are considering.

We then show in Sections 7.2 and 7.3 that the (call-by-value) type \overline{3} is a retract of \overline{2}—it follows easily from this that every type is a retract of \overline{2}. The required morphism I : \overline{3} → \overline{2} is easy to construct, and the bulk of the work involves the morphism H : \overline{2} → \overline{3}. We give the construction of H in Section 7.2, and the verification that I ∘ H = id in Section 7.3, along with other facts.

Some applications of this result will be given in Sections 8 and 9.

7.1 Call-by-value types

So far we have been considering the call-by-name interpretation of types in Mod(B) as given by Definition 3.5 (we will write this interpretation here as [[ −]]_{N}, and the corresponding type structure as R_{N}). At this point in the paper we switch our attention to the call-by-value interpretation [[ −]]_{V}, defined essentially as follows:

[[ \overline{0} ]]_{V} ≅ N, [[ σ_{1} → σ_{2} ]]_{V} ≅ ([[ σ_{2} ]]_{V ⊥})^{[[ σ_{1} ]]_{V}} .

By taking R_{V}^{σ} = |[[ σ]]_{V} | we obtain a call-by-value type structure, that is, a family of sets R_{V}^{σ} together with partial application functions · : R_{V}^{σ→τ} × R_{V}^{σ} ⇀ R_{V}^{τ}. Similarly we define the effective call-by-value interpretation [[ −]]_{V,eff} in Mod(B_{eff}), and the corresponding call-by-value type structure R_{V,eff}. (These turn out to be the appropriate objects for giving interpretations of call-by-value PCF—see Section 9.1 below.)

The reason for this shift is that the functional H lives most naturally in the call-by-value setting. We emphasize, however, that this is really just a matter of convenience. Indeed, the type structures R_{N} and R_{V} may each be recovered from the other, since each object [[ σ]]_{V} can be defined as a retract of some [[ τ ]]_{N}, and vice versa (see e.g. [31, Chapter 6]). This means that the results we are interested in will transfer easily between the two settings. We can therefore regard R_{N} and R_{V} as being in some sense just different presentations of the same thing.

For the rest of this section, we will write [[ −]] for [[ −]]_{V}, and R for R_{V}. Since most of the theorems and proofs in this section work identically in the full and effective settings, we will use undecorated notation when we could be referring to either case, and use the subscripts full and eff when we need to be specific. Thus, B may refer to either B_{full} or B_{eff}.

The interpretation [[ −]] (in both the full and effective cases) is given up to isomorphism by the above definition, but it will greatly simplify our task to work with judiciously chosen on-the-nose representations of these objects. Specifically, we take [[ \overline{0} ]] to be the object N as in Section 3.1, [[ \overline{1} ]] ≅ N_{⊥}^{N} to be the object of realizers B given by Definition 3.4. For our representation of [[ \overline{2} ]], we need the following ad hoc definition:

Definition 7.1 (Semi-irredundant realizers) We call an element r ∈ B semiirredundant if, for all α, β ∈ Seq(N),

• if r⟨α⟩ is defined then it is a question or an answer;

• if r⟨α⟩ is defined and β is a prefix of α then r⟨β⟩ is defined;

• if β is a prefix of α and r⟨α⟩ = r⟨β⟩ =?n then α = β.

Comparing this with Definition 2.9(i), any |-irredundant element is clearly semi-irredundant, but a semi-irredundant element may have inaccessible nodes underneath answer nodes. Note that if r is semi-irredundant then irr_{|}(r) ⊑ r. (In this section, unlike in Section 4, we will use “irredundant” without qualification to mean |-irredundant.)

We now define [[ \overline{2} ]] as follows:

|[[ \overline{2} ]]| = \{F | F is a morphism B → N_{⊥}\}
∥F ∥_{[[ \overline{2} ]]} = \{r | r is semi-irredundant ∧ ∀g ∈ B. r | g = F (g)\}.

(Our reasons for choosing this semi-irredundant representation will become more apparent in Section 7.2 below.) It is easy to check that [[ \overline{2} ]] ≅ N_{⊥}^{B}. Note that every semi-irredundant realizer belongs to some ∥F ∥_{X}; in fact, we may define an equivalence relation ∼ on semi-irredundant realizers by setting r ∼ r′ iff r, r′ ∈ ∥F ∥_{X} for some F.

For [[ \overline{3} ]] we take the following object:

|[[ \overline{3} ]]| = \{Φ | Φ is a morphism [[ \overline{2} ]] → N_{⊥}\}
∥Φ∥_{[[ \overline{3} ]]} = \{r | ∀F ∈ [[ \overline{2} ]]. ∀t ∈ ∥f∥. r | t = Φ(F)\}.

For all other types σ → τ we may take [[ σ → τ ]] = [[ τ ]]_{⊥}^{[[ σ]]} as usual. This completes the definition of [[ −]].

We remark briefly on the relationship between the full and effective interpretations of these types. Clearly [[ \overline{0} ]]_{full} and [[ \overline{0} ]]_{eff} are identical, and [[ \overline{1} ]]_{eff} can be identified with a subobject of [[ \overline{1} ]]_{full}. The observation above that every semi-irredundant r realizes some F ∈ [[ \overline{2} ]] (valid in both the full and effective settings) yields the following easy facts: every F ∈ [[ \overline{2} ]]_{eff} extends uniquely to an element F̂ ∈ [[ \overline{2} ]]_{full}, and every realizer for F is also a realizer for F̂. The relationship between [[ \overline{3} ]]_{eff} and [[ \overline{3} ]]_{full} is far from obvious, but it will be established in Section 8.

The call-by-value types (apart from \overline{0}) also have counterparts in the hypercoherence model. Indeed, for σ, τ ≠ \overline{0}, we may define

\begin{aligned}[[ \overline{0} → \overline{0} ]]_{HC} & = & N^{ω}, \\ [[ σ → \overline{0} ]]_{HC} & = & ([[ σ]]_{HC} ⇒ N), \\ [[ σ → τ ]]_{HC} & = & ([[ σ]]_{HC} ⇒ [[ τ ]]_{HC⊥}), \end{aligned}

where N^{ω} is as defined in Section 6. We will consider this interpretation in Section 8 below.

7.2 Construction of H

We now work towards the main result: in both Mod(B_{full}) and Mod(B_{eff}), the object [[ \overline{3} ]] is a retract of [[ \overline{2} ]]. As we shall see, the construction of the retraction is directly inspired by the combinatory algebra B.

The easy half of the retraction will be the morphism I : \overline{3} → \overline{2} defined as follows. Let bar : B × B → N_{⊥} be the morphism defined by (f, g) ↦ f | g, as in Section 3.1. Currying this, we obtain a morphism B → N_{⊥}^{B}, and hence a morphism b : [[ \overline{1} ]] → [[ \overline{2} ]], mapping f to f | −. Now let I : [[ \overline{3} ]] → [[ \overline{2} ]] be the morphism induced by precomposition with b: that is,

I = − ∘ b : ([[ \overline{2} ]] ⇒ [[ \overline{0} ]]_{⊥}) ⟶ ([[ \overline{1} ]] ⇒ [[ \overline{0} ]]_{⊥}).

Note that b is realized by the element irr_{|} of Section 2.3, and I itself is realized by ı = λ^{∗}xy. x(irr_{|} y).

The other half of the retraction will be a morphism H : [[ \overline{2} ]] → [[ \overline{3} ]] such that H ∘ I = id_{[[ \overline{3} ]]}. Since the construction of H is rather involved, we begin with an informal explanation.

We think of the type \overline{1} as the object B, and \overline{2} as the object B equipped with the partial equivalence relation ∼ defined above. Any element of B will realize some morphism B → N_{⊥} (that is, \overline{1} → \overline{0}), since each element of B has just one realizer; but an element r of B will realize a morphism \overline{2} → \overline{0} only if r acts extensionally on ∼-classes. The morphism I essentially takes a morphism (B, ∼) → N_{⊥} and treats it as a morphism B → N_{⊥}, just by forgetting the equivalence relation.

The morphism H, on the other hand, takes a morphism F : B → N_{⊥}, given by an arbitrary realizer r, and converts it into a morphism ext(F) : B → N_{⊥} that acts extensionally with respect to ∼, and can hence be treated as a morphism (B, ∼) → N_{⊥}. In some sense, ext(F) will be the closest approximation to F that is ∼-extensional.

We define ext(F) from F in something like the following way: for any r ∈ B we take ext(F)(r) = n if F (r′) = n whenever r′ ∼ r; if there is no such n we take ext(F)(r) = ⊥. (This is not quite right, but it gives the basic idea). Thus, ext(F) “homogenizes” F with respect to ∼. However, it is not immediately clear that ext(F)(r) can be computed by a sequential algorithm: it seems, on the face of it, we would need to test infinitely many realizers r′ ∼ r. The key to the proof is the observation that in some sense there are essentially only finitely many such realizers r′, and so it suffices to test a finite set of realizers that are representative of all of them.

We need to show, of course, that this testing can be done within B, so that we obtain a realizer for ext(F). Finally, we show that the passage from F to ext(F) can itself be performed within B, uniformly in F, so that we obtain a realizer for the morphism H.

We approach the formal construction of H by first establishing some facts about the set of realizers for an arbitrary type 2 function F. For any F ∈ [[ \overline{2} ]], we define its trace, written tr F, to be the set of all pairs (g, F g) where g : N ⇀ N is a finite partial function (given as a finite set of ordered pairs) which is minimal such that F g is defined. (Of course, this is exactly the trace in the sense of the hypercoherence model, although we will not need this fact.) Clearly F is determined by tr F, since F h = n iff (g, n) ∈ tr F for some g ⊆ h. Moreover, if p is any irredundant realizer for F, there is a bijective correspondence between elements of tr F and nodes α such that p⟨α⟩ is an answer. Explicitly, (g, F g) ∈ tr F corresponds to α if p⟨α⟩ =!F g and whenever β, m is a prefix of α and p⟨β⟩ =?n we have g(n) = m. (Note that in this situation the size of dom g is exactly the length of α).

We write F ⊑ F′ if tr F ⊆ tr F′. We say F is finite if tr F is finite. The following observations now provide the key to the whole construction:

Lemma 7.2 Suppose F ∈ [[ \overline{2} ]] is finite. Then (i) F has only finitely many irredundant realizers, each with finite domain; (ii) any realizer p ∈ ∥F ∥ extends exactly one of these irredundant realizers; (iii) the set of minimal realizers can be effectively computed (as a finite list of

finite graphs) from tr F.

Proof (i) Clearly, if p is an irredundant realizer for F then dom p consists of all ⟨β⟩ such that β is a prefix of some α with p⟨α⟩ an answer. But by the above remarks, if F is finite then there are just finitely many such α; hence dom p is finite. Moreover, for each (g, F g) ∈ tr F, p induces a total order ⪯_{p}^{g} on dom g, where n ⪯_{p}^{g} n′ iff there exist proper prefixes β, β′ of α with p⟨β⟩ = n, p⟨β′⟩ = n′ and β a prefix of β′. Clearly p may be recovered from tr F together with the orders ⪯_{p}^{g} as follows: if the elements of dom g in the order ⪯_{p}^{g} are precisely n_{1}, …, n_{l} then we have

p⟨gn_{1}, …, gn_{i}⟩ = ?n_{i+1} for 0 ≤ i < l; p⟨gn_{1}, …, gn_{l}⟩ = !F g.

But since there are only finitely many combinations of total orders ⪯_{p}^{g} on the sets dom g, there can be only finitely many irredundant realizers p.

(ii) If p is any semi-irredundant realizer for F then irr_{|}(p) is an irredundant realizer for F, and p extends irr_{|}(p). Furthermore, if q is any irredundant realizer for F such that p extends q, then irr_{|}(q) = q and irr_{|}(p) extends irr_{|}(q); hence clearly q = irr_{|}(p).

(iii) Given tr F (where for each element (g, F g), g is given as a finite list of pairs), we may effectively compute the finite set of all possible families of orderings (⪯^{g} | (g, F g) ∈ tr F) in which each ⪯^{g} is a total order on dom g.

Moreover, for each such family (⪯^{g}), we may effectively determine whether the ⪯^{g} all arise from some irredundant realizer p (this happens provided the above formulae for p in terms of the ⪯^{g} do not give rise to clashes). If the ⪯^{g} do all arise from some p, we may effectively compute the graph of p itself according to the above formulae. Thus we may effectively compute the finite set of (graphs of) irredundant realizers for F. □

The force of this proposition is that we may find a finite set of realizers for F that is representative of all of them. Part (ii) depends on the fact that our realizers for F are already semi-irredundant rather than arbitrary elements that track F. Note in passing that the set of irredundant realizers for a finite F is exactly the same in the full and effective settings.

The next lemma establishes a useful connection between the trace ordering on type 2 functions and the pointwise ordering on their realizers.

Lemma 7.3 Suppose given F, G ∈ [[ \overline{2} ]] such that F ⊑ G. Then for any irredundant realizer q ∈ ∥G∥ there is an irredundant realizer p ∈ ∥F_{0}∥ such p ⊑ q. Moreover, if F is finite then p can be chosen to be finite (and hence effective).

Proof Recall that the answer nodes of q correspond bijectively to the elements of tr G. Let p be the restriction of q to arguments ⟨β⟩ where β is a prefix of some answer node α corresponding to an element of tr F. Clearly p ⊆ q, and it is easy to see that p tracks F. Moreover, if F is finite then there are finitely many answer nodes corresponding to elements of tr F; hence p has finite domain. □

We are now ready to construct the morphism H. We proceed in several steps, beginning with the following definition:

Definition 7.4 (i) Suppose F, G_{0} ∈ [[ \overline{2} ]] with G_{0} finite. We say that F uniformly yields n on G_{0} if, for each irredundant realizer p_{0} ∈ ∥G_{0}∥, for all q ⊑ p_{0} in B we have F q = n iff q = p_{0}.

(ii) We provisionally define a function HF : |[[ \overline{2} ]]| → |[[ \overline{0} ]]| as follows: For each G ∈ [[ \overline{2} ]], set HF (G) = n iff there is some finite G_{0} ⊑ G such that F uniformly yields n on G_{0}.

To ensure that part (ii) of the above definition is sound, we need to show that G_{0}, if it exists, is unique. This and other useful information is given by the following proposition.

Proposition 7.5 Suppose given F, G ∈ [[ \overline{2} ]], p an irredundant realizer for G, r an irredundant realizer for F, and some finite G_{0} ⊑ G such that F uniformly yields n on G_{0}. Then

(i) r | p = n;

(ii) if p_{0} is the smallest subfunction of p such that r | p_{0} = n, then p_{0} is an irredundant realizer for G_{0};

(iii) if G_{1} ⊑ G is finite and F uniformly yields n on G_{1}, then G_{1} = G_{0}.

Proof (i) By Lemma 7.3 we may choose p′ ⊑ p such that p′ is an irredundant realizer for G_{0}. But then F p′ = n, so r | p′ = n, whence r | p = n.

(ii) The above realizer p′ ⊑ has the property that for all q ⊑ p′ in B we have F q = n iff q = p′. So if p_{0} is as given then p_{0} = p′; thus p_{0} is an irredundant realizer for G_{0}.

(iii) The realizer p_{0} is defined without reference to G_{0}. So if G_{1} is as given then p_{0} realizes both G_{0} and G_{1}, so G_{0} = G_{1}. □

Proposition 7.6 For each F ∈ [[ \overline{2} ]], the function HF defined above is realizable, i.e. is an element of [[ \overline{3} ]].

Proof Let r be an irredundant realizer for F. Note that if F uniformly yields n on some G_{0} and p_{0} is an irredundant realizer for G_{0}, then the answer node of r that produces the result of the computation of r | p_{0} corresponds to the element (γ, n) of tr F, where γ is the graph of p_{0}.

This suggests that we restrict r to a realizer r′ defined as follows. If α is an answer node of r corresponding to an element (γ, n) ∈ tr F, where γ is the graph of some irredundant realizer p_{0} for some finite G_{0} ∈ [[ \overline{2} ]], then take r′⟨α⟩ to be !n if F uniformly yields n on G_{0}, ⊥ otherwise. If a ∈ N is not of the form ⟨α⟩ for such a node α, then take r′a = ra. Clearly r′ is irredundant, and from the above observation it is easy to see that r′ tracks HF.

For the effective case, we also need to check that if r is effective then so is r′. Suppose r is effective and irredundant; then given a such that ra =!n we must have a = ⟨α⟩ for some α. Now given an answer node α of r we may effectively compute the values of r⟨β⟩ for all prefixes β of α; from this we may effectively obtain the element (γ, n) corresponding to α. We may then effectively decide whether γ is the graph of an irredundant element p_{0}; if so, p_{0} necessarily realizes some finite G_{0}, and we may effectively obtain tr G_{0} from γ. By Lemma 7.2, from tr G_{0} we may effectively compute the finite list of all irredundant realizers for G_{0}; and since r is effective, it is semi-decidable whether F uniformly yields n on G_{0}. Combining all this information we see that r′ is effective. □

We have thus defined a set-theoretic function H : |[[ \overline{2} ]]| → |[[ \overline{3} ]]|. Note that the definitions of H in the full and effective settings agree: given F ∈ [[ \overline{2} ]]_{full} such that F has an effective realizer and so restricts to an element F_{eff} ∈ [[ \overline{2} ]]_{eff}, the element H_{eff}F_{eff} coincides with the restriction of H_{full}F to [[ \overline{2} ]]_{eff}.

The last step in the construction is to show that the function H is itself realizable. In fact, exactly the same realizer will work in the full and effective settings. In the light of the above remarks, it suffices to show:

Proposition 7.7 There is an element h ∈ B_{eff} such that, for all F ∈ [[ \overline{2} ]]_{full}, if r ∈ ∥F ∥ then h • r ∈ ∥HF ∥.

Proof Essentially this amounts to showing that the construction of r′ from r in the previous proof can be carried out within B_{eff} itself. However, since this construction works only on irredundant realizers and we require h to work on all semi-irredundant realizers, we had better define h = λ^{∗}x.h′(irr_{|}x), where h′ embodies the above construction.

A completely formal definition of h′ would be unilluminating, so we content ourselves with an “anthropomorphic” description of the algorithm embodied by the ath decision tree in the forest represented by h′, for an arbitrary a ∈ N.

We first ask the question a (that is, h′⟨a⟩ =?a). Suppose this receives the answer b. If either a is not of the form ⟨α⟩ or b is not of the form !n, we simply return b as our final result (that is, h′⟨a, b⟩ =!b). Otherwise, we ask the question ⟨β⟩ for every prefix β of α in turn. From the answers received so far, we now “know” the element (γ, n) in the previous proof. If γ is not the graph of an irredundant realizer p_{0}, we simply give up and diverge. Otherwise, we now know p_{0} and hence the trace of the functional G_{0} it realizes. Let p_{1}, …, p_{N} be the list of all irredundant realizers of G_{0}, which we now know. We wish to check whether our argument r satisfies r | p_{i} = n for each i. To do this, we first simulate the play of r against p_{1}, by asking questions to r, and ourselves providing the answers to the questions r asks using our knowledge of p_{1}. If in fact r | p_{1} = n′, at some point we will receive the answer !n′. If n′ ≠ n, we again hang up and diverge. If n′ = n, we then proceed to the simulation of r against p_{2}, and so on. Finally, if we complete the simulation of r against each of the p_{i} and have received the answer n in every case, we return n as our final result.

It should be clear that h′ may be given effectively, and that if r is an irredundant realizer for F then h′ • r is the realizer r′ for HF described in the previous proof. It follows that h is also effective, and tracks H as required. □

This completes the construction of H.

7.3 Properties of H

We next show that H is indeed a one-sided inverse to I. For this, we need to establish some special properties of realizers for elements Φ ∈ [[ \overline{3} ]]. By definition, r is a realizer for some such Φ iff r acts extensionally on semi-irredundant realizers, that is, r | p = r | q whenever p ∼ q.

Proposition 7.8 Suppose r realizes Φ ∈ [[ \overline{3} ]], p realizes F ∈ [[ \overline{2} ]], and ΦF = n ∈ N. Let p_{0} be the unique smallest finite subfunction of p such that r | p_{0} = n. Then

(i) dom p_{0} is prefix-closed, i.e. if ⟨α⟩ ∈ dom p_{0} and β is a prefix of α then ⟨β⟩ ∈ dom p_{0};

(ii) p_{0} realizes some F_{0} ∈ [[ \overline{2} ]] such that ΦF_{0} = n;

(iii) for all α, p_{0}⟨α⟩ is an answer iff α is a leaf in p_{0} (i.e. α is not a proper prefix of any β where ⟨β⟩ ∈ dom p_{0}).

Proof (i) Extend p_{0} to a function p_{1} by setting p_{1}⟨β⟩ =!0 whenever β ∉ dom p_{0} is a prefix of some α ∈ dom p_{0}. Then dom p_{1} is finite and prefix-closed, and since p was semi-irredundant, so is p_{1}. Thus p_{1} realizes some F_{1} ∈ [[ \overline{2} ]]. Furthermore, since p_{0} ⊑ p_{1} we have r | p_{1} = n, so ΦF_{1} = n. Now let p_{2} = irr_{|}(p_{1}); then p_{2} also realizes F_{1}, and so r | p_{2} = n since r realizes Φ. Thus, we have p_{0}, p_{2} ⊑ p_{1} with r | p_{0} = r | p_{2} = n; hence p_{0} ⊑ p_{2} by minimality of p_{0}. But if there exists α ∈ dom p_{0} with a prefix β ∉ dom p_{0} then ⟨α⟩ ∉ dom p_{2}, a contradiction. So dom p_{0} is already prefix-closed, and p_{1} = p_{0}.

(ii) Since p is semi-irredundant, it now follows that p_{0} is semi-irredundant, and so realizes some F_{0} ∈ [[ \overline{2} ]] where ΦF_{0} = n.

(iii) By (i), p_{4} = irr_{|}(p_{0}) also realizes F_{0}, and so r | p_{4} = n. Since p_{4} ⊑ p_{0}, by minimality of p_{0} we have p_{4} = p_{0}, so p_{0} is irredundant. In particular, if p_{0}⟨α⟩ is an answer then α is a leaf in dom p_{0}. For the converse, suppose α is a leaf but p_{0}⟨α⟩ is a question. Let p_{5} be obtained as a restriction of p_{0} simply by removing the value at ⟨α⟩. Clearly p_{5} also realizes F_{0}, and so r | p_{5} = n, contradicting the minimality of p_{0}. □

Part (iii) of the above proposition is not actually required below, but it provides some additional insight into the situation. The proof of part (i) shows why we need the notion of semi-irredundant realizer. If we assumed only that r | p = n for all irredundant realizers p of F, we would not be able to show in the above proof that r | p_{2} = r | p_{1}. On the other hand, if we took as ∥F ∥ the set of all p tracking F, we would lose the property that every realizer for a finite F extends one of the finitely many irredundant realizers (Lemma 7.2(ii)).

Theorem 7.9 For the morphisms

[[ \overline{3} ]] [figure: I; \underline{H}] [[ \overline{2} ]]

defined above, we have H ∘ I = id_{[[ \overline{3} ]]}.

Proof Suppose Φ ∈ [[ \overline{3} ]], and take any irredundant r ∈ ∥IΦ∥. It is easy to see that r ∈ ∥Φ∥: take any G ∈ [[ \overline{2} ]] and note that for any g ∈ ∥G∥ we have

r | g = (IΦ)(g) = Φ(λf. g | f) = ΦG.

Let r′ be the realizer for H(IΦ) obtained from r as in the proof of Proposition 7.6. To show that H(IΦ) = Φ it will suffice to show that r′ = r. So suppose α is an answer node of r corresponding to (γ, n) ∈ tr IΦ, where γ is the graph of an irredundant realizer p_{0} ∈ ∥G_{0}∥ for some finite G_{0}. We wish to know that r′⟨α⟩ = r⟨α⟩ (note that we automatically have r′a = ra for all a not of this form). But r⟨α⟩ =!n, and so to show that r′⟨α⟩ =!n it is enough to show that IΦ uniformly yields n on G_{0}.

Suppose q_{0} is any irredundant realizer for G_{0}. Since r realizes Φ, we have r | q_{0} = ΦG_{0} = r | p_{0} = n. Now let q_{1} be the least subfunction of q_{0} such that (IΦ)q_{1} = n—that is, such that r | q_{1} = n. Then by Proposition 7.8(ii), q_{1} is an irredundant realizer for some G_{1} ⊑ G_{0} such that ΦG_{1} = n. But now by Lemma 7.3 we may find a realizer p_{1} ∈ ∥G_{1}∥ such that p_{1} ⊑ p_{0}. Since r realizes Φ, we have r | p_{1} = n. But p_{0} is clearly minimal such that r | p_{0} = n, and so p_{1} = p_{0}. Hence G_{1} = G_{0}, and since q_{0} is a minimal realizer for G_{0} we have q_{1} = q_{0}. So q_{0} is minimal such that (IΦ)q_{0} = n; thus IΦ uniformly yields n on G_{0} as required. □

Remark 7.10 It is natural to ask whether H (or some other one-sided inverse to I) can be characterized by a universal property involving I—for instance, as an adjoint or Kan extension. At present, the answer would seem to be no. However, one can obtain a characterization of this kind if one decomposes I into two components.

Specifically, let Z be the modest set defined by

|Z| = \{F : B → N_{⊥} | ∀g ∈ B. F (g) = F (irr_{|}(g))\}, ∥F ∥_{Z} = ∥F ∥_{[[ \overline{2} ]]}.

Let I_{1} : Z → [[ \overline{2} ]] be the evident inclusion; it is easy to see that I_{1} has a one-sided inverse H_{1}. Also I factors through I_{1} via a morphism I_{0} : [[ \overline{3} ]] → Z. Let H_{0} be the restriction of H to Z; then we have H_{0}I_{0} = id. The morphism H_{0}H_{1} is not exactly our morphism H, but at least it is a one-sided inverse to I. Moreover, one can characterize H_{0} and H_{1} abstractly as follows: H_{0} is a right adjoint of I_{0} with respect to the stable ordering, and H_{1} is a right adjoint of I_{1} with respect to the pointwise ordering.

It is perhaps surprising that no simpler characterization of a one-sided inverse to I is possible, if this is indeed the case.

It is now an easy step to show that every type is a retract of \overline{2}:

Theorem 7.11 (Universality of \overline{2}) In Mod(B), every object [[ σ]] is a retract of [[ \overline{2} ]].

Proof We first prove the result for all pure types \overline{n}. Clearly [[ \overline{0} ]], [[ \overline{1} ]], [[ \overline{2} ]] are all retracts of [[ \overline{2} ]]. We have shown above that [[ \overline{3} ]] ⊲ [[ \overline{2} ]]; and from a retraction (i, j) : [[ \overline{n + 1} ]] ⊲ [[ \overline{n}]] we obtain a retraction (− ∘ j, − ∘ i) : [[ \overline{n + 2} ]] ⊲ [[ \overline{n + 1} ]]. By composing such retractions, we have [[ \overline{n}]] ⊲ [[ \overline{2} ]] for all n ≥ 3.

To extend the result to arbitrary types, we just need to know that every object [[ σ]] is a retract of some [[ \overline{n}]]. This is a well known piece of folklore. For call-by-name types it is proved in [21, Section 8.1], and in fact the same proof also works for call-by-value types without any modification. □

Remark 7.12 If (i, j) : [[ σ]] ⊲ [[ \overline{2} ]] is a retraction in Mod(B), it is immediate that i, j themselves live in the type structure R: essentially i ∈ R^{σ→\overline{2}} and j ∈ R^{\overline{2}→σ}.

We thus have that for the call-by-value SR functionals, the type \overline{2} is universal among simple types. Of course exactly the same result holds for the call-by-name SR functionals, and one way to see this is as follows. By the results of [31, Chapter 6], every object [[ σ]]_{N} is a retract of some [[ τ ]]_{V}, and by the above results, this is in turn a retract of [[ \overline{2} ]]_{V}, which is a retract of [[ \overline{2} ]]_{N}.

It is interesting to compare our results with the situation for other known type structures. In both the full and effective Scott models, which correspond to a version of PCF with parallel operators, the type \overline{1} is already universal. (This follows easily from the fact that every finite type is a definable retract of Plotkin’s T^{ω}—see [34, Lemma 5.2].) However, in the full or effective games models, corresponding to pure PCF, there is no universal finite type.^{4} Remark 7.13 We end this paragraph with some informal remarks on the computational complexity of H. Although we do not know what is the best way to measure complexity at higher types precisely, it is intuitively clear that the main factor contributing to the complexity of H is the number of irredundant realizers for G_{0} that have to be tested in turn. In the worst case, this is factorial in the size of dom p_{0} (call this n), and each irredundant realizer p_{1} itself has size n. Moreover, n is essentially the number of queries made by F to the given realizer p for G. Thus, if we are given realizers r, p for F, G respectively, the time taken up by H in the computation of HF G is at most t.t!, where t is the time taken by F in the computation of F p.

4I am grateful to Samson Abramsky and Martin Hyland for informing me of this fact.

8 Applications of universality

One consequence of Theorem 7.11 is that, for many questions about the SR functionals, it suffices to consider low types. In this section we illustrate this principle by giving an alternative proof of van Oosten’s theorem (Theorem 5.8). We also consider the category of retracts of [[ \overline{2} ]] as a category of domains, and indicate how one can interpret recursive types there. Further applications of the universality theorem will be given in the next section.

8.1 Hypercoherences revisited

We now use Theorem 7.11 to give an alternative proof that the full SR functionals coincide with the strongly stable functionals (cf. Section 5.2). Unlike the proofs in [17, 43], which both involve elaborate inductions up the type structure, our proof concentrates on the types \overline{2} and \overline{3}; the extension to arbitrary types is then straightforward. Since the main interest of the proof is conceptual rather than technical, and result itself is not new, we concentrate on the main ideas, omitting some of the details.

The call-by-value interpretation [[ σ]]_{HC} for types σ ≠ \overline{0} was given in Section 7.1. We define sets D^{σ} by

D\overline{0} = N, D^{σ} = D([[ σ]]_{HC}) for σ ≠ \overline{0}.

These come equipped with partial application operations ·_{στ} : D^{σ→τ} × D^{σ} ⇀ D^{τ}. Our goal is to establish bijections β_{σ} : R^{σ} ≅ D^{σ} that commute with application (note that R^{σ} here means R_{V,}^{σ}_{full}). We will write R\overline{n}, D\overline{n}, β\overline{n} simply as R^{n}, D^{n}, β_{n}.

The bijections β_{0} and β_{1} are evident. For β_{2}, we proceed as follows. For each k > 0, let [k] be the flat hypercoherence with atoms 0, …, k − 1; then there are evident retractions [k] ⊲ N in HC, and the corresponding projections N → N form a chain whose limit is the identity. We also have retractions N^{k} ⊲ N^{ω} corresponding to the projection from N^{ω} onto its first k factors. Using these, we can construct a chain of retractions ([k]^{k} ⇒ [k])⊲(N^{ω} ⇒ N), with corresponding projections δ_{k} on N^{ω} ⇒ N where ⨆ ρ_{k} = id. Note that each δ_{k} : D^{2} → D^{2} has a finite image consisting entirely of finite elements. We regard D^{2} as equipped with the usual order on states of [[ \overline{2} ]]_{HC}; the image of each δ_{k} is then a full sub-poset of D^{2}.

Likewise, in Mod(B) we have evident retracts [k]_{⊥} ⊲ N_{⊥} for each k, and so we can construct increasing sequence of retractions ρ_{k} : R^{2} → R^{2} corresponding precisely to the δ_{k}. We regard R^{2} as equipped with the trace ordering as in Section 7.2, so that the image of each ρ_{k} is a full sub-poset of R^{2}.

Proposition 8.1 For each k there is an order-isomorphism Im δ_{k} ≅ Im ρ_{k}. Moreover, these isomorphisms commute with the retractions (Im δ_{l}) ⊲ (Im δ_{k}) and (Im ρ_{l}) ⊲ (Im ρ_{k}) for l ≤ k, and with the application operations.

Proof We wish to show that the poset P_{k} of elements of [k]_{⊥}^{k} ⇒ [k]_{⊥} in Mod(B) (with the trace ordering) is isomorphic to the poset Q_{k} of states of [k]^{k} ⇒ [k] in HC. But P_{k} is easily seen to be isomorphic to the poset S_{k} of Milner-Vuillemin sequential functions with the stable ordering (use the embedding SSeqFun → Mod(B) of Section 4.3). The bijection S_{k} ≅ Q_{k} is given by [9, Proposition 3], and this is an order-isomorphism since, for hypercoherences, the inclusion order on function spaces coincides with the stable order.

The isomorphisms P_{k} ≅ Q_{k} clearly respect application. They yield isomorphisms Im ρ_{k} ≅ Im δ_{k}, and the coherence conditions are easily verified. □

Let D_{fin}^{2} = ⋃ Im δ_{k}, R_{fin}^{2} = ⋃ Im ρ_{k}. It is clear from the construction that D^{2} is the chain-completion of the full sub-poset D_{fin}^{2}. We also know that any element x ∈ R^{2} is a least upper bound ⨆ ρ_{k}(x) of elements of R_{fin}^{2}. To establish the order-isomorphism β_{2} : R^{2} ≅ D^{2}, it therefore suffices to check:

Proposition 8.2 R^{2} (with the trace ordering) is a CPO.

Proof It suffices to check that any chain x_{1} ⊑ x_{2} ⊑ … where x_{k} ∈ Im ρ_{k} has a least upper bound in R^{2}. This an easy application of König’s Lemma, analogous to that in [17, Theorem 5] or our Proposition 5.13. □

In order to show that Mod(B) and HC contain the same morphisms at type \overline{3}, we characterize the hypercoherence structure of [[ \overline{2} ]] in terms of the realizability model. Recall that in Mod(B) we have a surjective morphism b : [[ \overline{1} ]] → [[ \overline{2} ]] mapping f to f | −, realized by irr_{|}. The crucial step will be to show that all chains and coherent sets in [[ \overline{2} ]] arise, via b, from chains and coherent sets in [[ \overline{1} ]]. This will allow us to reduce questions about type \overline{2} → \overline{0} to questions about \overline{1} → \overline{0}. (The basic idea here is inspired by [13].)

Lemma 8.3 (i) Under the bijections β_{1} and β_{2}, the morphisms R^{1} → R^{2} in Mod(B) correspond exactly to the strongly stable maps D^{1} → D^{2} in HC. In particular, the function b corresponds to a strongly stable map.

(ii) For every increasing chain x_{0} ⊑ x_{1} ⊑ … in R^{2}, there is an increasing chain y_{0} ⊑ y_{1} ⊑ … in R^{1} such that b(y_{i}) = x_{i} for all i.

(iii) For every coherent set U ⊆ R^{2} (that is, for every set corresponding to a coherent subset of D^{2}), there is a coherent set V ⊆ R^{1} such that b(V) = (U).

Proof (i) It is easy to give a definition of a retraction ([[ \overline{1} ]] ⇒ [[ \overline{2} ]]) ⊲ [[ \overline{2} ]] that works uniformly for both Mod(B) and HC. The corresponding idempotents are then identified by β_{2}, and the result follows easily.

(ii) By Proposition 8.2, take x = ⨆ x_{i} in R^{2}. Let r be any irredundant realizer for x. By Lemma 7.3, we may take irredundant realizers r_{i} for the x_{i} such that r_{i} ⊑ r and (by inspection of the proof of Lemma 7.3) r_{i} ⊑ r_{i+1}. Thus the r_{i} form an increasing chain in R^{1}, and x_{i} = b(r_{i}) for each i.

(iii) An important lemma (see e.g. [13, Lemma 3.2]) says that in any hypercoherence X, every coherent set is the image of a coherent set in N^{ω} via a strongly stable map N^{ω} → X. So take W ⊆ R^{1} coherent and g : R^{1} → R^{2} strongly stable such that g(W) corresponds to U. By (i), g may be regarded as a morphism [[ \overline{1} ]] → [[ \overline{2} ]] in Mod(B). Suppose r ∈ B tracks g; then g factors through b via a morphism g̃ : [[ \overline{1} ]] → [[ \overline{1} ]] tracked by r. But now g̃ : R^{1} → R^{1} is a strongly stable map, so V = g̃(W) is coherent in R^{1}, and b(V) = U. □

Proposition 8.4 Under the bijection β_{2}, the morphisms R^{2} → N_{⊥} in Mod(B) correspond exactly to the strongly stable maps D^{2} → N_{⊥} in HC.

Proof Given Φ : [[ \overline{2} ]] → N_{⊥} in Mod(B), we have Φ ∘ b : [[ \overline{1} ]] → N_{⊥} and so Φ ∘ b ∈ R^{2}. Hence Φ ∘ b is strongly stable. We wish to check that Φ is strongly stable, that is,

• Φ respects chains and their lubs;

• Φ respects coherent sets and their meets.

Suppose x_{0} ⊑ x_{1} ⊑ … is a chain in R^{2} with lub x. By Lemma 8.3(ii), take y_{0} ⊑ y_{1} ⊆ … in R^{1} such that b(y_{i}) = x_{i}, and let y = ⨆ y_{i}, so that b(y) = x. Since Φ ∘ b is strongly stable it respects the chain (y_{i}) and its limit; hence Φ respects the chain (x_{i}) and its limit.

Likewise, given U ⊆ R^{2} coherent, by Lemma 8.3(ii) take V ⊆ R^{1} coherent such that b(V) = U. Since b is strongly stable, we have b(⋀ V) = ⋀ U. But now Φ ∘ b respects the coherent set V and its meet; hence Φ respects the coherent set U and its meet. □

We thus obtain a bijection β_{3} : R^{3} ≅ D^{3} that respects application. We can now easily extend the isomorphism to all pure types:

Theorem 8.5 For every n there is a canonical bijection β_{n} : R^{n} ≅ D^{n}, and these bijections respect application.

Proof We already know the result for n = 0, 1, 2. We will prove by induction (starting from n = 2) that there is a bijection β_{n+1} : R^{n+1} ≅ D^{n+1} that respects application, and moreover there are retractions (i_{n}, j_{n}) : [[ \overline{n + 1} ]] ⊲ [[ \overline{n}]] in both Mod(B) and HC which are identified under β_{n+1} and β_{n}.

For n = 2, we already have a bijection β_{3} respecting application. Since we may define a retraction ([[ \overline{2} ]] ⇒ [[ \overline{3} ]]) ⊲ [[ \overline{3} ]] uniformly in both Mod(B) and HC, we have a bijection between morphisms R^{3} → R^{2} in Mod(B) and strongly stable maps D^{3} → D^{2} in HC. In particular, H is present as a strongly stable map in HC. Moreover, since the map b : [[ \overline{1} ]] → [[ \overline{2} ]] is present in both models, the map I = − ∘ b is present in both models. We therefore have retractions (I, H) : [[ \overline{3} ]] ⊲ [[ \overline{2} ]] in both Mod(B) and HC as required.

For the induction step, given i_{n} and j_{n} in both models as above, let i_{n+1} = λf : \overline{n}. f ∘ j_{n} and j_{n+1} = λg : \overline{n + 1}. g ∘ i_{n} Clearly (i_{n+1}, j_{n+1}) is a retraction [[ \overline{n + 2} ]] ⊲ [[ \overline{n + 1} ]] in both models. The corresponding idempotent on [[ n + 1 ]] is λf : \overline{n}.f ∘ j_{n} ∘ i_{n}, and this has the same meaning in both models modulo the bijection β_{n+1}, since by hypothesis the latter respects application. By restricting this bijection to the image of the idempotent, we obtain a bijection β_{n+2} : R^{n+2} ≅ D^{n+2}. Clearly this respects application, and the retractions (i_{n+1}, j_{n+1}) in the two models are identified under β_{n+2} and β_{n+1}. □

It is now routine to extend the isomorphism to arbitrary types σ by transporting the bijections β_{n} along appropriate retractions [[ σ]]⊲[[ \overline{n}]], defined (uniformly for both models) as in the proof of Theorem 7.11. Similarly, it is straightforward to obtain a isomorphism for the corresponding call-by-name type structures, since any call-by-name type may be obtained as a definable retract of a call-by-value type (cf. [31, Chapter 6]). We omit the rather uninteresting details.

8.2 The category of retracts of type \overline{2}

We now draw attention to another consequence of the universality theorem: the object [[ \overline{2} ]] can be regarded as a combinatory algebra, and its category of retracts is an attractive category of domains with much interesting structure. There is a close analogy with the situation described in [50] for Scott’s Pω, whose category of retracts is the very beautiful category of countably-based continuous lattices. Again we give just a sketch of the main ideas, omitting tedious details. The results of this section hold for both B_{full} and B_{eff}.

First recall that we already have operations on objects of Mod(B) corresponding to products, sums, exponentials and lifting. We may also define a separated sum operation ⊕ on objects by X ⊕ Y = (X + Y)_{⊥}.

Let us now write B_{2} for the object [[ \overline{2} ]] in Mod(B). We will be interested in objects which are retracts of B_{2} in Mod(B); we write K for the full subcategory consisting of such objects. The crucial observations are the following:

Proposition 8.6 (i) The objects B_{2} × B_{2}, B_{2}^{B_{2}}, B_{2⊥}, B_{2} ⊕ B_{2} are retracts of B_{2}.

(ii) The category K has products, exponentials, lifting and separated sums, all inherited from Mod(B).

(iii) Each object X of K comes with a lift algebra structure X_{⊥} → X, and has a canonical fixed point operator X^{X} → X.

Proof (i) It is routine to exhibit all these objects as retracts of [[ \overline{3} ]]. So by Theorem 7.9 they are retracts of B_{2}.

(ii) Given X ⊲ B_{2} and Y ⊲ B_{2}, we have induced retractions X × Y ⊲ B_{2} × B_{2}, Y^{X} ⊲ B_{2}^{B_{2}}, X_{⊥} ⊲ B_{2⊥} and X ⊕ Y ⊲ B_{2} ⊕ B_{2}. By (i) all these objects are retracts of B_{2}, and the result follows since K is full in Mod(B).

(iii) The evident lift algebra structure on B_{2} induces one on X via the retraction X_{⊥} ⊲ B_{2⊥}. For fixed points, it is easy to see that there is a fixed point operator Y : B_{2}^{B_{2}} → B_{2} tracked by y, since pre-irredundant realizers are closed under lubs of chains. (Otherwise, the existence of Y may be deduced from the connection with the hypercoherence model.) This transfers to a fixed point operator X^{X} → X via the retractions X^{X} ⊲ B_{2}^{B_{2}} and X ⊲ B_{2}. □

The retraction B_{2}^{B_{2}} ⊲ B_{2} in particular means that the elements of B_{2} form a combinatory algebra—indeed a λ-model, since Mod(B) is well-pointed (see [3]). We will write B_{2} for this combinatory algebra. Note that the monoid M_{2} of realizable endofunctions of B_{2} is precisely the monoid of endomorphisms of B_{2} in Mod(B), and since all idempotents have splittings in Mod(B), the Karoubi envelope K(M_{2}) is equivalent to K. It follows that there is a full embedding E_{2} : K → Mod(B_{2}), analogous to the embedding E : SSeqFun → Mod(B) of Section 4.3. The embedding E_{2} preserves products, exponentials, lifting and separated sums, and has one significant advantage over the inclusion K ↪ Mod(B): every object in the image of E_{2} is projective (each element has just one realizer).

To summarize, B gave rise to the category of retracts K(M), which included SSeqFun, but B_{2} gives rise to the category of retracts K. Since K is much larger than K(M) and has better closure properties (it is cartesian closed), we conclude that B_{2} is in some sense a better model than B. However, the construction of B_{2} is undoubtedly more complicated, and indeed proceeds via the construction of B.

The situation described above for B_{2} is very similar to that for Pω: the category of retracts of Pω is a good category of domains with products, exponentials, lifting and separated sums, and it embeds well in Mod(Pω) (see [31, Section 7.3]). Furthermore, it is shown in [50] that one can perform type operations on retracts of Pω within Pω itself, and hence construct recursive domains simply by taking fixed points in Pω. We can now see that one can do exactly the same thing for B_{2}. We give only a very brief outline, since the details are formally identical to those in [50].

An object X in K can be represented (up to isomorphism) by any element x ∈ B_{2} that realizes an idempotent B_{2} → B_{2} corresponding to some retraction X ⊲ B_{2}. Note that x satisfies xa = x(xa) for all a ∈ B_{2}; we will call any such element x ∈ B_{2} an idempotent. Clearly every idempotent x represents some object X. If F is a k-ary operation on objects of K, we say that F is realizable if there is an element f ∈ B_{2} such that whenever x_{1}, …, x_{k} are idempotents representing X_{1}, …, X_{k} respectively, the element fx_{1} … x_{k} is an idempotent representing F (X_{1}, …, X_{k}). The following proposition lets us construct many examples of realizable operations:

Proposition 8.7 (i) The product, exponential and separated sum operations are realizable binary operations on objects of K, and the lift operation is a realizable unary operation.

(ii) The identity operation on objects is realizable. Constant operations are realizable. Realizable operations are closed under composition.

Proof We consider exponentials as an example. Suppose r ∈ B_{2} represents the retraction B_{2}^{B_{2}}, and x, y represent retractions X ⊲ B_{2}, Y ⊲ B_{2} respectively. Then λ^{∗}a.λ^{∗}z. y((ra)(xz)) (interpreted in B_{2}) represents the induced retraction Y^{X} ⊲ B_{2}. Thus, λ^{∗}xyaz. y((ra)(xz)) realizes the exponential operation. The other cases are similar.

(ii) is trivial. □

It is now easy to obtain recursive types as fixed points of realizable operations:

Theorem 8.8 For any realizable unary operation F, there is an object X of K such that X ≅ F (X). In particular, K contains solutions to all recursive type equations X ≅ F (X) where F is a unary operation constructed using ×, ⇒, −_{⊥}, ⊕ and fixed objects of K.

Proof Suppose f realizes F. Define a sequence r_{0}, r_{1}, … in B_{2} by r_{0} = ⊥, r_{n+1} = fr_{n}. Clearly r_{0} is an idempotent, and hence every r_{n} is an idempotent. Moreover, the action of f gives a morphism B_{2} → B_{2} and so is monotone with respect to the trace ordering; thus r_{0} ⊑ r_{1} ⊑ . . .. By Proposition 8.2, take r = ⨆ r_{n} in B_{2}. Since each r_{n} is an idempotent, it is easy to see that r is an idempotent, and that fr = r. Take X an object represented by r; then X ≅ F (X). The rest of the theorem follows immediately by Proposition 8.7. □

Remark 8.9 The category HC also contains an object [[ \overline{2} ]] and has many of the closure properties mentioned above for K. It would therefore appear that HC and K have a large full subcategory in common, but at present we do not know the precise extent of the overlap. Since not all idempotents on [[ \overline{2} ]] split in HC, there are objects of K with no counterpart in HC; we do not know whether the converse is true.

9 PCF and universal functionals

We now consider interpretations of call-by-value PCF in Mod(B) and Mod(B_{eff}). We will show that the functional H of Section 7 is universal, in the sense that every effective SR functional is definable relative to H in PCF. We then consider the extended language PCF+H, which gives us yet another handle on the SR functionals. Next we briefly touch on a notion of “degree” for SR functionals under the relation of relative PCF-definability. Finally, we prove a technical result: there is no universal SR functional with an essentially lower type than H.

9.1 Call-by-value PCF

We review the syntax and semantics of call-by-value PCF (henceforth called PCF). The types of PCF are just the simple types as given by Definition 3.5(i). For each type σ we have an infinite supply of variables x_{0}^{σ}, x_{1}^{σ}, . . .. Exactly as in call-by-name PCF, the well-typed terms are built up from variables and the constants 0, 1, 2, …: \overline{0}, succ, pred : \overline{1} and cond : \overline{0} → \overline{0} → \overline{0} → \overline{0} by means of the following rules:

\frac{M : τ}{(λx_{i}^{σ}.M) : σ → τ}  \frac{M : σ → τ N : σ}{(MN) : τ}  \frac{M : σ}{(μx_{i}^{σ}.M) : σ}

A closed term is a value if it is either a numeral 0, 1, 2, … or a λ-abstraction; we use V to range over values.

We give an operational semantics by defining a (big-step) evaluation relation ⇓ from closed terms to values, such that for each closed term M we have M ⇓ V for at most one V. The relation ⇓ is defined inductively by the following derivation rules. Here ⌣ denotes truncated subtraction: m ⌣ n = max(m − n, 0).

V ⇓ V (V a value)  \frac{M[μx.M/x] ⇓ V}{μx.M ⇓ V}

\frac{M ⇓ n}{succ M ⇓ n + 1}  \frac{M ⇓ n}{pred M ⇓ n ⌣ 1}

\frac{M ⇓ 0 N ⇓ V}{cond MNP ⇓ V}  \frac{M ⇓ n + 1 P ⇓ V}{cond MNP ⇓ V}

\frac{M ⇓_{N} λx.M′ M′[N/x] ⇓_{N} V}{MN ⇓_{N} V}

We write M ⇑ to mean that there is no V such that M ⇓ V.

Next we give the denotational semantics of this language in Mod(B) (where B is either B_{full} or B_{eff}). The interpretation [[ −]] of types is given essentially as in Section 7; however, here it is convenient to interpret function types using the standard exponentials and lifting rather than the special objects used there. We will also write [σ] for [[ σ]]_{⊥}, and η for the inclusion [[ σ]] → [σ].

We now interpret a term M : τ whose free variables are included in Γ = ⟨x_{1}^{σ_{1}}, …, x_{n}^{σ_{n}}⟩, by a morphism [M]^{Γ} : [σ_{1}] × ⋯ × [σ_{n}] ⇒ [τ]. The definition of [M]^{Γ} is by induction on the structure of M. The clauses for variables, numerals, succ, pred and cond are evident. For the remaining clauses, some further notation is helpful. Let us write fix_{σ} : [σ]^{[σ]} → [σ] for the fixed point morphism given by Proposition 8.6. We also write α_{σ} for the evident lift algebra structure [[ σ]]_{⊥} → [[ σ]], and strict : B_{⊥}^{A} → B_{⊥}^{A_{⊥}} for the morphism that extends a map A → B_{⊥} to a strict map A_{⊥} → B_{⊥}. We then have:

[λx^{σ}.M]^{Γ} = η ∘ [σ]^{η} ∘ curry ([M]^{Γ,x^{σ}})
[MN]^{Γ} = eval ∘ ⟨strict ∘ α_{σ→τ} ∘ [M]^{Γ}, [N]^{Γ}⟩
[μx^{σ}.M]^{Γ} = fix_{σ} ∘ curry ([M]^{Γ,x^{σ}})

A closed term M : τ is interpreted as a morphism 1 → [τ], that is, an element of [τ]. The following theorem establishes the agreement between the operational and denotational semantics.

Theorem 9.1 (Adequacy) For any closed term M : \overline{0}, we have [M] = n if M ⇓ n, and [M] = ⊥ if M ⇑.

Proof The usual technique for proving adequacy works (see [45]). In fact the result follows immediately from results in [31, Chapter 6], as we shall see in Section 10. □

We now investigate the expressive power of PCF for defining SR functionals. As before, we will write R for either R_{full} or R_{eff}. We say that an element x ∈ R^{σ} is PCF-definable if there is a closed PCF term M : σ such that [M] = η(x). A function f : R^{σ} → R^{τ} is PCF-definable if η ∘ f is PCF-definable as an element of R^{σ→τ}.

Proposition 9.2 (i) The map b : R\overline{1} → R\overline{2} of Section 7.2 is PCF-definable. (ii) The map I : R\overline{3} → R\overline{2} is PCF-definable.

Proof (i) Let isans : \overline{1}, strip : \overline{1}, empty : \overline{0} and add : \overline{0} → \overline{0} → \overline{0} be PCF terms such that for our chosen effective codings [?,!] and ⟨⋯⟩ we have

[[ empty ]] = ⟨ϵ⟩ [[ add ]](n)(⟨α⟩) = ⟨α, n⟩
[[ isans ]](!n) = 0  [[ isans ]](?n) = 1
[[ strip ]](!n) = n  [[ strip ]](?n) = n.

Now let ρ ≡ \overline{1} → \overline{1} → \overline{0} → \overline{0}, and let play be the PCF term

μP^{ρ}. λf\overline{1}.λg\overline{1}.λa\overline{0}. cond (isans (f a)) (strip (f a)) (P f g (add a (g (strip (f a))))).

Finally, let b = λf\overline{1}. λg\overline{1}. play f g empty. We omit the tedious verification that b defines b.

(ii) Now let I = λΦ\overline{3}. λg\overline{1}. Φ(bar g). Then I defines I. □

As a consequence of this we obtain an important property of the function H.

Theorem 9.3 (Universality of H) Every element f ∈ [σ]_{eff} is PCF-definable relative to H: that is, there is a closed PCF term M : (\overline{2} → \overline{3}) → σ such that f = [M](η(η ∘ H)).

Proof Clearly the term μx^{σ}.x denotes ⊥ ∈ [σ]_{eff}, so it suffices to show that every f ∈ [[ σ]]_{eff} is definable from H. Firstly, any element r ∈ [[ \overline{1} ]]_{eff} is definable in pure PCF as it is simply a partial recursive function. Secondly, given any element F ∈ [[ \overline{2} ]]_{eff}, take r ∈ B_{eff} a realizer for F and M : \overline{1} denoting r; then [b M] = η(F). Thus every element of [[ \overline{2} ]]_{eff} is PCF-definable. Next, using Proposition 9.2(ii), both halves of the retraction (I, H) : [[ \overline{3} ]] ⊲ [[ \overline{2} ]] are PCF-definable relative to H, and it follows easily that for any σ, both halves of the induced retraction (i, j) : [[ σ]] ⊲ [[ \overline{2} ]] are PCF-definable relative to H. Now given any f ∈ [[ σ]], let P : \overline{2} be a PCF term denoting i(f), and let N : \overline{2} → (\overline{2} → σ) be a PCF term such that [N](η(η ∘ H)) = j. Then clearly λh. (Nh)P defines f relative to H. □

Remarks 9.4 (i) Clearly one can obtain an analogous result for the call-by-name setting by using a call-by-name analogue of H. As an easy corollary, one can derive Ehrhard’s result that any finite SR functional is definable relative to some SR functional of type level 2. Specifically, let H_{0} ⊑ H_{1} ⊑ … be the sequence of finite approximations to H induced by the standard sequence of finite retractions ρ_{0} ⊑ ρ_{1} ⊑ … on type \overline{2} (see Section 8.1). Any finite SR functional of any type is PCF-definable from H and hence from some H_{i}; but from the definition of ρ_{i} it is clear that H_{i} is itself definable from an element of type level 2. (See also Remark 9.23(ii) below.)

(ii) It follows from the proof of the above theorem that, in the presence of H, one only needs the PCF fixed point operator μx^{σ} up to and including type \overline{2} in order to define all effective SR functionals. (It is easy to see that the fixpoint operator for the type ρ in the proof of Proposition 9.2 may be defined from that for \overline{2}.) An analogous result for PCF with parallel features was pointed out in [45].

9.2 The language PCF+H

Let us now extend the language PCF by adding a new constant H : \overline{2} → \overline{3}. We can give a denotational semantics for the language PCF+H in Mod(B) simply by adding the clause [H]^{Γ} = η(η ∘ H) to the definition of [−]^{Γ}. We can then rephrase Theorem 9.3 as follows: every effective SR functional is definable in PCF+H.

Does the language PCF+H have an operational semantics? At present we do not have a palatable way to give a semantics using structural operational rules. (One particular problem is to see how to deal correctly with terms involving recursive calls to H.) However, one can give an “operational semantics” in a rather abstract sense, by specifying a way in which terms of PCF+H may be “compiled” to elements of B, which we can regard as a kind of abstract machine for which we already have an operational semantics. In particular, our denotational semantics of PCF+H suggests a way of mapping each term M to a particular choice of realizer for [M]. We can think of this mapping as a translation from PCF+H into the untyped setting of B.

Let us indicate one way to do this explicitly. Let K, S, Y be new constantsymbols. Given any closed term M of PCF+H, we first translate M into a term \overline{M} into a term of combinatory PCF+H, in which the terms are built up from the constants 0, 1, 2, …, succ, pred, cond, K, S, Y, H using application (subject to typing constraints). Specifically, \overline{M} be obtained from M as follows:

• First replace each subterm μx^{σ}.N by Y(λx^{σ}.N).

• Then replace each subterm λx^{σ}.N by its standard Curry translation into combinatory logic, working from innermost subterms outwards.

It is easy to give a denotational semantics [−] for (type-decorated) combinatory terms so that [\overline{M}] = [M].

We may now change our perspective and regard \overline{M} as an expression in an untyped language of combinators. Indeed, each of the above combinatory constants C has a denotation ≪ C ≫∈ B_{eff}. For C = 0, 1, 2, …, succ, pred, cond, H we simply take ≪ C ≫ to be some realizer for the corresponding element in Mod(B_{eff}); we also take ≪ K ≫= k, ≪ P S ≫= s, ≪ Y ≫= y. We can extend ≪ − ≫ to arbitrary closed combinatory terms simply by taking ≪ MN ≫ = ≪ M ≫ • ≪ N ≫. Since we have an operational definition of the operation • (e.g. a simple adaptation of Proposition 9.2(i) gives a definition of • in PCF), we have a kind of “operational semantics” for this untyped combinatory language, and hence for PCF+H.

If M is a closed term of PCF+H, we define ≪ M ≫=≪ \overline{M} ≫. We now define a big-step evaluation relation ⇓ for closed PCF+H terms of type \overline{0} by

M ⇓ n iff ≪ M ≫ (0) = n.

We may also define a unary termination predicate ⇓ for terms of any type σ by

M ⇓ iff ≪ M ≫ (0) ↓ .

The following facts are easily verified:

Theorem 9.5 (Adequacy for PCF+H) In both the full and effective models, (i) For any closed PCF+H term M : \overline{0} we have M ⇓ n iff [M] = n. (ii) For any closed term M : σ we have M ⇓ iff [M] ∈ [[ σ]] (that is, [M] ≠ ⊥).

Proof It is clear that for any combinatory term M, ≪ M ≫ is a realizer for [M] in both models. Hence the same holds for any PCF+H term M. But r ∈ B realizes n ∈ [\overline{0}] iff r(0) = n; hence [M] = n iff ≪ M ≫ (0) = n. For (ii), just recall that [M] = [[ σ]]_{⊥}, and from the standard description of lifting given in Section 10 we have that for any x ∈ X_{⊥} and r ∈ ∥x∥_{X_{⊥}} we have x ∈ X iff r(0) ↓. □

Remark 9.6 A rather more concrete way to specify an operational semantics for PCF+H might be to give a translation to a language such as PCF+catch [12] or μPCF [42], for which a structural operational semantics had already been given. Essentially this would amount to giving an implementation of H in the target language.

From the evaluation relation for PCF+H we may define a notion of observational equivalence for closed terms of the same type as usual: M ≈ N if for all contexts C[−] : \overline{0} we have C[M] ⇓ n ⇔ C[N] ⇓ n. The following results are now straightforward:

Theorem 9.7 (Full abstraction for PCF+H) For closed terms M, N : σ the following are equivalent:

(i) M ≈ N;

(ii) [M]_{eff} = [N]_{eff};

(iii) [M]_{full} = [N]_{full}.

Proof (i) ⇒ (ii): Suppose σ = σ_{1} → ⋯ → σ_{r} → \overline{0} (r ≥ 0) and M ≈ N. Given any x_{1} ∈ [[ σ_{1} ]]_{eff}, …, x_{r} ∈ [[ σ_{r}]]_{eff}, by universality we may take terms P_{1}, …, P_{r} such that [P_{i}]_{eff} = x_{i}; then MP_{1} … P_{r} = NP_{1} … P_{r} and so [M]_{eff}x_{1} … x_{r} = [N]_{eff}x_{1} … x_{r}. Since Mod(B_{eff}) is well-pointed, this implies [M]_{eff} = [N]_{eff}.

(ii) ⇒ (iii): For σ = \overline{2} the result is easy: if [M]_{eff} = [N]_{eff} then MP ≈ NP whenever P denotes a finite function; hence [M]_{full}(f) = [N]_{full}(f) for all finite f, which clearly implies [M]_{full} = [N]_{full}.

Now consider an arbitrary type σ. Let I_{σ} : σ → \overline{2} and J_{σ} : \overline{2} → σ be terms of PCF+H that denote the two halves of the canonical retraction [[ σ]] ⊲ [[ 2 ]] uniformly in both the full and effective models. Suppose [M]_{eff} = [N]_{eff}; then [I_{σ}M]_{eff} = [I_{σ}N]_{eff}, so [I_{σ}M]_{full} = [I_{σ}N]_{full} by the above, and so [J_{σ}(I_{σ}M)]_{full} = [J_{σ}(I_{σ}N)]_{full}. There are now two cases. If [M]_{eff} = ⊥ then ¬M ⇓ and so [M]_{full} = ⊥, and similarly for N; hence [M]_{full} = [N]_{full}. Otherwise we have [M]_{full} ∈ [[ σ]] and so [J_{σ}(I_{σ}M)]_{full} = [M]_{full}, and similarly for N, so again [M]_{full} = [N]_{full}.

(iii) ⇒ (i) is easy by the adequacy of [−]_{full}. □

One immediate consequence of full abstraction is the equational context lemma for PCF+H:

Proposition 9.8 (Context Lemma) For closed PCF+H terms M, N : σ = σ_{1} → ⋯ → σ_{r} → \overline{0}, we have M ≈ N iff for all closed P_{1} : σ_{1}, …, P_{r} : σ_{r}, MP_{1} … P_{r} = NP_{1} … P_{r}. □

Note however that the inequational version of the Context Lemma fails, because the observational ordering coincides with the stable order rather than the pointwise one.

Another corollary is that the type structure of effective SR functionals can be characterized as the term model for PCF+H. Specifically, suppose we have defined the syntax and operational semantics of PCF+H, and let ≈ be the notion of observational equivalence defined as above. For each type σ, let T^{σ} be the set of values (i.e. numerals or λ-abstractions) of PCF+H modulo ≈, and let · : T^{σ→τ} × T^{σ} ⇀ T^{τ} be the operation induced by juxtaposition. Then it is immediate from Theorems 9.3 and 9.7 that T ≅ R_{V,eff}. This characterization gives a genuinely new insight into the effective SR functionals; in particular we may now deduce the following pleasing recursion-theoretic property, which is not obvious from any of the previous characterizations:

Theorem 9.9 The type structure R_{V,eff} is effective in the following strong sense: there are total enumerations ϵ^{σ} of the set R_{V,eff}^{σ} (that is, surjective total functions N → R_{V,eff}^{σ}) and partial recursive functions φ_{στ} : N × N ⇀ N such that for all σ, τ, m, n we have

\begin{aligned}φ_{στ}(m, n) ↓ & ⟹ & ϵ^{σ→τ}(m) · ϵ^{σ}(n) = ϵ^{τ}(φ_{στ}(m, n)), \\ φ_{στ}(m, n) ↑ & ⟹ & ϵ^{σ→τ}(m) · ϵ^{σ}(n) ↑ . \end{aligned}

Proof For each type σ let ϵ^{σ} be induced by an effective surjective coding ⌈−⌉^{σ} of the (decidable) set of PCF+H values of type σ, via the bijection T^{σ} ≅ R_{v,eff}^{σ}. We wish to construct φ_{στ} such that, for all values M : σ → τ, N : σ,

• if MN ⇓ then φ_{στ}(⌈M⌉^{σ→τ}, ⌈N⌉^{σ}) = ⌈P ⌉^{τ} for some value P : τ such that

MN ≈ P;
• if ¬MN ⇓ then φ_{στ}(⌈M⌉^{σ→τ}, ⌈N⌉^{σ}) ↑.

There are two cases. If τ = \overline{0} then let φ_{στ} be the function which given ⌈M⌉^{σ→τ} and ⌈N⌉^{σ} returns ⌈n⌉\overline{0} if ≪ MN ≫ (0) = n, and diverges if ≪ MN ≫ (0) ↑. Clearly φ_{στ} is partial recursive and has the required properties. If τ = τ_{1} → τ_{2}, let φ_{στ} be the function which given ⌈M⌉^{σ→τ}, ⌈N⌉^{σ} returns ⌈λx^{τ_{1}}.MNx⌉^{τ} if ≪ MN ≫ (0) ↓, and diverges otherwise. Again this clearly has the required properties. □

We can also now read off the following fact, whose proof (essentially) we have been deferring since Section 3.2:

Theorem 9.10 R_{V,eff} is a substructure of R_{V}, i.e., there are inclusions R_{V,eff}^{σ} ↪ R_{V}^{σ} that commute with the application operations.

Proof Immediate from the fact that R_{V,eff} ≅ T and the values of PCF+H admit a fully abstract interpretation in R_{V}. □

Remarks 9.11 (i) The situation of the above theorem is typical for notions of higher-type partial functional: the computable objects obtained hereditarily as those that act on computable arguments can just as well be seen as acting on arbitrary continuous arguments. (For instance, the effective analogue of the Scott-continuous functionals yields a substructure of the full Scott-continuous type structure.) The situation is radically different for (hereditarily) total notions of computability: not all effective total type 2 operations on the total recursive functions can be extended to an effective total operation on arbitrary total functions (see e.g. [46]).

(ii) All the above results of course go through for the call-by-name SR functionals, using the call-by-name analogue of H.

(iii) Our general impression is that the existence of a universal SR functional is interesting, but the particular functional H is not. For both conceptual and practical reasons (cf. Remark 7.13), it would be very interesting if one could find a simpler functional with the same universality property. We show below that there can be no universal functional of an essentially simpler type than H, but it is open whether there is a universal functional of lower computational complexity than H.

9.3 Degrees of expressivity

Next we consider some effective SR functionals other than H. There is clearly a sense in which some SR functionals are more expressive than others, and indeed there is a structure of degrees of expressivity, analogous to the degrees of parallelism in the Scott model [49]. These ideas are made precise as follows. We will write PCF_{N} for the standard call-by-name version of PCF (as in [45]), and PCF_{V} for the call-by-value version described above. For simplicity, we will restrict our attention to degrees of effective SR functionals, and so for the rest of this section we will write R_{N}, R_{V} in place of R_{N,eff}, R_{V,eff}.

Definition 9.12 (i) Let |R_{X}| = ⨆ R_{X}^{σ}, where X is either N or V. Given f, g ∈ |R_{X}|, we write f ⪯ g if there is an element m ∈ R_{X}^{τ→σ}, definable in PCF_{X}, such that m · g = f. We write f ∼ g if both f ⪯ g and g ⪯ f.

(ii) A degree is an equivalence class for ∼; we write d_{X}(f) for the degree containing f. The partial order on degrees induced by ⪯ is also written as ⪯.

Our first observation is that degrees in R_{N} can be correlated with those in R_{V}, so that we really have just one universe of degrees. For each type σ we have types σ̂, σ̃ and standard retractions (δ^{σ}, ϵ^{σ}) : [[ σ]]_{N} ⊲ [[ σ̂]]_{V} and (ζ^{σ}, ξ^{σ}) : [[ σ]]_{V} ⊲ [[ σ̃]]_{N} in Mod(B_{eff}), as in [31, Chapter 6]. Roughly speaking, these retractions have the property that all possible composites of type [[ ρ]]_{N} → [[ ρ′]]_{N} are definable in PCF_{N}, and similarly for V (see [31] for details).

Given f ∈ R_{N}^{σ} and g ∈ R_{V}^{τ}, we say f ⪯ g if δ^{σ}(f) ⪯ g, or equivalently if f ⪯ ζ^{τ}(g). Likewise, g ⪯ f if ζ^{τ}(g) ⪯ f, or equivalently if f ⪯ δ^{σ}(g). We say f ∼ g ∼ f if both f ⪯ g and g ⪯ f. With these definitions, ⪯ becomes a preorder on the whole of |R| = |R_{N}| ⊔ |R_{V} |, with ∼ the induced equivalence relation. For f ∈ |R_{X}|, we write d(f) for the ∼-equivalence class of f in |R|. Clearly the poset of degrees in |R| is isomorphic to the poset of degrees on |R_{X}|, where X is either N or V. Henceforth we will freely mix call-by-name and call-by-value functionals in our discussion, using whichever seems most convenient.

The smallest degree (with respect to ⪯) is the degree d(0) of all PCF-definable functionals; the largest degree is d(H). The structure of the poset of degrees is probably extremely complicated, and in this paper we will do no more than consider a few examples.

An example of a degree strictly between these is the degree of the functional F ∈ R\overline{2} ; N defined in Remark 3.7(ii) (see also the Introduction). The fact that d(F) is strictly above d(0) is immediate from the pointwise non-monotonicity of F; the fact that d(F) is strictly below d(H) (i.e. that H is not definable from F) will be shown below.

Another SR functional that seems particularly interesting from the point of view of programming applications is the modulus functional M : R_{V}^{\overline{2}→\overline{1}→\overline{0}} specified as follows:

• If G·f ∈ N then M ·G·f = ⌈graph f_{0}⌉, where f_{0} is the unique smallest finite subfunction of f such that G · f_{0} = n, and ⌈graph f_{0}⌉ is the normalized graph of f_{0} (e.g. a sorted non-repetitive list of ordered pairs), coded as a natural number.

• If G · f = ⊥ then M · G · f = ⊥.

It is easy to check that M is indeed an effective call-by-value SR functional of the specified type. The following observation is due to Alex Simpson:

Proposition 9.13 d(M) = d(F).

Proof Let F′ ∈ R\overline{3} ; V be the functional

λG\overline{2}. cond (MG(λx\overline{0}.0) = ⌈∅⌉) 0 1

(we mix syntax and semantics in a semi-formal way). Intuitively F′ is a callby-value analogue of F, and indeed it is easy to see that d(F′) = d(F). Thus d(F) ⪯ d(M). For the converse, we may recover M from F′ as follows. Let conv : \overline{1} → \overline{0} → \overline{0} be the function λp\overline{1}. λx\overline{0}. cond (p 0) x x. Let insert : \overline{0} → \overline{0} → \overline{0} → \overline{0} be a function such that

insert x y ⌈γ⌉ = ⌈γ ∪ (x ↦ y)⌉

for all natural numbers x, y and graphs γ. Next, let M′ : \overline{2} → \overline{1} → \overline{0} → \overline{0} → \overline{0} be the function

λG\overline{2}.λf\overline{1}.μm^{\overline{0}→\overline{0}→\overline{0}}.λn\overline{0}.λg\overline{0}.
cond F (λp\overline{1}. G(λx\overline{0}. cond (x < n) (f x)(conv (p 0)(f x))))
g
cond F (λp\overline{1}. G(λx\overline{0}. cond (x ≠ n) (f x)(conv (p 0)(f x))))
(m (succ n) g)
(m (succ n) (insert n (f n) g).

Finally, take M = λGf. M′ G f 0 ⌈∅⌉. We leave it to the reader to check that M is indeed the modulus functional. □

More examples of degrees will appear in the next paragraph. A few further examples, and some discussion of their potential programming applications, are given in an electronically available Standard ML source file [33].

9.4 Types and universal functionals

We now ask what types a universal SR functional may have. Recall that H has call-by-value type \overline{2} → \overline{3}. Since it is easy to construct a retraction \overline{2} → \overline{3} ⊲ \overline{3}, we certainly have a universal functional of call-by-value type \overline{3}. It is natural to ask whether there is a universal functional of any “lower” type, in either call-by-name or call-by-value PCF. We only need consider call-by-name types of the form

(\overline{0}^{r_{1}} → \overline{0}) → ⋯ → (\overline{0}^{r_{n}} → \overline{0}) → \overline{0},

since all other types below \overline{3} are even lower than these. But any such type is a PCF-definable retract of some call-by-name type ρ_{r} ≡ (\overline{0}^{r} → \overline{0}) → \overline{0}, so it suffices to consider types ρ_{r}.

We will show, however, that there can be no such universal functional, and indeed the expressive power of the set of functionals of type ρ_{r} increases strictly with r. To this end we will exhibit, for each r, a denotational model of PCF that contains all the SR functionals of type ρ_{r} and below, but lacks certain functionals of type ρ_{r+1}.

Recall from [15] that HC is a full sub-CCC of the category of dI-domains with coherence, defined as follows.

Definition 9.14 (i) A dI-domain is an ω-algebraic bounded-complete dcpo X such that

• for all x, y, z ∈ X where y, z are bounded, x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z);

• every compact element has only finitely many lower bounds.

We write dI for the category of dI-domains and stable continuous functions.

(ii) A coherence on a dI-domain X is a family C of finite non-empty subsets of X, such that

• for all x ∈ X, {x} ∈ C;

• if A ∈ C and B ⊆_{fin} X is below A in the Egli-Milner order (that is, ∀x ∈ A.∃y ∈ B. x ≤ y and ∀y ∈ B.∃x ∈ A. x ≤ y), then B ∈ C.

• if D_{1}, …, D_{n} ⊆ X are directed and for all x_{1} ∈ D_{1}, …, x_{n} ∈ D_{n} we have {x_{1}, …, x_{n}} ∈ C, then {⨆ D_{1}, …, ⨆ D_{n}} ∈ C.

A dI-domain with coherence is a dI-domain X equipped with a coherence C(X); elements of C(X) are called coherent sets. A strongly stable function between dI-domains with coherence is a continuous function that respects coherent sets and their meets. We write dIC for the category of dI-domains with coherence and strongly stable functions.

(iii) If C is a coherence on X, a subset B ⊆ C is a basis for C if C is the coherence generated by B (that is, the smallest coherence on X containing B).

In a dI-domain with coherence, any bounded finite non-empty set is coherent. It follows that all strongly stable functions are stable; thus dIC is a (non-full) subcategory of dI.

The embedding of HC in dIC can be immediately read off from Definitions 5.5 and 5.6. We will write N_{⊥} for the object of dIC corresponding to N in HC, and [[ −]] for the interpretation of PCF types in dIC. Explicit definitions of products and exponentials in dIC can be found e.g. in [10].

We now define the models we want as full subcategories of dIC. We suppose r is any positive integer.

Definition 9.15 (i) Let X be a dI-domain with coherence. A set A ∈ C(X) is basic r-coherent if there exist a coherent set B ∈ C(N_{⊥}^{r}) and a strongly stable function f : N_{⊥}^{r} → X such that A = f(B). We say X is a dI-domain with r-coherence if the basic r-coherent sets form a basis for C(X). We write dIC_{r} for the category of dI-domains with r-coherence and strongly stable functions.

It turns out that both dIC_{1} and dIC_{2} are equivalent to dI, though we shall not need this below. We will show that dIC_{r} is a CCC, but (crucially) the inclusion dIC_{r} ↪ dIC does not preserve the CC structure. The following simple observations will be useful:

Lemma 9.16 Suppose X, Y are dI-domains, B a basis for C(X), and f : X → Y a stable continuous map. If f(A) ∈ C(Y) for all A ∈ B, then f(A) ∈ C(Y) for all A ∈ C(X).

Proof Let D = {A ∈ C(X) | f(A) ∈ C(Y)}. Then B ⊆ D, so to show that D = C(X) it suffices to check that D is a coherence. That D contains all singletons is trivial. If A ∈ D, B ∈ C(X) and B ⊑ A in the Egli-Milner order, then f(B) ⊑ f(A) ∈ C(Y) and so f(B) ∈ C(Y). The closure of D under directed lubs follows easily from the continuity of f. □

Proposition 9.17 The category dIC_{r} has finite products.

Proof The terminal object presents no problem. Given objects X, Y of dIC_{r}, let X × Y be the usual cartesian product of dI-domains, and let C(X × Y) be the coherence generated by the basis

B = {⟨f, g⟩(A) | f : N_{⊥}^{r} → X, g : N_{⊥}^{r} → Y strongly stable, A ∈ C(N_{⊥}^{r})}.

Clearly all the sets in B are then basic r-coherent, so X × Y is a dI-domain with r-coherence. The projection maps obviously respect all the coherent sets in B, so by Lemma 9.16 they respect arbitrary coherent sets. Since they also preserve all existing meets, they are strongly stable.

Now suppose we are given an object Z of dIC_{r} and strongly stable maps f : Z → X, g : Z → Y. We wish to check that the stable and continuous function ⟨f, g⟩ : Z → X × Y is strongly stable. But if A ∈ C(Z) is a basic r-coherent set induced by h : N_{⊥}^{r} → Z then ⟨f, g⟩(A) is a basic r-coherent set induced by ⟨fh, gh⟩. Thus ⟨f, g⟩ respects arbitrary coherent sets by Lemma 9.16. Moreover, it is easy to check that for any A ∈ C(Z) we have ⟨f, g⟩(⋀ A) = ⋀⟨f, g⟩(A). □

Proposition 9.18 The category dIC_{r} has exponentials.

Proof Given objects X, Y of dIC_{r}, let Y^{X} be the set of strongly stable functions X → Y, endowed with the stable ordering; then Y^{X} is a dI-domain by [10, Proposition 14]. Now let C(Y^{X}) be the coherence generated by the basis

B = {(curry f)(A) | f : N_{⊥}^{r} × X → Y strongly stable, A ∈ C(N_{⊥}^{r})},

where N_{⊥}^{r} × X is as given by the previous proposition. Again, all the sets in B are then basic r-coherent, so Y^{X} is a dI-domain with r-coherence.

To see that the evaluation map ϵ : Y^{X} ×X → Y is strongly stable, we compare our object Y^{X} with the exponential W = Y^{X} calculated in dIC (see [10]). We see that Y^{X} and W have the same underlying dI-domain, and B ⊆ C(W) so C(Y^{X}) ⊆ C(W). Since the evaluation map W × X → Y is known to be strongly stable, it follows that ϵ is strongly stable.

Now suppose we are given an object Z of dIC_{r} and a strongly stable map f : Z × X → Y. We wish to check that the stable and continuous function curry f : Z → Y^{X} is strongly stable. But if A ∈ C(Z) is a basic r-coherent set induced by h : N_{⊥}^{r} → Z, then (curry f)(A) is a basic r-coherent set induced by curry (f ∘(h×id)). Thus curry f respects arbitrary coherent sets by Lemma 9.16. Moreover, for any A ∈ C(Z) we have (curry f)(⋀ A) = ⋀(curry f)(A) in W, hence also in Y^{X}. □

Thus dIC_{r} is a cartesian closed category. Moreover, it is easy to see that dIC_{r} contains the dI-domain N_{⊥} with the usual coherence, and that any morphism f : X → X in dIC_{r} has least fixed point ⨆ f^{i}(⊥). It follows in the usual way that dIC_{r} is a model of PCF—that is, there is an adequate interpretation [[ −]]_{r} of call-by-name PCF in dIC_{r}, where [[ \overline{0} ]]_{r} = N_{⊥} and [[ σ → τ ]]_{r} = [[ τ ]]_{r}^{[[ σ]]_{r}} (calculated in dIC_{r}).

Let us write [N_{⊥}^{k}] for the product of k copies of N_{⊥} computed in dIC, and [N_{⊥}^{k}]_{r} for the product computed in dIC_{r}. The following proposition gives a measure of the similarity between the interpretations [[ −]]_{r} and [[ −]].

Proposition 9.19 For any 1 ≤ k ≤ r, (i) the objects [N_{⊥}^{k}]_{r} and [N_{⊥}^{k}] coincide; (ii) the objects [[ \overline{0}^{k} → \overline{0} ]]_{r} and [[ \overline{0}^{k} → \overline{0} ]] have the same underlying dI-domain,

and C([[ \overline{0}^{k} → \overline{0} ]]_{r}) ⊆ C([[ \overline{0}^{k} → \overline{0} ]]); (iii) every element of [[ ρ_{k}]] is also an element of [[ ρ_{k}]]_{r}.

Proof Part (i) follows from the easy observation that in [N_{⊥}^{k}] every coherent set is basic r-coherent. Part (ii) follows from this by comparing exponentials in dIC_{r} and dIC (as in the proof of Proposition 9.18). It is immediate from this that every strongly stable function [[ \overline{0}^{k} → \overline{0} ]] → N_{⊥} is also a strongly stable function [[ \overline{0}^{k} → \overline{0} ]]_{r} → N_{⊥}, which gives (iii). □

We now come to the main point of the exercise: we exhibit an element F_{r} of [[ ρ_{r+1} ]] that is not an element of [[ ρ_{r+1} ]]_{r}. For r ≥ 1 and 1 ≤ i ≤ r, let ϵ_{ri} ∈ N_{⊥}^{r} be the tuple (n − i + 1, …, n − 1, ⊥, 1, …, n − i). Let E_{r} = {ϵ_{r1}, …, ϵ_{rr}}; we call E_{r} the rth Berry set. Recall from [16] that E_{r} is coherent in [N_{⊥}^{r}], but no proper subsets of E_{r} of size greater than 1 are coherent.

Lemma 9.20 Suppose k ≥ 2, and A ⊆ N_{⊥}^{k} is such that E_{k} ⊆ A and E_{k} ⊑ A in the Egli-Milner order. Then A is not basic r-coherent for any r < k.

Proof Suppose for a contradiction this is false for some k and A. Take r minimal such that E_{k} is basic r-coherent; then clearly r > 1. Take B ∈ C(N_{⊥}^{r}) and f : N_{⊥}^{r} → N_{⊥}^{k} strongly stable such that f(B) = A. Let f_{i} = π_{i}∘f : N_{⊥}^{r} → N_{⊥} for 1 ≤ i ≤ k. Since none of the f_{i} are constant functions, each has some sequentiality index 1 ≤ j_{i} ≤ r. So there must be two of the f_{i}, say f_{i_{1}} and f_{i_{2}}, with the same sequentiality index j. Now consider an arbitrary element x = (x_{1}, …, x_{r}) ∈ N_{⊥}^{r}. Then f_{i_{1}}(x) ∈ N if f(x) ≠ ϵ_{ki_{1}}, and similarly for i_{2}; so in any case, we have x_{j} ∈ N. So ⊥ ∉ π_{j}(B), and since π_{j}(B) ∈ C(N_{⊥}), this means π_{j}(B) is a singleton. So by deleting the jth factor in N_{⊥}^{r} we can exhibit A as basic (r − 1)-coherent, contradicting the minimality of r. □

Let us write θ_{ri} : N_{⊥}^{r} → N_{⊥} for the least monotone function such that θ_{ri}(ϵ_{ri}) = 0. Now take ϕ_{r} = θ_{r1} and ψ_{r} the pointwise least upper bound of θ_{r2}, …, θ_{rr}. It is easy to see that both ϕ_{r} and ψ_{r} are PCF-definable, and so are morphisms in dIC and in any dIC_{r′}.

Proposition 9.21 Suppose r ≥ 2.

(i) The set E_{r+1} is coherent in [N_{⊥}^{r+1}]_{r+1} but not in [N_{⊥}^{r+1}]_{r}.

(ii) The elements θ_{(r+1)1}, …, θ_{(r+1)(r+1)} have an upper bound in [[ \overline{0}^{r+1} → \overline{0} ]]_{r} but not in [[ \overline{0}^{r+1} → \overline{0} ]]_{r+1}.

(iii) In [[ ρ_{r+1} ]] and [[ ρ_{r+1} ]]_{r+1}, but not in [[ ρ_{r+1} ]]_{r}, there is a function T_{r+1} such that T_{r+1}(ϕ_{r+1}) = 0 and T_{r+1}(ψ_{r+1}) = 1.

Proof (i) The first claim is immediate since E_{r+1} is coherent in [N_{⊥}^{r+1}], which coincides with [N_{⊥}^{r+1}]_{r+1}. To prove that E_{r+1} is not coherent in [N_{⊥}^{r+1}]_{r}, first note that every directed set in N_{⊥}^{r+1} already contains its lub; thus the first two closure conditions in Definition 9.14(ii) suffice to generate the coherence C([N_{⊥}^{r+1}]_{r}) from the basic r-coherent sets. So if E_{r+1} is coherent in [N_{⊥}^{r+1}]_{r} then we have E_{r+1} ⊑ A in the Egli-Milner order, where A is either a singleton or basic r-coherent. Since r ≥ 2, clearly A cannot be a singleton. But if A is basic r-coherent, by the above lemma we cannot have E_{r+1} ⊆ A. So take i such that ϵ_{(r+1)i} ∉ A; then clearly ⊥ ∉ π_{i}(A). But since π_{i}(A) is coherent and is not a singleton, we have a contradiction.

(ii) Let θ be any upper bound for the θ_{(r+1)i} in the stable order; then θ(E_{r+1}) = \{1, …, r + 1\} is not coherent, so θ is not an element of [[ \overline{0}^{r+1} → \overline{0} ]]_{r+1}. Now let θ_{r+1} be the (pointwise) least upper bound of the θ_{(r+1)i}; we claim that θ_{r+1} : [N_{⊥}^{r+1}]_{r} → N_{⊥} is strongly stable. Suppose A ∈ C([N_{⊥}^{r+1}]_{r}). If ⊥ ∈ θ_{r+1}(A) then θ_{r+1}(A) is automatically coherent and θ_{r+1}(⋀ A) = ⋀ θ_{r+1}(A). Otherwise, we must have ∀x ∈ A.∃y ∈ E_{r+1}. y ≤ x. Let E′ = {y ∈ E_{r+1} | ∃x ∈ A. y ≤ x}; then E′ ⊑ A and so E′ ∈ C([N_{⊥}^{r+1}]_{r}). But E_{r+1} ∉ C([N_{⊥}^{r+1}]_{r}) and no non-singleton proper subset of E_{r+1} is even in C([N_{⊥}^{r+1}]), so E′ is a singleton. It follows that θ_{r+1}(A) is a singleton (and hence coherent), and trivially θ_{r+1}(⋀ A) = ⋀ θ_{r+1}(A).

(iii) In [[ ρ_{r+1} ]] one may define T_{r+1} as follows:

T_{r+1}(f) = \{ \begin{matrix}0 & if ϕ_{r+1} ≤_{s} f, \\ 1 & if ψ_{r+1} ≤_{s} f, \\ ⊥ & otherwise \end{matrix}

This function is well-defined by (ii). To see that it is strongly stable, suppose A ∈ C([[ \overline{0}^{r+1} → \overline{0} ]]). If T_{r+1}(A) is not coherent then we must have T_{r+1}(A) = {0, 1}, so {θ_{(r+1)1}, θ_{(r+1)2}} ⊑ {ϕ, ψ} ⊑ A, so {θ_{(r+1)1}, θ_{(r+1)2}} is coherent, a contradiction. Hence T_{r+1}(A) is coherent, and a simple inspection of cases shows that T_{r+1}(⋀ A) = ⋀ T_{r+1}(A). Thus T_{r+1} ∈ [[ ρ_{r+1} ]], and it follows from Proposition 9.19(iii) that T_{r+1} ∈ [[ ρ_{r+1} ]]_{r+1}.

However, no such function T_{r+1} can exist in [[ ρ_{r+1} ]]_{r}, since ϕ_{r+1}, ψ_{r+1} ≤_{s} θ_{r+1} but 0, 1 have no upper bound in N_{⊥}. □

Note that θ_{3} is the Gustave function, the standard example (due to Berry) of a stable but not sequential function.

We may now read off the following result:

Theorem 9.22 There is no SR functional G of any type ρ_{r} such that all effective SR functionals, or even all finite SR functionals, are PCF-definable relative to G. Proof We show that the SR functional T_{r+1} (which is finite and hence effective) is not PCF-definable from G. Suppose M : ρ_{r} → ρ_{r+1} were a PCF term such that [[ M ]](G) = T_{r+1} in dIC. For each i let N_{i} be a PCF term denoting θ_{(r+1)i}; then [[ M ]](G)([[ N_{i}]]) = i for each i. But the evident logical relation between the PCF types in dIC and dIC_{r} relates G to G, [[ M ]] to [[ M ]]_{r}, and [[ N_{i}]] to [[ N_{i}]]_{r} (using the logical relations lemma). It follows that [[ M ]]_{r}(G) ∈ [[ ρ_{r+1} ]]_{r} fulfils the criteria for T_{r+1}, a contradiction. □

Remarks 9.23 (i) In fact the model dIC_{r} shows that T_{r+1} is not PCF-definable even from the set of all SR functionals of type ρ_{r} or below. This answers negatively a question implicitly posed at the very end of [17].

(ii) A simple corollary of the above theorem is that there is no finite SR functional G of any type whatever such that all the finite SR functionals are PCF-definable from G. For if such a G existed, it would be definable from some finite approximation H_{i} to H arising from the standard sequence of finite retractions; but each such H_{i} has the same degree as some functional of type ρ_{r}.

(iii) It is an easy exercise to show that each T_{r+1} is PCF-definable from T_{r+2}. We therefore have a strictly ascending chain of degrees d(T_{2}) ≺ d(T_{3}) ≺ . . .. Note that T_{2} is easily definable from the modulus functional, so d(T_{2}) = d(F) by Proposition 9.13. This shows that d(F) is strictly below d(H).

10 Synthetic domain theory

In this section we revisit our models Mod(B_{full}) and Mod(B_{eff}) from the standpoint of synthetic domain theory (see e.g. [19, 35, 48, 52]). We will see that at least two existing versions of synthetic domain theory work out very well in these models; we also point out some ways in which our models are rather different in flavour from most of those previously considered.

10.1 Well-complete and replete objects

Consider again the lift functor L = −_{⊥} on Mod(B) (where B is B_{full} or B_{eff}). As observed in Section 3.1, it is easy to make this into a monad, i.e. to give natural transformations η : id → L and μ : L^{2} → L satisfying the monad laws. Let Σ be the object 1_{⊥}, and let ⊤ be the morphism η_{1} : 1 → Σ. Pullbacks of ⊤ along morphisms X → Σ are called Σ-monos. It is easy to see that (Σ, ⊤) is a dominance on Mod(B)—that is, any Σ-mono Y ↣ X is the pullback of ⊤ along a unique classifying map X → Σ, and Σ-monos are closed under composition. (For the latter claim, we use the fact that the “generic” composite of Σ-monos ⊤_{⊥} ∘ ⊤ is classified by μ_{1}.) Indeed, in the terminology of [35], (Σ, ⊤) arises from a divergence on B, namely the singleton set {⊥}.

For general reasons, the functor ⊥ has both an initial algebra ω and a final coalgebra \overline{ω} (see e.g. [35].) In the case of Mod(B), the following concrete presentations of ω and \overline{ω} are especially convenient. For each n ∈ N define q_{n} ∈ B by q_{n}(m) = 0 if m < n, q_{n}(m) = ⊥ if m ≥ n; and take q_{∞} = λm.0. The objects ω, \overline{ω} may then be defined by

\begin{matrix}|ω| = N, & ∥n∥_{ω} = \{q_{n}\}, \\ |\overline{ω}| = N, & ∥n∥\overline{ω} = \{q_{n}\}, & ∥∞∥ = \{q_{∞}\}. \end{matrix}

The structure map ω_{⊥} → ω for the initial lift algebra is the isomorphism that just interchanges the points 0 and 1, and likewise for the final coalgebra. Moreover, the unique algebra map ι : ω → \overline{ω} is the evident inclusion. In all versions synthetic domain theory, the morphism ι (or something very similar) plays a fundamental role in formulating an appropriate notion of “chain-completeness” for predomains.

We will briefly consider two possible such categories of predomains in Mod(B): the well-complete objects introduced by Longley and Simpson [35], and the replete objects considered by Hyland [19] and Taylor [55]. We will show that both these notions yield good categories of predomains. First recall the following definition from [35]:

Definition 10.1 (Well-completeness) An object X is complete if X^{ι} : X\overline{ω} → X^{ω} is an isomorphism. An object X is well-complete if X_{⊥} is complete.

Actually the notions of complete and well-complete object coincide in Mod(B) (as they do in many other natural models), though we will not use this fact. The following proposition shows that strong completeness axiom of [35] holds in Mod(B):

Proposition 10.2 The object N in Mod(B) is well-complete.

Proof Suppose c is any morphism ω → N_{⊥}, realized by r. Then each r • q_{n} realizes some element of N, and r • q_{∞} = ⨆ r • q_{n}. But the set of realizers for elements of N_{⊥} is (trivially) closed under lubs, and so r • q_{∞} also realizes some element of N. Thus r realizes a (necessarily unique) morphism \overline{ω} → N_{⊥} extending c. So N_{⊥}^{ι} : N\overline{ω} ; ⊥ → N_{⊥}^{ω} is an isomorphism whose inverse is realized by λ^{∗}r.r. □

This shows that we are in the situation described for general realizability models in [31, 35], and indeed that all the axioms appearing in [48] or in [52] are true in Mod(B). This means that all the machinery of well-complete objects is available to us. In particular:

Theorem 10.3 (i) The well-complete objects in Mod(B) are closed under finite limits, dependent products (including exponentials), finite sums, lifting and retracts, and contain the natural number object.

(ii) For any well-complete object X equipped with a (necessarily unique) lift monad algebra structure α : X_{⊥} → X, every morphism X → X has a fixed point, and indeed there is a morphism y_{X} : X^{X} → X that computes it. Furthermore, for any f : X → X and any t : X → Σ, we have t(y_{X}f) = ⊤ iff t(f^{n}(α⊥)) = ⊤ for some n.

By the results of [31, Chapter 6], we also have adequate interpretations of call-by-name and call-by-value PCF. Moreover, the well-complete objects form a small complete category (i.e. an impredicative universe), so we can also interpret much more powerful type theories (see e.g. [18]).

Next we turn our attention to the replete objects in Mod(B). There are many equivalent definitions of repleteness (see e.g. [47]); here we recall a characterization due to Taylor [19].

Definition 10.4 (Repleteness) A morphism e : X → Z is called Σ-epi if Σ^{e} : Σ^{Z} → Σ^{X} is mono. A morphism f : X ↣ Y is called an extremal mono if, for any mono m and Σ-epi e with f = m ∘ e, e is an isomorphism. An object X is replete if the canonical map ϵ_{X} : X → Σ^{Σ^{X}} is an extremal mono.

In the situation of [35] it is always the case that every replete object is wellcomplete; in fact, one can regard the well-complete objects as the largest good category of predomains, and the replete objects as the smallest.

Proposition 10.5 The object N in Mod(B) is replete.

Proof Consider the canonical map ϵ : N → Σ^{Σ^{N}}. We first show that this is a regular mono—that is, there is a realizer p such that a ∈ ∥ϵn∥ implies p • a ∈ ∥n∥. For convenience we work with the following presentations of N, Σ and Σ^{N}: ∥n∥_{N} = {r_{n}} where r_{n}(0) = n, r_{n}(m + 1) = ⊥; ∥⊤∥_{Σ} = {r_{0}} and ∥⊥∥_{Σ} = {λm.⊥}; and for t : |N| → |Σ| we have ∥t∥_{Σ^{N}} = {r_{t}}, where r_{t}n = 0 if tn = ⊤, r_{t}n = ⊥ if tn = ⊥. In addition, we consider as realizers for f ∈ |Σ^{Σ^{N}} | all •-irredundant realizers for f considered as a morphism Σ^{N} → Σ (with respect to the above presentations).

Relative to these presentations, any realizer a for any ϵn : Σ^{N} → Σ clearly satisfies a⟨0⟩ =?n; From this, it is easy to construct the required realizer p that extracts n from a. So ϵ is a regular mono; in particular, it is maximal among subobjects of Σ^{Σ^{N}} whose points are exactly the elements ϵn.

To see that ϵ is an extremal mono, note first that if a is a •-irredundant realizer for any f : Σ^{N} → Σ, then f = ϵn iff a⟨0⟩ =?n and a⟨0, 0⟩ =!0. Using this, it is easy to construct a morphism C : Σ^{Σ^{N}} → Σ such that Cf is ⊤ if f = ϵn for some n, and Cf = ⊥ otherwise. Now suppose ϵ_{N} factors as N →^{e} Z →^{m} Σ^{Σ^{N}} where m is mono and e is Σ-epi. Clearly the maps C ∘ m and λz.⊤ : Z → Σ both induce the constant map λn.⊤ : N → Σ, and so C ∘ m = λz.⊤ since e is Σ-epi. Thus the image of m contains only the points ϵn, and so e is an isomorphism by the above. □

For general reasons (see [48]) we can now deduce the analogue of Theorem 10.3 for the replete objects. So the replete objects also suffice for interpreting PCF and indeed much richer languages. We do not know whether there are objects of Mod(B) that are well-complete but not replete.

Remark 10.6 Clearly the category K of Section 8.2 lies within the category of replete objects; hence so does the image of E : SSeqFun → Mod(B). Likewise, we expect that some good subcategory of HC embeds well into the replete objects.

10.2 The Σ-order

We now consider another basic notion from synthetic domain theory: the Σ-order (or intrinsic order) on objects. We shall see that in Mod(B) this coincides exactly with the stable order (at least for finite types). This comes as no surprise after the results of Section 5, but it means that the model Mod(B) has a completely different flavour from any of the models considered e.g. in [35], in which the Σ-order (seemingly) coincides with the pointwise order.

For any modest set X, the (external) Σ-preorder ⪯_{X} on |X| is defined by

x ⪯_{X} y ⟺ ∀t : X → Σ. (tx = ⊤ ⟹ ty = ⊤).

Clearly all morphisms between modest sets preserve the Σ-preorder. It is easy to see that in Mod(B) the Σ-preorder on N_{⊥} coincides with the usual partial order; and hence that for all finite types over N_{⊥} the Σ-preorder is a partial order. Since Σ is a retract of N_{⊥}, the definition of the Σ-order on the finite types R^{σ} can be formulated as follows:

x ⪯_{σ} y ⟺ ∀t ∈ R^{σ→\overline{0}}. (t · x = 0 ⟹ t · y = 0).

This emphasizes that the Σ-order is intrinsic to the type structure R and not dependent on any particular model for R such as the category Mod(B).

Proposition 10.7 For x, y ∈ R_{full}^{σ}, the following are equivalent:

(i) x ⪯_{σ} y.

(ii) x ⊑_{σ} y in the sense of Proposition 5.13.

(iii) x, y are path-related, i.e. there exists p ∈ R^{\overline{0}→σ} with p · ⊥ = x and p · ⊥ = y.

Proof For (i) ⇒ (ii), it seems easiest to work with the characterization of ⊑_{σ} given by the hypercoherence model (see Proposition 5.13). For each atom a in the underlying set of the hypercoherence X = [[ σ]]_{HC}, let t_{a} : X → N be the strongly stable function whose trace is {({a}, 0)}; then for z ∈ D(X) we have t_{a}(z) = 0 if a ∈ z and t_{a}(z) = ⊥ otherwise. So if x ⪯_{σ} y then (regarding x, y as states of X), for each a we have

a ∈ x ⟹ t_{a}(x) = 0 ⟹ t_{a}(y) = 0 ⟹ a ∈ y.

Thus x ⊆ y, and so x ⊑_{σ} y by Proposition 5.13.

(ii) ⇒ (iii): Suppose x ⊑_{σ} y, i.e. there exist realizers a ∈ ∥x∥, b ∈ ∥y∥ with a ⊑ b. It is trivial to construct a realizer r such that r •(λn.⊥) = a and r •r_{n} = b for any n (where r_{n}(0) = n and r_{n}(m + 1) = ⊥ as above). Clearly r realizes a morphism p with the required properties.

(iii) ⇒ (i): Given p ∈ R^{\overline{0}→Σ} as above and t ∈ R^{σ→\overline{0}}, if t · x = t · (p · ⊥) = 0 then t · y = t · (p · ⊥) = 0 since the map N_{⊥} → N_{⊥} given by t ∘ p is monotone. □

Note that the implication (ii) ⇒ (iii) fails in the effective case: if x, y ∈ R\overline{1} correspond to two partial recursive functions such that x ⊆ y but dom y − dom x is not r.e., there is no effective realizer for an element p with the required properties.

It follows from the above that the Σ-order on Σ^{Σ} is given by λx.⊥ ⪯ λx.x, λx.⊥ ⪯ λx.⊤. Indeed, it is amusing to note that the functional F described in the Introduction is actually an isomorphism Σ^{Σ} ≅ 2_{⊥} in Mod(B). Likewise, one can easily show that Σ^{ω} ≅ Σ\overline{ω} ≅ N_{⊥} in Mod(B).

Remark 10.8 The model Mod(B_{2}) also fits well with the theory of well-complete objects: the divergence {⊥} gives rise to a dominance in Mod(B_{2}) satisfying the Strong Completeness Axiom. As mentioned in Section 8.2, Mod(B_{2}) also has the potential advantage that most of the objects of interest are projective. It would be interesting to know whether the modified realizability model mRT(B) of Section 3.3 and the presheaf model [M^{op}, Set] in Section 6 also fit smoothly into some version of synthetic domain theory.

11 Notions of higher-type computability

We end the main body of the paper by comparing the SR functionals with other known type structures. The line of thought we describe here is part of a general investigation of notions of computability at higher types, which will be developed more fully in a forthcoming survey paper [30].

Our motivating philosophy is as follows: since it is not clear a priori what should be meant by the “computable” functionals of higher types, we take a step back and consider the space of all possible notions of higher-type computability. More precisely, we define a general concept of “class of computable functionals”, in such a way that any reasonable notion of higher-type computability can be expected to provide an example of such a class. Within this abstract framework, we can then collect particular notions of higher-type computability, and ask how they are related.

11.1 General definitions

Here we shall restrict attention to notions of (hereditarily) partial computable functional. In general, a class of partial higher-type functionals is embodied by a partial type structure, as in Definition 3.6(i) (see also Section 7.1). For definiteness, we will concentrate here on the call-by-name notion of type structure, though (as usual) this choice does not matter much. We repeat the definition here for convenience.

Definition 11.1 A partial type structure (PTS) T consists of

• a set T^{σ} for each type σ, where T \overline{0} = N_{⊥},
• for each σ, τ a total “application” function ·_{στ} : T^{σ→τ} × T^{σ} → T^{τ}.

We say T is extensional (or is an EPTS) if, for all types σ, τ and all f, g ∈ T^{σ→τ},

(∀x ∈ T^{σ}. f · x = g · x) ⟹ f = g.

It seems clear that any reasonable notion of computable partial functional will give rise to a PTS T in this sense, since we expect computable functionals to be closed under application. We would also expect T to be extensional, since the elements of T^{σ→τ} are just functions.^{5} Moreover, if T consists of computable partial functions, we expect it to be effective in some way. We can build a notion of effectivity onto the above definition as follows.

Definition 11.2 An effective structure on a PTS T assigns to each element f of each T^{σ} a non-empty set ∥f∥_{σ} ⊆ N of realizers for f, such that:

• for each σ, τ there is a partial recursive function φ_{στ} : N × N ⇀ N such that, for all f ∈ T^{σ→τ}, x ∈ T^{σ}, m, n ∈ N we have

m ∈ ∥f∥_{σ→τ} ∧ n ∈ ∥x∥_{σ} ⟹ φ(m, n) ∈ ∥f · x∥_{τ};

5This is a slight oversimplification: if the domain of definition of the functions in T^{σ→τ} were larger than T^{σ}, one could imagine distinct elements f, g ∈ T^{σ→τ} that had the same restriction to σ. We will discuss the issue of extensionality in more detail in [30].

• there is a partial recursive function ψ : N ⇀ N such that for all n ∈ N we have

ψ(n) ↓ ⟹ n ∈ ∥ψ(n)∥\overline{0}, ψ(n) ↑ ⟹ n ∈ ∥⊥∥\overline{0}.

A effective PTS is a PTS that admits at least one effective structure.

The reader may recognize that a PTS with effective structure is nothing other than a certain kind of PTS within the realizability model on the partial combinatory algebra K_{1}. The above definition is designed to be as liberal as possible so as to admit any conceivable notion of computable functional—for instance, there is no requirement that the set ⋃_{x∈T^{σ}} ∥x∥_{σ} of realizers for objects of type σ be recursively enumerable. Indeed, it seems reasonable to propose the following informal hypothesis:

Thesis 11.3 Any reasonable notion of computable hereditarily partial functional at higher types (henceforth “notion of computability”) is embodied in an effective extensional PTS.

(Of course, there are also many silly effective EPTSs that do not embody a reasonable notion of computability.) The above claim rests on Church’s Thesis and on the intuitive idea that “effective” objects of any kind are ultimately representable by natural numbers. It also depends on the supposition, true in all known cases of interest, that any reasonable class of functionals (for example, a class given as a call-by-value type structure) can be embodied in an “equivalent” call-by-name type structure. In the absence of any evidence to the contrary, we adopt the above thesis as a working hypothesis.

Given two EPTSs, it is natural to ask when one of them in some sense “contains” the other. Again, we seek the most liberal notion of containment that seems reasonable—for instance, the obvious definition of homomorphic inclusion, and even that of logical relation, seem too strong for our purposes. We propose the following notion:

Definition 11.4 Let T, U be EPTSs. A simulation s : T → U consists of a total relation s^{σ} : T^{σ} ⟶^{|} U^{σ} for each type σ, such that

• s\overline{0} is the identity relation on N_{⊥};
• for any f ∈ T^{σ→τ}, g ∈ U^{σ→τ}, x ∈ T^{σ}, y ∈ U^{σ} we have
s^{σ→τ}(f, g) ∧ s^{σ}(x, y) ⟹ s^{τ}(f · x, g · y).

We write T ≤ U if there exists a simulation s : T → U.

Thesis 11.5 If U embodies a notion of computability that includes or subsumes the notion embodied by T in any reasonable sense, then T ≤ U.

The intuition is that for any element x of T, there is at least one element y of U that represents or “simulates” x. Note that T ≤ U iff T arises as a homomorphic subquotient of U (where homomorphisms are required to be the identity on type \overline{0}).

It is clear that EPTSs and simulations between them form a category. It is also easy to see that the only simulation T → T is the identity; it follows that the relation ≤ is a partial order on EPTSs. We will write P for the poset of EPTSs ordered by ≤, and P_{eff} for the full sub-poset of effective EPTSs. (Note that we not impose any effectivity conditions on simulations between effective EPTSs.)

11.2 Three notions of computability

We now consider three important examples of effective EPTSs. These correspond to the three good candidates for a natural notion of computable partial functional at higher types that we are currently aware of, and each of them admits several different characterizations.

Examples 11.6 (i) The effective continuous functionals—that is, those present as effective elements of finite types in the standard Scott model—constitute an effective EPTS. By a universality result due to Plotkin [45] and Sazonov [49], all such functionals are definable in the programming language PCF + parallelor + exists (we call this language PCF^{++}). It follows that this EPTS can be characterized syntactically as the term model for PCF^{++} (that is, the type structure of closed PCF^{++} terms modulo observational equivalence). It is also the EPTS arising from the familiar category of modest sets over K_{1} (see e.g. [31, Chapter 7]). There are many other mathematical characterizations of this type structure—these will be surveyed in [30].

(ii) The effective PCF-sequential functionals constitute an effective EPTS. Syntactically this can be characterized as the term model for pure PCF. Semantic characterizations of this type structure are provided by the effective versions of the various game models for PCF [2, 21, 40]. There are also characterizations via realizability models (see [32] for a survey).

(iii) The effective SR functionals, as described in this paper, clearly constitute an effective EPTS. Of the many characterizations we have discussed, the syntactic characterization as the term model for PCF+H is most relevant to our present concerns.

Thesis 11.7 The above three type structures all represent reasonable notions of computability.

For convenience we name each of these type structures after the corresponding programming language, referring to them as T (PCF^{++}), T (PCF) and T (PCF+H) respectively. In each case, an effective structure on the PTS can be obtained from the corresponding language via a Gödel-numbering of closed terms (note that evaluation of terms of type \overline{0} is effective, and the application operation can be simply juxtaposition of terms.) In fact, for the arguments below we only need to posit that T (PCF^{++}) and T (PCF+H) represent reasonable notions of computability.

It is easy to see that the syntactic inclusions PCF ↪ PCF^{++} and PCF ↪ PCF+H induce simulations between the corresponding term models, so that we have T (PCF) ≤ T (PCF^{++}) and T (PCF) ≤ T (PCF+H). (Note that the total relations in question will not all be functions, since PCF terms that are observationally equivalent in PCF need not be so in PCF^{++} or PCF+H.)

Of course, many other interesting EPTSs are known. Some of these, such as the effective part of Berry’s stable model [4], appear to be mathematically natural, but no reasonable computational interpretation for the corresponding functionals is known. Others arise from degrees of parallelism [resp. the degrees defined in Section 9.3], and consequently lie between T (PCF) and T (PCF^{++}) [resp. T (PCF+H)]. Whilst these EPTSs do have a computational interpretation, none of them has yet emerged as particularly canonical in the sense that it admits other mathematical characterizations. It is for these reasons that we claim that our three EPTSs represent the only natural notions of partial higher-type computability known to date.

The following facts are easily established:

Proposition 11.8 (i) T (PCF^{++}) ≰ T (PCF+H).

(ii) T (PCF+H) ≰ T (PCF^{++}).

Proof (i) Suppose we had a simulation s : T (PCF^{++}) → T (PCF+H). Let p ∈ T (PCF^{++})^{\overline{0}→\overline{0}→\overline{0}} be some parallel operation—for instance, suppose that pxy = ⊥ iff x = y = ⊥. Take q ∈ T (PCF+H)^{\overline{0}→\overline{0}→\overline{0}} such that s(p, q). Since s\overline{0} = id, it is clear that q = p as a function N_{⊥} × N_{⊥} → N_{⊥}. But this is a contradiction, since p is not Milner-Vuillemin sequential and hence not SR.

(ii) Conversely, suppose we had a simulation t : T (PCF+H) → T (PCF^{++}). Let F ∈ T (PCF+H)\overline{2} be the functional defined in Remark 3.7(ii), and take G ∈ T (PCF^{++})\overline{2} such that t(F, G). Then clearly G also satisfies the specification given in Remark 3.7(ii). But this is impossible, since every G ∈ T (PCF^{++})\overline{2} is monotone with respect to the pointwise order. □

The relationships between our three type structures in P_{eff} may therefore be depicted as follows:

T (PCF^{++})  T (PCF+H)
[figure]
T (PCF)

It is already interesting to note that there are two seemingly natural but incomparable notions of computability. One might now ask whether there is some more generous notion of computability that subsumes both of them. We shall see that the answer is no: the notions of computability corresponding to PCF^{++} and PCF+H are essentially incompatible.

We will write T for the type structure T (PCF^{++}), We assume some familiarity with the characterization of T as the EPTS arising from Mod(K_{1}) (see [31]), and we write ∥ − ∥^{T} for the effective structure on T given by Mod(K_{1}).

Proposition 11.9 For each type σ there is a total recursive function ϵ_{σ} : N → N such that

• for any n ∈ N, ϵ_{σ}(n) ∈ ∥x∥_{σ}^{T} for some x ∈ T^{σ};
• if n ∈ ∥x∥_{σ}^{T} then also ϵ_{σ}(n) ∈ ∥x∥_{σ}^{T}.

Proof It is straightforward to construct such a function for the type \overline{1}. The result for arbitrary types then follows from the fact that every type T^{σ} is a PCF^{++}-definable retract of T \overline{1} (see [34, Lemma 5.2]). □

Lemma 11.10 The type structure T is a maximal element of P_{eff}.

Proof Suppose we have an EPTS U with effective structure ∥ − ∥^{U}, and a simulation s : T → U. We can regard each structure (U^{σ}, ∥ − ∥_{σ}^{U}), as well as each (T^{σ}, ∥−∥_{σ}^{T}), as an object in Mod(K_{1}). We will show that there are isomorphisms T^{σ} ≅ U^{σ} in Mod(K_{1}) that respect application.

For \overline{0} the bijection T \overline{0} ≅ U\overline{0} is immediate, and the fact that this is an isomorphism in Mod(K_{1}) follows from the existence of the functions ψ of Definition 11.4. For type σ → τ, given any f ∈ U^{σ→τ} and any n ∈ ∥f∥^{U} we may recursively obtain a Kleene index tracking f · − : U^{σ} → U^{τ}. By the recursive equivalence of T, U at σ and τ we may thence recursively obtain a Kleene index tracking f · − : T^{σ} → T^{τ}, that is, an element of ∥f∥_{σ→τ}^{T}. We thus have a morphism U^{σ→τ} → T^{σ→τ} in Mod(K_{1}) that respects application. Conversely, for every f ∈ T^{σ→τ} there exists f′ ∈ U^{σ→τ} such that s(f, f′), and so we certainly have a function f ↦ f′ respecting application. To see that this is a morphism T^{σ→τ} → U^{σ→τ}, we use the function ϵ_{σ→τ} of the above proposition. By extending ϵ_{σ→τ} to a strict function we can clearly regard ϵ_{σ→τ} as an element of T^{\overline{0}→(σ→τ)}. So take e ∈ U^{\overline{0}→(σ→τ)} such that s(ϵ_{σ→τ}, e); then from an element of ∥e∥^{U} one may construct a Kleene index for the morphism N → U^{σ→τ} corresponding to e, and this index tracks the required morphism T^{σ→τ} → U^{σ→τ}. □

Theorem 11.11 The type structures T (PCF^{++}) and T (PCF+H) have no upper bound in P_{eff}. Hence P_{eff} contains no top element.

Proof Immediate from the above lemma and Proposition 11.8(ii). □

From this and the above theses, it follows that there can be no reasonable notion of computability that subsumes all other reasonable notions—that is, there is no ultimate class of computable functionals containing “all” computable functionals of higher type. This observation seems to hold some philosophical interest in its own right, and is closely related to a problem posed by Kleene in [24, §1.2] (also quoted in [21]):

I aim to generate a class of functions … which shall coincide with all the partial functions which are “computable” or “effectively decidable”, so that Church’s 1936 will apply with the higher types included.

The above results suggest that Kleene’s problem, understood in a certain way, has no solution. If one is seeking a notion of computability that is inclusive as possible, one inevitably has to choose to exclude certain kinds of functional in order to include others. This fact may appear paradoxical at first sight— for instance, one might wonder whether there was not some class of functionals computable in the language PCF^{++}+H. The answer is that any attempt to design an operational semantics for such a language results in a system that is either noneffective or non-deterministic (depending on exactly how it is attempted): the question of whether a function needs to look at its argument in order to return a result cannot be answered effectively when we are dealing with infinitely many parallel threads of computation. Another way to say this is that the question of whether f looks at its argument is only sensible for intensional representations of f of a certain restricted kind.

Whilst our argument depends on the thesis that T (PCF^{++}) and T (PCF+H) both represent reasonable notions of computability, we have not needed to assume that the type structures we have considered represent the only reasonable such notions. Indeed, there appears to be no evidence for this at present, beyond the fact that no other compelling notions of computability are currently known. Thus, there remains the intriguing possibility that there are other natural notions awaiting discovery, represented by elements of P_{eff} but embodying some computational principle quite different from those above.

We conclude with some scattered observations about the poset P_{eff}. First, it is natural to ask whether T (PCF+H) is also a maximal element. In fact it is not: the effective elements of the hypercoherence model clearly constitute an effective EPTS, and it follows from the results of Section 5.3 that this is strictly larger than T (PCF+H). However, it would appear that this larger type structure is a distraction since it does not embody an interesting computational notion— certainly it is not “effectively sequential” in any way. We would conjecture that, in some informal sense, T (PCF+H) represents a maximal notion of effectively sequential functional, and perhaps even the unique maximal notion.

Secondly, one might ask whether T (PCF) is a greatest lower bound in P_{eff} for T (PCF^{++}) and T (PCF+H). In general, one can construct a greatest lower bound of two EPTSs T, U (not necessarily the unique one) by forming the product T × U and then taking the subquotient by the unary logical relation induced by the diagonal relation at ground type. Clearly if T, U are effective then so is the resulting type structure. However, if this is construction is applied to T (PCF^{++}) and T (PCF+H), the resulting type structure V is strictly greater than T (PCF). This can be seen from the fact that both T (PCF^{++}) and T (PCF+H), and hence also V, contain a function C : (\overline{0}^{2} → \overline{0}) → \overline{0} corresponding to Curien’s Third Counterexample (see [14, p.269]), which is not PCF-definable:

C f = \{ \begin{matrix}0 & if f 0 ⊥ = 0 or f ⊥ 0 = 0 or f ⊥ 1 = f 1 0 = 0, \\ ⊥ & otherwise. \end{matrix}

The idea that this counterexample survives even when the Scott model and the strongly stable model are combined is already implicit in [10]. Operationally, the function C can be implemented using either parallel operations such as parallel-or or SR functions such as H, though it cannot be implemented in pure PCF.

12 Conclusions and further directions

12.1 Review of results

We have presented a number of contrasting but equivalent characterizations of the type structures R, R_{eff}. For convenience we summarize them here (glossing over the difference between the call-by-name and call-by-value variants).

1. The type structure given by standard realizability over the combinatory algebra B or B_{eff} (Definition 3.6).

2. The type structure given by modified realizability over B or B_{eff} (Proposition 3.9).

3. The extensional collapse of the [effective] sequential algorithms model (Corollary 5.3).

4. (R_{eff} only) The extensional collapse of the programming languages μPCF and PCF+catch (Remark 5.4).

5. (R only) The type structure in the strongly stable model HC (Corollary 5.8; Section 8.1).

6. The type structure in the presheaf category [M^{op}, Set] (Section 6.2).

7. (R_{eff} only) The closed term model of the language PCF+H (Section 9.2).

A few of these characterizations (e.g. 1,6) seem sufficiently simple and appealing that even by themselves they suggest that the SR functionals are a mathematically natural object of study. More importantly, however, the fact that so many constructions of such diverse characters all give rise to the same type structure creates a strong impression that this type structure is a highly canonical mathematical object.

The above list provides a good example of how different mathematical characterizations can illuminate different facets of the same object. For instance, the characterizations 1–4 all have an intensional or operational flavour, and they show how the SR functionals arise from a natural and very general notion of sequential process. These constructions are all basically “extensional collapses” of some kind—that is, at each type level they pick out the set of elements that “just happen” to behave extensionally—thus, they do not immediately give much of a grasp on what these elements are. (Note, however, that characterization 1 leads to a proof of the universality of type \overline{2}, and we do not know whether this result can be obtained easily by any other means.) By contrast, the strongly stable model, while it does not directly reveal the computational aspect of the SR functionals, does give a “finitary” characterization of them in terms of a preservation property, and hence yields effective information (such as the decidability of equality for finite elements) that is not evident from any of the other characterizations. Likewise, the language PCF+H, while seemingly artificial in itself, provides a pleasing “constructive” handle on R_{eff} which is not given by any of the other descriptions—we can recursively enumerate all the effective SR functionals and only them. The functional H can also be used to establish the relationship between the full and effective type structures (Theorem 9.10).

We have also shown that the SR functionals enjoy some pleasing properties not shared by the PCF-sequential functionals: for instance, the decidable presentation of the finite elements (Proposition 5.10) and the existence of a universal type (Theorem 7.11). These results indicate that the class of SR functionals is in some sense of a lower “logical complexity” than the class of PCF-sequential functionals.

Though our main focus has been on the type structures R and R_{eff}, we believe our results also indicate that van Oosten’s combinatory algebra B is an attractive object worthy of study in its own right. It provides a simple mathematical setting in which sequential algorithms have a natural home, and it has directly inspired our construction of a retraction \overline{3} ⊲ \overline{2}. Moreover, the corresponding notion of realizability coincides with that embodied by Abramsky’s combinatory algebra A (see Remark 2.8). In addition, we suspect that the combinatory algebra B_{2}, discussed in Section 8.2, will also turn out to be a natural and important object.

12.2 The meaning of “sequentiality”

Having discussed the mathematical status of the SR functionals, it is worth considering their computational aspects, and in particular, examining more closely the claim that the SR functionals are “sequential” in some reasonable sense. As is pointed out in the Introduction to [2], there is a tension inherent in the the phrase “sequential functional”, since sequentiality refers primarily to a computational process rather than a mere function. Clearly, by specifying an abstract type structure such as R_{eff}, or even a functional such as H, we do not commit ourselves to any particular kind of operational implementation. Indeed, many different operational realizations of R_{eff} are possible (see e.g. Section 12.3 below). The claim that the SR functionals are sequential, therefore, can only mean (in our view) that at least some reasonable realizations of them have a “sequential” character.

The question, then, is what sequentiality should mean for computational processes. The problem here is that there is no agreed general definition of “sequentiality” for processes of higher type. We can therefore argue in two ways: we can demonstrate the relationship with other things that have been called “sequential”, or we can appeal to an informal understanding of what the word means. Regarding the first of these, we have shown that the SR functionals can all be computed by sequential algorithms, and that they can be implemented in languages such as PCF+catch and μPCF which are widely referred to as sequential.

Regarding the informal concept of sequentiality, it is instructive to compare a language such as PCF+catch with pure PCF. Intuitively, in both languages we can only “do one thing at a time”: slightly more precisely, we cannot have two subcomputations that are directly triggered by the same function call in progress at the same time. This contrasts with PCF+parallel-or, even when the latter is implemented using deterministic reduction rules, for example:

if M → M′ then parallel-or MN → parallel-or NM′.

In PCF, however, there is an additional requirement: each subcomputation must be “completed” before another subcomputation, directly triggered by the same function call, can be begun. (In game-theoretic terms, this can be enforced by a well-bracketing condition.) This requirement is not satisfied by PCF+catch, since the catch operator allows subcomputations to be aborted before they are completed. Our view is that sequentiality informally means “doing only one thing at a time”, which is not the same thing as “completing one thing before starting another”. On this informal understanding, the languages PCF and PCF+catch are both sequential, while PCF+parallel-or is not. Insofar as PCF+catch embodies one reasonable realization of the SR functionals, we therefore feel justified in referring to the SR functionals as sequential.

The above discussion suggests that, from at least one point of view, the difference between PCF-sequentiality and sequential realizability lies in whether or not computations are required to be well-bracketed. The same message is reinforced by Abramsky’s combinatory algebra A and its well-bracketed subalgebra A_{wb} (see Remark 2.8), which give realizability models of the SR and PCF-sequential functionals respectively.

We are anxious to point out, however, that we do not see the notions of sequential realizability and PCF-sequentiality as being in competition in any way. In our view, they both represent natural and compelling notions of sequentiality at higher types, and we are not inclined to argue over which is “the more canonical”. It is true, as we have seen, that in some ways the SR functionals have better mathematical properties than the PCF ones, but we think these should be distinguished from questions about the conceptual status of the two notions.

12.3 Game-theoretic models

Perhaps the biggest omission from our theoretical investigation of the SR functionals concerns their relationship to game models for sequential computation (see e.g. [2, 21]). Here we will briefly describe the situation as we see it, and suggest some questions for further investigation.

Abramsky has proposed an “intensional hierarchy” of computational phenomena, such as state and control features, which can be captured semantically via various relaxations of the constraints on strategies in the basic game model for PCF. Roughly speaking, for deterministic sequential languages there appear to be two main axes of interest along which such relaxations can be made: we may weaken either the well-bracketing condition on strategies (leading to models for languages with control features—see [27]), or the innocence condition (leading to models for languages with state—see e.g. [1]). These conditions can be relaxed to various degrees, and also in combination (this seems to be necessary to provide good models for ML-style exceptions, for example). In general, one tries to correlate particular programming language features with particular (combinations of) conditions on strategies, by means of full abstraction or universality results.

The recent Ph.D. thesis of Laird [28] makes explicit some of the connections between this work in game semantics and the results of the present paper. He considers a class of innocent unbracketed strategies, and shows that its observational quotient coincides exactly with the sequential algorithms model. It follows immediately from the results of our Section 5.1 that the extensional collapse of the innocent unbracketed games model yields the SR functionals, and similarly for the effective analogue. Laird also shows that every effective innocent unbracketed strategy is definable in μPCF. It follows from this that R_{eff} is the extensional collapse of μPCF (see our Remark 5.4), or indeed of any other language that defines the same class of strategies.

We believe that similar results will hold for many other interesting conditions on strategies (and for the corresponding programming languages). For instance, we have recently shown that our functional H (and hence all SR functionals) can be implemented using ML-style references of ground type. Consequently, it would appear that the SR functionals arise as the extensional collapse of a certain class of non-innocent strategies (or of a corresponding programming language with state). Likewise, H can be implemented using ML-style exceptions; we would expect this to lead to another result of the same kind.

Indeed, we would conjecture that more than this is true. It seems likely that, in some sense, any reasonable class of strategies that is “sufficiently unconstrained” along either axis (i.e. sufficiently larger than the basic class of PCF strategies) will yield the type structure R as its extensional collapse. This would suggest that a large class of sequential programming languages, including languages with continuations, exceptions and references of various kinds and in various combinations, would have as their extensional collapse the type structure R_{eff}. A precise result to this effect would constitute further evidence for the ubiquity of the SR functionals.

However, we are aware of at least one example of a sequential programming language of the above kind for which such a result does not hold. Our implementations of SR functionals using ML-style exceptions can fail to work if their arguments are allowed to contain wildcard exception handlers;^{6} thus, the extensional collapse of a certain extension of PCF with exceptions and wildcard handlers does not yield the effective SR functionals. However, this need not seriously challenge the kind of general result suggested above, since it appears that wildcard handlers do not fit comfortably into the general framework under consideration. (There is already some consensus that features such as wildcard handlers—a kind of control delimiter—are troublesome from a semantic point of view; see e.g. [11]).

Perhaps the most important open question in this area is whether there is (a sensible description of) a class of strategies whose observational quotient is exactly the type structure R. For all the extensional collapse constructions mentioned above, we have to throw away non-extensional junk in order to obtain just the SR functionals. It would be very interesting indeed if one could find a constraint on strategies (preferably of a “local” nature) that gave rise to the SR functionals without any such junk, in the same way that the fully constrained games model gives rise to the PCF type structure. Such a constraint on strategies would be likely to suggest a programming language for the SR functionals using some novel kind of language feature, rather than one obtained just by adding a universal functional to PCF.

6I am indebted to Nick Benton and Andrew Kennedy for this observation.

12.4 A programming language for SR functionals

We end by discussing the possibility of a practical programming language based on the SR functionals.

The existence of universal SR functionals means that, at least in principle, one could design a programming language that incorporates the full power of the effective SR functionals into its purely “functional” fragment. For example, a functional such as H could be built into the language, and programmers could use it and believe that they were doing pure functional programming. If this proved impractical, one could at least build in a selection of weaker functionals, such as the modulus functional M of Section 9.3, giving at least some of the power of the SR functionals.

One can imagine, in principle, several reasons why these possibilities might be interesting. Firstly, they would increase the power of the purely functional fragment of the programming language. In existing functional languages such as Standard ML, the pure functional fragment is based essentially on pure PCF. However, there are natural examples of “functional” programs in the SR sense which would be (variously) impossible, inefficient or just inelegant in pure PCF. For such programs, one would gain the transparency and ease of reasoning offered by pure functional programming, as well as increased scope for compiler optimization and perhaps garbage collection.

Secondly, an SR-based functional programming language would allow us to design better and simpler program logics than can be easily done for PCF-based languages. We have already pointed out that the class of SR functionals is in many ways mathematically simpler than the class of PCF-sequential functionals; this means that operational notions such as observational equivalence and definability are theoretically more tractable in the SR case. If one adopts the philosophy (advocated e.g. in [34]) that a good program logic should have a clear operational content of a kind easily grasped by programmers, it follows that it should be easier to design and axiomatize a good program logic (with reasonable completeness properties) for an SR-based programming language.

Thirdly, besides the hope that one could design a better program logic, it seems likely that one could also perform proofs about particular programs more easily within such a logic. In view of the lower “complexity” of the SR functionals, we would expect larger fragments of the logic to be decidable (e.g. equality for finite elements), and this would give greater scope for automation in machineassisted proofs.

It is worth noting that all of the above points would in principle apply to the parallel language PCF^{++}. In criticism of the above arguments, one might point out that despite the overwhelming mathematical naturalness and simplicity of the type structure T (PCF^{++}), no one has so far been seriously tempted to use PCF^{++} as the basis of a practical programming language. However, we feel there are some grounds for being more optimistic in the case of the SR functionals. Firstly, there is a consensus that parallel operators are “painful to implement and encourage hideously inefficient programming” [12], whereas the implementation of SR functionals is relatively straightforward owing to their sequential nature. (This is attested by the fact that many SR functionals can be implemented very easily in Standard ML.) Secondly, there is the question of the interaction with side-effects (such as exceptions or references) in an impure functional language. In a parallel language with side-effects, we would be obliged to sacrifice the deterministic character of the language (or else to specify a particular interleaving protocol in gruesome detail). In an SR-based language with side-effects, the deterministic character would be easily retained (again, this can be seen by reflecting on the fact that SR functionals can be implemented in ML).

The main weakness in our proposal, at present, is that the universal functional H has an unacceptably high computational complexity (as pointed out in Remark 7.13, it involves a factorial-size search), and we do not currently know of a universal functional that is essentially any better. We might respond to this in two ways: we could hope to discover a better universal functional than H (or perhaps some other way of designing a language for the SR functionals, as suggested at the end of Section 12.3); or else we could sacrifice some expressive power and content ourselves with a selection of simpler functionals (such as M) that were computationally feasible. Regarding the first possibility, we suspect that any universal functional will have at least an exponential complexity in the worst case, but we are hopeful that there may be universal functionals that are feasible in practice, since the offending “worst cases” would not arise in natural examples of programs. The second possibility—that of restricting ourselves to a proper subset of the SR functionals—would be aesthetically less satisfying, and we might lose some of the advantages of a clean and simple program logic that still had a clear operational meaning; however, we feel that it might ultimately turn out to be the most practical way forward.

Setting aside the issue of designing completely new programming languages, some of the advantages of an SR-based programming style can already be enjoyed simply by implementing a few useful SR functionals in a language such as Standard ML. This allows one to experiment easily with these functionals, and to discover the kinds of task to which such a programming style is particularly wellsuited. We have recently begun an investigation these practical issues. It would appear so far that the construction of general-purpose search algorithms and exact real-number computation both provide promising application areas for SR-based programming, though there may be many other possible applications, such as the static analysis of programs. It would be fair to admit that our examples to date do not provide clinching proof of the usefulness of SR-based programming, but they are certainly intriguing enough to encourage further investigation.

Some examples of SR functionals implementations in ML, and some tentative programming applications, may be found in the Standard ML source file [33], available electronically from the author’s web page.

References

[1] S. Abramsky, K. Honda, and G. McCusker. A fully abstract game semantics for general references. In Proc. 13th Annual Symposium on Logic in Computer Science. IEEE, 1998.

[2] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Accepted for publication, 1996.

[3] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.

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

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

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

[7] L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott. Type theory via exact categories. In Proc. 13th Annual Symposium on Logic in Computer Science. IEEE, 1998.

[8] A. Bucciarelli. Sequential models of PCF: some contributions to the domaintheoretic approach to full abstraction. PhD thesis, Dipartimento di Informatica, Università di Pisa, 1993.

[9] A. Bucciarelli and T. Ehrhard. Sequentiality and strong stability. In Proc. 6th Annual Symposium on Logic in Computer Science, pages 138–145. IEEE, 1991.

[10] A. Bucciarelli and T. Ehrhard. Sequentiality in an extensional framework. Information and Computation, 110:265–296, 1994.

[11] R. Cartwright, P.-L. Curien, and M. Felleisen. Fully abstract semantics for observably sequential languages. Information and Computation, 111(2):297– 401, 1994.

[12] R. Cartwright and M. Felleisen. Observable sequentiality and full abstraction. In Proc. 19th POPL, pages 328–342. ACM Press, 1992.

[13] L. Colson and T. Ehrhard. On strong stability and higher-order sequentiality. In Proc. 9th Annual Symposium on Logic in Computer Science, pages 103– 108. IEEE, 1994.

[14] P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Birkhäuser, second edition, 1993.

[15] T. Ehrhard. Hypercoherences: a strongly stable model of linear logic. Mathematical Structures in Computer Science, 3:365–385, 1993.

[16] T. Ehrhard. Projecting sequential algorithms on strongly stable functions. Annals of Pure and Applied Logic, 77:201–244, 1996.

[17] T. Ehrhard. A relative PCF-definability result for strongly stable functions and some corollaries. To appear in Information and Computation, 1997.

[18] J.M.E. Hyland. A small complete category. Annals of Pure and Applied Logic, 40:135–165, 1988.

[19] J.M.E. Hyland. First steps in synthetic domain theory. In Category Theory, Proceedings, Como, Lecture Notes in Mathematics 1488, pages 131–156. Springer, 1990.

[20] J.M.E. Hyland and C.-H. L. Ong. Modified realizability toposes and strong normalization proofs. In J.F. Groote and M. Bezem, editors, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 664, pages 179–194. Springer, 1993.

[21] J.M.E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Submitted for publication, 1996.

[22] G. Kahn and G.D. Plotkin. Concrete domains. Theoretical Computer Science, pages 187–277, 1993. First appeared in French as INRIA-LABORIA technical report, 1978.

[23] R. Kanneganti, R. Cartwright, and M. Felleisen. SPCF: its model, calculus, and computational power. In Proc. REX Workshop on Semantics and Concurrency, Lecture Notes in Computer Science 666, pages 318–347. Springer, 1993.

[24] S.C. Kleene. Recursive functionals and quantifiers of finite types revisited I. In J.E. Fenstad, R.O. Gandy, and G.E. Sacks, editors, Generalized Recursion Theory II, pages 185–222, 1978.

[25] S.C. Kleene and R.E. Vesley. The Foundations of Intuitionistic Mathematics. North-Holland, 1965.

[26] G. Kreisel. Interpretation of analysis by means of functionals of finite type. In A. Heyting, editor, Constructivity in Mathematics, pages 101–128. North-Holland, 1959.

[27] J. Laird. Full abstraction for functional languages with control. In Proc. 12th Annual Symposium on Logic in Computer Science, pages 58–67. IEEE, 1997.

[28] J. Laird. A Semantic Analysis of Control. PhD thesis, University of Edinburgh, 1998. Submitted for examination.

[29] R. Loader. Finitary PCF is not decidable. To appear, 1996.

[30] J.R. Longley. Notions of computability at higher types. In preparation.

[31] J.R. Longley. Realizability Toposes and Language Semantics. PhD thesis, University of Edinburgh, 1995. Available as ECS-LFCS-95-332.

[32] J.R. Longley. Realizability models for sequential computation. In preparation, 1998.

[33] J.R. Longley. When is a functional program not a functional program?: a walkthrough introduction to the sequentially realizable functionals. Standard

ML source file, available from http://www.dcs.ed.ac.uk/home/jrl/, 1998.

[34] J.R. Longley and G.D. Plotkin. Logical full abstraction and PCF. In J. Ginzburg et al., editor, Tbilisi Symposium on Language, Logic and Computation, pages 333–352. SiLLI/CSLI, 1997.

[35] J.R. Longley and A.K. Simpson. A uniform approach to domain theory in realizability models. Mathematical Structures in Computer Science, 7:469– 505, 1997.

[36] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. Springer, 1992.

[37] R. Milner. Fully abstract models of typed λ-calculi. Theoretical Computer Science, 4:1–22, 1977.

[38] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

[39] P.S. Mulry. Generalized Banach-Mazur functionals in the topos of recursive sets. Journal of Pure and Applied Algebra, 26:71–83, 1982.

[40] H. Nickau. Hereditarily sequential functionals. In Proc. 3rd Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science 813, pages 253–264. Springer, 1994.

[41] P.W. O’Hearn and J.G. Riecke. Kripke logical relations and PCF. Information and Computation, 120(1):107–116, 1995.

[42] C.-H.L. Ong and C.A. Stewart. A Curry-Howard foundation for functional computation with control. In Proc. Symposium on Principles of Programming Languages, pages 215–227. ACM Press, 1997.

[43] J. van Oosten. A combinatory algebra for sequential functionals of finite type. Technical Report 996, University of Utrecht, 1997. To appear in Proc. Logic Colloquium, Leeds.

[44] J. van Oosten. The modified realizability topos. Journal of Pure and Applied Algebra, 116:273–289, 1997.

[45] G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[46] G.D. Plotkin. Full abstraction, totality and PCF. Accepted for publication, 1997.

[47] B. Reus. Program Verification in Synthetic Domain Theory. PhD thesis, University of Munich, 1995.

[48] B. Reus and T. Streicher. General synthetic domain theory—a logical approach. In Category Theory in Computer Science, Lecture Notes in Computer Science 1290, pages 293–313. Springer, 1997.

[49] V.Yu. Sazonov. Degrees of parallelism in computations. In Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 45, pages 517–523. Springer, 1976.

[50] D.S. Scott. Data types as lattices. SIAM Journal of Computing, 5(3):522– 587, 1976.

[51] D.S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121:411–440, 1993. First written in 1969 and widely circulated in unpublished form since then.

[52] A.K. Simpson. Computational adequacy in an elementary topos. Presented at CSL ’98; submitted for publication, 1998.

[53] G.L. Steele and G.J. Sussman. The revised report on Scheme, a dialect of Lisp. Technical Report Memo 452, MIT AI Lab, 1978.

[54] T. Streicher. Investigations into intensional type theory. Habilitationsschrift, München, 1993.

[55] P. Taylor. The fixed point property in synthetic domain theory. In Proc. 6th Annual Symposium on Logic in Computer Science, pages 152–160. IEEE, 1991.

[56] M.B. Trakhtenbrot. On representation of sequential and parallel functions. In Proc. 4th Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 32, pages 411–417. Springer, 1975.

[57] J. Vuillemin. Syntaxe, Sémantique et Axiomatique d’un Langage de Programmation Simple. PhD thesis, Université Paris VII, 1974.