Abstract
The ability to use a polynomial iterpretation to prove termination of a rewrite system naturally prompts the question as to what restriction on complexity this imposes. The main result of this paper is that a polynomial interpretation termination proof of a rewrite system R which computes a number theoretic function implies a polynomial bound on that function's rate of growth.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
N. Dershowitz and J-P. Jouannaud. Notations for rewriting, 1991. LATEXscript.
O. Geupel. Terminationbeweise bei Termersetzungssytem, 1988. Diplomarbeit.
G. Huet and D.C. Oppen. Equations and rewrite rules: A survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349–405. Academic Press, 1980.
D. Lankford. Canonical algebraic simplification in computational logic. Report ATP-25, University of Texas, 1975.
D. Lankford. On proving term rewriting systems are noetherian. Report MTP-3, Louisiana Tech. University, 1979.
C. Lautemann. A note on polynomial interpretation. In Bulletin of the European Association for Theoretical Computer Science, volume 4, pages 129–131, October 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cichon, A., Lescanne, P. (1992). Polynomial interpretations and the complexity of algorithms. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_161
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_161
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive