2013/08/01 by Naohi Eguchi, Eguchi, Naohi
Computer Science · #F.3.3 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Natural Language Processing Techniques #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1308.0247
openalex publication_date 2013/08/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.