Document Open Access Logo

Equational Theories and Validity for Logically Constrained Term Rewriting

Authors Takahito Aoto , Naoki Nishida , Jonas Schöpf

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.31.pdf
  • Filesize: 0.87 MB
  • 21 pages

Document Identifiers

Author Details

Takahito Aoto
  • Niigata University, Japan
Naoki Nishida
  • Nagoya University, Japan
Jonas Schöpf
  • University of Innsbruck, Austria

Funding

This research was supported by the FWF (Austrian Science Fund) project I 5943-N and JSPS-FWF Grant Number JPJSBP120222001.
  • Aoto, Takahito: JSPS KAKENHI Grant Numbers 21K11750, 24K14817
  • Nishida, Naoki: JSPS KAKENHI Grant Number 24K02900
  • Schöpf, Jonas: FWF (Austrian Science Fund) project I 5943-N

Acknowledgements

We thank the anonymous reviewers for their valuable feedback, which improved the paper.

Cite AsGet BibTex

Takahito Aoto, Naoki Nishida, and Jonas Schöpf. Equational Theories and Validity for Logically Constrained Term Rewriting. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.31

Abstract

Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derives a new notion of consistency for constrained equational theories.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • constrained equation
  • constrained equational theory
  • logically constrained term rewriting
  • algebraic semantics
  • consistency

Metrics

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

Related Versions

References

  1. Takahito Aoto, Naoki Nishida, and Jonas Schöpf. Equational theories and validity for logically constrained term rewriting (full version). CoRR, abs/2405.01174, 2024. URL: https://doi.org/10.48550/arXiv.2405.01174.
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1145/505863.505888.
  3. Adel Bouhoula and Florent Jacquemard. Sufficient completeness verification for conditional and constrained TRS. Journal of Applied Logic, 10(1):127-143, 2012. URL: https://doi.org/10.1016/J.JAL.2011.09.001.
  4. Ştefan Ciobâcă and Dorel Lucanu. A coinductive approach to proving reachability properties in logically constrained term rewriting systems. In Proceedings of the 9th IJCAR, volume 10900 of Lecture Notes in Computer Science, pages 295-311. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_20.
  5. Hubert Comon. Completion of rewrite systems with membership constraints. part I: deduction rules. Journal of Symbolic Computation, 25(4):397-419, 1998. URL: https://doi.org/10.1006/JSCO.1997.0185.
  6. Hubert Comon. Completion of rewrite systems with membership constraints. part II: constraint solving. Journal of Symbolic Computation, 25(4):421-453, 1998. URL: https://doi.org/10.1006/JSCO.1997.0186.
  7. John Darlington and Yike Guo. Constrained equational deduction. In Proceedings of the 2nd CTRS, volume 516 of Lecture Notes in Computer Science, pages 424-435. Springer, 1991. URL: https://doi.org/10.1007/3-540-54317-1_111.
  8. Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas, and Ann S Ferebee. Mathematical logic, volume 1910. Springer, 1994. Google Scholar
  9. Carsten Fuhs, Cynthia Kop, and Naoki Nishida. Verifying procedural programs via constrained rewriting induction. ACM Transactions on Computational Logic, 18(2):14:1-14:50, 2017. URL: https://doi.org/10.1145/3060143.
  10. Claude Kirchner and Hélène. Kirchner. Constrained equational reasoning. In Proceedings of the 14th ISSAC, pages 3824-389. ACM, 1989. URL: https://doi.org/10.1145/74540.74585.
  11. Misaki Kojima and Naoki Nishida. From starvation freedom to all-path reachability problems in constrained rewriting. In Proceedings of the 25th PADL, volume 13880 of Lecture Notes in Computer Science, pages 161-179. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-24841-2_11.
  12. Misaki Kojima and Naoki Nishida. Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. Journal of Logical and Algebraic Methods in Programming, 135:1-19, 2023. URL: https://doi.org/10.1016/j.jlamp.2023.100903.
  13. Cynthia Kop and Naoki Nishida. Term rewriting with logical constraints. In Proceedings of the 9th FroCoS, volume 8152 of Lecture Notes in Computer Science, pages 343-358, 2013. URL: https://doi.org/10.1007/978-3-642-40885-4_24.
  14. José Meseguer. Twenty years of rewriting logic. Journal of Logic and Algebraic Programming, 81(7-8):721-781, 2012. URL: https://doi.org/10.1016/J.JLAP.2012.06.003.
  15. Naoki Nishida and Sarah Winkler. Loop detection by logically constrained term rewriting. In Proceedings of the 10th VSTTE, volume 11294 of Lecture Notes in Computer Science, pages 309-321. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03592-1_18.
  16. Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. URL: https://doi.org/10.1007/978-1-4757-3661-8.
  17. Jonas Schöpf and Aart Middeldorp. Confluence criteria for logically constrained rewrite systems. In Proceedings of the 29th CADE, volume 14132 of Lecture Notes in Artificial Intelligence, pages 474-490, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_27.
  18. Yoshihito Toyama. Membership conditional term rewriting systems. IEICE Transactions, E72(11):1224-1229, 1989. Google Scholar
  19. Dirk van Dalen. Logic and Structure. Springer-Verlag, Berlin, third edition, 1994. Google Scholar
  20. Sarah Winkler and Aart Middeldorp. Completion for logically constrained rewriting. In Proceedings of the 3rd FSCD, volume 108 of LIPIcs, pages 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.30.
  21. Sarah Winkler and Georg Moser. Runtime complexity analysis of logically constrained rewriting. In Proceedings of the 30th LOPSTR, volume 12561 of Lecture Notes in Computer Science, pages 37-55, 2021. URL: https://doi.org/10.1007/978-3-030-68446-4_2.
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