Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms

  • Thom FrühwirthEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10855)


We present a straightforward source-to-source transformation that introduces justifications for user-defined constraints into the CHR programming language. Then a scheme of two rules suffices to allow for logical retraction (deletion, removal) of constraints during computation. Without the need to recompute from scratch, these rules remove not only the constraint but also undo all consequences of the rule applications that involved the constraint. We prove a confluence result concerning the rule scheme and show its correctness.

When algorithms are written in CHR, constraints represent both data and operations. CHR is already incremental by nature, i.e. constraints can be added at runtime. Logical retraction adds decrementality. Hence any algorithm written in CHR with justifications will become fully dynamic. Operations can be undone and data can be removed at any point in the computation without compromising the correctness of the result.

We present two classical examples of dynamic algorithms, written in our prototype implementation of CHR with justifications that is available online: maintaining the minimum of a changing set of numbers and shortest paths in a graph whose edges change.



We thank Daniel Gall for implementing the online transformation tool for CHR\(^{\mathcal J}\). We also thank the anonymous reviewers for their helpful suggestions on how to improve the paper.


  1. [Abd97]
    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). Scholar
  2. [AFM99]
    Abdennadher, S., Frühwirth, T., Meuss, H.: Confluence and semantics of constraint simplification rules. Constraints 4(2), 133–165 (1999)MathSciNetCrossRefGoogle Scholar
  3. [Bet14]
    Betz, H.: A Unified Analytical Foundation for Constraint Handling Rules. BoD, Norderstedt (2014)Google Scholar
  4. [BM06]
    Brown, K.N., Miguel, I.: Uncertainty and change. In: Rossi, F., Van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, Chap. 21, pp. 731–760. Elsevier, Amsterdam (2006)CrossRefGoogle Scholar
  5. [DKSD08]
    De Koninck, L., Schrijvers, T., Demoen, B.: A flexible search framework for CHR. In: Schrijvers, T., Frühwirth, T. (eds.) Constraint Handling Rules. LNCS (LNAI), vol. 5388, pp. 16–47. Springer, Heidelberg (2008). Scholar
  6. [Duc12]
    Duck, G.J.: SMCHR: Satisfiability modulo constraint handling rules. Theory Pract. Logic Programm. 12(4–5), 601–618 (2012)MathSciNetCrossRefGoogle Scholar
  7. [FR18]
    Frühwirth, T., Raiser, F. (eds.): Constraint Handling Rules - Compilation, Execution, and Analysis. BOD (2018). ISBN 9783746069050Google Scholar
  8. [Frü09]
    Frühwirth, T.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009)CrossRefGoogle Scholar
  9. [Frü15]
    Frühwirth, T.: Constraint handling rules - what else? In: Bassiliades, N., Gottlob, G., Sadri, F., Paschke, A., Roman, D. (eds.) RuleML 2015. LNCS, vol. 9202, pp. 13–34. Springer, Cham (2015). Scholar
  10. [Fru17]
    Fruehwirth, T.: Implementation of logical retraction in constraint handling rules with justifications. In: 21st International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2017), September 2017Google Scholar
  11. [McA90]
    McAllester, D.A.: Truth maintenance. In: AAAI, vol. 90, pp. 1109–1116 (1990)Google Scholar
  12. [RBF09]
    Raiser, F., Betz, H., Frühwirth, T.: Equivalence of CHR states revisited. In: Raiser, F., Sneyers, J. (eds.) CHR 2009, pp. 33–48. Technical report CW 555, Deparment of Computer Science, KU Leuven, July 2009Google Scholar
  13. [SSW03]
    Stuckey, P.J., Sulzmann, M., Wazny, J.: Interactive type debugging in Haskell. In: Proceedings of the 2003 ACM SIGPLAN workshop on Haskell, pp. 72–83. ACM (2003)Google Scholar
  14. [WGG00]
    Wolf, A., Gruenhagen, T., Geske, U.: On the incremental adaptation of CHR derivations. Appl. Artif. Intell. 14(4), 389–416 (2000)CrossRefGoogle Scholar
  15. [Wol01]
    Wolf, A.: Adaptive constraint handling with CHR in Java. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 256–270. Springer, Heidelberg (2001). Scholar
  16. [Wol05]
    Wolf, A.: Intelligent search strategies based on adaptive constraint handling rules. Theory Pract. Logic Program. 5(4–5), 567–594 (2005)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Ulm UniversityUlmGermany

Personalised recommendations