Confluence Modulo Equivalence in Constraint Handling Rules

Henning Christiansen, Maja Hanne Kirkeby

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 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.
Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation : Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014
EditorsMaurizio Proietti, Hirohisa Seki
PublisherIstituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche
Publication date2014
Pages38-52
Publication statusPublished - 2014
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
SeriesCollana dei rapporti dell'Istituto di analisi dei sistemi ed informatica
ISSN1128-3378

Cite this

Christiansen, H., & Kirkeby, M. H. (2014). Confluence Modulo Equivalence in Constraint Handling Rules. In M. Proietti, & H. Seki (Eds.), Logic-Based Program Synthesis and Transformation: Preliminary Proceedings of the 24th International Symposium, LOPSTR 2014 Canterbury (UK), September 9–11, 2014 (pp. 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. editor / Maurizio Proietti ; Hirohisa Seki. Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche, 2014. pp. 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",
year = "2014",
language = "English",
pages = "38--52",
editor = "Maurizio Proietti and Hirohisa Seki",
booktitle = "Logic-Based Program Synthesis and Transformation",
publisher = "Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche",

}

Christiansen, H & Kirkeby, MH 2014, Confluence Modulo Equivalence in Constraint Handling Rules. in M Proietti & H Seki (eds), 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 , pp. 38-52, Canterbury, United Kingdom, 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. ed. / Maurizio Proietti; Hirohisa Seki. Istituto di Analisi dei Sistemi ed Informatica. Consiglio Nazionale delle Ricerche, 2014. p. 38-52.

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

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

ER -

Christiansen H, Kirkeby MH. Confluence Modulo Equivalence in Constraint Handling Rules. In Proietti M, Seki H, editors, 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. p. 38-52. (Collana dei rapporti dell'Istituto di analisi dei sistemi ed informatica ).