Infinite Families of Finite String Rewriting Systems and Their Confluence

We introduce parameterized rewrite systems for describing infinite families of finite string rewrite systems depending upon non-negative integer parameters, as well as ways to reason uniformly over these families. Unlike previous work, the vocabulary on which a rewrite system in the family is built depends itself on the integer parameters. Rewriting makes use of a toolkit for parameterized words which allows to describe a rewrite step made independently by all systems in an infinite family by a single, effective parameterized rewrite step. The main result is a confluence test for all systems in a family at once, based on a critical pair lemma classically based on computing finitely many overlaps between lefthand sides of parameterized rules and then checking for their joinability (which decidability is not garanteed).

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Jean-Pierre Jouannaud, Benjamin Monate
• Keywords: Automated Reasoning, Integer Parameters, LPAR 2010, Rewrite Step, Rewrite System