Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]

Research output: Book/ReportReportResearch

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.
Original languageEnglish
Place of PublicationRoskilde
PublisherRoskilde Universitet
Volume153
Number of pages20
ISBN (Print)0109-9779
Publication statusPublished - 3 Oct 2018
SeriesRoskilde Universitet. Computer Science. Computer Science Research Report
Volume153
ISSN0109-9779

Keywords

  • confluence
  • constraint handling rules
  • observable confluence modulo equivalence; confluence modulo equivalence
  • invariants
  • equivalence

Cite this

Christiansen, H., & Kirkeby, M. H. (2018). Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]. Roskilde Universitet. Roskilde Universitet. Computer Science. Computer Science Research Report, Vol.. 153