Abstract

Level-confluence is an important property of conditional term rewriting systems that allow extra variables in the rewrite rule 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.

BibTeX Entry

@inproceedings{SMI-RTA95,
 author    = "Taro Suzuki and Aart Middeldorp and Tetsuo Ida",
 title     = "Level-Confluence of Conditional Rewrite Systems with Extra
              Variables in Right-Hand Sides",
 booktitle = "Proceedings of the 6th International Conference on Rewriting
              Techniques and Applications",
 series    = "Lecture Notes in Computer Science",
 volume    = 914,
 pages     = "179--193",
 year      = 1995,
 doi       = "10.1007/3-540-59200-8\_56"
}