DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2011.267

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

Authors: Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract

Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound for every CTRS w.r.t. reduction, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling.

Cite as

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 267-282, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{nishida_et_al:LIPIcs.RTA.2011.267,
  author =	{Nishida, Naoki and Sakai, Masahiko and Sakabe, Toshiki},
  title =	{{Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{267--282},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.267},
  URN =		{urn:nbn:de:0030-drops-31244},
  doi =		{10.4230/LIPIcs.RTA.2011.267},
  annote =	{Keywords: conditional term rewriting, program transformation}
}

Search Results

Documents authored by Sakabe, Toshiki

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity

Abstract

Cite as

Thanks for your feedback!

Could not send message