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

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer 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.
OriginalsprogEngelsk
TitelFunctional and Constraint Logic Programming : 26.International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers
RedaktørerJosep Silva
Udgivelses stedCham
ForlagSpringer
Publikationsdato2019
Sider112-130
ISBN (Trykt)978-3-030-16201-6
DOI
StatusUdgivet - 2019
BegivenhedThe 26th International Workshop on Functional and Logic Programming - Göthe-University Frankfurt am Main, Frankfurt, Tyskland
Varighed: 6 sep. 20186 sep. 2018
Konferencens nummer: 26
http://ppdp-lopstr-18.cs.uni-frankfurt.de/wflp18.html

Konference

KonferenceThe 26th International Workshop on Functional and Logic Programming
Nummer26
LokationGöthe-University Frankfurt am Main
LandTyskland
ByFrankfurt
Periode06/09/201806/09/2018
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind11285
ISSN0302-9743
NavnTheoretical Computer Science and General Issues
Nummer11285

Citer dette

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