Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs

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

Abstract

Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating CHR programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated as is needed for confluence proofs, thus extending our previous theoretical results towards a practical implementation.
Original languageEnglish
Title of host publicationFunctional and Constraint Logic Programming : 26.International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers
EditorsJosep Silva
Place of PublicationCham
PublisherSpringer
Publication date2019
Pages112-130
ISBN (Print)978-3-030-16201-6
DOIs
Publication statusPublished - 2019
EventThe 26th International Workshop on Functional and Logic Programming - Göthe-University Frankfurt am Main, Frankfurt, Germany
Duration: 6 Sep 20186 Sep 2018
Conference number: 26
http://ppdp-lopstr-18.cs.uni-frankfurt.de/wflp18.html

Conference

ConferenceThe 26th International Workshop on Functional and Logic Programming
Number26
LocationGöthe-University Frankfurt am Main
CountryGermany
CityFrankfurt
Period06/09/201806/09/2018
Internet address
SeriesLecture Notes in Computer Science
Volume11285
ISSN0302-9743
SeriesTheoretical Computer Science and General Issues
Number11285

Cite this

Christiansen, H., & Kirkeby, M. H. (2019). Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs. In J. Silva (Ed.), Functional and Constraint Logic Programming : 26.International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers (pp. 112-130). Cham: Springer. Lecture Notes in Computer Science, Vol.. 11285, Theoretical Computer Science and General Issues, No. 11285 https://doi.org/10.1007/978-3-030-16202-3_7
Christiansen, Henning ; Kirkeby, Maja Hanne. / Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs. Functional and Constraint Logic Programming : 26.International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers. editor / Josep Silva. Cham : Springer, 2019. pp. 112-130 (Lecture Notes in Computer Science, Vol. 11285). (Theoretical Computer Science and General Issues; No. 11285).
@inproceedings{ae9314051271461a811beb8a2d3c6a1d,
title = "Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs",
abstract = "Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating CHR programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated as is needed for confluence proofs, thus extending our previous theoretical results towards a practical implementation.",
author = "Henning Christiansen and Kirkeby, {Maja Hanne}",
year = "2019",
doi = "10.1007/978-3-030-16202-3_7",
language = "English",
isbn = "978-3-030-16201-6",
pages = "112--130",
editor = "Josep Silva",
booktitle = "Functional and Constraint Logic Programming",
publisher = "Springer",

}

Christiansen, H & Kirkeby, MH 2019, Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs. in J Silva (ed.), Functional and Constraint Logic Programming : 26.International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers. Springer, Cham, Lecture Notes in Computer Science, vol. 11285, Theoretical Computer Science and General Issues, no. 11285, pp. 112-130, The 26th International Workshop on Functional and Logic Programming, Frankfurt, Germany, 06/09/2018. https://doi.org/10.1007/978-3-030-16202-3_7

Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs. / Christiansen, Henning; Kirkeby, Maja Hanne.

Functional and Constraint Logic Programming : 26.International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers. ed. / Josep Silva. Cham : Springer, 2019. p. 112-130 (Lecture Notes in Computer Science, Vol. 11285). (Theoretical Computer Science and General Issues; No. 11285).

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

TY - GEN

T1 - Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs

AU - Christiansen, Henning

AU - Kirkeby, Maja Hanne

PY - 2019

Y1 - 2019

N2 - Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating CHR programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated as is needed for confluence proofs, thus extending our previous theoretical results towards a practical implementation.

AB - Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating CHR programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated as is needed for confluence proofs, thus extending our previous theoretical results towards a practical implementation.

U2 - 10.1007/978-3-030-16202-3_7

DO - 10.1007/978-3-030-16202-3_7

M3 - Article in proceedings

SN - 978-3-030-16201-6

SP - 112

EP - 130

BT - Functional and Constraint Logic Programming

A2 - Silva, Josep

PB - Springer

CY - Cham

ER -

Christiansen H, Kirkeby MH. Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs. In Silva J, editor, Functional and Constraint Logic Programming : 26.International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers. Cham: Springer. 2019. p. 112-130. (Lecture Notes in Computer Science, Vol. 11285). (Theoretical Computer Science and General Issues; No. 11285). https://doi.org/10.1007/978-3-030-16202-3_7