modeq

On Proving Confluence Modulo Equivalence for Constraint Handling Rules

On Proving Confluence Modulo Equivalence for Constraint Handling Rules

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

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