Towards a constraint solver for proving confluence with invariant and equivalence of realistic CHR programs

Towards a constraint solver for proving confluence with invariant and equivalence of realistic CHR programs

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 […]

Read Me Leave comment

Confluence and Convergence Modulo Equivalence in Probabilistically Terminating Reduction Systems

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 […]

Read Me Leave comment

Confluence in Constraint Handling Rules (invited paper)

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 […]

Read Me Leave comment

Confluence of CHR revisited: invariants and modulo equivalence

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 […]

Read Me Leave comment

On Proving Confluence Modulo Equivalence for Constraint Handling Rules

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 […]

Read Me Leave comment

We are (a)live!

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 […]

Read Me Leave comment

Confluence Modulo Equivalence in Constraint Handling Rules

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 […]

Read Me Leave comment