TERMINATION PROOFS FOR TERM REWRITING SYSTEMS BY LEXICOGRAPHIC PATH ORDERINGS IMPLY MULTIPLY RECURSIVE DERIVATION LENGTHS

摘要

It is shown that a termination proof for a term rewriting system using a lexicographic path ordering yields a multiply recursive bound on the length of derivations, measured in the depth of the starting term. This result is essentially optimal since for every multiply recursive function f a rewrite system (which reduces under the lexicographic path ordering) can be found such that its derivation length cannot be bounded by f. [References: 14]