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 program- ming algorithms with pruning as well as a Union-Find program, which are not covered by previous confluence notions for CHR.

Links

• http://link.springer.com/chapter/10.1007%2F978-3-319-17822-6_3
• doi:10.1007/978-3-319-17822-6_3

BibTeX (Download)

@inbook{Christiansen2015,
title = {Confluence Modulo Equivalence in Constraint Handling Rules},
author = {Henning Christiansen and Maja H. Kirkeby},
editor = {Maurizio Proietti and Hirohisa Seki},
url = {http://link.springer.com/chapter/10.1007%2F978-3-319-17822-6_3},
doi = {10.1007/978-3-319-17822-6_3},
isbn = {978-3-319-17821-9},
year  = {2015},
date = {2015-10-01},
volume = {8981},
pages = {41-58},
publisher = {Springer International Publishing Switzerland},
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 program- ming algorithms with pruning as well as a Union-Find program, which are not covered by previous confluence notions for CHR.},
keywords = {CHR, Confluence Modulo Equivalence},
pubstate = {published},
tppubtype = {inbook}
}