Operational Semantics and Confluence of Constraint Propagation Rules
Operational Semantics and Confluence of Constraint Propagation Rules
复制标题
操作语义和约束传播规则的融合
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Slim Abdennadher
中科院分区：
文献类型：
--
作者：
Slim Abdennadher
Please try later.
Constraint Handling Rules (CHR) allow one to specify and implement both propagation and simplification for user-defined constraints. Since a propagation rule is applicable again and again, we present in this paper for the first time an operational semantics for CHR that avoids the termination problem with propagation rules.
In previous work [AFM96], a sufficient and necessary condition for the confluence of terminating simplification rules was given inspired by results about conditional term rewriting systems. Confluence ensures that the solver will always compute the same result for a given set of constraints independent of which rules are applied. The confluence of propagation rules was an open problem. This paper shows that we can also give a sufficient and a necessary condition for confluence of terminating CHR programs with propagation rules based on the more refined operational semantics.