Skip to main content
SpringerLink
Log in

Confluence of CHR Revisited: Invariants and Modulo Equivalence

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11408))

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 HThe invariant is formalizedandling 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.

This work is supported by The Danish Council for Independent Research, Natural Sciences, grant no. DFF 4181-00442.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In recent literature within term rewriting, the terms peaks and cliffs have been used for \(\alpha \) and \(\beta \) corners, respectively.

  2. 2.

    In the literature, the term critical pair is used for the pair of wing states of our critical corners.

  3. 3.

    Raiser et al. [27] defined “state” similarly to what we call state representation, and they defined an operational semantics over equivalence classes of such states. We have taken the natural step of promoting such equivalence classes to be our states.

  4. 4.

    An equation between multisets should be understood as an equation between suitable permutations of their elements.

  5. 5.

    Such an attempt might be \(\langle \texttt {p(X)},(\texttt {X=0}\vee \texttt {X=1})\rangle \); notice that X is a variable, thus breaking the invariant.

References

  1. Abdennadher, S.: Operational semantics and confluence of constraint propagation rules. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 252–266. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0017444

    Chapter  Google Scholar 

  2. Abdennadher, S., Frühwirth, T., Meuss, H.: On confluence of constraint handling rules. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 1–15. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61551-2_62

    Chapter  Google Scholar 

  3. Abdennadher, S., Frühwirth, T.W., Meuss, H.: Confluence and semantics of constraint simplification rules. Constraints 4(2), 133–165 (1999)

    Article  MathSciNet  Google Scholar 

  4. Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  5. Christiansen, H.: Automated reasoning with a constraint-based metainterpreter. J. Logic Program. 37(1–3), 213–254 (1998)

    Article  MathSciNet  Google Scholar 

  6. Christiansen, H., Kirkeby, M.: Confluence of CHR revisited: invariants and modulo equivalence. [Extended version with proofs], Computer Science Research Report, vol. 153. Roskilde University, October 2018. https://forskning.ruc.dk/files/63000759/ChrKir_LOPSTR2018_ExtReport.pdf

  7. Christiansen, H., Kirkeby, M.H.: Confluence modulo equivalence in constraint handling rules. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 41–58. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17822-6_3

    Chapter  Google Scholar 

  8. Christiansen, H., Kirkeby, M.H.: On proving confluence modulo equivalence for constraint handling rules. Formal Aspects Comput. 29(1), 57–95 (2017)

    Article  MathSciNet  Google Scholar 

  9. Christiansen, H., Kirkeby, M.H.: Towards a constraint solver for proving confluence with invariant and equivalence of realistic CHR programs. In: WFLP, LNCS, vol. 11285 (2018, to appear)

    Google Scholar 

  10. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL 1977, 238–252 (1977)

    Google Scholar 

  11. Curien, P.-L., Ghelli, G.: On confluence for weakly normalizing systems. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 215–225. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-53904-2_98

    Chapter  Google Scholar 

  12. Duck, G.J., Stuckey, P.J., de la Banda, M.G., Holzbaur, C.: The refined operational semantics of constraint handling rules. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 90–104. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27775-0_7

    Chapter  Google Scholar 

  13. Duck, G.J., Stuckey, P.J., Sulzmann, M.: Observable confluence for constraint handling rules. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 224–239. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74610-2_16

    Chapter  Google Scholar 

  14. Frühwirth, T.W.: User-defined constraint handling. In: ICLP 1993, pp. 837–838. MIT Press (1993)

    Google Scholar 

  15. Frühwirth, T.W.: Theory and practice of constraint handling rules. J. Logic Program. 37(1–3), 95–138 (1998)

    Article  MathSciNet  Google Scholar 

  16. Frühwirth, T.W.: Constraint Handling Rules. Cambridge University Press, New York (2009)

    Book  Google Scholar 

  17. Gall, D., Frühwirth, T.: Confluence modulo equivalence with invariants in constraint handling rules. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 116–131. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90686-7_8

    Chapter  Google Scholar 

  18. Hill, P., Gallagher, J.: Meta-programming in logic programming. In: Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 421–497. Oxford Science Publications, Oxford University Press (1994)

    Google Scholar 

  19. Hill, P.M., Lloyd, J.W.: Analysis of meta-programs. In: Meta-Programming in Logic Programming, pp. 23–51. The MIT Press (1988)

    Google Scholar 

  20. Holzbaur, C., Frühwirth, T.W.: A PROLOG constraint handling rules compiler and runtime system. Appl. Artif. Intell. 14(4), 369–388 (2000)

    Article  Google Scholar 

  21. Huet, G.P.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)

    Article  MathSciNet  Google Scholar 

  22. Jaffar, J., Lassez, J.: Constraint logic programming. In: Symposium on Principles of Programming Languages. POPL 1987, pp. 111–119. ACM Press (1987)

    Google Scholar 

  23. Kirkeby, M.H., Christiansen, H.: Confluence and convergence modulo equivalence in probabilistically terminating reduction systems. Int. J. Approximate Reasoning 105, 217–228 (2019)

    Article  MathSciNet  Google Scholar 

  24. Langbein, J., Raiser, F., Frühwirth, T.W.: A state equivalence and confluence checker for CHRs. In: Proceedings of the International Workshop on Constraint Handling Rules, Report CW 588, pp. 1–8. Katholieke Universiteit Leuven, Belgium (2010)

    Google Scholar 

  25. Newman, M.: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43(2), 223–243 (1942)

    Article  MathSciNet  Google Scholar 

  26. Park, D.M.R.: Concurrency and automata on infinite sequences. In: Proceedings of the Theoretical Computer Science, 5th GI-Conference, pp. 167–183 (1981)

    Google Scholar 

  27. Raiser, F., Betz, H., Frühwirth, T.W.: Equivalence of CHR states revisited. In: Proceedings of the International Workshop on Constraint Handling Rules, Report CW 555, pp. 33–48. Katholieke Universiteit Leuven, Belgium (2009)

    Google Scholar 

  28. Schrijvers, T., Demoen, B.: The K.U.Leuven CHR system: Implementation and Application. In: Workshop on Constraint Handling Rules: Selected Contributions, pp. 1–5. Ulmer Informatik-Berichte, Nr. 2004–01 (2004)

    Google Scholar 

Download references

Acknowledgement

We thank the anonymous reviewers for their insightful comments, suggesting to compare with a transformational approach, cf. Example 5, and helping us to clarify the relationship between abstract simulation and abstract interpretation.

Author information

Authors and Affiliations

  1. Computer Science, Roskilde University, Roskilde, Denmark

    Henning Christiansen & Maja H. Kirkeby

Authors
  1. Henning Christiansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maja H. Kirkeby
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Henning Christiansen or Maja H. Kirkeby .

Editor information

Editors and Affiliations

  1. University of Reunion Island, Sainte-Clotilde, France

    Fred Mesnard

  2. Monash University, Melbourne, VIC, Australia

    Peter J. Stuckey

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Christiansen, H., Kirkeby, M.H. (2019). Confluence of CHR Revisited: Invariants and Modulo Equivalence. In: Mesnard, F., Stuckey, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2018. Lecture Notes in Computer Science(), vol 11408. Springer, Cham. https://doi.org/10.1007/978-3-030-13838-7_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-13838-7_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-13837-0

  • Online ISBN: 978-3-030-13838-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation