We show that the bar recursion operators of Spector and Kohlenbach, considered as third-order functionals acting on total arguments, are not computable in Gödel’s System T plus minimization, which we show to be equivalent to a programming language with a higher-order iteration construct. The main result is formulated so as to imply the non-definability of bar recursion in within a variety of partial and total models, for instance the Kleene–Kreisel continuous functionals. The paper thus supplies proofs of some results stated in the book by Longley and Normann.
The proof of the main theorem makes serious use of the theory of nested sequential procedures (also known as PCF Böhm trees), and proceeds by showing that bar recursion cannot be represented by any sequential procedure within which the tree of nested function applications is well-founded.
In the study of computability theory in a higher-order setting, where ‘computable operations’ may themselves be passed as arguments to other computable operations, considerable interest attaches to questions of the relative power of different programming languages or other formalisms for computation [16]. In this paper, we shall compare the expressive power of a higher-order language supporting general iteration (in the sense of while loops) with one supporting general recursion (as in recursive function definitions).
On the one hand, it will be easy to see that our iteration constructs are definable via recursion, so that the second language subsumes the first. On the other hand, there is an example due to Berger [3] of a second-order functional H, informally of type , which is definable via recursion but not via iteration (see Section 1.1 below). So in this sense at least, we may already say that iteration is weaker than recursion.
However, it is crucial to Berger’s example that we are considering the behaviour of H on arbitrary (hereditarily) partial arguments rather than just on total ones: indeed, Berger also showed that if we merely ask which functionals of types are representable, then iteration (even in a weak form) turns out to be just as powerful as recursion. One may therefore wonder whether, more generally, iteration and recursion offer equally powerful means for defining operations on ‘hereditarily total’ arguments. The question is a natural one to ask in a computer science context, since it has sometimes been suggested that it is only the behaviour of a program on total arguments that is likely to matter for practical purposes (see Plotkin [23]).
The main contribution of this paper is to answer this question in the negative: at third order, there are ‘hereditarily total’ functionals definable by very simple kinds of recursion, but not by even the most general kind of iteration that we can naturally formulate. Indeed, one example of such a functional is the well-known bar recursion operator, first introduced by Spector in the context of interpretations of classical analysis [26]. Since bar recursion and its close relatives themselves offer a number of intriguing programming possibilities that are active topics of current research (e.g. within game theory [6,8] and proof mining [2,13,21]), we consider this to be an especially significant example of the expressivity difference between iteration and recursion.
More specifically, we will show that neither Spector’s original bar recursion functional nor the variant due to Kohlenbach [12] is computable in a language with ‘higher-order iteration’, even if we restrict attention to ‘hereditarily total’ arguments. As we shall see, there is more than one way to make such a statement precise, but we shall formulate our theorem in a robust form which (we shall argue) establishes the above claim in all reasonable senses of interest.
The main results of this paper were first stated in [16] (as Theorem 6.3.28 and Corollary 6.3.33), with a reference to a University of Edinburgh technical report [17] for the proof. The present paper is a considerably reworked and expanded version of this report, incorporating some minor corrections, and more fully developing the connection with familiar iteration constructs (hence the change in the title).
As our framework for computation with recursion, we shall work with Plotkin’s well-known language PCF for partial computable functionals [22], in which recursion is embodied by a fixed point operator for each type σ. For iteration, we shall introduce a bespoke language W with a higher-order while construct, and show that it is equivalent in power to Gödel’s System T extended with the familiar minimization (i.e. unbounded search) operator . In fact, both and have precursors and analogues in the earlier literature on higher-order computability, and the study of the relationship between (broadly) ‘recursive’ and ‘iterative’ styles of computation turns out to have quite deep historical roots. We now survey some of this history in order to provide some further context for our present work.
Historical context
In a landmark paper of 1959, Kleene [11] provided the first full-blown generalization of a concept of ‘effective computability’ to all finite type levels, working within the full set-theoretic type structure of hereditarily total functionals over . This consisted of an inductive definition of computations via nine schemes S1–S9, resulting in the identification of a substructure consisting of what we now call the Kleene computable functionals (Kleene himself called them general recursive). Kleene’s scheme S9, in particular, postulates in effect the existence of a ‘universal’ computable functional, and this in turn gives rise to a very general form of recursive function definition (see e.g. [16, Section 5.1.2]). Indeed, although Kleene’s S1–S9 definition looks superficially very different from Plotkin’s PCF, it turns out that in a certain sense, the two formalisms express exactly the same class of algorithms for higher-order computation: see [16, Sections 6.2 and 7.1]. (Strictly speaking, to obtain this equivalence at the algorithmic level, we need a mild extension of PCF with an operator as described in Section 2.2 below.)
In the same paper, Kleene also considered another notion of computability in which S9 was replaced by a weaker scheme S10 for minimization (= unbounded search), giving rise to a substructure of μ-computable functionals (Kleene’s terminology was μ-recursive). Whereas we can regard S9 as giving us ‘general recursion’, it is natural to think of S10 as giving us a particularly simple kind of ‘iteration’: indeed, from a modern perspective, we may say that S1–S8 + S10 corresponds to a certain typed λ calculus with strict ground-type iteration, or equivalently to a language with strict ground-type primitive recursion and minimization.
With the spectacles of hindsight, then, we can see that in [11] the stage was already set for a comparison between ‘iterative’ and ‘recursive’ flavours of higher-order computation. Indeed, in [11, Section 8], Kleene showed (in effect) that the System T recursor (a third-order functional in ) was Kleene computable but not μ-computable. However, Kleene’s proof relied crucially on the possibility of applying to ‘discontinuous’ arguments (in particular the second-order functional embodying quantification over ); it thus left open the question of whether every could be mimicked by some if one restricted attention to ‘computable’ arguments.
Over the next two decades, much of the focus of research shifted from the full set-theoretic model to the Kleene–Kreisel type structure of total continuous functionals, a realm of functionals of a more ‘constructive’ character than which was found to be better suited to many metamathematical applications (see e.g. [14]). Once again, the notions of μ-computability and Kleene computability respectively pick out substructures of , and Kreisel in [15, page 133] explicitly posed the question of whether these coincide. (The question is harder to answer here than for : Kleene’s counterexample Ψ can no longer be used, because the necessary discontinuous functionals such as are no longer present in .) This question remained open for some years until being answered by Bergstra [4], who used an ingenious construction based on the classical theory of c.e. degrees to produce an example of a third-order functional in but not in . On the face of it, Bergstra’s example seems ad hoc, but one can extract from his argument the fact that—once again—the System T recursor is Kleene computable but not μ-computable (see [16, Section 8.5.2]). The fact that Kreisel’s question remained open for so long in the face of such an ‘obvious’ counterexample suggests that non-computability results of this kind were not readily accessible to the proof techniques of the time.
Although Bergstra’s argument improves on Kleene’s in that it does not rely on the presence of discontinuous inputs, it still relies on the existence of non-computable second-order functions within . The argument is therefore not as robust as we might like: for example, it does not establish the non-μ-computability of within the type structure of hereditarily effective operations. For this, the necessary techniques had to await certain developments in the computer science tradition, which, in contrast to the work surveyed so far, tended to concentrate on type structures of hereditarily partial functionals rather than total ones.
As far as we are aware, the first study of the relative power of iteration and recursion in a partial setting was that of Berger [3], who (in effect) compared the languages and PCF in terms of the elements of Scott’s well-known model of partial continuous functionals that they define. Specifically, Berger introduced the partial functional defined informally by
and showed that H is readily definable in PCF (using the recursor ), but not at all in .
Although Berger concentrated on definability in , his argument also applies when we replace by the type structure of PCF-computable functionals, yielding a slightly stronger result (this point is explained in [16, Section 6.3]). Thus, Berger’s result is apparently the first to show that recursion is stronger than iteration in a sense that might matter to programmers: the behaviour of the functional H cannot be mimicked using ground-type iteration alone, even if we restrict attention to computable arguments (which we may here take to mean ‘arguments definable in ’). Note, however, that Berger’s example, unlike those of Kleene and Bergstra, does emphatically depend on the presence of the element ⊥ in the models.
Berger’s paper provided one of the main inspirations for the study of sublanguages of PCF in the book of Longley and Normann [16]. There, the focus was on modelling the ‘algorithms’ implicit in PCF programs as nested sequential procedures (NSPs), also known as Böhm trees. This is a model that had roots in early work of Sazonov [24], but which came into focus in the course of work on game semantics for PCF [1,10]. In summary, an NSP is a potentially infinite ‘decision tree’ recording the various function calls (including nested calls) that a higher-order program might make, along with the dependency of its behaviour on the results of such calls (further detail will be given in Section 2.2). One of the main ideas explored in [16, Chapter 6] was that certain sublanguages of PCF can be correlated with certain classes of NSPs: for instance, any NSP p definable in is left-bounded (that is, there is a finite global bound d on the nesting depth of function applications within p), while any NSP definable in is left-well-founded (that is, the tree of nested applications within p is well-founded).
It turns out that such observations, together with some concrete combinatorial analysis of NSP computations, can lead to interesting new non-definability results. For instance, one of the main new results of [16] (Theorem 6.3.27) is that no left-bounded procedure can have the same behaviour as when restricted to ‘total’ second-order arguments; it follows that no program of can faithfully represent the total functional on all ‘total’ computable inputs. As will become clear below, there is some ambiguity here as regards what ‘total’ ought to mean for NSPs; however, the theorem in [16] was formulated in a robust way so as to be applicable to any reasonable concept of totality. Moreover, it is also straightforward to transfer the result from NSPs to any total model with appropriate structure—in this way, we obtain a robust statement of the non-μ-computability of in such models [16, Corollary 6.3.33], not relying on the presence of non-computable or non-total arguments, and immediately applicable to a type structure such as .
This seems to offer a satisfactory conclusion to the story as regards the difference between μ-computability and more general (PCF or Kleene) computability. However, one is at this point tempted to ask whether the gap between these two notions might be closed simply by extending the former with all the System T recursors . Thus, a revised version of Kreisel’s question might read: Is the system as powerful as full Kleene computability for the purpose of defining elements of ? (In partial settings such as Scott’s , the corresponding question for and PCF is already answered negatively by Berger’s H functional, since Berger’s argument actually suffices for showing that H is not definable in .) Indeed, one may even feel that is the more natural level at which to pose such questions, given that corresponds in expressivity to a language W that embodies a very general and natural concept of iteration (as represented by while loops, possibly manipulating higher-order data).
Our main purpose in this paper is to show that, in fact, the famous bar recursion operator furnishes the desired example of a (third-order) total functional that is Kleene computable (and hence PCF computable) but not definable. Put briefly, we shall show that bar recursion does for everything that does for as described above. As a further piece of relevant background, a brief glance at the history of bar recursion is therefore in order.
Whereas the System T recursors allow us to construct functions by recursion on the natural numbers, bar recursion offers a powerful principle for defining functions by recursion on well-founded trees (the precise definition will be given in Section 2.3). Bar recursion was introduced by Spector [26] as a major plank of his remarkable extension of Gödel’s so-called ‘Dialectica’ interpretation of first-order arithmetic (modulo a double-negation translation) to the whole of classical analysis (i.e. full second-order arithmetic). Spector’s motivations were thus proof-theoretic: for instance, System T extended with bar recursion offered a language of total functionals powerful enough to define all functions provably total in classical analysis. Spector’s interpretation, and variations on it, continue to this day to be a fruitful source of results in applied proof theory [13].
Since System T itself defines only the provably total functions of first-order arithmetic, it was thus clear at the outset that bar recursion could not be definable within System T. However, these ideas are of little help when we move to languages such as , which defines all Turing computable functions—nor can methods such as diagonalization be used to establish non-definability in the ‘partial’ setting of . The results of the present paper thus require quite different techniques.
For the purpose of interpreting classical analysis, one requires versions of bar recursion at many different type levels; however, for the purpose of this paper, we may restrict attention to the simplest non-trivial instance of bar recursion (a third-order operation), since this already turns out to be non-computable in . Another subtlety concerns the way in which we represent the well-founded tree over which the recursion takes place. Typically the tree is specified via a functional passed as an argument to the bar recursor—however, different ways of representing trees by such functionals have turned out to have different proof-theoretic applications. In this paper we shall consider two possible choices: the one used by Spector, and a variant due to Kohlenbach [12]. As we shall see, the corresponding versions of bar recursion are actually interdefinable relative to , so that the difference is inessential from the point of view of our main result.
Spector’s original treatment of bar recursion was syntactic, but it became clear through work of Scarpellini [25] and Hyland [9] that bar recursors could be viewed as (Kleene computable) functionals within . Thus, bar recursion was very much in the consciousness of workers in in the early 1970s, although it was evidently not obvious at the time that it furnished a rather dramatic example of a Kleene computable but not μ-computable functional. We will show in this paper how the more recent perspective offered by nested sequential procedures helps to make such results accessible.
Content and structure of the paper
The main purpose of the paper is to show that the bar recursion functional , even at the simplest type level of interest and in a somewhat specialized form, is not definable in System . As we shall see, there are various choices involved in making this statement precise, but our formulation will be designed to be robust with respect to such variations. Our argument will be closely patterned on the proof of the analogous result for and the System T recursor (see [16, Theorem 6.3.27]). However, the present proof will also involve some further twists, illustrating some new possibilities for reasoning with nested sequential procedures.
In Section 2 we define the languages mentioned in the above discussion—, , W and —and establish some basic relationships between them, in particular showing that and W are equivalent in expressive power. We then summarize the necessary theory of nested sequential procedures (NSPs), relying heavily on [16] for proofs, and in particular introducing the crucial substructure of left-well-founded procedures, which suffices for modelling and W. We also explain the concepts of (Spector and Kohlenbach) bar recursion that we shall work with.
Section 3 is devoted to the proof of our main theorem: within the NSP model, no bar recursor can be left-well-founded, hence no program of or W can implement bar recursion, even in a weak sense. As mentioned above, the proof will be closely modelled on the corresponding theorem for : indeed, we shall take the opportunity to explain more fully certain aspects of that proof that were presented rather tersely in [16]. We shall also explain the new ingredients that form part of the present proof.
In Section 4, we show how our theorem for NSPs transfers readily to other models, both partial and total, under relatively mild conditions. As an example, we infer that bar recursion is not definable within the type structure of Kleene–Kreisel continuous functionals.
Definitions and prerequisites
In this section we summarize the necessary technical background and establish a few preliminary results. We introduce the languages in question in Section 2.1, the nested sequential procedure model in Section 2.2, and bar recursion in Section 2.3.
Some languages for recursion and iteration
We start by giving operational definitions of the languages we shall study—principally , and W—and establishing some basic relationships between them. A relatively easy result here will be that and W are equally expressive as sublanguages of . Of these, is of course the more widely known and has served as the vehicle for previous results in the area (e.g. in [16]); however, W appears to correspond very directly to a familiar concept of iteration via while loops, suggesting that this level of expressivity is a natural one to consider from the perspective of programming language theory.
Our version of will closely follow that of [16, Chapter 7], except that we shall also include product types, at least initially. We shall present all our languages as extensions of a common base language B.
Specifically, our types σ are generated by
Terms of B will be those of the simply typed λ-calculus (with binary products) constructed from the constants
Throughout the paper, we shall regard the type of a variable x as intrinsic to x, and will often write to indicate that x carries the type σ.
We endow B with a call-by-name operational semantics via the following (small-step) basic reduction rules.
We furthermore allow these reductions to be applied in certain term contexts. Specifically, the relation ⇝ is inductively generated by the basic rules above together with the clause: if then , where is one of the basic evaluation contexts
We shall consider extensions of B with operations embodying various principles of general recursion, iteration, primitive recursion and minimization. To these we also add some simple operations that allow us to pass arguments of type ‘by value’, for reasons we will explain shortly. The operations we consider are given as constants
(where abbreviates if ), with associated basic reduction rules
and with our repertoire of basic evaluation contexts augmented by
The constants , are familiar from and System T respectively, whilst is an inessential variant of the standard minimization operator μ. The operator is designed to capture that behaviour of a while loop that manipulates data of type σ: the argument C is the looping condition (with doing duty for the booleans, and 0 as true), X is the initial value of the data, and F is the transformation applied to the data on each iteration. The result returned by is then the final value of the data when the loop terminates (if it does).
The operator has a different character. The idea is that the evaluation of (where ) will proceed by first trying to compute the value of N, and if this succeeds, will then call ‘by value’ on . This ensures that the subterm N will be evaluated exactly once, whereas in the evaluation of , N may be evaluated zero times (e.g. if ) or many times (e.g. if ). It turns out that we need to augment PCF with such operators if we are to simulate the intended reduction behaviours of and correctly (see the definitions of and below). Closely related to this, the addition of to PCF is needed if we wish to define all computable elements in the NSP model (see Section 2.2): there are semantically possible ‘evaluation behaviours’ that cannot be expressed in PCF alone.
Our operators do essentially the same job as the operator of [16, Section 7.1], which in our present notation would be written as . Indeed, for many purposes one could identify with
but there is a fine-grained difference in reduction behaviour which will matter for Proposition 2 below.
Our languages of interest are obtained by extending the definition of B as follows:
For , we add the constant for each type σ.
For W, we add the constants .
For T, we add the constants .
We shall also consider the further extensions and , where we take the latter to include all .
Note that in each case, the reduction relation is generated inductively from the specified basic reduction rules together with the clause ‘if then ’, where ranges over the appropriately augmented set of basic evaluation contexts. We thus obtain reduction relations , etc. on the relevant sets of terms. However, we may, without risk of ambiguity, write ⇝ for the union of all these reduction relations, noting that ⇝ is still deterministic, and that if M belongs to one of our languages and then belongs to .
We write for the transitive closure of ⇝, and for its reflexive-transitive closure. It is easy to see that if M is any closed term of type , then either for some unique , or the unique reduction path starting from M is infinite; in the latter case we say that M diverges.
The following fundamental fact will be useful. It was first proved by Milner [20] for , but extends readily to (cf. [16, Section 7.1.4]). Recall that two closed terms are observationally equivalent (written ) if for every program context of (with a hole of type σ) and every , we have iff .
(Context lemma for ).
Suppose M,are closed terms of type. Theniff for all closed, …,we have.
For closed, we haveiffand.
For closed, we haveiff M,either both diverge or both evaluate to the same numeral.
Let us also write ≡ for the congruence on terms generated by ⇝ (i.e. the least equivalence relation containing ⇝ and respected by all term contexts ). Clearly if then ; hence also if then . In combination with the context lemma, this provides a powerful tool for establishing observational equivalences.
For any type σ, we write for the ‘everywhere undefined’ program . It is not hard to see that if admits an infinite reduction sequence then .
At this point, we may note that the addition of does not fundamentally affect the expressive power of , since as a simple application of the context lemma, we have
This in turn implies that every term is observationally equivalent to a term, and also that it makes no difference to the relation whether the observing contexts are drawn from or just . Even so, we shall treat as a separate language primitive rather than as a macro for the above term, since its evaluation behaviour is significantly different (cf. Section 2.2 below).
We now show how both W and may be translated into . To do this, we simply need to provide programs of the appropriate types to represent the constants , , . As a first attempt, one might consider natural implementations of these operations along the following lines:
In fact, the above program will serve our purpose as it stands, but for and we shall need to resort to more complicated programs that mimic the reduction behaviour of , in a more precise way, using to impose a certain evaluation order. We abbreviate the type of as ρ, and the type of as μ; we also write for .
We may then translate a term of W or to a term of simply by replacing each occurrence of , , by the corresponding program. The following facts are routine to check by induction on the generation of ⇝:
Ifthen.
Ifcan be reduced, then so can M: that is, ifthen there is somesuch that.
Henceiff.
Next, we show that W and are also intertranslatable, though in a looser sense. First, in either of these languages, it is an easy exercise to write a program that implements inequality testing. To assist readability, we shall use ≠ as an infix, and also allow ourselves some obvious pattern-matching notation for λ-abstractions on product types. To translate from to W, we use the following W programs.
We may then translate a term M to a W term simply by replacing each occurrence of by , respectively. However, it will not in general be the case for this translation that if then : the operational behaviour of M and at an intensional level may be quite different. Nevertheless, we can show that the translation is faithful in the sense that M and are observationally equivalent when both are transported to :
andasterms.
For any closed term M of, we have.
For any closedin, we haveiff.
(i) For , by Theorem 1 it suffices to show that for any closed PCF terms , and , we have
But this is routinely verified: if N diverges then both sides admit infinite reduction sequences and so are observationally equivalent to ; whilst if then an easy induction on n shows that
A similar approach works for .
(ii) follows immediately, since may be obtained from by replacing certain occurrences of , by , .
(iii) is now immediate from (ii) and Proposition 2(iii). □
To translate from W to , we may define
and translate a W term M to a term by replacing each with . Once again, the operational behaviour of is in general quite different from that of M: indeed, this translation is grossly inefficient from a practical point of view, since typically some subcomputations will be repeated several times over. Nonetheless, if we consider programs only up to observational equivalence, the translation is still faithful in the way that we require:
.
For any closed term M of W, we have.
For any closedin W, we haveiff.
Closely analogous to Proposition 3. For (i), we show that by induction on n that if whereas for each , then
Furthermore, we show that if there is no n with this property, then and both admit infinite reduction sequences, so that both are observationally equivalent to . □
In summary, we have shown that and W are equally expressive as sublanguages of , in the sense that a closed PCF term M is observationally equivalent to (the image of) a term iff it is observationally equivalent to a W term. As already noted, the language W appears to embody a natural general principle of iteration, suggesting that this level of expressive power is a natural one to consider.
Although not formally necessary for this paper, it is also worth observing that the above equivalence works level-by-level. For each , let us define sublanguages , , of , , W by admitting (respectively) the constants , , only for types σ of level . Then the translations , clearly restrict to translations between and , so that and are equally expressive as sublanguages of . (This hierarchy turns out to be strict, as will be shown in a forthcoming paper [19]. The strictness of the hierarchy of languages is established in [18].) In fact, for , we can even regard and as sublanguages of , since it is an easy exercise to replace our ‘precise’ translation for or by a translation up to observational equivalence that requires only . This does not work for , however, since the implementation of requires at least .
Weaker languages
A few weaker languages will play more minor roles in the paper. We introduce them here, suppressing formal justifications of points mentioned merely for the sake of orientation.
To motivate these languages, we note that even the primitive recursor of works in a ‘lazy’ way: it is possible for the value of to be defined even if that of is not, for example if , and . This contrasts with the ‘strict’ behaviour of Kleene’s original version of primitive recursion, in which the value of at is obtained by successively computing its values at , all of which must be defined. (Of course, the distinction is not very visible in purely total settings such as or .)
We may capture this stricter behaviour with the help of , which we shall here write as . From this, we may inductively define an operator
for each level 0 type σ by:
We may now use these operators to define ‘strict’ versions of and for any type σ of level 0. We do this by introducing constants and of the same types as , , with reduction rules
We also add as a basic evaluation context. By using these in place of their non-strict counterparts, and also including so that the operators are available, we obtain languages , and .
Our earlier PCF programs , may be readily adapted to yield faithful translations of these languages into . It can also be checked that and are intertranslatable in the same way as and , and so are equi-expressive as sublanguages of . Finally, we can regard the strict versions as sublanguages of the lazy ones up to observational equivalence, since for example
and it is easy to supply terms of B observationally equivalent to each .
It is natural to think of as the language for ‘everyday’ iterative computations on ground data. It is easy to check that at type level 1, and define all Turing computable functions, and indeed that (respectively) and are sufficient for this purpose.
It is shown in [16, Theorem 6.3.23] that for higher types, is strictly weaker than (note that is in essence the language known as in [16]). What is perhaps more surprising is that defines more total functionals at third order than does , despite the fact that , have the same behaviour on all total arguments [19].
The weakest language of all that we shall consider is . This will play an ancillary as a language for a rudimentary class of ‘non-controversially total’ functionals present in all settings of interest, enabling us to formulate our main theorem in a robust and portable form. In all total type structures of interest, the -definable functionals will clearly coincide with those given by Kleene’s S1–S8; at type level 1 these are just the usual primitive recursive functions. However, a somewhat subtle point is that for typical interpretations in partial type structures, will be slightly stronger than the usual formulations of S1–S8, since the constant will give us the power of strong definition by cases which is not achievable via S1–S8 alone. This point will be significant in Section 3, where we shall frequently claim that certain elements of the model are -definable; the reader should bear in mind here that strong definitions by cases are permitted. (In [16], this issue was addressed by introducing a specially defined class of strongly total elements of .)
Elimination of product types
So far, we have worked with languages with product types in order to manifest the equivalence of and W (and various restrictions thereof) in a perspicuous way. However, since the bar recursors that are the subject of our main theorem have a type not involving products, it will be sufficient from here on to work with types without ×, and it will simplify the presentation of nested sequential procedures (in the next subsection) to do so. From the point of view of expressivity, nothing of significance is lost by dispensing with product types, in view of the following proposition. Here we say a type σ is ×-free if it does not involve products, and a term M is ×-free if the types of M and all its subterms are ×-free. In particular, a ×-free term M may involve operators , , only for ×-free σ. We shall write for , and for .
Suppose σ is ×-free. Then any closed termof(resp., W) is observationally equivalent to a ×-free term of the same language.
This will be clear from familiar facts regarding the embeddability of arbitrary types in ×-free ones, as covered in detail in [16, Section 4.2]. More specifically, we may specify, for each type σ, a ×-free type such that σ is a -definable retract of up to observational equivalence: that is, there are closed B terms and such that . Moreover, we may choose these data in such a way that
and , and moreover we have , , and (these facts imply that for all ×-free σ we have and ),
pairing and projections are represented relative to this encoding by ×-free programs , , ,
for any σ we have , and similarly for and .
Using these facts, it is easy to construct a compositional translation assigning to each term (with free variables ) a ×-free term (with free variables ) such that (we omit the uninteresting details). In particular, for closed M of ×-free type σ, this yields , which achieves our purpose. □
From here onwards, we shall therefore use the labels , , W, etc. to refer to the ×-free versions of these languages, and shall only refer to types generated from via →.
Nested sequential procedures
Next, we summarize the necessary elements of the theory of nested sequential procedures (NSPs) also known as PCF Böhm trees, relying on [16] for further details and for the relevant proofs. (The term ‘nested sequential procedure’ was adopted in [16] as a neutral label for a notion that is of equal relevance to both PCF and Kleene computability.) Although we shall provide enough of the formal details to support what we wish to do, a working intuition for NSPs is perhaps more easily acquired by looking at examples. The reader may therefore wish to look at the examples appearing from Definition 10 onwards in conjunction with the following definitions.
As explained in Section 3.2.5 and Section 6.1 of [16], nested sequential procedures (or NSPs) are infinitary terms generated by the following grammar, construed coinductively:
Informally, an NSP captures the possible behaviours of a (sequential) program with inputs bound to the formal parameters , which may themselves be of function type. Such a program may simply diverge (⊥), or return a value n, or apply one of its inputs to some arguments—the subsequent behaviour of the program may depend on the numerical result i of this call. Here the arguments to which is applied are themselves specified via NSPs (which may also involve calls to ). In this way, NSPs should be seen as syntax trees which may be infinitely deep as well as infinitely broad.
We use t as a meta-variable ranging over all three kinds of NSP terms. We shall often use vector notation , for finite sequences and . Note that such sequences may be empty, so that for instance we have procedures of the form . As a notational concession, we will sometimes denote the application of a variable x to an empty list of arguments by . If , we will also allow the notation to mean . The notions of free variable and (infinitary) α-equivalence are defined in the expected way, and we shall work with terms only up to α-equivalence.
If variables x are considered as annotated with simple types σ (as indicated by writing ), there is an evident notion of a well-typed procedure term . Specifically, within any term t, occurrences of procedures (of any type), applications (of the ground type ) and expressions e (of ground type) have types that are related to the types of their constituents and of variables as usual in typed λ-calculus extended by case expressions of type . We omit the formal definition here since everything works as expected; for a more precise formulation see [15, Section 6.1.1].
For each type σ, we let be the set of well-typed procedures of type σ, and for the set of closed such procedures; note that . As a notational liberty, we will sometimes write the procedures simply as n, ⊥.
Note that in the language of NSPs, one cannot directly write e.g. , since the variable is not formally a procedure. However, we may obtain a procedure corresponding to via hereditary η-expansion: if , then we define a procedure inductively on types by
For example, the procedure corresponding to the identity on type σ may now be written as . Note that .
In order to perform computation with NSPs, and in particular to define the application of a procedure p to an argument list , we shall use an extended calculus of meta-terms, within which the terms as defined above will play the role of normal forms. Meta-terms are generated by the following infinitary grammar, again construed coinductively:
Again, our meta-terms will be subject to the evident typing rules which work as expected. Unlike terms, meta-terms are amenable to a notion of (infinitary) substitution: if T is a meta-term and are meta-procedures whose types match those of respectively, we have the evident meta-term .
We equip our meta-terms with a head reduction generated as follows:
We write for the reflexive-transitive closure of . We call a meta-term a head normal form if it cannot be further reduced using . The possible shapes of meta-terms in head normal form are ⊥, n, and , the first three optionally prefixed by .
We may now see how an arbitrary meta-term T may be evaluated to a normal form t, by a process analogous to the computation of Böhm trees in untyped λ-calculus. For the present paper a somewhat informal description will suffice; for a more formal treatment we refer to [16, Section 6.1]. First, we attempt to reduce T to head normal form by repeatedly applying head reductions. If a head normal form is never reached, the normal form is ⊥ (possibly prefixed by some appropriate to the type). If the head normal form is ⊥ or n (possibly prefixed by ), then this is the normal form of T. If the head normal form is , then we recursively evaluate the and to normal forms , by the same method, and take ; likewise for expressions prefixed by a λ, and for meta-terms . Since the resulting term t may be infinitely deep, this evaluation is in general an infinitary process in the course of which t crystallizes out, although any required finite portion of t may be computed by just finitely many reductions.
If and , we define the application to be the normal form of the meta-procedure . This makes the sets into a total applicative structure , and the sets of closed procedures into a total applicative structure .
We write ⊑ for the syntactic ordering on each , so that if p is obtained from by replacing certain subterms (perhaps infinitely many) by ⊥. It is not hard to check that each is a DCPO with this ordering, and that application is monotone and continuous with respect to this structure.
We also have an extensional preorder ⪯ on each defined as follows: if where , then
The following useful fact is established in Section 6.1.4 of [16]:
(NSP context lemma).
If, then for allwe have.
We now have everything we need to give an interpretation of simply typed λ-calculus in : a variable is interpreted by , application is interpreted by ·, λ-abstraction is interpreted by itself, and we may also add a constant p for each (interpreted by itself). The following non-trivial theorem, proved in [16, Section 6.1], ensures that many familiar kinds of reasoning work smoothly for NSPs:
is a typed -algebra: that is, ifare closed simply typed λ-terms with constants drawn fromand, then U, V denote the same element ofunder the above interpretation.
One of the mathematically interesting aspects of is the existence of several well-behaved substructures corresponding to more restricted flavours of computation. The two substructures of relevance to this paper are defined as follows:
The application tree of an NSP term t is simply the tree of all occurrences of applications within t, ordered by subterm inclusion.
An NSP term t is left-well-founded (LWF) if its application tree is well-founded.
A term t is left-bounded if its application tree is of some finite depth d.
The following facts are proved in [16, Section 6.3]:
LWF procedures are closed under application. Moreover, the substructureofconsisting of LWF procedures is a sub--algebra of.
Left-bounded procedures are closed under application, and the corresponding substructureis also a sub--algebra of.
Next, we indicate how NSPs provide us with a good model for the behaviour of terms of .
The NSP for , where .
To any term (possibly with free variables) we may associate a procedure (with the same or fewer free variables) in a compositional way, by recursion on the structure of M:
The NSP for is the archetypal example of a non-LWF procedure: the nested sequence of application subterms never bottoms out.
The following theorem, proved in [16, Section 7.1.3], confirms that this interpretation is faithful to the behaviour of programs:
(Adequacy of NSP model).
If M is any closedterm of type, theniff, and M diverges iff.
It is also the case that every computable element of any is denotable by a closed term of type σ (see [16, Section 7.1.5]), though we shall not need this fact in this paper.
We also obtain interpretations of and W in , induced by the translations of these languages into as described in Section 2.1. Applying the definition of above to the programs , , , we may thus obtain the appropriate NSPs for the constants , , , as shown in Figs 2, 3 and 4 respectively. To reduce clutter, we allow an application term a to stand for the expression . Where a case branch label involves a metavariable i or j, there is intended to be a subtree of the form displayed for each .
The NSP for .
The NSP for .
The NSP for .
Clearly, each of these NSPs is left-well-founded; the one for is even left-bounded, since there is no nesting of calls to n or f. Since also the NSPs for , , , and are plainly LWF, and LWF procedures are closed under λ-abstraction and application (Theorem 9(i)), we have the following important result:
The interpretation of any term ofor W is an LWF procedure.
The reader may also enjoy constructing the appropriate trees for and where σ is of level 0, and to observe that these trees are left-bounded (in contrast to those for and ). Since the trees for and all the constants of B are also left-bounded, we may infer by Theorem 9(ii) that the interpretation of any term of or is left-bounded. These observations may shed light on the discussion of Section 1, but are not formally required for the remainder of the paper.
Bar recursors
We conclude the section by explaining the notions of bar recursion that we shall use. Traditionally, bar recursion has usually been considered either as a purely syntactic operation (as in [26]), or as an element of a total type structure such as the Kleene–Kreisel total continuous functionals or Bezem’s strongly majorizable functionals . Here, for expository purposes, we shall introduce bar recursion first in a ‘naive’ way with reference to the full set-theoretic type structure , and then as an operation within defined by a certain program—the latter will provide the setup for the main theorem of Section 3. In Section 4, we will relate this to more familiar notions of bar recursion and will show how our results transfer relatively easily from to models such as and .
As explained in Section 1, bar recursion is in essence recursion over well-founded trees. For the purpose of this paper, a tree will be an inhabited prefix-closed subset of (the set of finite sequences over ), with the property that for every , one of the following holds:
There is no such that (we then say is a leaf of ).
For all , (we then say is an internal node of ).
We write , for the set of leaves and internal nodes of respectively.
A tree is well-founded if there is no infinite sequence over such that for every i. Thus, in a well-founded tree, every maximal path terminates in a leaf. If is well-founded, a function may be defined by recursion on the tree structure if we are given the following data:
A leaf function specifying the value of f on leaf nodes.
A branch function specifying the value of f on an internal node , assuming we have already defined the value of f on all the immediate children of f. Specifically, if gives the value of for every , then gives the value of .
Indeed, we may define the function obtained by bar recursion from L and G to be the unique function satisfying:
The existence and uniqueness of are easy consequences of well-foundedness.
It is easy to see how L and G may be represented by objects of simple type: elements of may be represented by elements of via some standard primitive recursive coding , so that we may consider L and G as functions and respectively. As regards the tree itself, we now introduce two related ways, due respectively to Spector [26] and Kohlenbach [12], for representing well-founded trees by means of certain functionals . We shall write for the length of a sequence , and if , shall write for the primitive recursive function defined by
Suppose F is any function .
We say satisfies the Spector bar condition (with respect to F) if
and the Kohlenbach bar condition if
The Spector tree of F, written , is the set of sequences such that no proper prefix of satisfies the Spector bar condition w.r.t. F. The Kohlenbach tree is defined analogously using the Kohlenbach bar condition.
Both and are clearly trees in our sense. Furthermore, the following important fact ensures a plentiful supply of functionals giving rise to well-founded trees.
If F is continuous with respect to the usual Baire topology on, then bothandare well-founded.
For any infinite sequence , there will be some ‘modulus of continuity’ m for F such that for all and all j we have . It follows easily that some finite subsequence will satisfy the Spector [resp. Kohlenbach] condition. The shortest such prefix will then be a leaf in [resp. ]. □
There are also other ways in which well-founded trees may arise—for instance, it is well-known that if F is majorizable then is well-founded—but it is the continuous case that will be most relevant to our purposes.
Using the above representations, we may now introduce our basic definition of bar recursion. We are here naively supposing that F, L, G are drawn from the full set-theoretic type structure , although this is not really the typical situation. Relativizations of this definition to other total type structures will be considered in Section 4.
(Bar recursors).
A Spector bar recursor (over ) is any partial function
such that for all with well-founded and for any and , we have
The notion of Kohlenbach bar recursor is defined analogously using .
Note that the above equations uniquely fix the value of for all . We shall not be concerned with the behaviour of bar recursors on sequences outside the tree in question, nor with their behaviour on arguments F such that is not well-founded. (Our definition of ‘bar recursor’ is thus slightly weaker than some given in the literature (e.g. in [16, Section 7.3]); this will in principle make our main theorem slightly stronger, although not in any deep or essential way.)
Our next step will be to re-construe the definition of bar recursors as a recursive program within . For this, we first note that both the Spector and Kohlenbach bar conditions are readily testable by means of programs in or indeed in . Although these languages have just a single base type , for clarity we shall write for occurrences of whose role is to represent sequences via their codes . We shall suppose we have a fixed choice of programs
such that for any , z, j, i we have
(where we omit the hats from PCF numerals). We also presuppose fixed implementations of = and <. Using this machinery, we may now define a term
by
or a little more formally by
The Kohlenbach version (of the same type) is defined analogously, replacing the subterm by .
Both of these PCF terms may be interpreted in , yielding NSPs which we shall also denote by and respectively. We shall refer to these as the canonical (Spector or Kohlenbach) bar recursors within .
It is not hard to see intuitively that these NSPs for and are non-LWF, since the unrolling of the recursion will lead to an infinite sequence of nested calls to G. To illustrate the phenomenon, in Fig. 5 we schematically depict part of the NSP for (so that evaluations of x are elided).
The NSP for a reduced version of .
It follows immediately by Theorem 12 that these particular bar recursors within are not denotable in . However, this does not in itself address the main question of interest: what we wish to know is that no element of can have the extensional behaviour of a bar recursor, even if we restrict attention to arguments F, L, G which represent total functionals in the spirit of Definition 15. This begs the question of what it means for an element of to ‘represent’ a total functional. We now briefly indicate why there is room for several reasonable answers to this question, thus motivating our ‘robust’ approach which is designed to work for all of them.
The general picture we have in mind is that of some chosen type structure T of total functionals over —that is, a family of sets where and is some set of total functions —along with some way of representing T within . The latter will in general consist of what in [16] we call a (type- and numeral-respecting) applicative simulation: that is, a family of total relations such that iff , and and imply . Relative to this, we may call an element of total if it is in the image of . We might then regard as a ‘bar recursor’ in any procedure Φ that satisfies (an analogue of) the equations of Definition 15 for all total of appropriate types.
However, there is scope for variation here, both in the choice of T (which could be either or , for example) and in the choice of the simulation γ. Different choices will in general lead to different notions of ‘total element’ within (this phenomenon is explored in [23]), and hence to different criteria for what it means to be a bar recursor in .
Our approach to dealing with this is to identify a core class of elements of which are likely to be ‘total’ under all reasonable choices of interest, and then postulate, as a minimal requirement for any proposed ‘bar recursor’ in , that the equations of Definition 15 should at least be satisfied by these core total elements. Our main theorem will then claim that even this minimal requirement cannot be met by any LWF procedure. As we shall argue in Section 4, this will demonstrate that in no reasonable sense can a bar recursor be definable in or W.
In fact, a suitable class of core total elements for our purpose will be those definable in the language of Section 2.1.1 (interpreted in via its translation to ). Our rationale for this is that all reasonable choices of the total type structure T can be expected to be models for (or equivalently for Kleene’s S1–S8), and that it is furthermore a mild requirement that γ should relate the interpretation of any closed term in T to its interpretation in . (This will in fact be so if it is the case for the standard programs k and s and for the constants , , , .) Our thesis, then, is that the -definable elements of can be expected to be ‘total’ in all senses of interest.
All of this leads us to the following definitions. Here we identify the PCF programs , , with their interpretations in .
Suppose
We say satisfies the Spector bar condition with respect to F if , and the Kohlenbach bar condition if .
The tree [resp. ] consists of all sequences such that no proper prefix of satisfies the Spector [resp. Kohlenbach] bar condition.
The following easy fact will be useful:
Ifis definable by a term of, then,are well-founded.
If F is -definable, clearly F will represent a total functional with respect to the obvious representation of functions within . Moreover, since application in is continuous, it is easy to see that will be continuous for the Baire topology, and so by Proposition 14 the trees and will be well-founded. □
A weak Spector bar recursor in is an element
such that the following hold for all -definable of appropriate types such that for all :
The notion of weak Kohlenbach bar recursor in is defined analogously.
Here the abstraction is understood simply as a λ-abstraction within the language of NSPs; note that for any given Φ, F, L, G, , the body of this abstraction will evaluate to an NSP with free variable z.
Clearly the canonical bar recursors , defined earlier are examples of weak bar recursors in this sense. Moreover:
If Φ is any weak (Spector or Kohlenbach) bar recursor, F, L, G are-definable, and, then the value ofis a numeral and is uniquely determined by the defining equations above.
For a given F, L, G, we show that the set S of for which the proposition holds contains all leaves and all internal nodes whose immediate children are all in S; it follows that S is the whole of since the latter is well-founded. For the step case, we use the fact that if G is -definable and is total (i.e. for all ), then for any . We show this by an easy induction on the term that denotes G, which we may assume to be some β-normal form , so that all variables are bound within M are of type level 0. □
Clearly, if F represents an element via any reasonable simulation γ, it will be automatic that is well-founded since any such is continuous. Indeed, since bar recursors exist as third-order functionals within , any elements that represent such will be total weak bar recursors relative to γ. The situation is different for the type structure : there are classically discontinuous functions , and if represents such an then may be non-well-founded, in which case Definition 18 places no condition on how Φ should behave on F.
In our main proof, we shall find it more convenient to work with the Kohlenbach definition, but the theorem will transfer readily to the Spector version in view of the following easy relative definability result. From here on, we shall allow k to denote the pure type of level k, so that 0 denotes and denotes .
Ifis any weak Spector bar recursor in, then a weak Kohlenbach bar recursorisdefinable relative to. Hence if an LWF weak Spector bar recursor exists in, then so does an LWF weak Kohlenbach bar recursor.
We first construct a definable element such that for any whose Kohlenbach tree is well-founded and is not simply , the Spector tree of is precisely the Kohlenbach tree of F. We may achieve this by defining (in PCF-style notation)
Using this, we may define
Since except in the trivial case, the equations stating that is a weak Spector bar recursor (as in Definition 18) now readily imply the corresponding equations stating that is a weak Kohlenbach bar recursor. □
Conversely, a more subtle argument (given in Kohlenbach [12]) shows that Spector bar recursion is definable from Kohlenbach bar recursion even in System T, though we shall not need this here. We also refer the reader to Escardó and Oliva [7] for a cornucopia of related functionals known to be either interdefinable with or stronger than Spector bar recursion over System T; our main theorem will thus yield that none of these functionals are definable in .
One final preliminary is needed. In order to ease notation in our main proof, we shall actually consider a simpler kind of bar recursor readily obtained as a specialization of those described above.
A simplified weak Spector bar recursor (in ) is an element
such that the following hold for all -definable of appropriate types such that for all :
The notion of simplified weak Kohlenbach bar recursor is defined analogously.
It is easily seen that a simplified weak (Spector or Kohlenbach) bar recursor is -definable from an ordinary one just by specializing the leaf function L to (this move is admittedly hard to motivate at this point!) and by eschewing the dependence of G on an argument x. By analogy with Proposition 19, we have:
If Φ is any simplified weak (Spector or Kohlenbach) bar recursor, F, G are-definable,is well-founded and, then the value ofis a numeral and is uniquely determined by the defining equations above.
The proof of Proposition 20 clearly also yields the following:
If an LWF simplified weak Spector bar recursor exists in, so does an LWF simplified weak Kohlenbach bar recursor.
Such simplified bar recursors were called restricted bar recursors in [16, Section 6.3.4], but the latter name clashes with a different use of the same term by Spector in [26]. In [16] we supposed that the simplified bar recursors were weaker than the general ones, so that they led to a slightly stronger non-definability result. Actually, it turns out to be not too hard to define general bar recursors from simplified ones (we leave this as an exercise for the interested reader). Nevertheless, we shall prove our main theorem for the simplified versions, both because that was what was claimed in [16], and because it does lighten the notational load in parts of our proof. Against this, the later parts of the proof (Sections 3.5 and 3.6) turn out to be a little more delicate in the simplified setting, but we think there is also some interest in the opportunity this gives for illustrating the versatility of our method of proof.
The main theorem
In this section, we shall prove the following theorem:
Within , no simplified weak Kohlenbach bar recursor can be LWF, and hence none can be definable in or in W.
The corresponding fact for simplified Spector bar recursion (stated as Theorem 6.3.28 in [16]) will then follow immediately by Proposition 23. It will also follow, a fortiori, that no ordinary Spector or Kohlenbach bar recursor in the sense of Definition 15 can be LWF. From here on we shall consider only Kohlenbach bar recursion, and will write simply as .
The proof of Theorem 24 follows the method of proof of Theorem 6.3.27 in [16], which shows that no NSP weakly representing the System T recursor can be definable in . The proof of this theorem is already quite intricate, and that of the present theorem adds some further ingredients. The reader may therefore find it helpful to study the proof of [16, Theorem 6.3.27] in conjunction with the present one—however, the account given here will be technically self-contained, and we shall also offer a more extended motivational discussion here than we did in [16].1
We take the opportunity here to draw attention here to a small error in the proof of [16, Theorem 6.3.27]. In the penultimate sentence of the proof (on page 258), we claim that . For this, we use the previously established fact that ; in the context of the proof, it is natural to denote this by . However, one also wants that is distinct from all of , which need not be the case here.
The problem is readily fixed by simply adding, at the point at which each is selected (for ), the further requirement that . For this, we need to add 1 to the lower bounds on the moduli from earlier in the proof, so that we take , , etc. Then, when picking the path through the tree for at the bottom of page 256, we should start by defining (so that actually ), then insert the requirements that differ from . (In the last line of page 256, was originally intended to read , but should now be modified to , .)
In the third-to-last line of page 257, the claim that now holds even when .
We start with an informal outline of our argument. Suppose that Φ is any genuine (simplified, weak) bar recursor as per Definition 21, and that Ψ is some LWF procedure purported to be such a bar recursor. We shall set and , so that is also LWF by Theorem 9(i). Our task will be to find some particular -definable arguments , such that . Since Φ here is an arbitrary bar recursor, this will show that Ψ is not a bar recursor after all.
The key idea is that Ψ, being LWF, will only be prepared to nest calls to G to a finite depth along any specified computation path. On the other hand, Φ, being a genuine bar recursor, must be willing to nest such calls to any depth required, as dictated by . In order to manifest an extensional difference between and , we therefore wish to construct an F such that that goes deeper on some path than is willing to explore, together with a G that forces the computation of to explore precisely this path. In this way, we can arrange that the computation of retrieves from within G some numerical value K that is not discoverable by , and propagates it to the top level.
Much of the proof is aimed at acquiring a sufficient grasp of the behaviour of that we can guarantee that does not return this value K. Our approach to this will be similar to that in [16, Theorem 6.3.27]. Assuming for the moment that we know how to obtain a suitable F, we shall start by considering the computation of for a certain very simple functional . Suppose that this evaluates to some number c. By analysing this and some related computations in detail, we shall discover a set of properties of that suffice to secure this computation, in the sense that for any other G with these properties, a precisely similar computation will go through, yielding the same result c. Put another way, we shall find a certain neighbourhood of such that for all we have . Moreover, the construction of will be so arranged that it is possible to pick some which forces to explore beyond the reach of in the manner suggested above. Indeed, by choosing such a with some care, we can ensure that evaluates to a number K chosen to be different from c. This establishes the required difference between and .
The main new ingredient, not present in the proof of [16, Theorem 6.3.27], concerns the way in which a suitable argument F is chosen. As indicated above, we want F to represent a well-founded tree that ‘undercuts’ the tree explored by in a certain computation; on the other hand, the computation performed by will itself depend partly on the argument F that we give it. This apparent circularity suggests that we should try to arrive at a suitable F (which we call ) by a process of successive approximation in tandem with our analysis of the computation of . This will allow us to ensure that undercuts with respect to the computation of itself.
More specifically, our proof will be structured as follows. In Section 3.1 we begin with some very simple functionals and , of which the latter will serve as the first step in the iterative construction of a suitable F. By analysing the computation of , initially just at the ‘top level’ (that is, without delving into the computations of the type 1 arguments passed to and ), we are able to glean some ‘neighbourhood information’ about which helps to secure aspects of this computation (and will also secure the corresponding computation for once the latter has been constructed). In the course of this, we will also have replaced by the next iteration .
However, the information about gathered so far does not by itself suffice to secure the entire computation: the top-level computation will typically rely on certain information about the arguments passed to F and G; and since these may themselves involve calls to G, some further constraints on may be needed to secure this information. We are thus led to repeat our analysis for certain subcomputations associated with the arguments to F and G—and so on recursively to whatever depth is required. This is done in Section 3.2.
A key step in the proof is to observe that since is LWF, this entire construction will eventually bottom out in a situation where no further subcomputations need to be analysed (there is a crucial appeal to König’s lemma here). We record what happens at this final stage of the construction in Section 3.3.
At the end of this computation analysis, we are left with two things. First, in the course of the analysis, the value of F we are considering will have been successively refined via an approximation process, and at the end we are able to fix on the definitive value (denoted by ) which we shall use to obtain a contradiction. Second, our analysis as a whole generates enough ‘neighbourhood conditions’ on to secure the entire computation: that is, we obtain a certain neighbourhood containing such that for any we have . The definition of together with this key property are established in Section 3.4.
The remainder of the proof proceeds along the lines already indicated. In Section 3.5, we draw on the above analysis to construct a certain procedure designed to force to explore parts of beyond the reach of . In Section 3.6 we verify the required properties of , namely that (so that ) and also that yields some value K different from c. Since this latter fact will hold for any genuine bar recursor Φ, this establishes that Ψ is not a genuine bar recursor.
We now proceed to the formal details of the proof.
Computation analysis: The top level
As indicated above, we begin by supposing that are simplified weak Kohlenbach bar recursors in the sense of Definition 21, and assuming for contradiction that Ψ is LWF. We set (or more formally ), and similarly . Clearly is LWF by Theorem 9(i).
In general, if t is any NSP term possibly containing , free, and , we shall write for the closed term obtained from t by instantiating F, G to , and then evaluating. (For instance, if t is a procedure then formally .)
To start our construction, we consider the -definable procedures
The purpose of the doubling in the definition of is hard to motivate here, but will emerge in Section 3.6. The functional represents a very simple well-founded tree: note that is not a leaf in , but is a leaf for every . Note too that the label on such a leaf node tells us the position of the node in the tree: this will be useful later for ensuring that certain numbers arising from different parts of the tree are always distinct.
The definition of simplified weak bar recursor now implies that now evaluates to a certain , or more formally to . (In fact , but we will not need this information.) By continuity of application, we may pick large enough that , where
(extending our notation for expressions in an obvious way). Note that . We shall actually use (rather than ) as the first step in our approximative construction of a suitable F.
Let us now look at the computation of . This will take the form of a head reduction of , and by inspection of the reduction rules in Section 2.2, it is clear that this will follow a path through the syntax tree of consisting of a finite sequence of calls to F or G (in any order), and leading to a leaf c. For example, such a path might have the form
where the and are themselves type 1 procedures which appear syntactically within and which may contain F, G as free variables (the superscript indicates that we are here analysing the computation at ‘level 0’). We can view the tracing of such a path through Ψ as the ‘top level computation’; in addition to this, there will be subcomputations showing (for instance) that evaluates to and evaluates to ,
Let be the complete list of such procedures appearing as arguments to F along this computation path, with the corresponding outcomes when F, G are instantiated to , . Likewise, let be the list of procedures appearing as arguments to G on this path, with the corresponding outcomes.
Of course, when and , the procedures and will be interrogated only on the argument 0. This suggests that in order to ‘secure’ the whole computation, we will also want to analyse the computations of and for each i. In fact, we shall do more: in order to give ourselves sufficient room for manoeuvre to construct the contrary example below (with the assurance of a similar evaluation behaviour for ), we shall analyse the behaviour of each on all integer arguments z up to a certain modulus. In fact, it will suffice to take
Again, this condition is hard to motivate at this stage; the reason for it will emerge during the construction of in Section 3.5, at the point where we select , the first step in our critical path through .
In order to proceed further, we need to extend our approximation to F. First, extend the procedure to a -definable :
(It is an easy exercise to verify that this is indeed -definable.) The idea is that will be a leaf node in when , but elsewhere will have depth 2.
We now consider the computation of . Since , this follows the same path through as before and features syntactically the same type 1 procedures and and the same outcomes , . Furthermore:
(i) For anyand, the evaluation ofyields a natural number, which we denote by.
(ii) For anyand, the evaluation ofyields a natural number, which we denote by.
(i) Suppose for contradiction that for some i, z, and let . Clearly is -definable. Also in the extensional preorder on NSPs, so by Theorem 6 we have
Moreover, for each application (respectively ) occurring before in the path in question, we have (respectively ), whence it is clear that is undefined. But this contradicts Proposition 22, since both , are -definable, is well-founded and .
The proof of (ii) is precisely similar. □
We shall make use of part (i) of the above lemma for all , and of part (ii) only when . (The apparently superfluous use of z in the latter case is intended to mesh with a more general situation treated below.)
We may now make explicit some significant properties of in the form of neighbourhoods, using the information gleaned so far. For each , define
Clearly for each i, because interrogates its argument only at 0. Also for each . This completes our analysis of the computation at top level; we shall refer to this as the depth 0 analysis.
The idea is that the sets will form part of a system of neighbourhoods recording all the necessary information about ; we will then be free to select any from the intersection of these neighbourhoods knowing that the computation will proceed as before. As things stand, the neigbourhoods do not achieve this: for an arbitrary G in all these neigbourhoods, there is no guarantee that the value of each at and G will agree with its value at and (and similarly for each ). To secure the whole computation, we therefore need a deeper analysis of these subcomputations in order to nail down the precise properties of on which these rely.
Computation analysis: The step case
The idea is that we repeat our analysis for each of the finitely many computations of
The analysis at this stage is in fact illustrative of the general analysis at depth w, assuming we have completed the analysis at depth . For notational simplicity, however, we shall concentrate here on the depth 1 analysis, adding a few brief remarks on the depth 2 analysis in order to clarify how the construction works in general.
First, since each of the above computations yields a numeral or as appropriate, we may choose such that all these computations yield the same results when is replaced by
Note in passing that no longer suffices here: there will be computations of values for that did not feature anywhere in the original computation of .
Everything we have said about the main computation and its subcomputations clearly goes through with replaced by . So let us consider the shape of the computations of
At top level, each of these consists of a finite sequence of applications of and (in any order), leading to the result or . Taking all these computations together, let and respectively denote the (occurrences of) type 1 procedures to which and are applied, with and the corresponding outcomes. Although we will not explicitly track the fact in our notation, we should consider each of the and as a ‘child’ of the procedure or from which it arose. Note that if is a child of (for example), then just as appears as a subterm within the syntax tree of , so appears as a subterm within the syntax tree of . Thus, each of the and corresponds to a path in with at least two left branches.
We now select a suitable modulus for our analysis of the . Choose
(Again, the reason for this choice will emerge in Section 3.5.) Extend to the -definable functional
Replacing by preserves all the structure established so far, and just as in Lemma 25 we have that at , yields a numeral for each and ; similarly at , yields a numeral for each and . (In fact, it is superfluous to consider in cases where , but it simplifies notation to use 2 here as our uniform modulus of inspection for the .) We may now augment our collection of neighbourhoods by defining
for each ; note once again that and that for each i. This completes our analysis of the computation at depth 1.
At the next stage, we choose so that the above all holds with replaced by
We now repeat our analysis for each of the computations of
Having identified the relevant type 1 procedures and that feature as arguments to F and G, we pick
and use this to define suitable sets , for . By this point, it should be clear how our construction may be continued to arbitrary depth.
Computation analysis: The bottom level
The crucial observation is that this entire construction eventually bottoms out. Indeed, using h as a symbol that can ambivalently mean either f or g (and likewise H for F or G), we have that for any sequence of type 1 procedures where each is a child of , the syntax tree of contains the descending sequence of subterms . Since is LWF by assumption, any such sequence must eventually terminate. Moreover, the tree of all such procedures is finitely branching, so by König’s lemma it is finite altogether.
Let us see explicitly what happens at the last stage of the construction. For some depth d, we will have constructed the , , , as usual, along with , , the numbers , and the neighbourhoods , but will then discover that : that is, none of the relevant computations of or (relative to and ) themselves perform calls to F or G.
At this point, we may settle on as the definitive version of F to be used in our counterexample, and henceforth call it . Explicitly:
Clearly is -definable and for . It is also clear from the above definition how represents a certain well-founded tree of depth . Note that if then ; indeed is a leaf in . It is this portion of the tree, not visited by any of the computations described so far, that we shall exploit when we construct our counterexample .
The critical neighbourhood of
We may now define the critical neighbourhood by
Clearly by construction. Moreover, the following lemma shows that provides enough constraints to secure the result of the entire computation:
For alland all, we have:
for alland.
for alland.
for all.
for all.
.
We prove claims 1–4 simultaneously by downwards induction on w. For , claims 1 and 2 hold because the computations in question make no use of or G. For any w, claim 1 implies claim 3: was chosen so that (among other things) is defined; moreover, interrogates its argument only on at most, so the established values of for suffice to ensure that , and hence that . Likewise, claim 2 implies claim 4, since by hypothesis, and the established values of secure that (at and G).
Assuming claims 3 and 4 hold for , it is easy to see that claims 1 and 2 hold for w: the relevant top-level computation may be reconstituted from left to right leading to the result or . Applying the same argument one last time also yields claim 5. □
The counterexample
It remains to construct our contrary example . The idea is that will be chosen so that according to the definition of simplified bar recursion, some value will be generated at depth of the tree and then propagated up to the surface of the computation via nested applications of . We work with paths beyond the horizon defined by to ensure that we do not encounter a leaf prematurely, and also exploit the choice of moduli to ensure that the type 1 functions at intermediate levels steer clear of the sets .
Recall that Φ is assumed to be a genuine simplified bar recursor within . Set . If x is any sequence code and , we shall write for the sequence code , so that is the number computed by .
Since and the leaf function has been fixed at , we have that for any sequence code x, will take one of the values
according to where a leaf of appears in the sequence . In particular, for any fixed j, if we know that , we can recover from and even from , where denotes the unique odd number such that for some t. We shall write for the result of appending t occurrences of 0 to the sequence number x; note that will have the value for some t.
We construct a finite path through the tree for in the following way, along with associated numbers . Start by setting . Next, note that the mappings and are injective; so because , we may pick with such that:
differs from (more precisely from ) for each ,
differs from .
Likewise, the mapping is injective, so since we may pick with such that
is different from all and where , ,
is different from and .
In general, we pick with such that
is different from all with and ,
is different from .
In each case, the first condition ensures that the type 1 function steers clear of the sets , so that the functional to be defined below remains within . The second condition will ensure that the nested calls to do not interfere with one another in their role of propagating the special value K. Since for each , we have that is a leaf of .
We now take K to be some natural number larger than any that has featured in the construction so far, and in particular different from c, and define
Here we understand i, j as ‘pattern variables’ that catch all cases not handled by the preceding clauses. In particular, the clauses , mean that unless g possesses some special property explicitly handled by some other clause, we will have . It is straightforward to verify that is -definable, bearing in mind the availability of in (see the discussion in Section 2.1.1).
Properties of
We first check that falls within the critical neighbourhood:
, whence.
Suppose and ; we will show . Consider an arbitrary (note that g is not assumed to represent a total function); we want to show that . From the definition of we have , so for , we have by choice of . If also for each then as required. If for some , then . However, since we have , and K was assumed to be larger than this, so once again .
We now work towards showing that, by contrast, . Set , and for , denote by .
for all.
Recall that , which has the form where and is a leaf for , so that . Note also that if then , which is distinct from (this is the point of the doubling in the definition of ), and also from all the other since are all distinct.
We may now see by reverse induction on that . When , this holds because is a leaf for so . Assuming this holds for with , because is not a leaf we have
using the observation that is distinct from all of the .
In particular, , so the lemma is established. □
for all.
By reverse induction on w. For the case , we have by the previous lemma that , and since is not a leaf for , we have
For , again we have by the previous lemma that , and the induction hypothesis gives us . Since is not a leaf for , we have
establishing the lemma. □
In particular, when we have . Combining this with Lemma 27, we have
Since this argument applies for any genuine weak simplified bar recursor Ψ, we may conclude that Ψ is not a restricted bar recursor after all. This completes the proof of Theorem 24.
Other models
Finally, we show how our non-definability result now transfers readily to settings other than , both partial and total. The combined message of these results will be that bar recursion is not computable in or W in any reasonable sense whatever, however one chooses to make such a statement precise.
Partial models
It is relatively easy to transfer Theorem 24 to other ‘partial’ settings, by which we here mean simply-typed λ-algebras A with . As a first step, it is convenient to detach our main theorem from and present its content in purely syntactic terms.
Let be a closed term of . Using the program ‘’ introduced in Section 2.3, and reinstating the hat notation for programming language numerals, we may say a sequence satisfies the Kohlenbach bar condition w.r.t. F if the closed terms
evaluate to the same numeral; we may thus define to be the tree of sequences such that no proper prefix of satisfies this bar condition. It is clear that this purely syntactic definition of agrees with Definition 16 for NSPs: if is the denotation of F in , then by the adequacy of .
This allows us to reformulate the content of Theorem 24 syntactically as follows. Here we write = to mean that the closed programs on either side evaluate to the same numeral.
There is no closedtermsuch that the following hold for all closedtermswithwell-founded, and for all:
If such a term existed, then by adequacy of , would be a definable simplified weak Kohlenbach recursor, contradicting Theorem 24. □
Now suppose A is any simply typed λ-algebra equipped with elements , , , , , of the appropriate types, such that the induced interpretation of in A is adequate: that is, for closed programs and , we have iff . Note that this requires to contain elements other than the numerals, since in the presence of , diverging programs are possible. In most cases of interest, we will have : typical examples include the Scott model of partial continuous functionals, its effective submodel , the model of PCF-sequential functionals (arising as the extensional quotient of ) and its effective submodel of PCF-computable functionals.
In this setting, we have a notion of -definable element of A, so Definitions 16, 18 and 21 immediately relativize to A, giving us the notion of a (simplified) weak (Spector or Kohlenbach) bar recursor within A. We are now able to conclude:
No simplified weak Kohlenbach bar recursor withinAcan bedefinable.
If were a term of defining a simplified weak Kohlenbach bar recursor in A, then by adequacy of , would satisfy the conditions in Theorem 30, a contradiction. □
The corresponding results for Spector bar recursion follow by Proposition 20 relativized to A. It is also clear that we obtain similar results with W in place of .
Total models
We now consider the situation for total type structures such as and . We work in the general setting of a simply-typed total combinatory algebra A with .
Our formulation for total models will have a character rather different from the above: since no suitable element will be present in A, we cannot induce an interpretation straightforwardly from an interpretation of the constants—indeed, there will be terms of that have no denotation in A. Instead, we resort to an approach more in the spirit of Kleene’s original definition of computability in total settings, adapting the treatment in [16]. It is best here to assume that A is extensional: in fact, we shall assume that each is a set of functions . It is well-known that this implies that A is a typed λ-algebra (see [16, Section 4.1]). We shall furthermore assume that A is a model of : that is, A contains elements , , , and for σ of level 0 satisfying the usual defining equations for these constants. (Note that in the total extensional setting, there is no real difference between and , or between and , and the operator is redundant. We shall henceforth use in this context as it is directly a sublanguage of .)
First, we recall that every term is -equivalent to one in long-normal form—that is, to a β-normal term in which every occurrence of any variable or constant f is fully applied (i.e. appears at the head of a subterm of type ). We shall define a (partial) interpretation in A for terms of this kind, and will in general write for the long -normal form of M. (The correspondence between β-normal forms and Kleene-style indices is explained in [16, Section 5.1]. Here we use long -normal forms in this role because of our treatment of and as first-class constants.)
For a given term M, a valuation ν for M will be a map assigning to each free variable within M an element . We shall define a partial interpretation assigning to certain terms and valuations ν for M an element . This takes the form of an inductive definition of the relation , where M is a -normal form of some type σ, ν is a valuation for M, and .
.
If then and , where is truncated subtraction.
If and , then .
If and , then .
If and , then .
If and , then .
If and , then .
If , and , then .
If and for all , where , then .
If and for each , then .
Other ways of treating the recursors would be possible: the definition chosen above errs on the side of generosity, in that it is possible e.g. for to be defined even when is not. Note too that we are not assuming that all the System T operators are actually present in A—if they are not, there will of course be many System T terms whose denotations in A are undefined.
We say a partial function is computable if there is a closed term with free variables among such that for all and all we have
where ≃ means Kleene equality.
Comparing this with the treatment in [16, Section 5.1], it is clear that if we restrict our language to , the computable partial functions over A obtained as above coincide exactly with Kleene’s μ-computable partial functions. We also note in passing that if the language is extended with the operator described in [16, Section 5.1], the computable partial functions are exactly the Kleene S1–S9 computable ones.
Next, we may adapt earlier definitions to say what it means to be a bar recursor with respect to A. Note that since A is a model of , all functions as defined in Section 2.3 are present in .
For any , the Kohlenbach tree consists of all such that no proper prefix of satisfies .
A partial function is a simplified Kohlenbach bar recursor if for all with well-founded, and for all , we have
We shall take it to be part of the meaning of the latter condition that the relevant function is indeed present in ; this is in effect a further hypothesis on A which holds in all cases of interest.
We mention a few examples, all of which fall within the scope of Theorem 36 below:
In the Kleene–Kreisel model , it is the case for any that is well-founded, and indeed a simplified bar recursor Φ is present within itself, as an element of . It is known, furthermore, that such an element is Kleene S1–S9 computable (see [16, Section 8.3]).
By contrast, in the model , there are functionals F such that is not well-founded (such functionals arise from the Kleene tree as explained in [16, Section 9.1]), and consequently it is not possible to find a total bar recursor within itself. Nonetheless, partial simplified bar recursors as defined above do exist and are Kleene computable, by the same algorithm as for . The situation is in fact precisely similar for the full set-theoretic model : thus, partial bar recursors in the spirit of Definition 15 are Kleene computable over .
Another model of a quite different character is Bezem’s type structure of strongly majorizable functionals [5], which has been found to be valuable in proof theory. Here, as in , a bar recursor lives as a total object within the model itself—despite the presence of discontinuous type 2 elements in the model.
We shall show that no simplified Kohlenbach bar recursor for A can be computable in the sense above. This will follow easily from Theorem 30 once we have established the ‘adequacy’ of our partial interpretation . This we do by means of a standard logical relations argument. For each σ, let us define a relation between closed terms and elements as follows:
iff .
iff for all and , implies .
We often omit the type annotations and may refer to any of the as R.
Ifandfor allfree in M, then.
By induction on the generation of via clauses 1–10 above. The cases for clauses 1–4 are trivial, and those for clauses 5–8 are very straightforward, using the fact that any term M is observationally equivalent to by the context lemma.
For clause 9, suppose we have arising from for all , and suppose also that for all free in . We wish to show that : that is, that for all and , implies . So suppose . By assumption, we have and for all i, so by the induction hypothesis. The desired conclusion follows, since
and it is easy to see by induction on types that if and then .
For clause 10, suppose we have arising from and for each i, and suppose again that for all i. Writing ∗ for the substitution , we have , so it will suffice to show that . But we have where , and also for each i by the induction hypothesis, so by definition of where σ is the type of , we have as required. □
The converse to Lemma 34 is not true. For instance, if , and , then and , but is undefined because receives no denotation. In this sense, computability in a total model is a stricter condition than it would be in a partial model. It is therefore not too surprising that no bar recursor for a total model can be computable.
Recall that we are assuming that A is a model of , in the sense that A contains suitable elements , , , satisfying the relevant equations, giving rise via the λ-algebra structure of A to an interpretation of which we shall denote by I. We may now verify that our two ways of interpreting terms are in accord:
Suppose M is any long-normalterm, andis any valuation for M. Thenis defined and is equal to.
A routine induction on the structure of M. □
We now have all the pieces needed for the main result of this section, which establishes Corollary 6.3.33 of [16]. It is worth noting that the proof makes use of a bar induction principle at the meta-level, namely that if is a well-founded tree as defined in Section 2.3, then
for a certain predicate P to be specified in the course of the proof. (This principle also featured in the proof of Proposition 19.) This is of course unproblematic if our metatheory is classical; there may also be weaker metatheories that suffice for our arguments, but we will not enter into an investigation of this here.
No simplified Kohlenbach bar recursor forAcan becomputable.
Suppose B were a term with free variables , , defining a simplified Kohlenbach bar recursor as above. We claim that satisfies the conditions of Theorem 30, yielding a contradiction. Indeed, suppose are closed terms with well-founded. Construing , as terms, we obtain elements by Lemma 35, and it is clear from Lemma 34 that = .
Now suppose . We now show by meta-level bar induction on that for all such , is defined and agrees with the value of , and moreover the latter satisfies the relevant condition of Theorem 30.
First, if , then by Definitions 32 and 33 we have
Now by Lemma 34 we have , and , so by the same again we have , meaning that
Hence satisfies the first condition of Theorem 30, and all parts of the induction claim are established.
Now suppose that , where each child , z satisfies the induction claim. We first show that
For this, it suffices to show that if and (i.e. ), then
But this holds by the induction hypothesis along with the observational equivalence
Since , we may conclude that
so that the term on the left evaluates to (the numeral for) the value on the right. But also by Definitions 32 and 33 we have
In particular, is defined, so using Lemma 34 as before, we see that also evaluates to . Thus the induction claim is established for .
We have thus shown that satisfies the conditions of Theorem 30, so a contradiction with that theorem is established. □
Clearly, similar results hold for Spector bar recursion or for the language W.
Footnotes
Acknowledgements
I am grateful to Martín Escardó, Dag Normann, Paulo Oliva and Thomas Powell for valuable input, and to the anonymous reviewer for helpful suggestions for improvement.
References
1.
S.Abramsky, R.Jagadeesan and P.Malacaria, Full abstraction for PCF, Information and Computation163(2) (2000), 409–470. doi:10.1006/inco.2000.2930.
2.
S.Berardi, P.Oliva and S.Steila, An analysis of the Podelski-Rybalchenko termination theorem via bar recursion, Journal of Logic and Computation (2015).
3.
U.Berger, Minimization vs. recursion on the partial continuous functionals, in: In the Scope of Logic, Methodology and Philosophy of Science, Cracow, August 1999, P.Gärdenfors, J.Woleński and K.Kijania-Placek, eds, Kluwer, Dordrecht, 2002, pp. 57–64.
4.
J.Bergstra, Continuity and computability in finite types, Ph.D. dissertation, University of Utrecht, 1976.
5.
M.Bezem, Strongly majorizable functionals of finite type: A model for bar recursion containing discontinuous functionals, Journal of Symbolic Logic50 (1985), 652–660. doi:10.2307/2274319.
6.
M.H.Escardó and P.Oliva, Computing Nash equilibria of unbounded games, in: Proceedings of the Turing Centenary Conference, EPiC Series, Vol. 10, Manchester, 2012, pp. 53–65.
7.
M.H.Escardó and P.Oliva, Bar recursion and products of selection functions, Journal of Symbolic Logic80(1) (2015), 1–28. doi:10.1017/jsl.2014.82.
8.
J.Hedges, P.Oliva, E.Winschel, V.Winschel and P.Zahn, Higher-order decision theory, in: Proceedings of the 5th International Conference on Algorithmic Decision Theory, 2017.
9.
J.M.E.Hyland, Recursion Theory on the Countable Functionals, D.Phil. Dissertation, University of Oxford, 1975.
10.
J.M.E.Hyland and C.-H.L.Ong, On full abstraction for PCF: I, II and III, Information and Computation163 (2000), 285–408. doi:10.1006/inco.2000.2917.
11.
S.C.Kleene, Recursive functionals and quantifiers of finite types I, Transactions of the American Mathematical Society91(1) (1959), 1–52.
12.
U.Kohlenbach, Theory of Majorizable and Continuous Functionals and their Use for the Extraction of Bounds from Non-Constructive Proofs: Effective Moduli of Uniqueness for Best Approximations from Ineffective Proofs of Uniqueness, Ph.D. dissertation, Frankfurt, 1990.
13.
U.Kohlenbach, Applied Proof Theory: Proof Interpretations and Their, Use in Mathematics, Springer-Verlag, 2008.
14.
G.Kreisel, Interpretation of analysis by means of constructive functionals of finite types, in: Constructivity in Mathematics: Proceedings of the Colloquium Held in Amsterdam, 1957, A.Heyting, ed., North-Holland, Amsterdam, 1959, pp. 101–128.
15.
G.Kreisel, Set theoretic problems suggested by the notion of potential totality, in: Infinitistic Methods, Proceedings of the Symposium on Foundations of Mathematics, Pergamon Press, Warsaw, 1959, pp. 103–140, Oxford, 1961.
16.
J.Longley and D.Normann, Higher-Order Computability, Theory and Applications of Computability, Springer-Verlag, 2015.
17.
J.R.Longley, Bar recursion is not T + min definable, Informatics Research Report EDI-INF-RR-1420, University of Edinburgh, 2015.
18.
J.R.Longley, The recursion hierarchy for is strict, Logical Methods in Computer Science14(3:8) (2018), 1–51.
19.
J.R.Longley, On the relative expressive power of some sublanguages of , in preparation.
P.Oliva and T.Powell, A constructive interpretation of Ramsey’s theorem via the product of selection functions, Mathematical Structures in Computer Science25(8) (2015), 1755–1778. doi:10.1017/S0960129513000340.
22.
G.D.Plotkin, LCF considered as a programming language, Theoretical Computer Science5(3) (1977), 223–255. doi:10.1016/0304-3975(77)90044-5.
23.
G.D.Plotkin, Full abstraction, totality and PCF, Mathematical Structures in Computer Science9(1) (1999), 1–20. doi:10.1017/S0960129598002692.
24.
V.Yu.Sazonov, Expressibility in D. Scott’s LCF language, Algebra and Logic15(3) (1976), 192–206. doi:10.1007/BF01876321.
25.
B.Scarpellini, A model for barrecursion of higher types, Compositio Mathematica23 (1971), 123–153.
26.
C.Spector, Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, in: Recursive Function Theory, Proceedings of Symposia in Pure Mathematics, Vol. 5, J. Dekker, ed., AMS, Providence, 1962, pp. 1–27. doi:10.1090/pspum/005/0154801.
