License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.11
URN: urn:nbn:de:0030-drops-123338
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12333/
Go to the corresponding LIPIcs Volume Portal

Yamaguchi, Masaomi ; Aoto, Takahito

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

pdf-format:
LIPIcs-FSCD-2020-11.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{yamaguchi_et_al:LIPIcs:2020:12333,
  author =	{Masaomi Yamaguchi and Takahito Aoto},
  title =	{{A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12333},
  URN =		{urn:nbn:de:0030-drops-123338},
  doi =		{10.4230/LIPIcs.FSCD.2020.11},
  annote =	{Keywords: uniqueness of normal forms w.r.t. conversion, shallow term rewriting systems, decision procedure}
}

Keywords: uniqueness of normal forms w.r.t. conversion, shallow term rewriting systems, decision procedure
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: Our implementations as well as the details of the experiments can be found in the webpage http://www.nue.ie.niigata-u.ac.jp/experiments/fscd20/.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI