On Proving Confluence Modulo Equivalence for Constraint Handling Rules

TL;DR

This paper extends confluence proofs for Constraint Handling Rules by introducing confluence modulo equivalence and accommodating non-logical, incomplete predicates, with a new operational semantics and a formal meta-language for proofs.

Contribution

It introduces confluence modulo equivalence for CHR, allowing more realistic programs, and develops a new operational semantics that includes non-logical predicates, along with a formal proof framework.

Findings

Extended confluence results to larger CHR classes.

Developed a new operational semantics including non-logical predicates.

Created a formal meta-language for systematic proof enumeration.

Abstract

Previous results on proving confluence for Constraint Handling Rules are extended in two ways in order to allow a larger and more realistic class of CHR programs to be considered confluent. Firstly, we introduce the relaxed notion of confluence modulo equivalence into the context of CHR: while confluence for a terminating program means that all alternative derivations for a query lead to the exact same final state, confluence modulo equivalence only requires the final states to be equivalent with respect to an equivalence relation tailored for the given program. Secondly, we allow non-logical built-in predicates such as var/1 and incomplete ones such as is/2, that are ignored in previous work on confluence. To this end, a new operational semantics for CHR is developed which includes such predicates. In addition, this semantics differs from earlier approaches by its simplicity without loss of generality, and it may also be recommended for future studies of CHR. For the purely logical subset of CHR, proofs can be expressed in first-order logic, that we show is not sufficient in the present case. We have introduced a formal meta-language that allows reasoning about abstract states and derivations with meta-level restrictions that reflect the non-logical and incomplete predicates. This language represents subproofs as diagrams, which facilitates a systematic enumeration of proof cases, pointing forward to a mechanical support for such proofs.