约束处理规则的完备终止执行模型
A Complete and Terminating Execution Model for Constraint Handling Rules
摘要：
我们观察到，多年来提出的约束处理规则的操作语义的各种表述属于从分析到实用的范围。虽然现有的分析公式促进了程序分析和程序属性的形式化证明，但它们不能照原样实现。我们提出了一种新的操作语义，它具有强大的分析基础，同时具有终止执行模型。我们证明了它的健全性和完整性，就现有的分析配方，我们提供了一个实现的形式，源到源的转换，以规则的优先级。
英文摘要：
We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we provide an implementation in the form of a source-to-source transformation to CHR with rule priorities.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
