Predicative Lexicographic Path Orders: An Application of Term Rewriting to the Region of Primitive Recursive Functions

Abstract

In this paper we present a novel termination order the {\em predicative lexicographic path order} (PLPO for short), a syntactic restriction of the lexicographic path order. As well as lexicographic path orders, several non-trivial primitive recursive equations, e.g., primitive recursion with parameter substitution, unnested multiple recursion, or simple nested recursion, can be oriented with PLPOs. It can be shown that the PLPO however only induces primitive recursive upper bounds on derivation lengths of compatible rewrite systems. This yields an alternative proof of a classical fact that the class of primitive recursive functions is closed under those non-trivial primitive recursive equations.