Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-23T11:08:48.297Z Has data issue: false hasContentIssue false
  • English
  • Français

Diagrammatic confluence for Constraint Handling Rules*

Published online by Cambridge University Press:  05 September 2012

RÉMY HAEMMERLÉ
RÉMY HAEMMERLÉ*
Affiliation:
Technical University of Madrid
Get access Rights & Permissions [Opens in a new window]

Abstract

Confluence is a fundamental property of Constraint Handling Rules (CHR) since, as in other rewriting formalisms, it guarantees that the computations are not dependent on rule application order, and also because it implies the logical consistency of the program declarative view. In this paper we are concerned with proving the confluence of non-terminating CHR programs. For this purpose, we derive from van Oostrom's decreasing diagrams method a novel criterion on CHR critical pairs that generalizes all preexisting criteria. We subsequently improve on a result on the modularity of CHR confluence, which permits modular combinations of possibly non-terminating confluent programs, without loss of confluence.

Keywords

CHRconfluencedecreasing diagramsmodularity of confluence
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 12 , Issue 4-5: 28th International Conference on Logic Programming , July 2012 , pp. 737 - 753
Copyright
Copyright © Cambridge University Press 2012

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 Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). LNCS, vol. 1330. Springer, Berlin, Germany, 252–266.Google Scholar
Abdennadher, S. and Frühwirth, T. 1999. Operational equivalence of CHR programs and constraints. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). LNCS, vol. 1713. Springer, Berlin, Germany, 43–57.Google Scholar
Abdennadher, S., Frühwirth, T. and Meuss, H. 1996. On confluence of Constraint Handling Rules. In Proceedings of the International Conference on Principles and Practice of Constraint Programming (CP). LNCS, vol. 1118. Springer, Berlin, Germany, 1–15.Google Scholar
Abdennadher, S., Frühwirth, T. W. and Meuss, H. 1999. Confluence and semantics of constraint simplification rules. Constraints 4, 2, 133–165.CrossRefGoogle Scholar
Duck, G. J., Stuckey, P. J., Garcíade la Banda, M. de la Banda, M. and Holzbaur, C. 2005. The refined operational semantics of Constraint Handling Rules. In Proceedings of the International Conference on Logic Programming (ICLP). LNCS, vol. 3668. Springer, Berlin, Germany, 90–104.Google Scholar
Duck, G. J., Stuckey, P. J. and Sulzmann, M. 2007. Observable confluence for Constraint Handling Rules. In Proceedings of the International Conference on Logic Programming (ICLP). LNCS, vol. 4670. Springer, Berlin, Germany, 224–239.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, 95–138.CrossRefGoogle Scholar
Frühwirth, T. 2005. Parallelizing union-find in Constraint Handling Rules using confluence. In Proceedings of the International Conference on Logic Programming (ICLP). LNCS, vol. 3668. Springer, Berlin, Germany, 113–127.Google Scholar
Frühwirth, T. 2009. Constraint Handling Rules. Cambrige University Press, Cambrige, UK.CrossRefGoogle Scholar
Guy, R. 2004. Unsolved Problems in Number Theory. Problem Books in Mathematics. Springer, Berlin, Germany.CrossRefGoogle Scholar
Haemmerlé, R. 2011a. (Co)-Inductive semantics for Constraint Handling Rules. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue 11, 4–5, 593–609.Google Scholar
Haemmerlé, R. 2011b. Observational equivalences for linear logic concurrent constraint languages. Theory and Practice of Logic Programming, 27th Int'l. Conference on Logic Programming (ICLP'11) Special Issue 11, 4–5, 469–485.Google Scholar
Haemmerlé, R. and Fages, F. 2007. Abstract critical pairs and confluence of arbitrary binary relations. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA). LNCS, vol. 4533. Springer, Berlin, Germany, 214–228.Google Scholar
Haemmerlé, R., López, P. and Hermenegildo, M. 2011. CLP projection for Constraint Handling Rules. In Proceedings of the International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP). ACM Press, New York, NY, USA, 137–148.Google Scholar
Hirokawa, N. and Middeldorp, A. 2010. Decreasing diagrams and relative termination. In IJCAR. LNCS, vol. 6173. Springer, Berlin, Germany, 487–501.Google Scholar
Huet, G. 1980. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. Journal of the ACM 27, 4, 797–821.CrossRefGoogle Scholar
Jouannaud, J.-P. and vanOostrom, V. Oostrom, V. 2009. Diagrammatic confluence and completion. In Proceedings of 36th Internatilonal Collogquium on Automata, Languages and Programming: ICALP 2009. LNCS, vol. 5556. Springer, Berlin, Germany, 212–222.CrossRefGoogle Scholar
Meister, M. 2006. Fine-grained parallel implementation of the preflow-push algorithm in CHR. In Workshop on Logic Programming (WLP). INFSYS Research report 1843-06-02. T.U.Wien, Vienna, Austria, 172–181.Google Scholar
Milner, R. 1999. Communicating and Mobile Systems - the Pi-Calculus. Cambrige University Press, Cambrige, UK.Google Scholar
Newman, M. H. A. 1942. On theories with a combinatorial definition of “equivalence”. Annals of Mathematics 43, 2.CrossRefGoogle Scholar
Raiser, F., Betz, H. and Frühwirth, T. 2009. Equivalence of CHR states revisited. In Proceedings of the International Workshop on Constraint Handling Rules (CHR). Report CW 555. Kath. University Leuven, Leuven, Belgium, 34–48.Google Scholar
Raiser, F. and Tacchella, P. 2007. On confluence of non-terminating CHR programs. In Proceedings of the International Workshop on Constraint Handling Rules (CHR). 63–76.Google Scholar
Sneyers, J., Schrijvers, T. and Demoen, B. 2009. The computational power and complexity of Constraint Handling Rules. ACM Transactions on Programming Languages and Systems 31, 2.CrossRefGoogle Scholar
Terese. 2003. Term Rewriting Systems. Cambrige University Press, Cambrige, UK.Google Scholar
vanOostrom, V. Oostrom, V. 1994. Confluence by decreasing diagrams. Theoretical Computer Science 126, 2, 259–280.Google Scholar
vanOostrom, V. Oostrom, V. 2008. Confluence by decreasing diagrams converted. In Proceedings of the International Conference on Rewriting Techniques and Applications (RTA). LNCS. Springer, Berlin, Germany, 306–320.Google Scholar