Hostname: page-component-7c8c6479df-nwzlb Total loading time: 0 Render date: 2024-03-28T02:13:59.491Z Has data issue: false hasContentIssue false

The hereditary partial effective functionals and recursion theory in higher types1

Published online by Cambridge University Press:  12 March 2014

G. Longo
Affiliation:
Università di Pisa, Pisa, Italy
E. Moggi
Affiliation:
Università di Pisa, Pisa, Italy

Abstract

A type-structure of partial effective functionals over the natural numbers, based on a canonical enumeration of the partial recursive functions, is developed. These partial functionals, defined by a direct elementary technique, turn out to be the computable elements of the hereditary continuous partial objects; moreover, there is a commutative system of enumerations of any given type by any type below (relative numberings).

By this and by results in [1] and [2], the Kleene-Kreisel countable functionals and the hereditary effective operations (HEO) are easily characterized.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1984

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.)

Footnotes

1

Research partially supported by Min. P.I. (fondi 60%) and, in part, by Consiglio Nazionale delle Ricerche (Comitato per la Matematica).

References

REFERENCES

[1]Ershov, Yu. L., The theory of A-spaces, Algebra and Logic, vol. 12 (1973), pp. 209232.CrossRefGoogle Scholar
[2]Ershov, Yu. L., Model C of partial continuous functionals, Logic Colloquium '76 (Gandy, R. O. and Hyland, J. M. E., editors), North-Holland, Amsterdam, 1977, pp. 455467.Google Scholar
[3]Giannini, P. and Longo, G., Effectively given domains and lambda-calculus semantics, Nota Scientifica S803, Università di Pisa, Pisa, 1983 (to appear).Google Scholar
[4]Kleene, S. C., Countable functionals, Constructhity in mathematics (Heyting, A., editor), North-Holland, Amsterdam, 1959, pp. 81100.Google Scholar
[5]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
[6]Longo, G., Hereditary partial effective functionals in any finite type(preliminary note), Forschungsinstitut der Mathematik, Eidgenössische Technische Hochschule, Zürich, 1982.Google Scholar
[7]Myhill, J. and Shepherdson, J., Effective operations on partial recursive functions, Zeitschrift für Mathematische Logik and Grundlagen der Mathematik, vol. 1 (1955), pp. 310317.CrossRefGoogle Scholar
[8]Normann, D., Recursion on the countable functionals, Lecture Notes in Mathematics, vol. 811, Springer-Verlag, Berlin, 1980.CrossRefGoogle Scholar
[9]Scott, D. S., Continuous lattices, Toposes, algebraic geometry and logic (Lawvere, F. W., editor), Lecture Notes in Mathematics, vol. 274, Springer-Verlag, Berlin, 1972, pp. 97136.CrossRefGoogle Scholar
[10]Scott, D. S., Lectures on a mathematical theory of computation, Oxford University Computation Laboratory Technical Monograph no. PRG-19, Oxford, 1981; revised version in Ordered sets (Rival, I., editor), Reidel, Dordrecht, 1982, pp. 677717.Google Scholar
[11]Visser, A., Numerations, λ-calculus & arithmetic, To H. B. Curry: essays on combinatory logic, lambda calculus and formalism (Hindley, R. and Seldin, J. P., editors), Academic Press, New York, 1980, pp. 259284.Google Scholar