Christiansen, H. & Kirkeby, M. H. (2019). “Towards a constraint solver for proving confluence with invariant and equivalence of realistic CHR programs”. In Functional and Constraint Logic Programming, 2019, 26th International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers. A part of Lecture Notes in Computer Science, Vol. 11285, pp. 112–130. DOI: 10.1007/978-3-030-16202-3_7 Abstract Confluence of a nondeterministic program ensures a functional […]
Confluence and Convergence Modulo Equivalence in Probabilistically Terminating Reduction Systems
Kirkeby, M.H. & Christiansen, H. (2019). “Confluence and Convergence Modulo Equivalence in Probabilistically Terminating Reduction Systems“. In International Journal of Approximate Reasoning, Vol. 105(2), pp. 217–228, DOI: 10.1016/j.ijar.2018.11.018 Abstract Convergence of an abstract reduction system is the property that the possible derivations from a given initial state all end in the same final state. Relaxing this by “modulo equivalence” means that these final states need not […]
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 […]
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 […]
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 […]