Abstract
We refer to the intrinsic theories of [14, 17], a generic framework for uncoded reasoning about equational programs. In particular, a natural notion of provable functions corresponds to the provably recursive functions of Peano Arithmetic and similar systems. A natural-deduction formulation of these systems map directly, via a Curry-Howard morphism, to terms of the simply typed lambda calculus with recurrence, with a termination proof for a function f mapping to a representation of f.
In [16] we showed that natural structural restrictions on derivations correspond to major complexity classes. When induction is restricted to positive formulas, a generalization of Σ 01 formulas, exactly the primitive recursive functions are provable. When only a “predicative” form of induction is allowed we obtain the Kalmar elementary functions. The combination of both restrictions yields the functions computable in polynomial time.
We show here that induction over arbitrary formulas does not add new provable functions if we disallow in derivations the closing of multiple data-complex assumptions. This significantly extends the class of proofs that can be accepted as “feasible mathematics.”
We also show that if multiple closing of data-complex assumptions is only prohibited when above distinct premises of implication elimination, then the provable functions are precisely the functions computable in polynomial space.
Research partially supported by NSF grant CCR-0105651.
Chapter PDF
References
A. Beckmann and A. Weiermann. A term rewriting characterization of the polytime functions and related complexity classes. Archive for Mathematical Logic, 36: 11–30, 1996.
Stephen Bellantoni and Martin Hofmann. A new feasible arithmetic. Journal for Symbolic Logic, 2001.
Stephen J. Bellantoni, Karl-Heinz Niggl, and Helmut Schwichtenberg. Higher type recursion, ramification and polynomial time. Annals of Pure and Applied Logic, 104 (1–3): 17–30, 2000.
A. Chandra, D. Kozen, and L. Stockmeyer. Alternation. Journal of the ACM, 28: 114–133, 1981.
Jean-Yves Girard. Light linear logic. Information and Computation, 143, 1998.
Jean-Yves Girard, Andre Scedrov, and Philip Scott. Bounded linear logic: A modular approach to polynomial time computability. Theoretical Computer Science, 97: 1–66, 1992.
Kurt Gödel. Über eine bisher noch nicht benutzte erweiterung des finiten standpunktes. Dialectica, 12: 280–287, 1958.
E. Grädel. Capturing Complexity Classes by Fragments of Second Order Logic. Theoretical Computer Science, 101: 35–57, 1992.
Martin Hofmann. A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion. In Proceedings of CSL ‘87, pages 275–294. Springer-Verlag LNCS 1414, 1998.
Martin Hofmann. Linear types and non-size-increasing polynomial time computation. In Proceedings of LICS’99, pages 464–473. IEEE Computer Society, 1999.
Martin Hofmann. Safe recursion with higher types and bck-algebra. Annals of Pure and Applied Logic, 104 (1–3): 113–166, 2000.
Daniel Leivant. Descriptive characterizations of computational complexity. In Second Annual Conference on Structure in Complexity Theory, pages 203–217, Washington, 1987. IEEE Computer Society Press. Revised in Journal of Computer and System Sciences, 39:51–83, 1989.
Daniel Leivant. Contracting proofs to programs. In P. Odifreddi, editor, Logic and Computer Science, pages 279–327. Academic Press, London, 1990.
Daniel Leivant. Intrinsic theories and computational complexity. In D. Leivant, editor, Logic and Computational Complexity, LNCS, pages 177–194, Berlin, 1995. Springer-Verlag.
Daniel Leivant. Applicative control and computational complexity. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic (Proceedings of the Thirteenth CSL Conference, pages 82–95, Berlin, 1999. Springer Verlag (LNCS 1683 ).
Daniel Leivant. Termination proofs and complexity certification. In Naoki Kobayashi and Benjamin C. Pierce, editors, Theoretical Aspects of Computer Software (TACS 2001), Springer LNCS 2215, pages 183–200, 2001.
Daniel Leivant. Intrinsic reasoning about functional programs I: first order theories. Annals of Pure and Applied Logic, 114: 117–153, 2002.
Daniel Leivant and Jean-Yves Marion. Ramified recurrence and computational complexity IV: Predicative functionals and poly-space. Information and Computation. To appear.
Daniel Leivant and Jean-Yves Marion. Predicative functional recurrence and poly-space. In M.Bidoit and M. Dauchet, editors, Theory and Practice of Software Development, LNCS 1214, pages 369–380, Berlin, 1997. Springer-Verlag.
Edward Nelson. Predicative Arithmetic. Princeton University Press, Princeton, 1986.
Kurt Schütte. Proof Theory. Springer-Verlag, Berlin, 1977.
Helmut Schwichtenberg. An arithmetic for polynomial-time computation. Submitted for publication, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media New York
About this chapter
Cite this chapter
Leivant, D. (2002). Substructural Verification and Computational Feasibility. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds) Foundations of Information Technology in the Era of Network and Mobile Computing. IFIP — The International Federation for Information Processing, vol 96. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35608-2_41
Download citation
DOI: https://doi.org/10.1007/978-0-387-35608-2_41
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5275-5
Online ISBN: 978-0-387-35608-2
eBook Packages: Springer Book Archive