FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Confluence of Prefix-Constrained Rewrite Systems

Authors: Nirina Andrianarivelo and Pierre Rety

Paper Information

Title:Confluence of Prefix-Constrained Rewrite Systems
Authors:Nirina Andrianarivelo and Pierre Rety
Proceedings:FSCD Presented Papers
Editor: Helene Kirchner
Keywords:prefix-constrained term rewriting, confluence, critical pair
Abstract:

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.

Pages:16
Talk:Jul 12 17:00 (Session 80: Confluence)
Paper: