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. We hereby 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 very abstract operational semantics of CHR into FreeCHR, using the free algebra, generated by the endofunctor. We give proofs for soundness and completeness w.r.t. its original definition. We also propose a first abstract execution algorithm and prove correctness w.r.t. the operational semantics. Finally, we show the practicability of our approach by giving two possible implementations of this algorithm in Haskell and Python. Under consideration in Theory and Practice of Logic Programming (TPLP).

翻译：本文提出了FreeCHR框架，该框架利用范畴论中的初始代数语义概念，形式化地将约束处理规则（CHR）嵌入到宿主语言中。由此，我们为CHR建立了一个高层实现方案，并为理论和实践提供了一个共同的形式化基础。我们通过在集合范畴Set中利用自函子，提出了CHR语法的提升方法，并利用该自函子生成的自由代数，将CHR的抽象操作语义提升到FreeCHR中。我们给出了关于其原始定义的可靠性与完备性证明。我们还提出了首个抽象执行算法，并证明了其相对于操作语义的正确性。最后，我们通过给出该算法在Haskell和Python中的两种可能实现，展示了我们方法的实用性。本文已提交至《逻辑程序设计理论与实践》（TPLP）期刊审议。