An instance of FreeCHR with refined operational semantics

TL;DR

This paper refines the operational semantics of FreeCHR, a framework for unifying CHR embedding into host languages, by introducing an execution algorithm that addresses practical issues and proves its soundness.

Contribution

It introduces an execution algorithm for FreeCHR based on refined operational semantics, improving practical implementation and correctness assurance.

Findings

Derived from refined operational semantics

Proved soundness of the execution algorithm

Provides guidelines for new CHR implementations

Abstract

Constraint Handling Rules (CHR) is a rule-based programming language which is typically embedded into a general-purpose language. There exists a plethora of implementations of CHR for numerous host languages. However, the existing implementations often reinvent the way to embed CHR, which impedes maintenance and weakens assertions of correctness. To formalize and thereby unify the embedding of CHR into arbitrary host languages, we introduced the framework FreeCHR and proved it to be a valid representation of classical CHR. Until now, this framework only includes a translation of the very abstract operational semantics of CHR which, due to its abstract nature, introduces several practical issues. In this paper, we introduce an execution algorithm for FreeCHR. We derive it from the refined operational semantics of CHR, which resolve the issues introduced by the very abstract semantics. We also prove soundness of the algorithm with respect to the very abstract semantics of FreeCHR. Hereby we provide a unified and an easy to implement guideline for new CHR implementations, as well as an algorithmic definition of the refined operational semantics.