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

Henning Christiansen, Maja Hanne Kirkeby

Publikation: Bog/antologi/afhandling/rapportRapportForskning

Resumé

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.
OriginalsprogEngelsk
Udgivelses stedRoskilde
ForlagRoskilde Universitet
Vol/bind153
Antal sider20
ISBN (Trykt)0109-9779
StatusUdgivet - 3 okt. 2018
NavnRoskilde Universitet. Computer Science. Computer Science Research Report
Vol/bind153
ISSN0109-9779

Emneord

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

Citer dette

Christiansen, H., & Kirkeby, M. H. (2018). Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]. Roskilde: Roskilde Universitet. Roskilde Universitet. Computer Science. Computer Science Research Report, Bind. 153
Christiansen, Henning ; Kirkeby, Maja Hanne. / Confluence of CHR revisited : invariants and modulo equivalence [Extended version with proofs]. Roskilde : Roskilde Universitet, 2018. 20 s. (Roskilde Universitet. Computer Science. Computer Science Research Report, Bind 153).
@book{3ebc1c4a5d4348beb79a5d6836e8f255,
title = "Confluence of CHR revisited: invariants and modulo equivalence [Extended version with proofs]",
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 = "confluence, constraint handling rules, observable confluence modulo equivalence; confluence modulo equivalence, invariants, equivalence, confluence, constraint handling rules, observable confluence modulo equivalence; confluence modulo equivalence, invariants, equivalence",
author = "Henning Christiansen and Kirkeby, {Maja Hanne}",
year = "2018",
month = "10",
day = "3",
language = "English",
isbn = "0109-9779",
volume = "153",
publisher = "Roskilde Universitet",

}

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

Confluence of CHR revisited : invariants and modulo equivalence [Extended version with proofs]. / Christiansen, Henning; Kirkeby, Maja Hanne.

Roskilde : Roskilde Universitet, 2018. 20 s.

Publikation: Bog/antologi/afhandling/rapportRapportForskning

TY - RPRT

T1 - Confluence of CHR revisited

T2 - invariants and modulo equivalence [Extended version with proofs]

AU - Christiansen, Henning

AU - Kirkeby, Maja Hanne

PY - 2018/10/3

Y1 - 2018/10/3

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

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

KW - confluence

KW - constraint handling rules

KW - observable confluence modulo equivalence; confluence modulo equivalence

KW - invariants

KW - equivalence

KW - confluence

KW - constraint handling rules

KW - observable confluence modulo equivalence; confluence modulo equivalence

KW - invariants

KW - equivalence

M3 - Report

SN - 0109-9779

VL - 153

BT - Confluence of CHR revisited

PB - Roskilde Universitet

CY - Roskilde

ER -

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