Document Open Access Logo

A Verified Algorithm for Deciding Pattern Completeness

Authors René Thiemann , Akihisa Yamada

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.27.pdf
  • Filesize: 0.79 MB
  • 17 pages

Document Identifiers

Author Details

René Thiemann
  • University of Innsbruck, Austria
Akihisa Yamada
  • National Institute of Advanced Industrial Science and Technology, Tokyo, Japan

Funding

This research was supported by the Austrian Science Fund (FWF) project I 5943.

Acknowledgements

We thank Takahito Aoto and Fabian Mitterwallner for their help in conducting experiments with the tools AGCP and FORT-h, respectively; and we thank Dohan Kim for his contributions to the formalization of an auxiliary algorithm. We are grateful to all reviewers for their helpful remarks and suggestions.

Cite AsGet BibTex

René Thiemann and Akihisa Yamada. A Verified Algorithm for Deciding Pattern Completeness. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.27

Abstract

Pattern completeness is the property that the left-hand sides of a functional program cover all cases w.r.t. pattern matching. In the context of term rewriting a related notion is quasi-reducibility, a prerequisite if one wants to perform ground confluence proofs by rewriting induction. In order to certify such confluence proofs, we develop a novel algorithm that decides pattern completeness and that can be used to ensure quasi-reducibility. One of the advantages of the proposed algorithm is its simple structure: it is similar to that of a regular matching algorithm and, unlike an existing decision procedure for quasi-reducibility, it avoids enumerating all terms up to a given depth. Despite the simple structure, proving the correctness of the algorithm is not immediate. Therefore we formalize the algorithm and verify its correctness using the proof assistant Isabelle/HOL. To this end, we not only verify some auxiliary algorithms, but also design an Isabelle library on sorted term rewriting. Moreover, we export the verified code in Haskell and experimentally evaluate its performance. We observe that our algorithm significantly outperforms existing algorithms, even including the pattern completeness check of the GHC Haskell compiler.

Subject Classification

ACM Subject Classification
  • Theory of computation → Pattern matching
  • Theory of computation → Program verification
  • Theory of computation → Higher order logic
Keywords
  • Isabelle/HOL
  • pattern matching
  • term rewriting

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Takahito Aoto and Yoshihito Toyama. Ground confluence prover based on rewriting induction. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 33:1-33:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.FSCD.2016.33.
  2. Adel Bouhoula. Simultaneous checking of completeness and ground confluence for algebraic specifications. ACM Trans. Comput. Log., 10(3):20:1-20:33, 2009. URL: https://doi.org/10.1145/1507244.1507250.
  3. Adel Bouhoula and Florent Jacquemard. Sufficient completeness verification for conditional and constrained TRS. J. Appl. Log., 10(1):127-143, 2012. URL: https://doi.org/10.1016/j.jal.2011.09.001.
  4. Hubert Comon. Sufficient completness, term rewriting systems and "anti-unification". In Jörg H. Siekmann, editor, 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, volume 230 of Lecture Notes in Computer Science, pages 128-140. Springer, 1986. URL: https://doi.org/10.1007/3-540-16780-3_85.
  5. Stephan Falke and Deepak Kapur. Rewriting induction + linear arithmetic = decision procedure. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of Lecture Notes in Computer Science, pages 241-255. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_20.
  6. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT competition 2020. Artif. Intell., 301:103572, 2021. URL: https://doi.org/10.1016/J.ARTINT.2021.103572.
  7. Deepak Kapur, Paliath Narendran, Daniel J. Rosenkrantz, and Hantao Zhang. Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica, 28(4):311-350, 1991. URL: https://doi.org/10.1007/BF01893885.
  8. Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395-415, 1987. URL: https://doi.org/10.1007/BF00292110.
  9. Cynthia Kop. Quasi-reductivity of logically constrained term rewriting systems. CoRR, 2017. URL: https://arxiv.org/abs/1702.02397.
  10. Alexander Krauss. Partial and nested recursive function definitions in higher-order logic. J. Autom. Reasoning, 44(4):303-336, 2010. URL: https://doi.org/10.1007/s10817-009-9157-2.
  11. Alain Laville. Lazy pattern matching in the ML language. In Kesav V. Nori, editor, Foundations of Software Technology and Theoretical Computer Science, Seventh Conference, Pune, India, December 17-19, 1987, Proceedings, volume 287 of Lecture Notes in Computer Science, pages 400-419. Springer, 1987. URL: https://doi.org/10.1007/3-540-18625-5_64.
  12. Azeddine Lazrek, Pierre Lescanne, and Jean-Jacques Thiel. Tools for proving inductive equalities, relative completeness, and omega-completeness. Inf. Comput., 84(1):47-70, 1990. URL: https://doi.org/10.1016/0890-5401(90)90033-E.
  13. Aart Middeldorp, Alexander Lochmann, and Fabian Mitterwallner. First-order theory of rewriting for linear variable-separated rewrite systems: Automation, formalization, certification. J. Autom. Reason., 67(2):14, 2023. URL: https://doi.org/10.1007/S10817-023-09661-7.
  14. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  15. Uday S. Reddy. Term rewriting induction. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, volume 449 of Lecture Notes in Computer Science, pages 162-177. Springer, 1990. URL: https://doi.org/10.1007/3-540-52885-7_86.
  16. Peter Sestoft. MK pattern match compilation and partial evaluation. In Olivier Danvy, Robert Glück, and Peter Thiemann, editors, Partial Evaluation, International Seminar, Dagstuhl Castle, Germany, February 12-16, 1996, Selected Papers, volume 1110 of Lecture Notes in Computer Science, pages 446-464. Springer, 1996. URL: https://doi.org/10.1007/3-540-61580-6_22.
  17. Christian Sternagel and René Thiemann. First-order terms. Archive of Formal Proofs, February 2018. , Formal proof development. URL: https://isa-afp.org/entries/First_Order_Terms.html.
  18. Jean-Jacques Thiel. Stop losing sleep over incomplete data type specifications. In Ken Kennedy, Mary S. Van Deusen, and Larry Landweber, editors, Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, Salt Lake City, Utah, USA, January 1984, pages 76-82. ACM Press, 1984. URL: https://doi.org/10.1145/800017.800518.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact