Skip to main content

2015 | OriginalPaper | Buchkapitel

Confluence Modulo Equivalence in Constraint Handling Rules

verfasst von : Henning Christiansen, Maja H. Kirkeby

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Previous results on confluence for Constraint Handling Rules, CHR, are generalized to take into account user-defined state equivalence relations. This allows a much larger class of programs to enjoy the advantages of confluence, which include various optimization techniques and simplified correctness proofs. A new operational semantics for CHR is introduced that significantly reduces notational overhead and allows to consider confluence for programs with extra-logical and incomplete built-in predicates. Proofs of confluence are demonstrated for programs with redundant data representation, e.g., sets-as-lists, for dynamic programming algorithms with pruning as well as a Union-Find program, which are not covered by previous confluence notions for CHR.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
It may be the case that \(\pi '_1\) was produced and pruned at an earlier stage, so the propagation history prevents the creation of \(\pi '_1\) anew. A detailed argument can show, that in this case, there will be another constraints \(\pi ''_1\) in the store similar to \(\pi '_1\) but with a \(\ge \) probability, and \(\pi ''_1\) can be used for pruning \(\pi '_2\) and obtain the desired result in that way.
 
Literatur
1.
Zurück zum Zitat Abdennadher, S.: Operational semantics and confluence of constraint propagation rules. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 252–266. Springer, Heidelberg (1997) CrossRef Abdennadher, S.: Operational semantics and confluence of constraint propagation rules. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 252–266. Springer, Heidelberg (1997) CrossRef
2.
Zurück zum Zitat Abdennadher, S., Frühwirth, T.W., Meuss, H.: On confluence ofconstraint handling rules. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 1–15. Springer, Heidelberg (1996) CrossRef Abdennadher, S., Frühwirth, T.W., Meuss, H.: On confluence ofconstraint handling rules. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 1–15. Springer, Heidelberg (1996) CrossRef
3.
Zurück zum Zitat Aho, A.V., Sethi, R., Ullman, J.D.: Code optimization and finite Church-Rosser systems. In: Rustin, R. (ed.) Design and Optimization of Compilers, pp. 89–106. Prentice-Hall, Englewood Cliffs (1972) Aho, A.V., Sethi, R., Ullman, J.D.: Code optimization and finite Church-Rosser systems. In: Rustin, R. (ed.) Design and Optimization of Compilers, pp. 89–106. Prentice-Hall, Englewood Cliffs (1972)
4.
Zurück zum Zitat Christiansen, H., Have, C.T., Lassen, O.T., Petit, M.: 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, pp. 17–24. Katholieke Universiteit Leuven, Belgium (2010) Christiansen, H., Have, C.T., Lassen, O.T., Petit, M.: 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, pp. 17–24. Katholieke Universiteit Leuven, Belgium (2010)
5.
Zurück zum Zitat Duck, G.J., Stuckey, P.J., García de la Banda, M., Holzbaur, C.: The refined operational semantics of constraint handling rules. In: Bart, D., Vladimir, L. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 90–104. Springer, Heidelberg (2004) CrossRef Duck, G.J., Stuckey, P.J., García de la Banda, M., Holzbaur, C.: The refined operational semantics of constraint handling rules. In: Bart, D., Vladimir, L. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 90–104. Springer, Heidelberg (2004) CrossRef
6.
Zurück zum Zitat Duck, G.J., Stuckey, P.J., Sulzmann, M.: Observable confluence for constraint handling rules. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 224–239. Springer, Heidelberg (2007) CrossRef Duck, G.J., Stuckey, P.J., Sulzmann, M.: Observable confluence for constraint handling rules. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 224–239. Springer, Heidelberg (2007) CrossRef
7.
Zurück zum Zitat Durbin, R., Eddy, S., Krogh, A., Mitchison, G.: Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, Cambridge (1999) Durbin, R., Eddy, S., Krogh, A., Mitchison, G.: Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, Cambridge (1999)
8.
Zurück zum Zitat Frühwirth, T.W.: Theory and practice of Constraint Handling Rules. J. Logic Progr. 37(1–3), 95–138 (1998)CrossRefMATH Frühwirth, T.W.: Theory and practice of Constraint Handling Rules. J. Logic Progr. 37(1–3), 95–138 (1998)CrossRefMATH
9.
Zurück zum Zitat Frühwirth, T.W.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009) CrossRefMATH Frühwirth, T.W.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009) CrossRefMATH
10.
Zurück zum Zitat Haemmerlé, R.: Diagrammatic confluence for Constraint Handling Rules. TPLP 12(4–5), 737–753 (2012)MATH Haemmerlé, R.: Diagrammatic confluence for Constraint Handling Rules. TPLP 12(4–5), 737–753 (2012)MATH
11.
Zurück zum Zitat Huet, G.P.: Confluent reductions: abstract properties and applications to term rewriting systems: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)CrossRefMATHMathSciNet Huet, G.P.: Confluent reductions: abstract properties and applications to term rewriting systems: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)CrossRefMATHMathSciNet
12.
Zurück zum Zitat Langbein, J., Raiser, F., Frühwirth, T.W.: A state equivalence and confluence checker for CHRs. In: Weert, P.V., Koninck, L.D. (eds.) Proceedings of the 7th International Workshop on Constraint Handling Rules. Report CW 588, pp. 1–8. Katholieke Universiteit Leuven, Belgium (2010) Langbein, J., Raiser, F., Frühwirth, T.W.: A state equivalence and confluence checker for CHRs. In: Weert, P.V., Koninck, L.D. (eds.) Proceedings of the 7th International Workshop on Constraint Handling Rules. Report CW 588, pp. 1–8. Katholieke Universiteit Leuven, Belgium (2010)
13.
Zurück zum Zitat Newman, M.: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43(2), 223–243 (1942)CrossRefMATH Newman, M.: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43(2), 223–243 (1942)CrossRefMATH
14.
Zurück zum Zitat Raiser, F., Betz, H., Frühwirth, T.W.: Equivalence of CHR states revisited. In: Raiser, F., Sneyers, J. (eds.) Proceedings of the 6th International Workshop on Constraint Handling Rules, Report CW 555, pp. 33–48. Katholieke Universiteit Leuven, Belgium (2009) Raiser, F., Betz, H., Frühwirth, T.W.: Equivalence of CHR states revisited. In: Raiser, F., Sneyers, J. (eds.) Proceedings of the 6th International Workshop on Constraint Handling Rules, Report CW 555, pp. 33–48. Katholieke Universiteit Leuven, Belgium (2009)
15.
Zurück zum Zitat Raiser, F., Tacchella, P.: On confluence of non-terminating CHR programs. In: Djelloul, K., Duck, G.J., Sulzmann, M. (eds.) CHR 2007, pp. 63–76. Porto, Portugal (2007) Raiser, F., Tacchella, P.: On confluence of non-terminating CHR programs. In: Djelloul, K., Duck, G.J., Sulzmann, M. (eds.) CHR 2007, pp. 63–76. Porto, Portugal (2007)
16.
Zurück zum Zitat Schrijvers, T., Frühwirth, T.W.: Analysing the CHR implementation of union-find. In: Wolf, A., Frühwirth, T.W., Meister, M. (eds.) W(C)LP. Ulmer Informatik-Berichte, vol. 2005-01, pp. 135–146. Universität Ulm, Ulm (2005) Schrijvers, T., Frühwirth, T.W.: Analysing the CHR implementation of union-find. In: Wolf, A., Frühwirth, T.W., Meister, M. (eds.) W(C)LP. Ulmer Informatik-Berichte, vol. 2005-01, pp. 135–146. Universität Ulm, Ulm (2005)
18.
Zurück zum Zitat Sneyers, J., Weert, P.V., Schrijvers, T., Koninck, L.D.: As time goes by: Constraint Handling Rules. TPLP 10(1), 1–47 (2010)MATH Sneyers, J., Weert, P.V., Schrijvers, T., Koninck, L.D.: As time goes by: Constraint Handling Rules. TPLP 10(1), 1–47 (2010)MATH
19.
Zurück zum Zitat Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245–281 (1984)CrossRefMATH Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245–281 (1984)CrossRefMATH
20.
Zurück zum Zitat Viterbi, A.J.: Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Trans. Inform. Theory 13, 260–269 (1967)CrossRefMATH Viterbi, A.J.: Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Trans. Inform. Theory 13, 260–269 (1967)CrossRefMATH
Metadaten
Titel
Confluence Modulo Equivalence in Constraint Handling Rules
verfasst von
Henning Christiansen
Maja H. Kirkeby
Copyright-Jahr
2015
DOI
https://doi.org/10.1007/978-3-319-17822-6_3