Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-24T23:41:16.168Z Has data issue: false hasContentIssue false
  • English
  • Français

Polynomial time operations in explicit mathematics

Published online by Cambridge University Press:  12 March 2014

Thomas Strahm
Thomas Strahm*
Affiliation:
Institut für Informatik und Angewandte Mathematik, Universität Bern, Neubrückstrasse 10, CH-3012 Bern, Switzerland, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper we study (self-)applicative theories of operations and binary words in the context of polynomial time computability. We propose a first order theory PTO which allows full self-application and whose provably total functions on = {0, 1}* are exactly the polynomial time computable functions. Our treatment of PTO is proof-theoretic and very much in the spirit of reductive proof theory.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 62 , Issue 2 , June 1997 , pp. 575 - 594
Copyright
Copyright © Association for Symbolic Logic 1997

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] Barendregt, H. P., The Lambda calculus, revised ed., North Holland, Amsterdam, 1984.Google Scholar
[2] Beeson, M. J., Foundations of constructive mathematics: Metamathematical studies, Springer-Verlag, Berlin, 1985.CrossRefGoogle Scholar
[3] Buchholz, W. and Sieg, W., A note on polynomial time computable arithmetic, Contemporary Mathematics, vol. 106 (1990), pp. 51–55.CrossRefGoogle Scholar
[4] Buss, S. R., Bounded arithmetic, Bibliopolis, Napoli, 1986.Google Scholar
[5] Buss, S. R., A conservation result concerning bounded theories and the collection axiom, Proceedings of the AMS, vol. 100 (1987), no. 4, pp. 709–715.CrossRefGoogle Scholar
[6] Cantini, A., On the computational content of theories of operations with total application, hand-written notes, 06 1995.Google Scholar
[7] Cantini, A., Asymmetric interpretation for bounded theories, Mathematical Logic Quarterly, vol. 42 (1996), pp. 270–288.CrossRefGoogle Scholar
[8] Cobham, A., The intrinsic computational difficulty of functions, Logic, methodology and philosophy of science II, North Holland, Amsterdam, 1964, pp. 24–30.Google Scholar
[9] Cook, S. A. and Kapron, B. M., Characterizations of the basic feasible functionals of finite type, Feasible mathematics, Birkhäuser, Basel, 1990, pp. 71–95.CrossRefGoogle Scholar
[10] Cook, S. A. and Urquhart, A., Functional interpretations of feasibly constructive arithmetic, Annals of Pure and Applied Logic, vol. 63 (1993), no. 2, pp. 103–200.CrossRefGoogle Scholar
[11] Feferman, S., A language and axioms for explicit mathematics, Algebra and logic, Lecture Notes in Mathematics, vol. 450, Springer-Verlag, Berlin, 1975, pp. 87–139.CrossRefGoogle Scholar
[12] Feferman, S., Constructive theories of functions and classes, Logic Colloquium '78, North-Holland, Amsterdam, 1979, pp. 159–224.Google Scholar
[13] Feferman, S., Hilbert's program relativized: proof-theoretical and foundational studies, this Journal, vol. 53 (1988), pp. 364–384.Google Scholar
[14] Feferman, S. and Jäger, G., Systems of explicit mathematics with non-constructive ü-operator. Part I, Annals of Pure and Applied Logic, vol. 65 (1993), no. 3, pp. 243–263.CrossRefGoogle Scholar
[15] Feferman, S. and Jäger, G., Systems of explicit mathematics with non-constructive ü-operator. Part II, Annals of Pure and Applied Logic, vol. 79 (1996), no. 1.CrossRefGoogle Scholar
[16] Ferreira, F., Polynomial time computable arithmetic and conservative extensions, Ph.D. thesis, Pennsylvania State University, 1988.Google Scholar
[17] Ferreira, F., Polynomial time computable arithmetic, Contemporary Mathematics, vol. 106 (1990), pp. 137–156.CrossRefGoogle Scholar
[18] Ferreira, F., A feasible theory for analysis, this Journal, vol. 59 (1994), no. 3, pp. 1001–1011.Google Scholar
[19] Ferreira, F., A note on a result of Buss concerning bounded theories and the collection scheme, Portugaliae Mathematica, vol. 52 (1995), no. 3, pp. 331–336.Google Scholar
[20] Glaß, T. and Strahm, T., Systems of explicit mathematics with non-constructive ü-operator and join, Annals of Pure and Applied Logic, to appear.Google Scholar
[21] Hinman, P. G., Recursion-theoretic hierarchies, Springer-Verlag, Berlin, 1978.CrossRefGoogle Scholar
[22] Jäger, G. and Strahm, T., Totality in applicative theories, Annals of Pure and Applied Logic, vol. 74 (1995), no. 2, pp. 105–120.CrossRefGoogle Scholar
[23] Seth, A., Complexity theory of higher type functionals, Ph.D. thesis, Tata Institute of Fundamental Research, Bombay, 1994.Google Scholar
[24] Strahm, T., Theories with self-application of strength PRA, Master's thesis, Institut für Informatik und angewandte Mathematik, Universität Bern, 1992.Google Scholar
[25] Troelstra, A. and van Dalen, D., Constructivism in mathematics vol. I, North-Holland, Amsterdam, New York, 1988.Google Scholar
[26] Troelstra, A. and van Dalen, D., Constructivism in mathematics vol. II, North-Holland, Amsterdam, 1988.Google Scholar