FreeCHR: An Algebraic Framework for CHR-Embeddings
Abstract
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).
Keywords
Cite
@article{arxiv.2306.00642,
title = {FreeCHR: An Algebraic Framework for CHR-Embeddings},
author = {Sascha Rechenberger and Thom Frühwirth},
journal= {arXiv preprint arXiv:2306.00642},
year = {2025}
}
Comments
Extended version of the original paper which was presented at the 7th International Joint Conference on Rules and Reasoning (RuleML+RR 2023). Under consideration in Theory and Practice of Logic Programming (TPLP)