Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms : Theory, Implementations, and Complexity

• Autorzy: Frühwirth Thom

Identyfikatory

DOI

10.3233/FI-2020-1924

• Języki publikacji: EN

Abstrakty

EN

We present a concise source-to-source transformation that introduces justifications for user-defined constraints into the rule-based Constraint Handling Rules (CHR) programming language. There is no need to introduce a new semantics for justifications. This leads to a conservative extension of the language, as we can show the equivalence of rule applications. A scheme of two rules suffices to allow for logical retraction (deletion, removal) of CHR constraints during computation. Without the need to recompute from scratch, these rules remove the constraint and also undo all its consequences. We prove a confluence result concerning the rule scheme. We prove its correctness in general and tighten the results for confluent programs. We give an implementation, show its correctness, present two classical examples of dynamic algorithms, and improve the implementation. The computational overhead of introducing justifications and of performing logical retraction, i.e. the additional time and space needed, is proportional to the derivation length in the original program. This overhead may increase space complexity, but does not change the worst-case time complexity.

Słowa kluczowe

EN

computational logic; confluence; constraint deletion; logic programming; rule-based programming; source-to-source program transformation; truth maintenance

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 173, nr 4
• Strony: 253--283
• Opis fizyczny: Bibliogr 23 poz.

Twórcy

autor

Frühwirth Thom

• Ulm University, Germany

Bibliografia

• [1] McAllester DA. Truth Maintenance. In: AAAI, volume 90. 1990 pp. 1109-1116.
• [2] Brown KN, Miguel I. Uncertainty and Change, Chapter 21. Handbook of Constraint Programming, 2006. pp. 731-760. doi:10.1016/S1574-6526(06)80025-8.
• [3] Frühwirth T. Constraint Handling Rules. Cambridge University Press, 2009. ISBN 9780521877763. URL http://www.constraint-handling-rules.org.
• [4] Frühwirth T. Constraint Handling Rules - What Else? In: Rule Technologies: Foundations, Tools, and Applications, pp. 13-34. Springer International Publishing, 2015. doi:10.1007/978-3-319-21542-6_2.
• [5] Frühwirth T, Raiser F (eds.). Constraint Handling Rules - Compilation, Execution, and Analysis. BOD, ISBN 9783746069050, 2018. ISBN 9783746069050.
• [6] Fruehwirth T. Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms. 27th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR 2017, 2017. 1706.07946.
• [7] 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). 2017 pp. 37-5. doi:10.1007/978-3-030-00801-7_3.
• [8] Fruehwirth T. Parallelism, concurrency and distribution in constraint handling rules: A survey. Theory and Practice of Logic Programming, 2018. 18(5-6):759-805. URL https://doi.org/10.1017/S1471068418000078.
• [9] Raiser F, Betz H, Frühwirth T. Equivalence of CHR States Revisited. In: Raiser F, Sneyers J (eds.), CHR’09. K.U.Leuven, Dept. Comp. Sc., Technical report CW 555, 2009 pp. 33-48.
• [10] Betz H. A unified analytical foundation for constraint handling rules. BoD, 2014. URL https://oparu.uni-ulm.de/xmlui/license_v3.
• [11] Schrijvers T, Frühwirth T. Optimal Union-Find in Constraint Handling Rules, Programming Pearl. Theory and Practice of Logic Programming (TPLP), 2006. 6(1). URL http://arxiv.org/abs/cs.PL/0501073.
• [12] Duck GJ, Stuckey PJ, García de la Banda M, Holzbaur C. The Refined Operational Semantics of Constraint Handling Rules. In: Demoen B, Lifschitz V (eds.), ICLP ’04, volume 3132 of LNCS. Springer. ISBN 978-3-540-22671-0, 2004 pp. 90-104. doi:10.1007/b99475.
• [13] Schrijvers T, Demoen B. The K.U.Leuven CHR system: Implementation and application. In: Frühwirth T, Meister M (eds.), CHR ’04, Selected Contributions. 2004 pp. 8-12. URL http://people.cs.kuleuven.be/~tom.schrijvers/CHR/.
• [14] Van Weert P. Efficient Lazy Evaluation of Rule-Based Programs. IEEE Transactions on Knowledge and Data Engineering, 2010. 22(11):1521-1534. doi:10.1109/TKDE.2009.208.
• [15] Abdennadher S. Operational Semantics and Confluence of Constraint Propagation Rules. In: Smolka G (ed.), CP ’97: Proc. Third Intl. Conf. Principles and Practice of Constraint Programming, volume 1330 of LNCS. Springer, 1997 pp. 252-266. doi:10.1007/BFb0017444.
• [16] Abdennadher S, Frühwirth T, Meuss H. Confluence and Semantics of Constraint Simplification Rules. Constraints, 1999. 4(2):133-165. doi:10.1023/A:1009842826135.
• [17] Wolf A, Gruenhagen T, Geske U. On the incremental adaptation of CHR derivations. Applied Artificial Intelligence, 2000. 14(4):389-416. URL https://doi.org/10.1080/088395100117052.
• [18] Wolf A. Adaptive constraint handling with CHR in Java. In: International Conference on Principles and Practice of Constraint Programming. Springer, 2001 pp. 256-270. doi:10.1007/3-540-45578-7_18.
• [19] Wolf A. Intelligent search strategies based on adaptive Constraint Handling Rules. Theory and Practice of Logic Programming, 2005. 5(4-5):567-594. URL https://doi.org/10.1017/S1471068405002383.
• [20] Wolf A. Adaptive Solving of Equations over Rational Trees. In: Principles and Practice of Constraint Programming. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-49481-2, 1998 pp. 475-475. doi:10.1007/3-540-49481-2_46. URL http://dx.doi.org/10.1007/3-540-49481-2_46.
• [21] De Koninck L, Schrijvers T, Demoen B. A flexible search framework for CHR. In: Constraint Handling Rules — Current Research Topics, volume LNAI 5388, pp. 16-47. Springer, 2008. doi:10.1007/978-3-540-92243-8_2.
• [22] Stuckey PJ, Sulzmann M, Wazny J. Interactive type debugging in Haskell. In: Proceedings of the 2003 ACM SIGPLAN workshop on Haskell. ACM, 2003 pp. 72-83. doi:10.1145/871895.871903.
• [23] Duck GJ. SMCHR: Satisfiability modulo constraint handling rules. Theory and Practice of Logic Programming, 2012. 12(4-5):601-618. URL https://doi.org/10.1017/S1471068412000208.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).