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 […]
We are (a)live!
The project is going well! We are already on our way with the first primitive prototype, have planned the first visit and (as you might have suspected) launched the project website. For the curious reader, we have collected a (guaranteed incomplete) selection of background publications: The projects main background article “Confluence Modulo Equivalence for Constraint Handling Rules” (Christiansen and Kirkeby 2015) Confluence and Observable Confluence in […]
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 […]