Testing confluence of nonterminating rewriting systems

Abstract

A key problem in the implementation of equational logic programming is how to check that an equational program is confluent. The current version of the equation compiler allows no critical pairs, or overlaps, between left-hand sides of rules. Normal approaches to proving confluence in the presence of critical pairs require that all reductions terminate, but many of the most useful techniques in equational logic programming involve lazy evaluation of terms with nonterminating reductions. In this paper, we give a theorem, showing how confluence can be determined only by critical pairs and their relations in left-linear term rewriting system.

The research of these authors was supported in part by NSF grant CMPS 8805503.

Yiyun Chen is supported by a grant from the People's Republic of China.