Type 2 recursion theory

In [5], Kleene extended previous notions of computations to objects of higher finite type in the maximal type-structure of functionals given by:Tp(0) = N = the natural numbers,Tp(n + 1) = NTp(n) = the set of total maps from Tp(n) to N.He gave nine schemata, S1–S9, for describing algorithms for computations from a finite list of functionals, and indices to denote these algorithms. It is generally agreed that S1-S9 give a natural concept of computations in higher types.The type-structure of countable functions, Ct(n) for n ϵ N, was first developed by Kleene [6] and Kreisel [7]. It arises from the notions of ‘constructivity’, and has been extensively studied as a domain for higher type recursion theory. Each countable functional is globally described by a countable amount of information coded in its associate, and it is determined locally by a finite amount of information about its argument. The countable functionals are well summarised in Normann [9], and treated in detail in Normann [8].The purpose of this paper is to discuss a generalisation of the countable functionals, which we shall call the countably based functions, Cb(n) for n ϵ N. It is suggested by the notions of ‘predicativity’, in which we view N as a completed totality, and build higher types on it in a constructive manner. So we shall allow quantification over N and include application of 2E in our schemata. Each functional is determined locally by a countable amount of information about its argument, and so is globally described by a continuum of information coded in its associate, which will now be a type-2 object. This generalisation, obtained via associates, was proposed by Wainer, and seems to reflect topological properties of the countable functionals.

Download Full-text

Type two partial degrees

Journal of Symbolic Logic ◽

10.2307/2273500 ◽

1978 ◽

Vol 43 (4) ◽

pp. 623-629

Author(s):

Ko-Wei Lih

Keyword(s):

Recursive Function ◽

Natural Extension ◽

Degree Theory ◽

Recursion Theory ◽

Natural Numbers ◽

Partial Functions ◽

Reduction Procedure ◽

Turing Reducibility

Roughly speaking partial degrees are equivalence classes of partial objects under a certain notion of relative recursiveness. To make this notion precise we have to state explicitly (1) what these partial objects are; (2) how to define a suitable reduction procedure. For example, when the type of these objects is restricted to one, we may include all possible partial functions from natural numbers to natural numbers as basic objects and the reduction procedure could be enumeration, weak Turing, or Turing reducibility as expounded in Sasso [4]. As we climb up the ladder of types, we see that the usual definitions of relative recursiveness, equivalent in the context of type-1 total objects and functions, may be extended to partial objects and functions in quite different ways. First such generalization was initiated by Kleene [2]. He considers partial functions with total objects as arguments. However his theory suffers the lack of transitivity, i.e. we may not obtain a recursive function when we substitute a recursive function into a recursive function. Although Kleene's theory provides a nice background for the study of total higher type objects, it would be unsatisfactory when partial higher type objects are being investigated. In this paper we choose the hierarchy of hereditarily consistent objects over ω as our universe of discourse so that Sasso's objects are exactly those at the type-1 level. Following Kleene's fashion we define relative recursiveness via schemes and indices. Yet in our theory, substitution will preserve recursiveness, which makes a degree theory of partial higher type objects possible. The final result will be a natural extension of Sasso's Turing reducibility. Due to the abstract nature of these objects we do not know much about their behaviour except at the very low types. Here we pay our attention mainly to type-2 objects. In §2 we formulate basic notions and give an outline of our recursion theory of partial higher type objects. In §3 we introduce the definitions of singular degrees and ω-consistent degrees which are two important classes of type-2 objects that we are most interested in.

Download Full-text

Selection in abstract recursion theory

Journal of Symbolic Logic ◽

10.1017/s0022481200051847 ◽

1976 ◽

Vol 41 (1) ◽

pp. 153-158 ◽

Cited By ~ 3

Author(s):

L. A. Harrington ◽

D. B. Macqueen

Keyword(s):

General Result ◽

Recursion Theory ◽

Normal Type ◽

Arbitrary Integer ◽

Selection Theorem ◽

Arbitrary Type ◽

Direct Generalization ◽

Existential Quantification

In [1] Gandy established the following selection theorem for recursion in type-2 objects.Theorem. Let F be a normal type-2 object. Then it is possible to select (uniformly and effectively in F) an integer from each nonempty set of integers semirecursive in F.Notice that this really asserts that the predicates semirecursive in F are closed under existential quantification over type-0. Moschovakis [6] has essentially proven this theorem for F of arbitrary type.In [2] Grilliot stated a powerful generalization of Gandy's result, namely:Grilliot's Selection Theorem. Let F be a normal type-(n + 2) object (n an arbitrary integer). Then it is possible to select (uniformly and effectively in F) a nonempty recursive in F subset of each nonempty semirecursive in F set oftype-(n − 1) objects.Notice again that this actually says that predicates semirecursive in F are closed under quantification over type-(n − 1) objects.Despite the similarity of these two results, Gandy and Grilliot proposed rather different methods of proof. Furthermore, the proof that Grilliot presented in [2] contains an error which cannot easily be corrected. (We will comment on the nature of this error at the end of §1.) Fortunately, however, Grilliot's theorem is valid. We will present a proof of Grilliot's selection theorem which is a direct generalization of the proof of Gandy's theorem given in [6]. In fact, we will prove a general result (the theorem stated in §2) which subsumes both Gandy's and Grilliot's results.

Download Full-text

Effective discontinuity and a characterisation of the superjump

Journal of Symbolic Logic ◽

10.2307/2274221 ◽

1985 ◽

Vol 50 (2) ◽

pp. 349-358 ◽

Cited By ~ 2

Author(s):

John P. Hartley

Keyword(s):

Recursion Theory ◽

Type 3 ◽

Effective Proof

One of the most fundamental results of higher-type recursion theory was first proved by Thomas Grilliot [3]. He showed that the functional embodying number quantification, 2E, is computable from a type-2 object F if and only if F has an effective discontinuity. For the background to this work we recommend Normann's book [9] or his summary [10], and for an example of its many applications Normann-Wainer [11].The purpose of §1 of this paper is to give an effective proof of the “only if” part of this result: i.e. a construction of a discontinuity of F from the information 2E = {e}F. This contrasts with Grilliot's argument which is topological and nonconstructive, and shows that “Grilliot's trick” for computing 2E from a discontinuity of F is essentially the only method.We then apply the method to two more general situations in which it gives new results. In §2 we treat type-3 objects in which 3E is computable (assuming AC and CH), and obtain a strengthening of the result of Hartley [5, §5]. In §3 we consider the superjump and characterise it as the least among a class of functionals with a particular sort of family of discontinuities.

Download Full-text

On characterizing Spector classes

Journal of Symbolic Logic ◽

10.2307/2272264 ◽

1975 ◽

Vol 40 (1) ◽

pp. 19-24 ◽

Cited By ~ 5

Author(s):

Leo A. Harrington ◽

Alexander. S. Kechris

Keyword(s):

Recursion Theory ◽

Partial Answer ◽

Normal Type ◽

Abstract Characterization ◽

Structural Characterizations

We study in this paper characterizations of various interesting classes of relations arising in recursion theory. We first determine which Spector classes on the structure of arithmetic arise from recursion in normal type 2 objects, giving a partial answer to a problem raised by Moschovakis [8], where the notion of Spector class was first essentially introduced. Our result here was independently discovered by S. G. Simpson (see [3]). We conclude our study of Spector classes by examining two simple relations between them and a natural hierarchy to which they give rise.The second part of our paper is concerned with finding structural characterizations of classes of relations on the reals in the spirit of Moschovakis [7]. Our main result provides a single abstract characterization for the class of relations on the reals and the 2-envelope of 3E, the first one being valid if projective determinacy is true, the second if V = L is true.

Download Full-text