Confluence Modulo Equivalence in Constraint Handling Rules

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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 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
Pages41-58
ISBN (Print)978-3-319-17821-9
ISBN (Electronic) 978-3-319-17822-6
DOIs
Publication statusPublished - 2015
EventLogic-Based Program Synthesis and Transformation - University of Kent, Canterbury, Canterbury, United Kingdom
Duration: 9 Sep 201411 Sep 2014
http://www.iasi.cnr.it/events/lopstr14/

Conference

ConferenceLogic-Based Program Synthesis and Transformation
LocationUniversity of Kent, Canterbury
CountryUnited Kingdom
CityCanterbury
Period09/09/201411/09/2014
Internet address
SeriesLecture Notes in Computer Science
Volume8981
ISSN0302-9743

Cite this

Christiansen, H., & Kirkeby, M. H. (2015). Confluence Modulo Equivalence in Constraint Handling Rules. In M. Proietti, & H. Seki (Eds.), Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014, Canterbury, UK, September 9-11, 2014. Revised Selected Papers (pp. 41-58). Lecture Notes in Computer Science, Vol.. 8981 https://doi.org/10.1007/978-3-319-17822-6_3