Confluence in Constraint Handling Rules (invited paper)

Henning Christiansen, Maja H. Kirkeby: “Confluence in Constraint Handling Rules,” in  IWC 2018 (invited paper).

Abstract

Constraint Handling Rules, CHR, is a nondeterministic programming language whose programs consists of rewrite rules over program states, and being able to show confluence may be an important part of a program correctness proof. In fact, most CHR implementations are deterministic, yet confluence is useful as the programmer does not need to consider the details of the underlying execution strategy.

The initial results on proving confluence in CHR, developed during to the 1990s, were formulated with respect to a logic-based semantics. This choice gave elegant proofs based on the Critical Pair Theorem and Newman’s lemma but can only describe a limited class of programs, namely logical (and terminating) programs.

It can be argued that invariants and confluence modulo equivalence are important from a practical point of view. Most programs are developed with a particular set of initial queries in mind, which reduces the set of reachable states. Therefore, taking the induced invariant into account makes a much larger class of programs confluent. Confluence modulo equivalence is a generalization where forked states must reach equivalent states, rather than a common state. For instance, a program may produce redundant data structures such as representing sets as lists, and the equivalence states that the order of the elements does not matter. Both the invariant and the equivalence relation may be tailored for the individual program.

In our recent work, we have extended previous methods for proving confluence to include invariants and confluence modulo equivalence. We have focused on a more realistic semantics that reflects the de-facto standard implementations of CHR upon Prolog, including a correct treatment of Prolog’s non-logical devices (e.g., var/1, nonvar/1, is/2) and runtime errors. As part of this, we developed a notion of abstract simulations that may be interesting also for other kinds of transition and rewriting systems. The classical critical pair constructions are generalized, having the transition system of interest simulated by another meta-level system (rather that reusing the system itself). This is useful especially for invariants and state equivalences that – by nature – are meta-level statements that typically cannot be expressed in the original system.