LIPIcs.RTA.2011.235.pdf
- Filesize: 0.55 MB
- 16 pages
Document
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
Authors
-
Part of:
Volume:
22nd International Conference on Rewriting Techniques and Applications (RTA'11) (RTA 2011)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2011-04-26
Cite As Get BibTex
Georg Moser and Andreas Schnabl. Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 235-250, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/LIPIcs.RTA.2011.235
Abstract
We study the complexity of rewrite systems shown terminating via the dependency pair framework using processors for reduction pairs, dependency graphs, or the subterm criterion. The complexity of such systems is bounded by a multiple recursive function, provided the complexity induced by the employed base techniques is at most multiple recursive. Moreover this upper bound is tight.
Subject Classification
Keywords
- Complexity
- DP Framework
- Multiple Recursive Functions
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads