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
Journal articles

Algorithms with Polynomial Interpretation Termination Proof

Abstract : We study the effect of polynomial interpretation termination proofs of deterministic (resp. non-deterministic) algorithms defined by confluent (resp. non-confluent) rewrite systems over data structures which include strings, lists and trees, and we classify them according to the interpretations of the constructors. This leads to the definition of six function classes which turn out to be exactly the deterministic (resp. non-deterministic) polynomial time, linear exponential time and linear doubly exponential time computable functions when the class is based on confluent (resp. non-confluent) rewrite systems. We also obtain a characterisation of the linear space computable functions. Finally, we demonstrate that functions with exponential interpretation termination proofs are super-elementary.
Document type :
Journal articles
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:51:34 PM
Last modification on : Friday, February 4, 2022 - 3:21:42 AM


  • HAL Id : inria-00100819, version 1



Guillaume Bonfante, Adam Cichon, Jean-Yves Marion, Helene Touzet. Algorithms with Polynomial Interpretation Termination Proof. Journal of Functional Programming, Cambridge University Press (CUP), 2001, 11 (1), pp.33-53. ⟨inria-00100819⟩



Record views