×

Certifying confluence proofs via relative termination and rule labeling. (English) Zbl 1398.68485

Summary: The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] T. Aoto. Automated confluence proof by decreasing diagrams based on rule-labelling. In Proc. 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics, pages 7–16, 2010. doi:10.4230/LIPIcs.RTA.2010.7. · Zbl 1236.68114
[2] T. Aoto, N. Hirokawa, J. Nagele, N. Nishida, and H. Zankl. Confluence Competition 2015. In Proc. 25th International Conference on Automated Deduction, volume 9195 of Lecture Notes in Artificial Intelligence, pages 101–104, 2015. doi:10.1007/978-3-319-21401-6 5. · Zbl 1465.68118
[3] T. Aoto, J. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In Proc. 20th International Conference on Rewriting Techniques and Applications, volume 5595 of Lecture Notes in Computer Science, pages 93–102, 2009. doi:10.1007/978-3-642-02348-4 7. · Zbl 1242.68125
[4] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. doi:10.2277/0521779200. · Zbl 0948.68098
[5] E. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain. Automated certified proofs with CiME3. In Proc. 22nd International Conference on Rewriting Techniques and Applications, volume 10 of Leibniz International Proceedings in Informatics, pages 21–30, 2011. doi:10.4230/LIPIcs.RTA.2011.21. · Zbl 1236.68219
[6] B. Felgenhauer. Decreasing diagrams II. Archive of Formal Proofs, August 2015. Formal proof development, http://www.isa-afp.org/entries/Decreasing-Diagrams-II.shtml.
[7] B. Felgenhauer and V. van Oostrom. Proof orders for decreasing diagrams. In Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of Leibniz International Proceedings in Informatics, pages 174–189, 2013. doi:10.4230/LIPIcs.RTA.2013.174. · Zbl 1356.03054
[8] A.L. Galdino and M. Ayala-Rinc’on. A formalization of Newman’s and Yokouchi’s lemmas in a higherorder language. Journal of Formalized Reasoning, 1(1):39–50, 2008. doi:10.6092/issn.1972-5787/1347. · Zbl 1171.68713
[9] A.L. Galdino and M. Ayala-Rinc’on. A formalization of the Knuth-Bendix(-Huet) critical pair theorem. Journal of Automated Reasoning, 45(3):301–325, 2010. doi:10.1007/s10817-010-9165-2. · Zbl 1207.68338
[10] F. Haftmann. Code Generation from Specifications in Higher Order Logic. Dissertation, Technische Universit”at M”unchen, M”unchen, 2009. urn:nbn:de:bvb:91-diss-20091208-886023-1-1.
[11] F. Haftmann and T. Nipkow. Code generation via higher-order rewrite systems. In Proc. 10th International Symposium on Functional and Logic Programming, volume 6009 of Lecture Notes in Computer Science, pages 103–117. Springer, 2010. doi:10.1007/978-3-642-12251-4 9. · Zbl 1284.68131
[12] N. Hirokawa and A. Middeldorp. Decreasing diagrams and relative termination. In Proc. 5th International · Zbl 1243.68199
[13] N. Hirokawa and A. Middeldorp. Decreasing diagrams and relative termination. Journal of Automated Reasoning, 47(4):481–501, 2011. doi:10.1007/s10817-011-9238-x. · Zbl 1243.68199
[14] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, 1980. doi:10.1145/322217.322230. · Zbl 0458.68007
[15] G. Huet. Residual theory in lambda-calculus: A formal development. Journal of Functional Programming, 4(3):371–394, 1994. doi:10.1017/S0956796800001106.
[16] D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970. doi:10.1016/B978-0-08012975-4.50028-X. · Zbl 0188.04902
[17] J. Nagele, B. Felgenhauer, and A. Middeldorp. Improving automatic confluence analysis of rewrite systems by redundant rules. In Proc. 26th International Conference on Rewriting Techniques and Applications, volume 36 of Leibniz International Proceedings in Informatics, pages 257–268, 2015. doi:10.4230/LIPIcs.RTA.2015.257. · Zbl 1366.68125
[18] J. Nagele and A. Middeldorp. Certification of classical confluence results for left-linear term rewrite systems. In Proc. 7th International Conference on Interactive Theorem Proving, volume 9807 of Lecture Notes in Computer Science, pages 290–306, 2016. doi:10.1007/978-3-319-43144-4 18. · Zbl 1478.68117
[19] J. Nagele and R. Thiemann. Certification of confluence proofs using CeTA. In Proc. 3rd International Workshop on Confluence, pages 19–23, 2014. arXiv:1505.01337.
[20] J. Nagele and H. Zankl. Certified rule labeling. In Proc. 26th International Conference on Rewriting Techniques and Applications, volume 36 of Leibniz International Proceedings in Informatics, pages 269–284, 2015. doi:10.4230/LIPIcs.RTA.2015.269. · Zbl 1366.68126
[21] T. Nipkow. More Church-Rosser proofs. Journal of Automated Reasoning, 26(1):51–66, 2001. doi:10.1023/A:1006496715975. · Zbl 0958.03011
[22] T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL – A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-45949-9. · Zbl 0994.68131
[23] V. van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 126(2):259–280, 1994. doi:10.1016/0304-3975(92)00023-K. · Zbl 0803.68058
[24] V. van Oostrom. Confluence by decreasing diagrams – converted. In Proc. 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 306–320, 2008. doi:10.1007/978-3-540-70590-1 21. · Zbl 1146.68044
[25] F. Pfenning. A proof of the Church-Rosser theorem and its representation in a logical framework. Technical Report CMU-CS-92-186, School of Computer Science, Carnegie Mellon University, 1992.
[26] B.K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, 20(1):160–187, 1973. doi:10.1145/321738.321750. · Zbl 0267.68013
[27] J.-L. Ruiz-Reina, J.-A. Alonso, M.-J. Hidalgo, and F.-J. Mart’ın-Mateos. Formal proofs about rewriting using ACL2. Annals of Mathematics and Artificial Intelligence, 36(3):239–262, 2002. doi:10.1023/A:1016003314081. · Zbl 1015.68169
[28] N. Shankar. A mechanical proof of the Church-Rosser theorem. Journal of the ACM, 35(3):475–522, 1988. doi:10.1145/44483.44484. · Zbl 0654.68103
[29] C. Sternagel. Well-quasi-orders. Archive of Formal Proofs, April 2012. Formal proof development, http://isa-afp.org/entries/Well_Quasi_Orders.shtml.
[30] C. Sternagel. Certified Kruskal’s tree theorem. Journal of Formalized Reasoning, 7(1):45–62, 2014. doi:10.6092/issn.1972-5787/4213.
[31] C. Sternagel and R. Thiemann. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of Leibniz International Proceedings in Informatics, pages 287–302, 2013. doi:10.4230/LIPIcs.RTA.2013.287. · Zbl 1356.68201
[32] C. Sternagel and R. Thiemann. The certification problem format. In Proc. 11th International Workshop on User Interfaces for Theorem Provers, volume 167 of Electronic Proceedings in Theoretical Computer Science, pages 61–72, 2014. doi:10.4204/EPTCS.167.8.
[33] K. Støvring. Extending the extensional lambda calculus with surjective pairing is conservative. Logical Methods in Computer Science, 2(2:1):1–14, 2006. doi:10.2168/LMCS-2(2:1)2006. · Zbl 1126.03019
[34] M. Takahashi. Parallel reductions in {\(\lambda\)}-calculus. Information and Computation, 118(1):120–127, 1995. doi:10.1006/inco.1995.1057. · Zbl 0827.68060
[35] R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In Proc. 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 452–468, 2009. doi:10.1007/978-3-642-03359-9 31. · Zbl 1252.68265
[36] Y. Toyama. Commutativity of term rewriting systems. In K. Fuchi and L. Kott, editors, Programming of Future Generation Computers II, pages 393–407. North-Holland, 1988. · Zbl 0675.68022
[37] H. Zankl. Confluence by decreasing diagrams – formalized. In Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of Leibniz International Proceedings in Informatics, pages 352–367, 2013. doi:10.4230/LIPIcs.RTA.2013.352. · Zbl 1356.68207
[38] H. Zankl. Automating the conversion version of decreasing diagrams for first-order rewrite systems, 2016. Draft, 1 page, http://cl-informatik.uibk.ac.at/users/hzankl/new/publications/ZA16_01.pdf.
[39] H. Zankl, B. Felgenhauer, and A. Middeldorp. CSI – A confluence tool. In Proc. 23rd International Conference on Automated Deduction, volume 6803 of Lecture Notes in Artificial Intelligence, pages 499–505, 2011. doi:10.1007/978-3-642-22438-6 38. · Zbl 1341.68199
[40] H. Zankl, B. Felgenhauer, and A. Middeldorp. Labelings for decreasing diagrams. Journal of Automated Reasoning, 54(2):101–133, 2015. doi:10.1007/s10817-014-9316-y. 1. Introduction2. Preliminaries3. Formalized Confluence Results for Abstract Rewriting4. Formalized Confluence Results for Term Rewriting4.1. Local Peaks4.2. Local Decreasingness5. Checkable Confluence Proofs5.1. Checkable Confluence Proofs for Linear TRSs5.2. Checkable Confluence Proofs for Left-linear TRSs5.3. Certificates6. Experiments7. Conclusion7.1. Related Work7.2. Assessment7.3. Summary and ConclusionAcknowledgmentsReferences
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.