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.
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.
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
Date2015
Pages41-58
ISBN (Print)978-3-319-17821-9
ISBN (Electronic) 978-3-319-17822-6
DOIs
StatePublished - 2015
EventLogic-Based Program Synthesis and Transformation - University of Kent, Canterbury, Canterbury, United Kingdom
Duration: 9 Sep 201411 Sep 2014
Conference number: 24

Conference

ConferenceLogic-Based Program Synthesis and Transformation
Number24
LocationUniversity of Kent, Canterbury
CountryUnited Kingdom
CityCanterbury
Period09/09/201411/09/2014
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, DOI: 10.1007/978-3-319-17822-6_3
Christiansen, Henning ; Kirkeby, Maja Hanne. / Confluence Modulo Equivalence in Constraint Handling Rules. Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014, Canterbury, UK, September 9-11, 2014. Revised Selected Papers. editor / Maurizio Proietti ; Hirohisa Seki. 2015. pp. 41-58 (Lecture Notes in Computer Science, Vol. 8981).
@inproceedings{8a96d272d9134346b1231d67cdbb4505,
title = "Confluence Modulo Equivalence in Constraint Handling Rules",
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.",
author = "Henning Christiansen and Kirkeby, {Maja Hanne}",
note = "Revised and extended version of paper first printed in preliminary proceedings 2014 (same title)",
year = "2015",
doi = "10.1007/978-3-319-17822-6_3",
language = "English",
isbn = "978-3-319-17821-9",
pages = "41--58",
editor = "Maurizio Proietti and Hirohisa Seki",
booktitle = "Logic-Based Program Synthesis and Transformation",

}

Christiansen, H & Kirkeby, MH 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. Lecture Notes in Computer Science, vol. 8981, pp. 41-58, Canterbury, United Kingdom, 09/09/2014. DOI: 10.1007/978-3-319-17822-6_3

Confluence Modulo Equivalence in Constraint Handling Rules. / Christiansen, Henning; Kirkeby, Maja Hanne.

Logic-Based Program Synthesis and Transformation: 24th International Symposium, LOPSTR 2014, Canterbury, UK, September 9-11, 2014. Revised Selected Papers. ed. / Maurizio Proietti; Hirohisa Seki. 2015. p. 41-58.

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

TY - GEN

T1 - Confluence Modulo Equivalence in Constraint Handling Rules

AU - Christiansen,Henning

AU - Kirkeby,Maja Hanne

N1 - Revised and extended version of paper first printed in preliminary proceedings 2014 (same title)

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-17822-6_3

DO - 10.1007/978-3-319-17822-6_3

M3 - Article in proceedings

SN - 978-3-319-17821-9

SP - 41

EP - 58

BT - Logic-Based Program Synthesis and Transformation

ER -

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