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

An hierarchy of terminating algorithms with semantic interpretation termination proofs

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 : We study deterministic (non-deterministic) algorithms define by mean of confluent (resp. non-confluent) rewrite system admitting polynomial interpretation termination proofs. Data structures of the algorithms include strings, lists and trees. We classify them according to the interpretations of constructors This leads to the definition of six classes, which turn out to be exactly the deterministic (non-deterministic) poly-time, linear exponential-time and doubly linear exponential time computable functions when the class is based on confluent (resp. non-confluent) systems. Next, we demonstrate that functions with exponential interpretation termination proofs are super-elementary.
Document type :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Monday, September 25, 2006 - 5:03:29 PM
Last modification on : Friday, February 4, 2022 - 3:31:19 AM


  • HAL Id : inria-00098563, version 1



Jean-Yves Marion. An hierarchy of terminating algorithms with semantic interpretation termination proofs. [Intern report] 98-R-273 || marion98a, 1998, 17 p. ⟨inria-00098563⟩



Record views