Constraint Handling Rules (CHR) is a rule-based programming language which is typically embedded into a general-purpose language. There exists a plethora of implementations for numerous host languages. However, the existing implementations often re-invent the way to embed CHR, which impedes maintenance and weakens assertions of correctness. To formalize and thereby standardize the embedding into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical ground CHR. Until now, this framework only includes a translation of the very abstract operational semantics which, due to its abstract nature, is not a sufficient base for practical implementations. In this paper we present a translation of the refined operational semantics for FreeCHR and prove it to be both a valid concretization of the very abstract semantics of FreeCHR, and an equivalent representation of the refined semantics of CHR. This will establish implementations of FreeCHR as equivalent in behavior and expressiveness to existing implementations of CHR.

翻译：约束处理规则（CHR）是一种基于规则的编程语言，通常嵌入到通用目的语言中。针对众多宿主语言存在大量的实现。然而，现有实现常常重新发明嵌入CHR的方式，这阻碍了维护并削弱了正确性断言。为了形式化并从而标准化对任意宿主语言的嵌入，我们引入了FreeCHR框架，并证明它是经典基础CHR的一个有效表示。迄今为止，该框架仅包含对非常抽象的操作语义的翻译，由于其抽象性，这不足以作为实际实现的基础。在本文中，我们提出了FreeCHR的精化操作语义的翻译，并证明它既是FreeCHR非常抽象语义的一个有效具体化，也是CHR精化语义的一个等价表示。这将确立FreeCHR实现在行为和表达能力上与现有CHR实现的等价性。