2026-07-25T02:54:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12333 2024-03-06T10:49:59Z ddc:004 open_access

A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems Yamaguchi, Masaomi Aoto, Takahito uniqueness of normal forms w.r.t. conversion shallow term rewriting systems decision procedure 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Masaomi Yamaguchi and Takahito Aoto 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.11 urn:nbn:de:0030-drops-123338 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.11 eng https://creativecommons.org/licenses/by/3.0/legalcode