SpringerLink
Log in

On proving confluence modulo equivalence for Constraint Handling Rules

  • Original Article
  • Published:
Formal Aspects of Computing

Abstract

Previous results on proving confluence for Constraint Handling Rules are extended in two ways in order to allow a larger and more realistic class of CHR programs to be considered confluent. Firstly, we introduce the relaxed notion of confluence modulo equivalence into the context of CHR: while confluence for a terminating program means that all alternative derivations for a query lead to the exact same final state, confluence modulo equivalence only requires the final states to be equivalent with respect to an equivalence relation tailored for the given program. Secondly, we allow non-logical built-in predicates such as var/1 and incomplete ones such as is/2, that are ignored in previous work on confluence.

To this end, a new operational semantics for CHR is developed which includes such predicates. In addition, this semantics differs from earlier approaches by its simplicity without loss of generality, and it may also be recommended for future studies of CHR.

For the purely logical subset of CHR, proofs can be expressed in first-order logic, that we show is not sufficient in the present case. We have introduced a formal meta-language that allows reasoning about abstract states and derivations with meta-level restrictions that reflect the non-logical and incomplete predicates. This language represents subproofs as diagrams, which facilitates a systematic enumeration of proof cases, pointing forward to a mechanical support for such proofs.

The Project is supported by The DanishCouncil for IndependentResearch, Natural Sciences, Grant No. DFF4181-00442. The second author’s contribution received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under Grant Agreement No. 318337, ENTRA—Whole-Systems Energy Transparency.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Germany)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abdennadher S (1997) Operational semantics and confluence of constraint propagation rules. In: Smolka G (ed) CP, Constraint Programming, Lecture Notes in Computer Science, vol 1330. Springer, New York, pp 252–266

  2. Abdennadher S, Frühwirth TW (2003) Integration and optimization of rule-based constraint solvers. In: Bruynooghe M (ed) Logic Based Program Synthesis and Transformation, 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25–27, 2003, Revised Selected Papers, Lecture Notes in Computer Science, vol 3018. Springer, New York, pp 198–213

  3. Abdennadher S, Frühwirth TW, Meuss H (1996) On confluence of Constraint Handling Rules. In: Freuder EC (ed) CP, Lecture Notes in Computer Science, vol 1118. Springer, New York, pp 1–15

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

    Article  MathSciNet  MATH  Google Scholar 

  5. Aho AV, Sethi R, Ullman JD (1972) Code optimization and finite Church-Rosser systems. In: Rustin R (ed) Design and Optimization of Compilers. Prentice-Hall, USA, pp 89–106

  6. Aiken A, Widom J, Hellerstein JM (1992) Behavior of database production rules: Termination, confluence, and observable determinism. In: Stonebraker M (ed) Proceedings of the 1992 ACM SIGMOD International Conference on Management of Data, San Diego, California. ACM Press, USA, pp 59–68

  7. Apt KR, Marchiori E, Palamidessi C (1994) A declarative approach for first-order built-in’s of Prolog. Appl Algebra Eng Commun Comput 5: 159–191

    Article  MathSciNet  MATH  Google Scholar 

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

    MATH  Google Scholar 

  9. Betz H, Raiser F, Frühwirth TW (2010) A complete and terminating execution model for constraint handling rules. TPLP 10(4–6): 597–610

    MathSciNet  MATH  Google Scholar 

  10. Christiansen H (2005) CHR Grammars. Int J Theory Pract Logic Program 5(4–5): 467–501

    Article  MathSciNet  MATH  Google Scholar 

  11. Christiansen H, Have CT, Lassen OT, Petit M (2010) The Viterbi algorithm expressed in Constraint Handling Rules. In: Van Weert P, De Koninck L (eds) Proceedings of the 7th International Workshop on Constraint Handling Rules, Report CW 588. Katholieke Universiteit Leuven, Belgium, pp 17–24

  12. Christiansen H, Kirkeby MH (2010) Confluence modulo equivalence in Constraint Handling Rules. In: Proietti M, Seki H (eds) Logic-Based Program Synthesis and Transformation—24th International Symposium, LOPSTR 2014, Canterbury, UK, September 9–11, 2014. Revised Selected Papers, Lecture Notes in Computer Science, vol 8981. Springer, New York, pp 41–58

  13. Drabent W (1997) A Floyd-Hoare method for Prolog. Tech. Rep. 2(13), Linkö** Electronic Articles in Computer and Information Science

  14. Duck GJ, Stuckey PJ, De la Banda MJG, Holzbaur C (2004) The refined operational semantics of Constraint Handling Rules. In: Demoen B, Lifschitz V (eds) Proc. Logic Programming, 20th International Conference, ICLP 2004, Lecture Notes in Computer Science, vol 3132. Springer, New York, pp 90–104

  15. Duck GJ, Stuckey PJ, Sulzmann M (2007) Observable confluence for Constraint Handling Rules. In: Dahl V, Niemelä I (eds) ICLP, Lecture Notes in Computer Science, vol 4670. Springer, New York, pp 224–239

  16. Durbin R, Eddy S, Krogh A, Mitchison G (1999) Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, Cambridge

    MATH  Google Scholar 

  17. Falaschi M, Gabbrielli M, Marriott K, Palamidessi C (1997) Confluence in concurrent constraint programming. Theor Comput Sci 183(2): 281–315

    Article  MathSciNet  MATH  Google Scholar 

  18. Frühwirth T, Raiser F (eds) (2011) Constraint Handling Rules, Compilation, Execution, and Analysis. Books on Demand GmbH. Norderstedt

  19. Frühwirth TW (1993) User-defined constraint handling. In: Warren DS (ed) Logic Programming, Proceedings of the Tenth International Conference on Logic Programming. MIT Press, Budapest, Hungary, pp 837–838

  20. Frühwirth TW (1994) Constraint Handling Rules. In: Podelski A (ed) Constraint Programming: Basics and Trends, Châtillon Spring School, Châtillon-sur-Seine, France, May 16–20, 1994, Selected Papers, Lecture Notes in Computer Science, vol 910. Springer, New York, pp 90–107

  21. Frühwirth TW (1998) Theory and practice of Constraint Handling Rules. J Logic Program 37(1–3): 95–138

    Article  MathSciNet  MATH  Google Scholar 

  22. Frühwirth TW (2009) Constraint Handling Rules. Cambridge University Press, Cambridge

    Book  MATH  Google Scholar 

  23. Haemmerlé R (2012) Diagrammatic confluence for Constraint Handling Rules. TPLP 12(4–5): 737–753

    MathSciNet  MATH  Google Scholar 

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

  25. Holzbaur C, Frühwirth TW (2000) A PROLOG Constraint Handling Rules compiler and runtime system. Appl Artif Intell 14(4): 369–388

    Article  Google Scholar 

  26. Huet GP (1980) Confluent reductions: Abstract properties and applications to Knuth systems: abstract properties and applications to Term Rewriting Systems. J ACM 27(4): 797–821

    Article  MathSciNet  MATH  Google Scholar 

  27. Knuth D, Bendix P (1970) Simple word problems in universal algebras. In: Leech J (ed) Computational Problems in Universal Algebras. Pergamon Press, Oxford, pp 263–297

  28. Langbein J, Raiser F, Frühwirth TW (2010) A state equivalence and confluence checker for CHRs. In: Weert PV, Koninck LD (eds) Proceedings of the 7th International Workshop on Constraint Handling Rules, Report CW 588. Katholieke Universiteit Leuven, Belgium, pp 1–8

  29. Mayr R, Nipkow T (1998) Higher-order rewrite systems and their confluence. Theor Comput Sci 192(1): 3–29

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  31. Niehren J (2000) Uniform confluence in concurrent computation. J Funct Program 10(5): 453–499

    Article  MathSciNet  MATH  Google Scholar 

  32. Niehren J, Smolka G (1994) A confluent relational calculus for higher-order programming with constraints. In: Jouannaud J (ed) Constraints in Computational Logics, First International Conference, CCL’94, Munich, Germant, September 7–9, 1994, Lecture Notes in Computer Science, vol 845. Springer, New York, pp 89–104

  33. Raiser F, Betz H, Frühwirth TW (2009) Equivalence of CHR states revisited. In: Raiser F, Sneyers J (eds) Proc. 6th International Workshop on Constraint Handling Rules, Report CW 555. Katholieke Universiteit Leuven, Belgium, pp 33–48

  34. Raiser F, Tacchella P (2007) On confluence of non-terminating CHR programs. In: Djelloul K, Duck GJ, Sulzmann M (eds) Constraint Handling Rules, 4th Workshop, CHR 2007. Porto, Portugal, pp 63–76

  35. Personal communication with Tom Schrijvers (2016)

  36. Schrijvers T, Demoen B (2004) The K.U.Leuven CHR system: implementation and application. In: Frühwirth T, Meister M (eds) First Workshop on Constraint Handling Rules: Selected Contributions. Ulmer Informatik-Berichte, Nr. 2004-01, pp 1–5

  37. Schrijvers T, Frühwirth TW (eds) (2008) Constraint Handling Rules, Current Research Topics, Lecture Notes in Computer Science, vol 5388. Springer, New York

  38. Sethi R (1974) Testing for the Church-Rosser property. J ACM 21(4): 671–679

    Article  MathSciNet  MATH  Google Scholar 

  39. Sneyers J, Weert PV, Schrijvers T, Koninck LD (2010) As time goes by: Constraint Handling Rules. TPLP 10(1): 1–47

    MathSciNet  MATH  Google Scholar 

  40. Tarjan RE, Van Leeuwen J (1984) Worst-case analysis of set union algorithms. J ACM 31(2): 245–281

    Article  MathSciNet  MATH  Google Scholar 

  41. Viterbi AJ (1967) Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Trans Inf Theory 13: 260–269

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research group PLIS: Programming, Logic and Intelligent Systems, Department of People and Technology, 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 author

Correspondence to Henning Christiansen.

Additional information

Maurizio Proietti, Hirohisa Seki and Jim Woodcock

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Christiansen, H., Kirkeby, M.H. On proving confluence modulo equivalence for Constraint Handling Rules. Form Asp Comp 29, 57–95 (2017). https://doi.org/10.1007/s00165-016-0396-9

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-016-0396-9

Search

Navigation