Substructural Verification and Computational Feasibility
Daniel M. Leivant · 2002
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 Σ 1 0 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.