The Kleene–Kreisel density theorem is one of the tools used to investigate the denotational semantics of programs involving higher types.We give a brief introduction to the classic density theorem, then show how this may be generalized to set theoretical models for algorithms accepting real numbers as inputs, and finally survey some recent applications of this generalization.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S. and Jung, A., Domain Theory, in S. Abramsky, D.M. Gabbay and T.S.E. Maibaum (eds.), Handbook of Logic in Computer Science, vol. 3, Clarendon Press (1994)
Amadio, R. M. and Curien, P. -L. , Domains and Lambda-Calculi, Cambridge University Press (1998)
Bauer, A., Escardó, M.H. and Simpson, A., Comparing Functional Paradigms for Exact Real-number Computation, in Proceedings ICALP 2002, Springer LNCS 2380, 488-500 (2002)
Berger, U., Totale Objekte und Mengen in der Bereichtheorie (in German), Thesis, München (1990)
DeJaeger, F., Calculabilité sur les Réels, Thesis, Paris VII (2003)
DiGianantonio, P., A Functional Approach to Computability on Real Numbers, Thesis, Università di Pisa - Genova - Udine, (1993)
DiGianantonio, P., Real number computability and domain theory, Inform. and Comput.127,11-25 (1996)
DiGianantonio, P., An abstract data type for real numbers, Theoret. Comput. Sci. 221,295-326 (1999)
Ershov, Yu. L., Maximal and everywhere defined functionals, Algebra and Logic 13, 210-225(1974)
Gandy, R.O. and Hyland, J.M.E., Computable and recursively countable functions of higher type, Logic Colloquium ’76, 407-438, North-Holland (1977)
Hyland, J.M.E., Recursion on the Countable Functionals, Dissertation, Oxford (1975)
Kleene, S. C., Recursive functionals and quantifiers of finite types I, Trans. Amer. Math. Soc. 91, 1-52 (1959)
Kleene, S. C., Countable Functionals, in A. Heyting (ed.) Constructivity in Mathematics,81-100, North-Holland (1959)
Kreisel, G. , Interpretation of Analysis by Means of Functionals of Finite Type, in A. Heyting (ed.) Constructivity in Mathematics, North-Holland, 101-128 (1959)
Longley, J.R., On the ubiquity of certain total type structures, Electr. Notes Theor. Com-put. Sci. 73, 87-109 (2004)
Longo, G. and Moggi, E., The hereditary partial effective functionals and recursion the-ory in higher types, J. Symbolic Logic 49, 1319-1332 (1984)
Milner, R., Fully abstract models for typed λ-calculi, Theoret. Comput. Sci. 4, 1-22 (1977)
Moldestad, J., Computations in Higher Types, Springer Lecture Notes in Mathematics No. 574, Springer Verlag (1977)
Normann, D., The continuous functionals; computations, recursions and degrees, Annals of Mathematical Logic 21, 1-26 (1981)
Normann, D., Computing with functionals - computability theory or computer science?, Bull. Symbolic Logic 12(1), 43-59, (2006)
Normann, D., Computability over the partial continuous functionals, J. Symbolic Logic 65,1133-1142 (2000)
Normann, D., The Cook-Berger problem - A guide to the solution, Electr. Notes Theor. Comput. Sci. 35, (2000)
Normann, D., The Continuous Functionals of Finite Types over the Reals, in K. Keimel, G.Q. Zhang, Y. Liu and Y. Chen (eds.) Domains and Processes, Kluwer Academic Publishers, 103-124, (2001)
Normann, D., Hierarchies of total functionals over the reals, Theoret. Comput. Sci. 316, pp. 137-151 (2004)
Normann, D., Definability and reducibility in higher types over the reals, to appear in the proceedings og Logic Colloquium ’03
Normann, D., Comparing hierarchies of total functionals, Logical Methods in Computer Science 1(2), (2005)
Platek, R. A., Foundations of Recursion Theory, Thesis, Stanford University (1966)
Plotkin, G., LCF considered as a programming language, Theoret. Comput. Sci. 5, 223-255(1977)
Plotkin, G., Full abstraction, totality and P CF , Math. Struct. in Comp. Science, 11, 1-20 (1999)
Schröder, M., Admissible representations of limit spaces, in J. Blanck, V. Brattka, P. Hertling and K. Weihrauch (eds.), Computability and Complexity in Analysis, vol. 237, Informatik Berichte, 369-388, (2000)
Scott, D., A type-theoretical alternative to ISWIM, CUCH, OWHY, Unpublished notes, Oxford (1969). Printed with suplementary comments in Theoret. Comput. Sci. 121, 411-440 (1993)
Simpson, A., Lazy functional Algorithms for Exact Real Functionals, Mathematical Foun-dations of Computer Science 1998, Springer LNCS 1450, 456-464, (1998)
Stoltenberg-Hansen, V., Lindström, I. and Griffor, E.R., Mathematical Theory of Do-mains, Cambridge Tracts in Theor. Comp. Sci. 22, Cambridge University Press (1994)
Tait, W.W., Continuity properties of partial recursive functionals of finite type, unpub-lished notes (1958)
Weihrauch, K., Computable Analysis, in Texts in Theoretical Computer Science, Springer Verlag, Berlin, (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Normann, D. (2008). Applications of the Kleene–Kreisel Density Theorem to Theoretical Computer Science. In: Cooper, S.B., Löwe, B., Sorbi, A. (eds) New Computational Paradigms. Springer, New York, NY. https://doi.org/10.1007/978-0-387-68546-5_6
Download citation
DOI: https://doi.org/10.1007/978-0-387-68546-5_6
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-36033-1
Online ISBN: 978-0-387-68546-5
eBook Packages: Computer ScienceComputer Science (R0)