Confluence Modulo Equivalence in Constraint Handling Rules

Henning Christiansen; Maja Hanne Kirkeby

doi:10.1007/978-3-319-17822-6_3

Confluence Modulo Equivalence in Constraint Handling Rules

Henning Christiansen, Maja Hanne Kirkeby

Programmering, logik og intelligente systemer

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer 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.

Originalsprog	Engelsk
Titel	Logic-Based Program Synthesis and Transformation : 24th International Symposium, LOPSTR 2014, Canterbury, UK, September 9-11, 2014. Revised Selected Papers
Redaktører	Maurizio Proietti, Hirohisa Seki
Publikationsdato	2015
Sider	41-58
ISBN (Trykt)	978-3-319-17821-9
ISBN (Elektronisk)	978-3-319-17822-6
DOI	https://doi.org/10.1007/978-3-319-17822-6_3
Status	Udgivet - 2015
Begivenhed	Logic-Based Program Synthesis and Transformation - University of Kent, Canterbury, Canterbury, Storbritannien Varighed: 9 sep. 2014 → 11 sep. 2014 http://www.iasi.cnr.it/events/lopstr14/

Konference

Konference	Logic-Based Program Synthesis and Transformation
Lokation	University of Kent, Canterbury
Land/Område	Storbritannien
By	Canterbury
Periode	09/09/2014 → 11/09/2014
Internetadresse	http://www.iasi.cnr.it/events/lopstr14/

Navn	Lecture Notes in Computer Science
Vol/bind	8981
ISSN	0302-9743

Bibliografisk note

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

Link til dokument

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

chp_10.1007_978-3-319-17822-6_3Accepteret manuskript, 311 KBLicens: CC BY-NC-ND

Citer dette

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. red. / Maurizio Proietti ; Hirohisa Seki. 2015. s. 41-58 (Lecture Notes in Computer Science, Bind 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); Logic-Based Program Synthesis and Transformation ; Conference date: 09-09-2014 Through 11-09-2014",

year = "2015",

doi = "10.1007/978-3-319-17822-6_3",

language = "English",

isbn = "978-3-319-17821-9",

series = "Lecture Notes in Computer Science",

publisher = "Physica-Verlag",

pages = "41--58",

editor = "Maurizio Proietti and Hirohisa Seki",

booktitle = "Logic-Based Program Synthesis and Transformation",

url = "http://www.iasi.cnr.it/events/lopstr14/",

}

Christiansen, H & Kirkeby, MH 2015, Confluence Modulo Equivalence in Constraint Handling Rules. i M Proietti & H Seki (red), 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, bind 8981, s. 41-58, Logic-Based Program Synthesis and Transformation, Canterbury, Storbritannien, 09/09/2014. https://doi.org/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. red. / Maurizio Proietti; Hirohisa Seki. 2015. s. 41-58 (Lecture Notes in Computer Science, Bind 8981).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer 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

T3 - Lecture Notes in Computer Science

SP - 41

EP - 58

BT - Logic-Based Program Synthesis and Transformation

A2 - Proietti, Maurizio

A2 - Seki, Hirohisa

T2 - Logic-Based Program Synthesis and Transformation

Y2 - 9 September 2014 through 11 September 2014

ER -

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