Operational semantics and confluence of constraint propagation rules
Constraint Handling Rules (CHR) allow one to specify and implement both propagation and simplification for user-defined constraints. Since a propagation rule is applicable again and again, we present in this paper for the first time an operational semantics for CHR that avoids the termination problem with propagation rules.
In previous work [AFM96], a sufficient and necessary condition for the confluence of terminating simplification rules was given inspired by results about conditional term rewriting systems. Confluence ensures that the solver will always compute the same result for a given set of constraints independent of which rules are applied. The confluence of propagation rules was an open problem. This paper shows that we can also give a sufficient and a necessary condition for confluence of terminating CHR programs with propagation rules based on the more refined operational semantics.
KeywordsOperational Semantic Critical Pair Constraint Solver Minimal Pair Applicability Condition
Unable to display preview. Download preview PDF.
- Abd97.S. Abdennadher. Rewriting concepts in the study of confluence of constraint handling rules. Technical report PMS-FB-1997-15, Institute of Computer Science, Ludwig-Maximilians-University Munich, January 1997.Google Scholar
- AFM96.S. Abdennadher, T. Frühwirth, and H. Meuss. On confluence of constraint handling rules. In E. Freuder, editor, Proceedings of the Second International Conference on Principles and Practice of Constraint Programming, CP'96, LNCS 1118. Springer, August 1996.Google Scholar
- BFL+94.P. Brisset, T. Frühwirth, P. Lim, M. Meier, T. Le Provost, J. Schimpf, and M. Wallace. ECL iPSe 3.4 Extensions User Manual. ECRC Munich Germany, July 1994.Google Scholar
- DOS88.N. Dershowitz, N. Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, LNCS 308, pages 31–44, 1988.Google Scholar
- Frü95.T. Frühwirth. Constraint handling rules. In A. Podelski, editor, Constraint Programming: Basics and Trends, LNCS 910. Springer, 1995.Google Scholar
- JM94.J. Jaffar and M. J. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 20:503–581, 1994.Google Scholar
- Meu96.Holger Meuss. Konfluenz von Constraint-Handling-Rules-Programmen. Master's thesis, Institut für Informatik, Ludwig-Maximilians-Universität München, 1996.Google Scholar
- New42.M. H. A. Newman. On theories with a combinatorial definition of equivalence. In Annals of Math, volume 43, pages 223–243, 1942.Google Scholar
- Sar93.V.A. Saraswat. Concurrent Constraint Programming. MIT Press, Cambridge, 1993.Google Scholar
- vH91.P. van Hentenryck. Constraint logic programming. The Knowledge Engineering Review, 6:151–194, 1991.Google Scholar
- ZR85.H. Zhang and J. L. Remy. Contextual rewriting. In Jean-Pierre Jouannaud, editor, Proceedings of the 1st International Conference on Rewriting Techniques and Applications, volume 202 of LNCS, pages 46–62, Dijon, France, May 1985. Springer.Google Scholar