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 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 and incomplete built-in predicates. Proofs of confluence are demonstrated for programs with redundant data representation, e.g., sets-as-lists, for dynamic programming 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 : 24th International Symposium, LOPSTR 2014, Canterbury, UK, September 9-11, 2014. Revised Selected Papers
EditorsMaurizio Proietti, Hirohisa Seki
Publication date2015
ISBN (Print)978-3-319-17821-9
ISBN (Electronic) 978-3-319-17822-6
Publication statusPublished - 2015
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
Country/TerritoryUnited Kingdom
Internet address
SeriesLecture Notes in Computer Science

Cite this