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 […]
On Proving Confluence Modulo Equivalence for Constraint Handling Rules
DOI: 10.1007/s00165-016-0396-9 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 […]
Confluence Modulo Equivalence in Constraint Handling Rules
Abstract Previous results on confluence for Constraint Handling Rules, CHR, are generalized to take into account user-defined state equivalence relations. This allows a much larger class of programs to enjoy the advantages of confluence, which include various optimization techniques and simplified correctness proofs. A new operational semantics for CHR is introduced that significantly reduces notational overhead and allows to consider confluence for programs with extra-logical […]