Diagrammatic confluence for Constraint Handling Rules

TL;DR

This paper introduces a new criterion for proving confluence in non-terminating Constraint Handling Rules (CHR) programs, enhancing modularity and generalizing previous methods to ensure logical consistency regardless of rule application order.

Contribution

It develops a novel confluence criterion based on decreasing diagrams for CHR, extending applicability to non-terminating programs and improving modular confluence results.

Findings

Derived a generalized criterion for CHR confluence

Extended confluence proofs to non-terminating CHR programs

Improved modularity results for CHR confluence

Abstract

Confluence is a fundamental property of Constraint Handling Rules (CHR) since, as in other rewriting formalisms, it guarantees that the computations are not dependent on rule application order, and also because it implies the logical consistency of the program declarative view. In this paper we are concerned with proving the confluence of non-terminating CHR programs. For this purpose, we derive from van Oostrom's decreasing diagrams method a novel criterion on CHR critical pairs that generalizes all preexisting criteria. We subsequently improve on a result on the modularity of CHR confluence, which permits modular combinations of possibly non-terminating confluent programs, without loss of confluence.