Document Open Access Logo

A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems

Authors Masaomi Yamaguchi , Takahito Aoto

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.11.pdf
  • Filesize: 0.63 MB
  • 23 pages

Document Identifiers

Author Details

Masaomi Yamaguchi
  • Tohoku University, Sendai, Japan
Takahito Aoto
  • Niigata University, Niigata, Japan

Funding

This work is partially supported by JSPS KAKENHI No. 18K11158.

Acknowledgements

Thanks are due to the anonymous reviewers for many valuable comments.

Cite AsGet BibTex

Masaomi Yamaguchi and Takahito Aoto. A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.11

Abstract

Uniqueness of normal forms w.r.t. conversion (UNC) of term rewriting systems (TRSs) guarantees that there are no distinct convertible normal forms. It was recently shown that the UNC property of TRSs is decidable for shallow TRSs (Radcliffe et al., 2010). The existing procedure mainly consists of testing whether there exists a counterexample in a finite set of candidates; however, the procedure suffers a bottleneck of having a sheer number of such candidates. In this paper, we propose a new procedure which consists of checking a smaller number of such candidates and enumerating such candidates more efficiently. Correctness of the proposed procedure is proved and its complexity is analyzed. Furthermore, these two procedures have been implemented and it is experimentally confirmed that the proposed procedure runs much faster than the existing procedure.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • uniqueness of normal forms w.r.t. conversion
  • shallow term rewriting systems
  • decision procedure

Metrics

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

Supplementary Materials

References

  1. T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp, J. Nagele, N. Nishida, K. Shintani, and H. Zankl. Confluence competition 2018. In Proc. of 3rd FSCD, volume 108 of LIPIcs, pages 32:1-32:5. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.32.
  2. T. Aoto, N. Hirokawa, J. Nagele, N. Nishida, and H. Zankl. Confluence competition 2015. In Proc. of 25th CADE, volume 9195 of LNCS, pages 101-104. Springer-Verlag, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_5.
  3. T. Aoto and Y. Toyama. On composable properties of term rewriting systems. In Proc. of 6th ALP and 3rd HOA, volume 1298 of LNCS, pages 114-128. Springer-Verlag, 1997. URL: https://doi.org/10.1007/BFb0027006.
  4. T. Aoto and Y. Toyama. Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems. In Proc. of 12th FroCoS, volume 11715 of LNAI, pages 330-347. Springer-Verlag, 2019. URL: https://doi.org/10.1007/978-3-030-29007-8_19.
  5. T. Aoto, Y. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In Proc. of 20th RTA, volume 5595 of LNCS, pages 93-102. Springer-Verlag, 2009. URL: https://doi.org/10.1007/978-3-642-02348-4_7.
  6. F. Baader. and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  7. L. Bachmair, N. Dershowitz, and D. A. Plaisted. Completion without failure. In H. Aït Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2, pages 1-30. Academic Press, 1989. URL: https://doi.org/10.1016/B978-0-12-046371-8.50007-9.
  8. H. Comon, M. Haberstrau, and J. P. Jouannaud. Syntacticness, cycle-syntacticness, and shallow theories. Information and Computation, 111(1):154-191, 1994. URL: https://doi.org/10.1006/inco.1994.1043.
  9. M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In Proc. of 5th LICS, pages 242-248. IEEE Computer Society Press, 1990. URL: https://doi.org/10.1109/LICS.1990.113750.
  10. R. C. de Vrijer. Conditional linearization. Indagationes Mathematicae, 10(1):145-159, 1999. URL: https://doi.org/10.1016/S0019-3577(99)80012-3.
  11. B. Felgenhauer. Deciding confluence and normal form properties of ground term rewrite systems efficiently. Logical Methods in Computer Science, 14(4:7):1-35, 2018. URL: https://doi.org/10.23638/LMCS-14(4:7)2018.
  12. S. Kahrs and C. Smith. Non-ω-overlapping TRSs are UN. In Proc. of 1st FSCD, volume 52 of LIPIcs, pages 22:1-17. Schloss Dagstuhl, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.22.
  13. A. Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Vrije Universiteit, Amsterdam, 1990. Google Scholar
  14. A. Middeldorp, J. Nagele, and K. Shintani. Confluence competition 2019. In Proc. of 25th TACAS, volume 11429 of LNCS, pages 25-40. Springer-Verlag, 2019. URL: https://doi.org/10.1007/978-3-030-17502-3_2.
  15. I. Mitsuhashi, M. Oyamaguchi, and F. Jacquemard. The confluence problem for flat TRSs. In Proc. of 8th AISC, volume 4120 of LNAI, pages 68-81. Springer-Verlag, 2006. URL: https://doi.org/10.1007/11856290_8.
  16. N. Radcliffe and R. M. Verma. Uniqueness of normal forms is decidable for shallow term rewrite systems. In Proc. of 30th FSTTCS, volume 8 of LIPIcs, pages 284-295. Schloss Dagstuhl, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.284.
  17. N. R. Radcliffe, L. F. T. Moreas, and R. M. Verma. Uniqueness of normal forms for shallow term rewrite systems. ACM Transactions on Computational Logic, 18(2):17:1-17:20, 2017. URL: https://doi.org/10.1145/3060144.
  18. F. Rapp and A. Middeldorp. Automating the first-order theory of rewriting for left-linear right-ground rewrite systems. In Proc. of 1st FSCD, volume 52 of LIPIcs, pages 36:1-17. Schloss Dagstuhl, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.36.
  19. Y. Toyama and M. Oyamaguchi. Conditional linearization of non-duplicating term rewriting systems. IEICE Transactions on Information and Systems, E84-D(4):439-447, 2001. Google Scholar
  20. J. Zinn and R. M. Verma. A polynomial algorithm for uniqueness of normal forms of linear shallow term rewrite systems. Applicable Algebra in Engineering, Communication and Computing, 21(6):459-485, 2010. URL: https://doi.org/10.1007/s00200-010-0133-1.
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