Algorithms with polynomial interpretation termination proof

Citation
G. Bonfante et al., Algorithms with polynomial interpretation termination proof, J FUNCT PRO, 11, 2001, pp. 33-53
Citations number
21
Categorie Soggetti
Computer Science & Engineering
Journal title
JOURNAL OF FUNCTIONAL PROGRAMMING
ISSN journal
09567968 → ACNP
Volume
11
Year of publication
2001
Part
1
Pages
33 - 53
Database
ISI
SICI code
0956-7968(200101)11:<33:AWPITP>2.0.ZU;2-E
Abstract
We study the effect of polynomial interpretation termination proofs of dete rministic (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 t he constructors. This leads to the definition of six function classes which turn out to be exactly the deterministic (resp. non-deterministic) polynom ial time, linear exponential time and linear doubly exponential time comput able functions when the class is based on confluent (resp. non-confluent) r ewrite systems. We also obtain a characterisation of the linear space compu table functions. Finally, we demonstrate that functions with exponential in terpretation termination proofs are super-elementary.