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

  • Henning ChristiansenEmail author
  • Maja H. KirkebyEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11285)


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.


  1. 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). Scholar
  2. 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). Scholar
  3. 3.
    Abdennadher, S., Frühwirth, T.W., Meuss, H.: Confluence and semantics of constraint simplification rules. Constraints 4(2), 133–165 (1999)MathSciNetCrossRefGoogle Scholar
  4. 4.
    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). Scholar
  5. 5.
    Christiansen, H., Kirkeby, M.H.: On proving confluence modulo equivalence for constraint handling rules. Formal Aspects Comput. 29(1), 57–95 (2017)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Christiansen, H., Kirkeby, M.H.: Confluence of CHR revisited: invariants and modulo equivalence. In: LOPSTR 2018, vol. 11408. LNCS, pp. 83–99. Springer, Heidelberg (2019)Google Scholar
  7. 7.
    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). Scholar
  8. 8.
    Endrullis, J., de Vrijer, R.C., Waldmann, J.: Local termination: theory and practice. Logical Methods Comput. Sci. 6(3), 1–37 (2010)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Frühwirth, T.W.: User-defined constraint handling. In: ICLP, pp. 837–838. MIT Press (1993)Google Scholar
  10. 10.
    Frühwirth, T.W.: Theory and practice of constraint handling rules. J. Logic Program. 37(1–3), 95–138 (1998)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Frühwirth, T.: Proving termination of constraint solver programs. In: Apt, K.R., Monfroy, E., Kakas, A.C., Rossi, F. (eds.) WC 1999. LNCS (LNAI), vol. 1865, pp. 298–317. Springer, Heidelberg (2000). Scholar
  12. 12.
    Frühwirth, T.W.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009)CrossRefGoogle Scholar
  13. 13.
    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). Scholar
  14. 14.
    Holzbaur, C., Frühwirth, T.W.: A PROLOG constraint handling rules compiler and runtime system. Appl. Artif. Intell. 14(4), 369–388 (2000)CrossRefGoogle Scholar
  15. 15.
    Huet, G.P.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Langbein, J., Raiser, F., Frühwirth, T.W.: A state equivalence and confluence checker for CHRs. In: Proceedings International Workshop on Constraint Handling Rules, Report CW 588, pp. 1–8. Katholieke Universiteit Leuven, Belgium (2010)Google Scholar
  17. 17.
    Newman, M.: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43(2), 223–243 (1942)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Pilozzi, P., De Schreye, D.: Automating termination proofs for CHR. In: Hill, P.M., Warren, D.S. (eds.) ICLP 2009. LNCS, vol. 5649, pp. 504–508. Springer, Heidelberg (2009). Scholar
  19. 19.
    Pilozzi, P., De Schreye, D.: Improved termination analysis of CHR using self-sustainability analysis. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 189–204. Springer, Heidelberg (2012). Scholar
  20. 20.
    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

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Computer ScienceRoskilde UniversityRoskildeDenmark

Personalised recommendations