Context:Constraint Handling Rules (CHR) is a rule-based programing language that is designed to be embedded into a general-purpose language. Having a CHR implementation available enables software developers to solve problems in a declarative and elegant manner. While the implementations adhere to the formally defined operational semantics, they are not direct implementations of a common formal model. Therefore, the two aspects of CHR (formalism and programing language) are not strictly connected with each other and there is hence no strict guarantee that the results on the formalism CHR are applicable on the programing language CHR.
Objective: We intend to formalize and thereby standardize the way of implementing CHR as an internal DSL for arbitrary host languages.
Method: 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 with its original definition. We also propose a first abstract execution algorithm and prove correctness with the operational semantics. Finally, we show the practicability of our approach by giving two possible implementations of this algorithm in Haskell and Python.
Conclusion: We established FreeCHR as a valid representation of the original definition of CHR and a usable standardizing framework for the implementation of CHR in a wide range of host languages. Moreover, are the presented execution algorithm and the implementations of it, although very simple, to our knowledge the first implementations of CHR for which there is an actual prove of correctness with respect to to a formal definition of their operational semantics.