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.2018.6
URN: urn:nbn:de:0030-drops-91762
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9176/
Go to the corresponding LIPIcs Volume Portal

Andrianarivelo, Nirina ; Réty, Pierre

Confluence of Prefix-Constrained Rewrite Systems

pdf-format:
LIPIcs-FSCD-2018-6.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{andrianarivelo_et_al:LIPIcs:2018:9176,
  author =	{Nirina Andrianarivelo and Pierre R{\'e}ty},
  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 =	{H{\'e}l{\`e}ne Kirchner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9176},
  URN =		{urn:nbn:de:0030-drops-91762},
  doi =		{10.4230/LIPIcs.FSCD.2018.6},
  annote =	{Keywords: prefix-constrained term rewriting, confluence, critical pair}
}

Keywords: prefix-constrained term rewriting, confluence, critical pair
Collection: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Issue Date: 2018
Date of publication: 04.07.2018

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