Búsqueda avanzada

A characterization of local confluence of conditional term rewriting systems


When using non-deterministic reduction-based systems, guaranteeing that two diverging steps can be eventually rejoined is crucial for a faithful use in most applications. This property of reduction systems is called local confluence. Gérard Huet provided a characterization of local confluence for term rewriting systems. In conditional term rewriting systems, reduction steps may depend on the satisfaction of specific conditions in rules. Although conditional rewriting was introduced and used already in the 1970s and deeply investigated in the early 1980s, only partial characterizations or sufficient conditions of local confluence of conditional term rewriting have been obtained so far. In this paper, we char- acterize local confluence of conditional rewrite systems as the joinability of a set of conditional pairs including the usual conditional critical pairs and a new kind of pairs we call conditional variable pairs.

Palabras Clave:

Automated reasoning - Conditional rewriting - Confluence - First-Order Logic - Program analysis





Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex