FreeCHR: An Algebraic Framework for CHR-Embeddings

TL;DR

FreeCHR provides a formal algebraic framework for embedding Constraint Handling Rules into host languages, enabling high-level implementation, formalization, and practical execution in Haskell and Python.

Contribution

It introduces a novel algebraic approach to formalize CHR embeddings using category theory, unifying theory and practice with proofs and implementations.

Findings

Soundness and completeness of the framework are proven.

A new abstract execution algorithm is proposed and verified.

Practical implementations in Haskell and Python demonstrate feasibility.

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).