1 Search Results for "Yamaguchi, Masaomi"

Document
DOI: 10.4230/LIPIcs.FSCD.2020.11
A Fast Decision Procedure For Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems

Authors: Masaomi Yamaguchi and Takahito Aoto

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{yamaguchi_et_al:LIPIcs.FSCD.2020.11,
  author =	{Yamaguchi, Masaomi and Aoto, Takahito},
  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 =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.11},
  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}
}
  • Refine by Author
  • 1 Aoto, Takahito
  • 1 Yamaguchi, Masaomi

  • Refine by Classification
  • 1 Theory of computation → Equational logic and rewriting

  • Refine by Keyword
  • 1 decision procedure
  • 1 shallow term rewriting systems
  • 1 uniqueness of normal forms w.r.t. conversion

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2020

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