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 :
Reports
Liste complète des métadonnées

https://hal.inria.fr/inria-00098563
Contributor : Publications Loria <>
Submitted on : Monday, September 25, 2006 - 5:03:29 PM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM

Identifiers

  • HAL Id : inria-00098563, version 1

Collections

Citation

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

Share

Metrics

Record views

94