DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2018.26

Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems

Authors: Naoki Nishida and Yuya Maeda

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract

A narrowing tree for a constructor term rewriting system and a pair of terms is a finite representation for the space of all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. Narrowing trees have grammar representations that can be considered regular tree grammars. Innermost narrowing is a counterpart of constructor-based rewriting, and thus, narrowing trees can be used in analyzing constructor-based rewriting to normal forms. In this paper, using grammar representations, we extend narrowing trees to syntactically deterministic conditional term rewriting systems that are constructor systems. We show that narrowing trees are useful to prove two properties of a normal conditional term rewriting system: one is infeasibility of conditional critical pairs and the other is quasi-reducibility.

Cite as

Naoki Nishida and Yuya Maeda. Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{nishida_et_al:LIPIcs.FSCD.2018.26,
  author =	{Nishida, Naoki and Maeda, Yuya},
  title =	{{Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.26},
  URN =		{urn:nbn:de:0030-drops-91964},
  doi =		{10.4230/LIPIcs.FSCD.2018.26},
  annote =	{Keywords: conditional term rewriting, innermost narrowing, regular tree grammar}
}

Search Results

Documents authored by Maeda, Yuya

Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems

Abstract

Cite as

Thanks for your feedback!

Could not send message