Abstract
It is shown that term rewriting systems with primitive recursively bounded derivation heights can be simulated by rewriting systems that have termination proofs using generalized embedding, a very restricted class of simplification orderings. As a corollary we obtain a characterization of the class of relations computable by rewrite systems having primitive recursively bounded derivation heights using recent results on termination proofs by multiset path orderings.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Börger, E. Computability, Complexity, Logic, North Holland (1989).
Cichon, E.A. Bounds on Derivation Lengths from Termination Proofs, Report CSD-TR-622, University of London, Egham (1990). To appear in Proc. Conf. on Proof Theory, Leeds (1990).
Dershowitz, N. Orderings for term rewriting systems, TCS 17 (3) (1982), pp. 279–301.
Dershowitz, N., Jouannaud, J.-P. Rewrite systems, in: Handbook of Theoretical Computer Science, Vol. 2, Ed. J. van Leeuwen, North Holland (1990).
Dershowitz, N., Okada, M. Proof-theoretic techniques for term rewriting theory, Proc. 3rd LICS (1989), pp. 104–111.
Drewes, F., Lautemann, C. Incremental Termination Proofs and the Length of Derivations, Report 7/90, Universität Bremen (1990).
Geser, A. Termination relative, Ph.D. thesis, Univ. Passau (1990).
Hofbauer, D. Termination proofs by multiset path orderings imply primitive recursive derivation lengths, Proc. 2nd ALP, LNCS 463 (1990), pp. 347–358.
Hofbauer, D. Time bounded rewrite systems and termination proofs by generalized embedding, Report, Technische Universität Berlin (1991).
Hofbauer, D., Lautemann, C. Termination proofs and the length of derivations, Proc. 3rd RTA, LNCS 355 (1989), pp. 167–177.
Jouannaud, J.-P., Lescanne, P., Reinig, F. Recursive decomposition ordering, IFIP Working Conf., Ed. Bjørner, North Holland (1982), pp. 331–348.
Klop, J.W. Term rewriting systems: A tutorial, Bulletin of the EATCS 32 (1987), pp. 143–183.
Kapur, D., Narendran, P., Sivakumar, G. A path ordering for proving termination of term rewriting systems, Proc. 10th CAAP, LNCS 185 (1985), pp. 173–187.
Plaisted, D. A recursively defined ordering for proving termination of term rewriting systems, Report UIUCDCS-R-78-943, University of Illinois, Urbana (1978).
Rose, H.E. Subrecursion: Functions and hierarchies, Oxford University Press (1984).
Rusinowitch, M. Path of subterms ordering and recursive decomposition ordering revisited, J. Symbolic Comp. 3 (1&2) (1987), pp. 117–131.
Steinbach, J. Extensions and comparison of simplification orderings, Proc. 3rd RTA, LNCS 355, pp. 434–448.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hofbauer, D. (1991). Time bounded rewrite systems and termination proofs by generalized embedding. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_86
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_86
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive