Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Analyzing Array Manipulating Programs by Program Transformation Read chapter Read first chapter

2015 | OriginalPaper | Chapter

Confluence Modulo Equivalence in Constraint Handling Rules

Authors : Henning Christiansen, Maja H. Kirkeby

Published in: Logic-Based Program Synthesis and Transformation

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Analysing and Compiling Coroutines with Abstract Conjunctive Partial Deduction
next chapter Exhaustive Execution of CHR Through Source-to-Source Transformation
Footnotes
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.
 
Literature
1.
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.
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.
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.
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.
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.
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.
Durbin, R., Eddy, S., Krogh, A., Mitchison, G.: Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, Cambridge (1999)
8.
Frühwirth, T.W.: Theory and practice of Constraint Handling Rules. J. Logic Progr. 37(1–3), 95–138 (1998)CrossRefMATH
9.
10.
Haemmerlé, R.: Diagrammatic confluence for Constraint Handling Rules. TPLP 12(4–5), 737–753 (2012)MATH
11.
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.
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.
Newman, M.: On theories with a combinatorial definition of “equivalence”. Ann. Math. 43(2), 223–243 (1942)CrossRefMATH
14.
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.
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.
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)
17.
18.
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.
Tarjan, R.E., van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245–281 (1984)CrossRefMATH
20.
Viterbi, A.J.: Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Trans. Inform. Theory 13, 260–269 (1967)CrossRefMATH
Metadata
Title
Confluence Modulo Equivalence in Constraint Handling Rules
Authors
Henning Christiansen
Maja H. Kirkeby
Copyright Year
2015
Book
Logic-Based Program Synthesis and Transformation

Print ISBN: 978-3-319-17821-9

Electronic ISBN: 978-3-319-17822-6

Copyright Year: 2015

DOI
https://doi.org/10.1007/978-3-319-17822-6_3

Premium Partner

    Image Credits