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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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
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
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
Abdennadher S, Frühwirth TW, Meuss H (1999) Confluence and semantics of constraint simplification rules. Constraints 4(2): 133–165
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
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
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
Baader F, Nipkow T (1999) Term rewriting and all that. Cambridge University Press, Cambridge
Betz H, Raiser F, Frühwirth TW (2010) A complete and terminating execution model for constraint handling rules. TPLP 10(4–6): 597–610
Christiansen H (2005) CHR Grammars. Int J Theory Pract Logic Program 5(4–5): 467–501
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
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
Drabent W (1997) A Floyd-Hoare method for Prolog. Tech. Rep. 2(13), Linköping Electronic Articles in Computer and Information Science
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
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
Durbin R, Eddy S, Krogh A, Mitchison G (1999) Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, Cambridge
Falaschi M, Gabbrielli M, Marriott K, Palamidessi C (1997) Confluence in concurrent constraint programming. Theor Comput Sci 183(2): 281–315
Frühwirth T, Raiser F (eds) (2011) Constraint Handling Rules, Compilation, Execution, and Analysis. Books on Demand GmbH. Norderstedt
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
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
Frühwirth TW (1998) Theory and practice of Constraint Handling Rules. J Logic Program 37(1–3): 95–138
Frühwirth TW (2009) Constraint Handling Rules. Cambridge University Press, Cambridge
Haemmerlé R (2012) Diagrammatic confluence for Constraint Handling Rules. TPLP 12(4–5): 737–753
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
Holzbaur C, Frühwirth TW (2000) A PROLOG Constraint Handling Rules compiler and runtime system. Appl Artif Intell 14(4): 369–388
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
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
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
Mayr R, Nipkow T (1998) Higher-order rewrite systems and their confluence. Theor Comput Sci 192(1): 3–29
Newman M (1942) On theories with a combinatorial definition of “equivalence”. Ann Math 43(2): 223–243
Niehren J (2000) Uniform confluence in concurrent computation. J Funct Program 10(5): 453–499
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
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
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
Personal communication with Tom Schrijvers (2016)
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
Schrijvers T, Frühwirth TW (eds) (2008) Constraint Handling Rules, Current Research Topics, Lecture Notes in Computer Science, vol 5388. Springer, New York
Sethi R (1974) Testing for the Church-Rosser property. J ACM 21(4): 671–679
Sneyers J, Weert PV, Schrijvers T, Koninck LD (2010) As time goes by: Constraint Handling Rules. TPLP 10(1): 1–47
Tarjan RE, Van Leeuwen J (1984) Worst-case analysis of set union algorithms. J ACM 31(2): 245–281
Viterbi AJ (1967) Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Trans Inf Theory 13: 260–269
Author information
Authors and Affiliations
Corresponding author
Additional information
Maurizio Proietti, Hirohisa Seki and Jim Woodcock
Rights and permissions
About this article
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
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0396-9