Abstract
This paper describes the Conditional Confluence tool, a fully automatic confluence checker for first-order conditional term rewrite systems. The tool implements various confluence criteria that have been proposed in the literature. A simple technique is presented to test conditional critical pairs for infeasibility, which makes conditional confluence criteria more useful. Detailed experimental data is presented.
The research described in this paper is supported by FWF (Austrian Science Fund) projects P22467 and I963.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 93–102. Springer, Heidelberg (2009)
Avenhaus, J., Loría-Sáenz, C.: On conditional rewrite systems with extra variables and deterministic logic programs. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 215–229. Springer, Heidelberg (1994)
Baader, F., Nipkow, T.: Term Rewriting and All That. CUP (1998)
Bergstra, J.A., Klop, J.W.: Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences 32(3), 323–362 (1986)
Dershowitz, N., Okada, M., Sivakumar, G.: Confluence of conditional rewrite systems. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 31–44. Springer, Heidelberg (1988)
Ganzinger, H.: A completion procedure for conditional equations. Journal of Symbolic Computation 11(1/2), 51–81 (1991)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)
Gmeiner, K., Nishida, N., Gramlich, B.: Proving confluence of conditional term rewriting systems via unravelings. In: Proc. 2nd IWC, pp. 35–39 (2013)
González-Moreno, J.C., Hortalá-González, M.T., Rodríguez-Artalejo, M.: Denotational versus declarative semantics for functional programming. In: Kleine Büning, H., Jäger, G., Börger, E., Richter, M.M. (eds.) CSL 1991. LNCS, vol. 626, pp. 134–148. Springer, Heidelberg (1992)
Hirokawa, N., Klein, D.: Saigawa: A confluence tool. In: Proc. 1st IWC, p. 49 (2012)
Kounalis, E., Rusinowitch, M.: A proof system for conditional algebraic specifications. In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol. 516, pp. 51–63. Springer, Heidelberg (1991)
Marchiori, M.: On deterministic conditional rewriting. Computation Structures Group Memo, vol. 405. MIT Laboratory for Computer Science (1987)
Marchiori, M.: Unravelings and ultra-properties. In: Hanus, M., Rodríguez-Artalejo, M. (eds.) ALP 1996. LNCS, vol. 1139, pp. 107–121. Springer, Heidelberg (1996)
Nishida, N., Sakai, M., Sakabe, T.: Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity. Logical Methods in Computer Science 8, 1–49 (2012)
Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (2002)
Suzuki, T., Middeldorp, A., Ida, T.: Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 179–193. Springer, Heidelberg (1995)
Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI – A confluence tool. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 499–505. Springer, Heidelberg (2011)
Zhang, H.: Implementing contextual rewriting. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 363–377. Springer, Heidelberg (1993)
Zhang, H., Remy, J.-L.: Contextual rewriting. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 46–62. Springer, Heidelberg (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Sternagel, T., Middeldorp, A. (2014). Conditional Confluence (System Description). In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-08918-8_31
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08917-1
Online ISBN: 978-3-319-08918-8
eBook Packages: Computer ScienceComputer Science (R0)