HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Actual arithmetic and feasibility

Jean-Yves Marion 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents a methodology for reasoning about the computational complexity of functional programs. We introduce a first order arithmetic $\StrictTa$ which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which are provably total in $\StrictTa$, is exactly the set of polynomial time functions.The cut-elimination process is polynomial time computable. Compared to others feasible arithmetics, $\StrictTa$ is conceptually simpler. The main feature of $\StrictTa$ concerns the treatment of the quantification. The range of quantifiers is restricted to the set of {\em actual terms} which is the set of constructor terms with variables. The inductive formulas are restricted to conjunctions of atomic formulas.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:43:37 PM
Last modification on : Friday, February 4, 2022 - 3:32:25 AM


  • HAL Id : inria-00100424, version 1



Jean-Yves Marion. Actual arithmetic and feasibility. International Workshop on Computer Science Logic - CSl'2001, 2001, Paris, France, pp.115--129. ⟨inria-00100424⟩



Record views