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 […]
Confluence of CHR revisited: invariants and modulo equivalence
H. Christiansen, M. H. Kirkeby: “Confluence of CHR revisited: invariants and modulo equivalence”. In Logic-Based Program Synthesis and Transformation, 28th International Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised Selected Papers. A part of Lecture Notes in Computer Science, Vol. 11408, pp. 83–99. DOI: 10.1007/978-3-030-13838-7_6 Abstract Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class […]
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 […]