Document Open Access Logo

Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems

Authors Kentaro Kikuchi, Takahito Aoto

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.49.pdf
  • Filesize: 0.62 MB
  • 15 pages

Document Identifiers

Author Details

Kentaro Kikuchi
  • Tohoku University, Sendai, Japan
Takahito Aoto
  • Niigata University, Niigata, Japan

Funding

This work was partially supported by JSPS KAKENHI Grant Numbers JP17K00005, JP19K11891, JP20H04164 and JP21K11750.

Acknowledgements

We are grateful to the anonymous reviewers for valuable comments.

Cite As Get BibTex

Kentaro Kikuchi and Takahito Aoto. Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSTTCS.2021.49

Abstract

A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. Proof methods for sufficient completeness of terminating TRSs have been well studied. In this paper, we introduce a simple derivation system for proving sufficient completeness of possibly non-terminating TRSs. The derivation system consists of rules to manipulate a set of guarded terms, and sufficient completeness of a TRS holds if there exists a successful derivation for each function symbol. We also show that variations of the derivation system are useful for proving special cases of local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Equational logic and rewriting
Keywords
  • Term rewriting
  • Sufficient completeness
  • Local sufficient completeness
  • Non-termination
  • Derivation rule
  • Well-founded induction schema

Metrics

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

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  2. H. Comon and F. Jacquemard. Ground reducibility is EXPTIME-complete. Inf. Comput., 187(1):123-153, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00134-2.
  3. I. Gnaedig and H. Kirchner. Computing constructor forms with non terminating rewrite programs. In Proceedings of the 8th PPDP, pages 121-132. ACM, 2006. URL: https://doi.org/10.1145/1140335.1140351.
  4. I. Gnaedig and H. Kirchner. Proving weak properties of rewriting. Theor. Comput. Sci., 412(34):4405-4438, 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.028.
  5. D. Găină, M. Nakamura, K. Ogata, and K. Futatsugi. Stability of termination and sufficient-completeness under pushouts via amalgamation. Theor. Comput. Sci., 848:82-105, 2020. URL: https://doi.org/10.1016/j.tcs.2020.09.024.
  6. J. V. Guttag. The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto, 1975. Google Scholar
  7. J. V. Guttag and J. J. Horning. The algebraic specification of abstract data types. Acta Informatica, 10(1):27-52, 1978. URL: https://doi.org/10.1007/BF00260922.
  8. J. Hendrix and J. Meseguer. On the completeness of context-sensitive order-sorted specifications. In Proceedings of the 18th RTA, volume 4533 of Lecture Notes in Computer Science, pages 229-245. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73449-9_18.
  9. D. Kapur, P. Narendran, and H. 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.
  10. K. Kikuchi, T. Aoto, and I. Sasano. Inductive theorem proving in non-terminating rewriting systems and its application to program transformation. In Proceedings of the 21st PPDP, pages 13:1-13:14. ACM, 2019. URL: https://doi.org/10.1145/3354166.3354178.
  11. A. Lazrek, P. Lescanne, and J. J. Thiel. Tools for proving inductive equalities, relative completeness, and ω-completeness. Inf. Comput., 84(1):47-70, 1990. URL: https://doi.org/10.1016/0890-5401(90)90033-E.
  12. S. Lucas. Context-sensitive computations in functional and functional logic programs. J. Funct. Log. Program., 1998(1), 1998. URL: http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-01/A98-01.html.
  13. S. Lucas. Completeness of context-sensitive rewriting. Inf. Process. Lett., 115(2):87-92, 2015. URL: https://doi.org/10.1016/j.ipl.2014.07.004.
  14. E. Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. Google Scholar
  15. T. Shiraishi, K. Kikuchi, and T. Aoto. A proof method for local sufficient completeness of term rewriting systems. In Proceedings of the 18th ICTAC, volume 12819 of Lecture Notes in Computer Science, pages 386-404. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85315-0_22.
  16. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  17. Y. Toyama. How to prove equivalence of term rewriting systems without induction. Theor. Comput. Sci., 90(2):369-390, 1991. Google Scholar
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 About DROPS Imprint Privacy Contact