publication . Preprint . 2013

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

Eguchi, Naohi;
Open Access English
  • Published: 01 Aug 2013
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-triv...
Subjects
ACM Computing Classification System: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
free text keywords: Mathematics - Logic, Computer Science - Logic in Computer Science, F.4.1, F.3.3
Download from

1. Eguchi, N.: Predicative Lexicographic Path Orders: Towards a Maximal Model for Primitive Recursive Functions. In Waldmann, J., ed.: Proceedings of 13th International Workshop on Termination (WST 2013). (2013) 41-45

2. Cichon, E.A., Weiermann, A.: Term Rewriting Theory for the Primitive Recursive Functions. Annals of Pure and Applied Logic 83(3) (1997) 199-223 [OpenAIRE]

3. Avanzini, M., Moser, G.: Closing the Gap Between Runtime Complexity and Polytime Computability. In: Proceedings of 21st International Conference on Rewriting Techniques and Applications (RTA 2010). Volume 6 of Leibniz International Proceedings in Informatics. (2010) 33-48

4. Avanzini, M., Moser, G.: Complexity Analysis by Rewriting. In: Proceedings of Functional and Logic Programming, 9th International Symposium (FLOPS 2008). Volume 4989 of Lecture Notes in Computer Science. (2008) 130-146

5. Avanzini, M., Eguchi, N., Moser, G.: A Path Order for Rewrite Systems that Compute Exponential Time Functions. In: Proceedings of 22nd International Conference on Rewriting Techniques and Applications (RTA 2011). Volume 10 of Leibniz International Proceedings in Informatics. (2011) 123-138

6. Avanzini, M., Eguchi, N., Moser, G.: A New Order-theoretic Characterisation of the Polytime Computable Functions. In: Programming Languages and Systems: Proceedings of 10th Asian Symposium on Programming Languages and Systems (APLAS 2012). Volume 7705 of Lecture Notes in Computer Science. (2012) 280- 295

7. P´eter, R.: Recursive Functions. Academic Press, New York-London, The 3rd revised edition, Translated from the German (1967)

8. Simmons, H.: The Realm of Primitive Recursion. Archive for Mathematical Logic 27 (1988) 177-188

9. Weiermann, A.: Termination Proofs for Term Rewriting Systems by Lexicographic Path Ordering Imply Multiply Recursive Derivation Lengths. Theoretical Computer Science 139(1-2) (1995) 355-362 [OpenAIRE]

10. Bellantoni, S., Cook, S.A.: A New Recursion-theoretic Characterization of the Polytime Functions. Computational Complexity 2(2) (1992) 97-110

11. Leivant, D.: Ramified Recurrence and Computational Complexity I: Word Recurrence and Poly-time. In Clote, P., Remmel, J.B., eds.: Feasible Mathematics II, Progress in Computer Science and Applied Logic. Volume 13. Birkh¨auser Boston (1995) 320-343

12. Cichon, E.A.: Termination Orderings and Complexity Characterizations. In Aczel, P., Simmons, H., Wainer, S.S., eds.: Proof Theory. Cambridge University Press (1992) 171-193

13. Weiermann, A.: A Termination Ordering for Primitive Recursive Schemata. Preprint, 20 pages (2013)

14. Hofbauer, D.: Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths. Theoretical Computer Science 105(1) (1992) 129- 140 [OpenAIRE]

Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue