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.
Type de document :
Rapport
[Intern report] 98-R-273 || marion98a, 1998, 17 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00098563
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:03:29
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

85