Confluence Modulo Equivalence in Constraint Handling Rules

Henning Christiansen; Maja Hanne Kirkeby

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 ad- vantages of confluence, which include various optimization techniques and simplified correctness proofs. A new operational semantics for CHR is introduced that reduces notational overhead significantly 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 pro- gramming 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 : Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014
Redaktører	Maurizio Proietti, Hirohisa Seki
Forlag	Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche
Publikationsdato	2014
Sider	38-52
Status	Udgivet - 2014
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	Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica
ISSN	1128-3378

Bibliografisk note

En gennemgribende revideret udgave af artiklen vil blive publiceret i en bind af Springer Lecture Notes in Computer Science, 2015

Citer dette

Christiansen, H., & Kirkeby, M. H. (2014). Confluence Modulo Equivalence in Constraint Handling Rules. I M. Proietti, & H. Seki (red.), Logic-Based Program Synthesis and Transformation: Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014 (s. 38-52). Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche. Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica

Christiansen, Henning ; Kirkeby, Maja Hanne. / Confluence Modulo Equivalence in Constraint Handling Rules. Logic-Based Program Synthesis and Transformation: Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014. red. / Maurizio Proietti ; Hirohisa Seki. Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche, 2014. s. 38-52 (Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica ).

@inproceedings{03c82f0f9fd742839f843bcb6256e46a,

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 ad- vantages of confluence, which include various optimization techniques and simplified correctness proofs. A new operational semantics for CHR is introduced that reduces notational overhead significantly 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 pro- gramming 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 = "En gennemgribende revideret udgave af artiklen vil blive publiceret i en bind af Springer Lecture Notes in Computer Science, 2015; null ; Conference date: 09-09-2014 Through 11-09-2014",

year = "2014",

language = "English",

series = "Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica ",

publisher = "Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche",

pages = "38--52",

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 2014, Confluence Modulo Equivalence in Constraint Handling Rules. i M Proietti & H Seki (red), Logic-Based Program Synthesis and Transformation: Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014. Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche, Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica , s. 38-52, Logic-Based Program Synthesis and Transformation, Canterbury, Storbritannien, 09/09/2014.

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

Logic-Based Program Synthesis and Transformation: Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014. red. / Maurizio Proietti; Hirohisa Seki. Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche, 2014. s. 38-52 (Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica ).

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 - En gennemgribende revideret udgave af artiklen vil blive publiceret i en bind af Springer Lecture Notes in Computer Science, 2015

PY - 2014

Y1 - 2014

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 ad- vantages of confluence, which include various optimization techniques and simplified correctness proofs. A new operational semantics for CHR is introduced that reduces notational overhead significantly 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 pro- gramming 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 ad- vantages of confluence, which include various optimization techniques and simplified correctness proofs. A new operational semantics for CHR is introduced that reduces notational overhead significantly 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 pro- gramming algorithms with pruning as well as a Union-Find program, which are not covered by previous confluence notions for CHR.

M3 - Article in proceedings

T3 - Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica

SP - 38

EP - 52

BT - Logic-Based Program Synthesis and Transformation

A2 - Proietti, Maurizio

A2 - Seki, Hirohisa

PB - Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche

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: Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014. Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche. 2014. s. 38-52. (Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica ).