Cited By
View all- Schöpf JMitterwallner FMiddeldorp A(2024)Confluence of Logically Constrained Rewrite Systems RevisitedAutomated Reasoning10.1007/978-3-031-63501-4_16(298-316)Online publication date: 2-Jul-2024
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Pages 147 - 161
Abstract
Parallel critical pairs (PCPs) have been used to design sufficient criteria for confluence of term rewrite systems. In this work we formalize PCPs and the criteria of Gramlich, Toyama, and Shintani and Hirokawa in the proof assistant Isabelle. In order to reduce the amount of bureaucracy we deviate from the paper-definition of PCPs, i.e., we switch from a position-based definition to a context-based definition. This switch not only simplifies the formalization task, but also gives rise to a simple recursive algorithm to compute PCPs. We further generalize all mentioned criteria from confluence to commutation and integrate them in the certifier CeTA, so that it can now validate confluence- and commutation-proofs based on PCPs. Because of our results, CeTA is now able to certify proofs by the automatic confluence tool Hakusan, which makes heavy use of PCPs. These proofs include term rewrite systems for which no previous certified confluence proof was known.
References
[1]
Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama. 2009. Proving Confluence of Term Rewriting Systems Automatically. In Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, Ralf Treinen (Ed.) (Lecture Notes in Computer Science, Vol. 5595). Springer, 93–102. https://doi.org/10.1007/978-3-642-02348-4_7
[2]
Franz Baader and Tobias Nipkow. 1998. Term rewriting and all that. Cambridge University Press. isbn:978-0-521-45520-6
[3]
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, C. R. Ramakrishnan and Jakob Rehof (Eds.) (Lecture Notes in Computer Science, Vol. 4963). Springer, 337–340. https://doi.org/10.1007/978-3-540-78800-3_24
[4]
Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, and Jiaxiang Liu. 2022. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Math. Struct. Comput. Sci., 32, 7 (2022), 898–933. https://doi.org/10.1017/S0960129522000044
[5]
Bernhard Gramlich. 1995. Confluence without Termination via Parallel Critical Pairs. Fachbereich Informatik, Universität Kaiserslautern.
[6]
Bernhard Gramlich. 1996. Confluence without Termination via Parallel Critical Pairs. In Trees in Algebra and Programming - CAAP’96, 21st International Colloquium, Linköping, Sweden, April, 22-24, 1996, Proceedings, Hélène Kirchner (Ed.) (Lecture Notes in Computer Science, Vol. 1059). Springer, 211–225. https://doi.org/10.1007/3-540-61064-2_39
[7]
Nao Hirokawa and Aart Middeldorp. 2011. Decreasing Diagrams and Relative Termination. J. Autom. Reason., 47, 4 (2011), 481–501. https://doi.org/10.1007/s10817-011-9238-x
[8]
Nao Hirokawa, Julian Nagele, and Aart Middeldorp. 2018. Cops and CoCoWeb: Infrastructure for Confluence Tools. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Didier Galmiche, Stephan Schulz, and Roberto Sebastiani (Eds.) (Lecture Notes in Computer Science, Vol. 10900). Springer, 346–353. https://doi.org/10.1007/978-3-319-94205-6_23
[9]
Nao Hirokawa, Julian Nagele, Vincent van Oostrom, and Michio Oyamaguchi. 2019. Confluence by Critical Pair Analysis Revisited. In Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Pascal Fontaine (Ed.) (Lecture Notes in Computer Science, Vol. 11716). Springer, 319–336. https://doi.org/10.1007/978-3-030-29436-6_19
[10]
Gérard P. Huet. 1980. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems. J. ACM, 27, 4 (1980), 797–821. https://doi.org/10.1145/322217.322230
[11]
Brian Huffman and Ondrej Kuncar. 2013. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, Georges Gonthier and Michael Norrish (Eds.) (Lecture Notes in Computer Science, Vol. 8307). Springer, 131–146. https://doi.org/10.1007/978-3-319-03545-1_9
[12]
Donald E. Knuth and Peter B. Bendix. 1970. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, J. Leech (Ed.). Pergamon Press, 263–297. https://doi.org/10.1016/B978-0-08-012975-4.50028-X
[13]
Christina Kohl and Aart Middeldorp. 2023. A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (Eds.). ACM, 197–210. https://doi.org/10.1145/3573105.3575667
[14]
Christina Kohl and Aart Middeldorp. 2023. Formalizing Almost Development Closed Critical Pairs (Short Paper). In 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Biał ystok, Poland, Adam Naumowicz and René Thiemann (Eds.) (LIPIcs, Vol. 268). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 38:1–38:8. https://doi.org/10.4230/LIPIcs.ITP.2023.38
[15]
Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. 2009. Tyrolean Termination Tool 2. In Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, Ralf Treinen (Ed.) (Lecture Notes in Computer Science, Vol. 5595). Springer, 295–304. https://doi.org/10.1007/978-3-642-02348-4_21
[16]
Aart Middeldorp, Julian Nagele, and Kiraku Shintani. 2021. CoCo 2019: report on the eighth confluence competition. Int. J. Softw. Tools Technol. Transf., 23, 6 (2021), 905–916. https://doi.org/10.1007/s10009-021-00620-4
[17]
Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, and Bertram Felgenhauer. 2021. Certifying Proofs in the First-Order Theory of Rewriting. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, Jan Friso Groote and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science, Vol. 12652). Springer, 127–144. https://doi.org/10.1007/978-3-030-72013-1_7
[18]
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. 2015. Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (LIPIcs, Vol. 36). 257–268. https://doi.org/10.4230/LIPIcs.RTA.2015.257
[19]
Julian Nagele, Bertram Felgenhauer, and Harald Zankl. 2017. Certifying Confluence Proofs via Relative Termination and Rule Labeling. Log. Methods Comput. Sci., 13, 2 (2017), https://doi.org/10.23638/LMCS-13(2:4)2017
[20]
Julian Nagele and Aart Middeldorp. 2016. Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, Jasmin Christian Blanchette and Stephan Merz (Eds.) (Lecture Notes in Computer Science, Vol. 9807). Springer, 290–306. https://doi.org/10.1007/978-3-319-43144-4_18
[21]
Julian Nagele and Aart Middeldorp. 2016. Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, Jasmin Christian Blanchette and Stephan Merz (Eds.) (Lecture Notes in Computer Science, Vol. 9807). Springer, 290–306. https://doi.org/10.1007/978-3-319-43144-4_18
[22]
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL - A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science, Vol. 2283). Springer. isbn:3-540-43376-7 https://doi.org/10.1007/3-540-45949-9
[23]
Kiraku Shintani and Nao Hirokawa. 2022. Compositional Confluence Criteria. In 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, Amy P. Felty (Ed.) (LIPIcs, Vol. 228). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 28:1–28:19. https://doi.org/10.4230/LIPIcs.FSCD.2022.28
[24]
Kiraku Shintani and Nao Hirokawa. 2023. Compositional Confluence Criteria. arXiv. https://doi.org/10.48550/arXiv.2303.03906
[25]
Christian Sternagel and René Thiemann. 2013. Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. In 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands, Femke van Raamsdonk (Ed.) (LIPIcs, Vol. 21). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 287–302. https://doi.org/10.4230/LIPIcs.RTA.2013.287
[26]
the Isabelle community. 2023. Tutorials and manuals for Isabelle2023. https://isabelle.in.tum.de/documentation.html Accessed: 2023-11-22
[27]
René Thiemann and Christian Sternagel. 2009. Certification of Termination Proofs Using CeTA. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.) (Lecture Notes in Computer Science, Vol. 5674). Springer, 452–468. https://doi.org/10.1007/978-3-642-03359-9_31
[28]
Yoshihito Toyama. 1981. On the Church-Rosser property of term rewriting systems. NTT ECL Technical Report (Japanese), 17672 (1981).
[29]
Yoshihito Toyama. 1988. Commutativity of Term Rewriting Systems. In Programming of Future Generation Computers II. North-Holland, 393–407.
[30]
Vincent van Oostrom. 1997. Developing Developments. Theor. Comput. Sci., 175, 1 (1997), 159–181. https://doi.org/10.1016/S0304-3975(96)00173-9
[31]
Vincent van Oostrom. 2008. Confluence by Decreasing Diagrams. In Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, Andrei Voronkov (Ed.) (Lecture Notes in Computer Science, Vol. 5117). Springer, 306–320. https://doi.org/10.1007/978-3-540-70590-1_21
[32]
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. 2011. CSI - A Confluence Tool. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans (Eds.) (Lecture Notes in Computer Science, Vol. 6803). Springer, 499–505. https://doi.org/10.1007/978-3-642-22438-6_38
[33]
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. 2015. Labelings for Decreasing Diagrams. J. Autom. Reason., 54, 2 (2015), 101–133. https://doi.org/10.1007/s10817-014-9316-y
Index Terms
- Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Index terms have been assigned to the content through auto-classification.
Recommendations
Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables
Logic-Based Program Synthesis and TransformationAbstractNominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. Recently, a new format of nominal rewriting has been introduced where rewrite rules are defined with atom-...
A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
Frontiers of Combining SystemsAbstractThe rewrite relation of a conditional term rewriting system (CTRS) can be divided into a hierarchy of rewrite relations of term rewriting systems (TRSs) by the depth of the recursive use of rewrite relation in conditions; a CTRS is said to be ...
Abstract Relations Between Restricted Termination And Confluence Properties Of Rewrite Systems
We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, and their interrelations. New criteria are ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
290 pages
ISBN:9798400704888
DOI:10.1145/3636501
- General Chairs:
- Amin Timany,
- Dmitriy Traytel,
- Program Chairs:
- Brigitte Pientka,
- Sandrine Blazy
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 January 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Austrian Science Fund (FWF)
- Japan Society for the Promotion of Science (JSPS) KAKENHI
- Japan Society for the Promotion of Science and Austrian Science Fund JSPS-FWF
Conference
CPP '24
Sponsor:
CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 15 - 16, 2024
London, UK
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 172Total Downloads
- Downloads (Last 12 months)172
- Downloads (Last 6 weeks)17
Reflects downloads up to 09 Nov 2024
Other Metrics
Citations
Cited By
View all- Schöpf JMitterwallner FMiddeldorp A(2024)Confluence of Logically Constrained Rewrite Systems RevisitedAutomated Reasoning10.1007/978-3-031-63501-4_16(298-316)Online publication date: 2-Jul-2024
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in