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,并给出其相对于原始定义的可靠性与完备性证明。