Level-confluence of conditional rewrite systems with extra variables in right-hand sides

Abstract

Level-confluence is an important property of conditional term rewriting systems that allow extra variables in the rewrite rale because it guarantees the completeness of narrowing for such systems. In this paper we present a syntactic condition ensuring level-confluence for orthogonal, not necessarily terminating, conditional term rewriting systems that have extra variables in the right-hand sides of the rewrite rules. To this end we generalize the parallel moves lemma. Our result bears practical significance since the class of systems that fall within its scope can be viewed as a computational model for functional logic programming languages with local definitions, such as let-expressions and where-constructs.