Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-17T17:23:11.611Z Has data issue: false hasContentIssue false

The countably based functionals

Published online by Cambridge University Press:  12 March 2014

John P. Hartley*
Affiliation:
University of Leeds, Leeds LS2 9JT, England

Extract

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.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1983

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Bergstra, J., The continuous functionate and 2E, Generalised recursion theory. II (Fenstad, J.E., Gandy, R.O. and Sacks, G.E., Editors), North-Holland, Amsterdam, 1978, pp. 3954.Google Scholar
[2]Gandy, R.O. and Hyland, J.M.E., Computable and recursively countable functionals of higher type, Logic Colloquium 1976 (Gandy, R.O. and Hyland, J.M.E., Editors), North-Holland, Amsterdam, 1977, pp. 907938.Google Scholar
[3]Grilliot, T.J., On effectively discontinuous type-2 objects, this Journal, vol. 36 (1971), pp. 245248.Google Scholar
[4]Hyland, J.M.E., Filter spaces and continuous functionals, Annals of Mathematical Logic, vol. 16 (1979), pp. 101143.CrossRefGoogle Scholar
[5]Kleene, S.C., Recursive functionals and quantifiers of finite types. I, Transactions of the American Mathematical Society, vol. 91 (1959), pp. 152.Google Scholar
[6]Kleene, S.C., Countable functionals, Constructhity in mathematics (Heyting, A., Editor), North-Holland, Amsterdam, 1959, pp. 87100.Google Scholar
[7]Kreisel, G., Interpretation of analysis by means of functionals of finite type, Constructhity in mathematics (Heyting, A., Editor), North-Holland, Amsterdam, 1959, pp. 101128.Google Scholar
[8]Normann, D., Recursion on the countable functionals, Lecture Notes in Mathematics, vol. 811, Springer-Verlag, Berlin and New York, 1980.Google Scholar
[9]Normann, D., The recursion theory of the continuous functionals, Recursion theory: its generalisations and applications (Drake, F.R. and Wainer, S.S., Editors), London Mathematical Society Lecture Notes, vol. 45, Cambridge University Press, 1980, pp. 171183.CrossRefGoogle Scholar