Confluence Modulo Equivalence in Constraint Handling Rules

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-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.
Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation : Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014
EditorsMaurizio Proietti, Hirohisa Seki
PublisherIstituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche
Publication date2014
Publication statusPublished - 2014
EventLogic-Based Program Synthesis and Transformation - University of Kent, Canterbury, Canterbury, United Kingdom
Duration: 9 Sep 201411 Sep 2014


ConferenceLogic-Based Program Synthesis and Transformation
LocationUniversity of Kent, Canterbury
CountryUnited Kingdom
Internet address
SeriesCollana dei rapporti dell'Istituto di analisi dei sistemi ed informatica

Cite this