We introduce the framework FreeCHR, which formalizes the embedding of Constraint Handling Rules (CHR) into a host-language, using the concept of initial algebra semantics from category theory, to establish a high-level implementation scheme for CHR, as well as a common formalization for both theory and practice. We propose a lifting of the syntax of CHR via an endofunctor in the category Set and a lifting of the operational semantics, using the free algebra, generated by the endofunctor. We then lift the very abstract operational semantics of CHR into FreeCHR, and give proofs for soundness and completeness w.r.t. their original definition.

翻译：我们提出了FreeCHR框架，该框架利用范畴论中初始代数语义的概念，形式化了约束处理规则（CHR）嵌入宿主语言的过程，从而为CHR建立了高级实现方案，并为理论与实践提供了统一的数学形式化方法。我们通过集合范畴中的自函子对CHR语法进行提升，并利用该自函子生成的自由代数对其操作语义进行提升。随后，我们将CHR的抽象操作语义提升到FreeCHR中，并给出了其相对于原始定义的可靠性和完备性证明。