Certified ACKBO
Pages 144 - 151
Abstract
Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding AC-rules to a rewrite system, we switch to the notion of AC-termination. AC-termination can for example be shown using AC-compatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an AC-compatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of AC-termination proofs generated by automated termination tools.
References
[1]
Franz Baader and Tobias Nipkow. 1999. Term Rewriting and All That. Cambridge University Press.
[2]
Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. 2017. A Transfinite Knuth-Bendix Order for LambdaFree Higher-Order Terms. In Proceedings of the 26th International Conference on Automated Deduction (CADE) (Lecture Notes in Computer Science), Vol. 10395. Springer, 432–453.
[3]
Manuel Clavel Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. 2007. All About Maude – A High-Performance Logical Framework . Lecture Notes in Computer Science, Vol. 4350. Springer.
[4]
Donald E. Knuth and Peter B. Bendix. 1970. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, John Leech (Ed.). Pergamon, 263–297.
[5]
Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. 2009. Tyrolean Termination Tool 2. In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA) (Lecture Notes in Computer Science), Vol. 5595. Springer, 295–304.
[6]
Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL – A Proof Assistant for Higher-Order Logic . Lecture Notes in Computer Science, Vol. 2283. Springer.
[7]
Christian Sternagel. 2014. Certified Kruskal’s Tree Theorem. Journal of Formalized Reasoning 7, 1 (2014), 45–62.
[8]
Christian Sternagel and René Thiemann. 2013. Formalizing KnuthBendix Orders and Knuth-Bendix Completion. In Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA) (Leibniz International Proceedings in Informatics), Vol. 21. Schloss Dagstuhl, 287–302.
[9]
Christian Sternagel and René Thiemann. 2014. The Certification Problem Format. In Proceedings of the 11th Workshop on User Interfaces for Theorem Provers (UITP) (Electronic Proceedings in Theoretical Computer Science), Vol. 167. 61–72.
[10]
Makarius Wenzel. 2002. Isabelle/Isar - A Versatile Environment for Human-Readable Formal Proof Documents . Ph.D. Dissertation. Technische Universität München, Institut für Informatik.
[11]
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara. 2013. Mult-Completion with Termination Tools. Journal of Automated Reasoning 50, 3 (2013), 317–354.
[12]
Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. 2014. Nagoya Termination Tool. In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications (RTA) and 12th International Conference on Typed Lambda Calculi and Applications (TLCA) (Lecture Notes in Computer Science), Vol. 8560. Springer, 466–475.
[13]
Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari. 2016. AC Dependency Pairs Revisited. In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL) (Leibniz International Proceedings in Informatics), Vol. 62. Schloss Dagstuhl, 8:1– 8:16.
[14]
Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp. 2016. AC-KBO Revisited. Theory and Practice of Logic Programming 16, 2 (2016), 163–188.
Recommendations
Generalized and formalized uncurrying
FroCoS'11: Proceedings of the 8th international conference on Frontiers of combining systemsUncurrying is a termination technique for applicative term rewrite systems. During our formalization of uncurrying in the theorem prover Isabelle, we detected a gap in the original pen-and-paper proof which cannot directly be filled without further ...
External Rewriting for Skeptical Proof Assistants
This paper presents the design, the implementation, and experiments of the integration of syntactic, conditional possibly associative-commutative term rewriting into proof assistants based on constructive type theory. Our approach is called external ...
A3PAT, an approach for certified automated termination proofs
PEPM '10: Proceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and program manipulationSoftware engineering, automated reasoning, rule-based programming or specifications often use rewriting systems for which termination, among other properties, may have to be ensured.This paper presents the approach developed in Project A3PAT to discover ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2019
261 pages
Copyright © 2019 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: 14 January 2019
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
CPP '19
Sponsor:
CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 14 - 15, 2019
Cascais, Portugal
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 286Total Downloads
- Downloads (Last 12 months)62
- Downloads (Last 6 weeks)14
Reflects downloads up to 14 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in