Abstract
In this paper we present a novel termination order the 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.
This is the full version of the extended abstract [1] that appeared in the proceedings of the 13th International Workshop on Termination (WST 2013). This work is generously supported by Grant-in-Aid for JSPS Fellows (Grant No. \(25 \cdot 726\)) and partially by the Austrian Science Fund (Project No. P25781). The JSPS fellowship is granted at Graduate School of Science, Chiba University, Japan.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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), pp. 41–45 (2013)
Cichon, E.A., Weiermann, A.: Term rewriting theory for the primitive recursive functions. Ann. Pure Appl. Logic 83(3), 199–223 (1997)
Seiffertt, J., Wunsch, D.C.: An application of unified computational intelligence. In: Seiffertt, J., Wunsch, D.C. (eds.) Unified Computational Intell. for Complex Sys. ALO, vol. 6, pp. 33–48. Springer, Heidelberg (2010)
Avanzini, M., Moser, G.: Complexity analysis by rewriting. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 130–146. Springer, Heidelberg (2008)
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), vol. 10, pp. 123–138. Leibniz International Proceedings in Informatics (2011)
Avanzini, M., Eguchi, N., Moser, G.: A new order-theoretic characterisation of the polytime computable functions. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 280–295. Springer, Heidelberg (2012)
Péter, R.: Recursive Functions. Academic Press, New York (1967). (The 3rd revised edn., Translated from the German)
Simmons, H.: The realm of primitive recursion. Arch. Math. Logic 27, 177–188 (1988)
Weiermann, A.: Termination proofs for term rewriting systems by lexicographic path ordering imply multiply recursive derivation lengths. Theoret. Comput. Sci. 139(1–2), 355–362 (1995)
Bellantoni, S., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. Comput. Complex. 2(2), 97–110 (1992)
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, vol. 13, pp. 320–343. Birkhäuser, Boston (1995)
Cichon, E.A.: Termination orderings and complexity characterizations. In: Aczel, P., Simmons, H., Wainer, S.S. (eds.) Proof Theory, pp. 171–193. Cambridge University Press, Cambridge (1992)
Weiermann, A.: A termination ordering for primitive recursive schemata, 20 p. (2013, Preprint)
Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theoret. Comput. Sci. 105(1), 129–140 (1992)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Eguchi, N. (2014). Predicative Lexicographic Path Orders. In: Dal Lago, U., Peña, R. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2013. Lecture Notes in Computer Science(), vol 8552. Springer, Cham. https://doi.org/10.1007/978-3-319-12466-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-12466-7_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12465-0
Online ISBN: 978-3-319-12466-7
eBook Packages: Computer ScienceComputer Science (R0)