Hostname: page-component-78c5997874-4rdpn Total loading time: 0 Render date: 2024-11-08T06:31:57.839Z Has data issue: false hasContentIssue false
  • English
  • Français

A complete and terminating execution model for Constraint Handling Rules

Published online by Cambridge University Press:  09 July 2010

HARIOLF BETZ ,
FRANK RAISER  and
THOM FRÜHWIRTH
HARIOLF BETZ
Affiliation:
Faculty of Engineering and Computer Science, Ulm University, Germany (e-mail: [email protected])
FRANK RAISER
Affiliation:
Faculty of Engineering and Computer Science, Ulm University, Germany (e-mail: [email protected])
THOM FRÜHWIRTH
Affiliation:
Faculty of Engineering and Computer Science, Ulm University, Germany (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics ω!, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we provide an implementation in the form of a source-to-source transformation to CHR with rule priorities.

Keywords

Constraint Handling Rulesoperational semanticsexecution modelpersistent constraints
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 10 , Special Issue 4-6: 26th International Conference on Logic Programming , July 2010 , pp. 597 - 610
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abdennadher, S. 1997. Operational semantics and confluence of constraint propagation rules. In 3rd International Conf. on Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, 1330. Springer, 252–266.Google Scholar
Abdennadher, S. and Frühwirth, T. 1999. Operational equivalence of CHR programs and constraints. In Principles and Practice of Constraint Programming, CP 1999, Jaffar, J., Ed. Lecture Notes in Computer Science, vol. 1713. Springer, 43–57.Google Scholar
Abdennadher, S., Frühwirth, T., and Meuss, H. 1999. Confluence and semantics of constraint simplification rules. Constraints 4, 2, 133–165.CrossRefGoogle Scholar
Betz, H. and Frühwirth, T. 2005. A linear-logic semantics for constraint handling rules. In Principles and Practice of Constraint Programming, 11th International Conference, CP 2005, van Beek, P., Ed. Lecture Notes in Computer Science, vol. 3709. Springer, Sitges, Spain, 137–151.CrossRefGoogle Scholar
Betz, H., Raiser, F., and Frühwirth, T. 2009. Persistent constraint in constraint handling rules. In Proceedings of 23rd Workshop on (Constraint) Logic Programming, WLP 2009 (to appear).Google Scholar
Betz, H., Raiser, F., and Frühwirth, T. 2010. A Complete and Terminating Execution Model for Constraint Handling Rules. Technical Report 01, Ulm University.Google Scholar
De Koninck, L. 2009. Logical Algorithms meets CHR: A meta-complexity result for Constraint Handling Rules with rule priorities. Theory and Practice of Logic Programming 9, 2 (March), 165–212.CrossRefGoogle Scholar
De Koninck, L., Schrijvers, T., and Demoen, B. 2007. User-definable rule priorities for CHR. In PPDP '07: Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming. ACM, New York, 25–36.CrossRefGoogle Scholar
De Koninck, L., Stuckey, P. J., and Duck, G. J. 2008. Optimizing compilation of CHR with rule priorities. In Functional and Logic Programming, 9th International Symposium (FLOPS), Garrigue, J. and Hermenegildo, M. V., Eds. Lecture Notes in Computer Science, vol. 4989. Springer, 32–47.CrossRefGoogle Scholar
Duck, G. J., Stuckey, P. J., García de la Banda, M., and Holzbaur, C. 2004. The refined operational semantics of Constraint Handling Rules. In Logic Programming, 20th International Conference, ICLP 2004, Demoen, B. and Lifschitz, V., Eds. Lecture Notes in Computer Science, vol. 3132. Springer, Saint-Malo, France, 90–104.Google Scholar
Frühwirth, T. 1998. Theory and practice of constraint handling rules. Journal of Logic Programming, Special Issue on Constraint Logic Programming 37, 1–3 (October), 95–138.CrossRefGoogle Scholar
Frühwirth, T. 2005. Parallelizing union-find in constraint handling rules using confluence analysis. In Logic Programming, 21st International Conference, ICLP 2005, Gabbrielli, M. and Gupta, G., Eds. Lecture Notes in Computer Science, vol. 3668. Springer, Sitges, Spain, 113–127.Google Scholar
Frühwirth, T. 2009. Constraint Handling Rules. Cambridge University Press.CrossRefGoogle Scholar
Frühwirth, T. and Abdennadher, S. 2003. Essentials of Constraint Programming. Springer.CrossRefGoogle Scholar
Frühwirth, T. and Hanschke, P. 1993. Terminological reasoning with Constraint Handling Rules. In Principles and Practice of Constraint Programming. MIT Press, 80–89.Google Scholar
Gabbrielli, M., Mauro, J., and Meo, M. C. 2009. On the expressive power of priorities in CHR. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Porto, A. and López-Fraguas, F. J., Eds. ACM, Coimbra, Portugal, 267–276.Google Scholar
Ganzinger, H. and McAllester, D. A. 2002. Logical algorithms. In Logic Programming, 18th International Conference, ICLP 2002, Stuckey, P. J., Ed. Lecture Notes in Computer Science, vol. 2401. Springer, 209–223.Google Scholar
Pilozzi, P. and De Schreye, D. 2009. Proving termination by invariance relations. In 25th International Conference Logic Programming, ICLP, Hill, P. M. and Warren, D. S., Eds. Lecture Notes in Computer Science, vol. 5649. Springer, Pasadena, CA, 499–503.Google Scholar
Raiser, F., Betz, H., and Frühwirth, T. 2009. Equivalence of CHR states revisited. In 6th International Workshop on Constraint Handling Rules (CHR), Raiser, F. and Sneyers, J., Eds. 34–48.Google Scholar
Sarna-Starosta, B. and Ramakrishnan, C. 2007. Compiling Constraint Handling Rules for efficient tabled evaluation. In 9th Intl. Symp. Practical Aspects of Declarative Languages, PADL, Hanus, M., Ed. Lecture Notes in Computer Science, vol. 4354. Springer, Nice, France, 170–184.Google Scholar
Simmons, R. J. and Pfenning, F. 2008. Linear logical algorithms. In Automata, Languages and Programming, 35th International Colloquium, ICALP 2008, Aceto, L., Damgård, I., Goldberg, L. A., Halldórsson, M. M., Ingólfsdóttir, A., and Walukiewicz, I., Eds. Lecture Notes in Computer Science, vol. 5126. Springer, 336–347.Google Scholar
Sneyers, J., Van Weert, P., Schrijvers, T., and De Koninck, L. 2010. As time goes by: Constraint Handling Rules–A survey of CHR research between 1998 and 2007. Theory and Practice of Logic Programming 10, 1, 1–47.CrossRefGoogle Scholar
Sulzmann, M. and Lam, E. S. L. 2007. A concurrent constraint handling rules semantics and its implementation with software transactional memory. In Proceedings of the POPL 2007 Workshop on Declarative Aspects of Multicore Programming, Glew, N. and Blelloch, G. E., Eds. ACM, 19–24.Google Scholar
Sulzmann, M. and Lam, E. S. L. 2008. Parallel execution of multi-set constraint rewrite rules. In Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), Antoy, S. and Albert, E., Eds. ACM, Valencia, Spain, 20–31.Google Scholar