Automatic support for Proving
Confluence Modulo Equivalence
for Constraint Handling Rules

Constraint Handling Rules, CHR, is a programming language consisting of rewrite rules over sets of logical atoms. CHR has become an important language for various forms of logic reasoning and application. A desired property of a CHR program is confluence, i.e., the final state, i.e., the result of running the program, is independent of the order in which the rules are applied. A confluent program may be optimized by a control of the rule order or parallel execution, and a proof of confluence is often involved in the proof of program correctness.

This project aims at extending existing results on proving confluence for CHR programs to confluence modulo an equivalence relation (CME). Given an equivalence relation ≈, a program is CME whenever alternative end states are equivalent modulo ≈. CME is highly relevant for CHR as it extends the notion of confluence to a much larger class of programs, including dynamic programming algorithms with pruning (such as Viterbi and Dijkstra’s shortest path) and programs with redundant data structures (e.g., representing sets as lists or trees as in Union-Find).

We refer to the background article “Confluence modulo equivalence in Constraint Handling Rules” by Christiansen and Kirkeby.

This project is funded by Danish Council for Independent Research | Natural Sciences, 1 November 2015 until 30 September 2018.