Confluence Modulo Equivalence in Constraint Handling Rules

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review


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 ad- vantages of confluence, which include various optimization techniques and simplified correctness proofs. A new operational semantics for CHR is introduced that reduces notational overhead significantly and allows to consider confluence for programs with extra-logical and incomplete built-in predicates. Proofs of confluence are demonstrated for programs with redundant data representation, e.g., sets-as-lists, for dynamic pro- gramming algorithms with pruning as well as a Union-Find program, which are not covered by previous confluence notions for CHR.
TitelLogic-Based Program Synthesis and Transformation : Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014
RedaktørerMaurizio Proietti, Hirohisa Seki
ForlagIstituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche
StatusUdgivet - 2014
BegivenhedLogic-Based Program Synthesis and Transformation - University of Kent, Canterbury, Canterbury, Storbritannien
Varighed: 9 sep. 201411 sep. 2014


KonferenceLogic-Based Program Synthesis and Transformation
LokationUniversity of Kent, Canterbury
NavnCollana dei rapporti dell'Istituto di analisi dei sistemi ed informatica

Bibliografisk note

En gennemgribende revideret udgave af artiklen vil blive publiceret i en bind af Springer Lecture Notes in Computer Science, 2015

Citer dette