A compositional semantics for CHR

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

A compositional semantics for CHR

Full text

Pdf (283 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 2 (February 2009) table of contents

Article No.: 11

Year of Publication: 2009

ISSN:1529-3785

Authors

Maurizio Gabbrielli	Università di Bologna, Bologna, Italy
Maria Chiara Meo	Università “G. D'Annunzio” di Chieti-Pescara, Pescara, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 68, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1462179.1462183 What is a DOI?

ABSTRACT

Constraint Handling Rules (CHR) is a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached.

CHR has received considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multiheaded clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far.

In this article we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Abdennadher, S. 1997. Operational semantics and confluence of constraint propagation rules. In Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP'97), G. Smolka, Ed. Lecture Notes in Computer Science, vol. 1330. Springer.
	2	Thom Fruewirth , Slim Abdennadher, Essentials of Constraint Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
	3	Betz, H. and Frühwirth, T. 2005. A linear-logic semantics for constraint handling rules. In Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP '05). Lecture Notes in Computer Science, vol. 3709. Springer.
	4	Frank S. De Boer , Maurizio Gabbrielli , Elena Marchiori , Catuscia Palamidessi, Proving concurrent constraint programs correct, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.685-725, Sept. 1997 [doi>10.1145/265943.265954]
	5	F. S. de Boer , M. Gabbrielli , M. C. Meo, A timed concurrent constraint language, Information and Computation, v.161 n.1, p.45-83, Aug. 25, 2000 [doi>10.1006/inco.1999.2879]
	6	Frank S. De Boer , Maurizio Gabbrielli , Maria Chiara Meo, Proving correctness of timed concurrent constraint programs, ACM Transactions on Computational Logic (TOCL), v.5 n.4, p.706-731, October 2004 [doi>10.1145/1024922.1024926]
	7	Frank S. de Boer , Maurizio Gabbrielli , Maria C. Meo, A Timed Linda Language and its Denotational Semantics, Fundamenta Informaticae, v.63 n.4, p.309-330, June 2004
	8	Frank S. de Boer , Joost N. Kok , Catuscia Palamidessi , Jan J. M. M. Rutten, The Failure of Failures in a Paradigm for Asynchronous Communication, Proceedings of the 2nd International Conference on Concurrency Theory, p.111-126, August 26-29, 1991
	9	Frank S. de Boer , Catuscia Palamidessi, A fully abstract model for concurrent constraint programming, Proceedings of the international joint conference on theory and practice of software development on Colloquium on trees in algebra and programming (CAAP '91): vol 1, p.296-319, April 1991, Brighton, United Kingdom
	10	A. Bossi , M. Gabbrielli , G. Levi , M. C. Meo, A compositional semantics for logic programs, Theoretical Computer Science, v.122 n.1-2, p.3-47, Jan. 3, 1994
	11	Brookes, S. 1993. A fully abstract semantics of a shared variable parallel language. In Proceedings of the 8th IEEE Symposium on Logic In Computer Science. IEEE Computer Society Press.
	12	Michael Codish , Saumya K. Debray , Roberto Giacobazzi, Compositional analysis of modular logic programs, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.451-464, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158703]
	13	Davey, B. A. and Priestley, H. A. 1990. Introduction to Lattices and Order. Cambridge University Press.
	14	Giorgio Delzanno , Maurizio Gabbrielli , Maria Chiara Meo, A compositional semantics for CHR, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.209-217, July 11-13, 2005, Lisbon, Portugal [doi>10.1145/1069774.1069794]
	15	Duck, G. J., de la Banda, M. G., and Stuckey, P. J. 2004. The refined operational semantics of constraint handling rules. In Proceedings of the 20th International Conference on Logic Programming, (ICLP'04).
	16	Falaschi, M., Gabbrielli, M., Marriott, K., and Palamidessi, C. 1993. Compositional analysis of concurrent constraint languages. In Proceedings of the 8th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press.
	17	Frühwirth, T. 1991. Introducing simplification rules. Tech. rep. TR ECRC-LP-63, ECRC Munich. October.
	18	Frühwirth, T. 1998. Theory and practice of constraint handling rules. J. Logic Program. 37, 1-3, 95--138.
	19	Gabbrielli, M., Meo, M. C., and Tacchella, P. 2006. A compositional semantics for CHR with propagation rules. In Proceedings of the 3rd Workshop on Constraint Handling Rules. Tech. rep. CW 425, Katholieke Universiteit Leuven. June.
	20	Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani, You Assume, We Guarantee: Methodology and Case Studies, Proceedings of the 10th International Conference on Computer Aided Verification, p.440-451, June 28-July 02, 1998
	21	Bengt Jonsson, A model and proof system for asynchronous networks, Proceedings of the fourth annual ACM symposium on Principles of distributed computing, p.49-58, August 1985, Minaki, Ontario, Canada [doi>10.1145/323596.323601]
	22	Michael J. Maher, Propagation Completeness of Reactive Constraints, Proceedings of the 18th International Conference on Logic Programming, p.148-162, July 29-August 01, 2002
	23	Meister, M., Djelloul, K., and Robin, J. 2007. A unified semantics for CHR in transaction logic. In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07). Lecture Notes in Artificial Intelligence, vol. 4483, Springer, 201--213.