Abstract
We present a new and powerful criterion for confluence of terminating (terms in) join conditional term rewriting systems. This criterion is based on a certain joinability property for shared parallel critical peaks and does neither require the systems to be decreasing nor left-linear nor normal, but only terminating.
This research was supported in part by ‘DFG, SFB 314 D4’.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. Avenhaus and C. Loría-Sáenz. On conditional rewrite systems with extra variables and deterministic logic programs. In F. Pfenning, ed., Proc. 5th LPAR, LNAI 822, pp. 215–229, Springer-Verlag, 1994.
L. Bachmair and N. Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1–18, 1988.
J. Bergstra and J. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32:323–362, 1986.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, ed., Formal models and semantics, Handbook of Theoretical Computer Science, vol. B, ch. 6, pp. 243–320. Elsevier-The MIT Press, 1990.
N. Dershowitz, M. Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In S. Kaplan and J.-P. Jouannaud, eds., Proc. 1st CTRS (1987), LNCS 308, pp. 31–44, Springer-Verlag, 1988.
B. Gramlich. On termination and confluence of conditional rewrite systems. In N. Dershowitz and N. Lindenstrauss, eds., Proc. 4th CTRS (1994), LNCS 968, pp. 166–185. Springer-Verlag, 1995.
B. Gramlich. Confluence without termination via parallel critical pairs. In H. Kirchner, ed., Proc. 21st CAAP, LNCS 1059, pp. 211–225. Springer-Verlag, 1996.
S. Kaplan. Conditional rewrite rules. TCS, 33:175–193, 1984.
D. Kapur, D. Musser, and P. Narendran. Only prime superpositions need be considered in the Knuth-Bendix completion procedure. JSC, 1988(6):19–36, 1988.
J. W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, eds., Handbook of Logic in Computer Science, vol. 2, ch. 1, pp. 2–117. Clarendon Press, Oxford, 1992.
T. Suzuki, A. Middeldorp, and T. Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In J. Hsiang, ed., Proc. 6th RTA, LNCS 914, pp. 179–193, Kaiserslautern, Springer-Verlag, 1995.
C.-P. Wirth. Syntactic confluence criteria for constructor-based positive/negativeconditional term rewriting systems. SEKI-Report SR-95-09, Fachbereich Informatik, Universität Kaiserslautern, 1995.
C.-P. Wirth and B. Gramlich. A constructor-based approach for positive/negative conditional equational specifications. JSC, 17:51–90, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gramlich, B., Wirth, CP. (1996). Confluence of terminating conditional rewrite systems revisited. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_56
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_56
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61464-7
Online ISBN: 978-3-540-68596-8
eBook Packages: Springer Book Archive