Polynomial Interpretations and the Complexity of Algorithms

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.

• Type: Conference
• Year: 1992
• Where: CADE
• Authors: Adam Cichon, Pierre Lescanne
• Keywords: CADE 1992, Logical Reasoning, Polynomial Bound, Polynomial Interpretation Termination, Polynomial Iterpretation