Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Dynamic algorithms for dynamic problems should not be confused with dynamic programming.
- 2.
A variant (renaming) of an expression is obtained by uniformly replacing its variables by fresh variables.
- 3.
For a related strip function, see the proof of Theorem 3.
- 4.
More precisely, a simplification rule is generated if there are no kept constraints and a propagation rule is generated if there are no removed constraints.
References
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). https://doi.org/10.1007/BFb0017444
Abdennadher, S., Frühwirth, T., Meuss, H.: Confluence and semantics of constraint simplification rules. Constraints 4(2), 133–165 (1999)
Betz, H.: A Unified Analytical Foundation for Constraint Handling Rules. BoD, Norderstedt (2014)
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)
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). https://doi.org/10.1007/978-3-540-92243-8_2
Duck, G.J.: SMCHR: Satisfiability modulo constraint handling rules. Theory Pract. Logic Programm. 12(4–5), 601–618 (2012)
Frühwirth, T., Raiser, F. (eds.): Constraint Handling Rules - Compilation, Execution, and Analysis. BOD (2018). ISBN 9783746069050
Frühwirth, T.: Constraint Handling Rules. Cambridge University Press, Cambridge (2009)
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). https://doi.org/10.1007/978-3-319-21542-6_2
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 2017
McAllester, D.A.: Truth maintenance. In: AAAI, vol. 90, pp. 1109–1116 (1990)
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 2009
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)
Wolf, A., Gruenhagen, T., Geske, U.: On the incremental adaptation of CHR derivations. Appl. Artif. Intell. 14(4), 389–416 (2000)
Wolf, A.: Adaptive constraint handling with CHR in Java. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 256–270. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45578-7_18
Wolf, A.: Intelligent search strategies based on adaptive constraint handling rules. Theory Pract. Logic Program. 5(4–5), 567–594 (2005)
Acknowledgements
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Frühwirth, T. (2018). Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms. In: Fioravanti, F., Gallagher, J. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2017. Lecture Notes in Computer Science(), vol 10855. Springer, Cham. https://doi.org/10.1007/978-3-319-94460-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-94460-9_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94459-3
Online ISBN: 978-3-319-94460-9
eBook Packages: Computer ScienceComputer Science (R0)