Confluence of CHR revisited: invariants and modulo equivalence
Abstract
Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.
Keywords
Cite
@article{arxiv.1805.10438,
title = {Confluence of CHR revisited: invariants and modulo equivalence},
author = {Henning Christiansen and Maja H. Kirkeby},
journal= {arXiv preprint arXiv:1805.10438},
year = {2018}
}
Comments
Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326)