Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides
Level-Confluence of Conditional Rewrite Systems with Extra Variables in Right-Hand Sides
复制标题
右侧带有额外变量的条件重写系统的级别汇合
DOI：
10.1007/3-540-59200-8_56
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
T. Ida
中科院分区：
文献类型：
--
作者：
Taro Suzuki;A. Middeldorp;T. Ida
水平汇合是条件项重写系统的一个重要属性，它允许重写规则中有额外的变量，因为它保证了这种系统的收缩的完整性。在本文中，我们提出了一个语法条件，确保水平汇合的正交，不一定终止，条件项重写系统，有额外的变量在右手边的重写规则。为此，我们推广了平行移动引理。我们的结果具有实际意义，因为属于其范围内的系统类可以被看作是一个计算模型的功能逻辑编程语言与本地定义，如让表达式和哪里构造。
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.