A Complete and Terminating Execution Model for Constraint Handling Rules

TL;DR

This paper introduces a new operational semantics for Constraint Handling Rules that is both analytically sound and guarantees termination, bridging the gap between theoretical analysis and practical implementation.

Contribution

It proposes a novel, terminating execution model for CHR with a strong analytical foundation, and proves its soundness and completeness relative to existing semantics.

Findings

Proposed a new operational semantics for CHR

Proved the semantics' soundness and completeness

Implemented the semantics via source-to-source transformation

Abstract

We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we provide an implementation in the form of a source-to-source transformation to CHR with rule priorities.