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

TL;DR

This paper introduces the predicative lexicographic path order (PLPO), a new termination order that can orient complex primitive recursive equations and demonstrates that it bounds derivation lengths by primitive recursive functions, providing an alternative proof of a classical closure property.

Contribution

The paper presents the PLPO, a novel syntactic restriction of lexicographic path orders, capable of handling complex primitive recursive equations and establishing primitive recursive bounds.

Findings

PLPO can orient primitive recursive equations like nested recursion.

Derivation lengths under PLPO are bounded by primitive recursive functions.

Provides an alternative proof of the closure 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.