DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2018.6

Confluence of Prefix-Constrained Rewrite Systems

Authors: Nirina Andrianarivelo and Pierre Réty

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

Abstract

Prefix-constrained rewriting is a strict extension of context-sensitive rewriting. We study the confluence of prefix-constrained rewrite systems, which are composed of rules of the form L: l -> r where L is a regular string language that defines the allowed rewritable positions. The usual notion of Knuth-Bendix's critical pair needs to be extended using regular string languages, and the convergence of all critical pairs is not enough to ensure local confluence. Thanks to an additional restriction we get local confluence, and then confluence for terminating systems, which makes the word problem decidable. Moreover we present an extended Knuth-Bendix completion procedure, to transform a non-confluent prefix-constrained rewrite system into a confluent one.

Cite as

Nirina Andrianarivelo and Pierre Réty. Confluence of Prefix-Constrained Rewrite Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{andrianarivelo_et_al:LIPIcs.FSCD.2018.6,
  author =	{Andrianarivelo, Nirina and R\'{e}ty, Pierre},
  title =	{{Confluence of Prefix-Constrained Rewrite Systems}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{6:1--6:15},
  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.6},
  URN =		{urn:nbn:de:0030-drops-91762},
  doi =		{10.4230/LIPIcs.FSCD.2018.6},
  annote =	{Keywords: prefix-constrained term rewriting, confluence, critical pair}
}

Document

DOI: 10.4230/LIPIcs.RTA.2013.128

Over-approximating Descendants by Synchronized Tree Languages

Authors: Yohan Boichut, Jacques Chabin, and Pierre Réty

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract

Over-approximating the descendants (successors) of a initial set of terms by a rewrite system is used in verification. The success of such verification methods depends on the quality of the approximation. To get better approximations, we are going to use non-regular languages. We present a procedure that always terminates and that computes over-approximation of descendants, using synchronized tree-(tuple) languages expressed by logic programs.

Cite as

Yohan Boichut, Jacques Chabin, and Pierre Réty. Over-approximating Descendants by Synchronized Tree Languages. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 128-142, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{boichut_et_al:LIPIcs.RTA.2013.128,
  author =	{Boichut, Yohan and Chabin, Jacques and R\'{e}ty, Pierre},
  title =	{{Over-approximating Descendants by Synchronized Tree Languages}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{128--142},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.128},
  URN =		{urn:nbn:de:0030-drops-40580},
  doi =		{10.4230/LIPIcs.RTA.2013.128},
  annote =	{Keywords: rewriting systems, non-regular approximations, logic programming, tree languages, descendants}
}

Search Results

Documents authored by Réty, Pierre

Confluence of Prefix-Constrained Rewrite Systems

Abstract

Cite as

Over-approximating Descendants by Synchronized Tree Languages

Abstract

Cite as

Thanks for your feedback!

Could not send message