Abstract
Constraint Handling Rules (CHR) is a concurrent, committed-choice, rule-based language. One of the first CHR programs is the classic constraint solver for syntactic equality of rational trees that performs unification. We first prove its exponential complexity in time and space for non-flat equations and deduce from this proof a quadratic complexity for flat equations. We then present an extended CHR solver for solving existentially quantified conjunctions of non-flat equations in the theory of finite or infinite trees. We reach a quadratic complexity by first flattening the equations and introducing new existentially quantified variables, then using the classic solver, and finally eliminating particular equations and quantified variables.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Colmerauer, A.: Prolog and infinite trees. In: Clark, K.L., Tärnlund, S.-A. (eds.) Logic Programming, pp. 231–251. Academic Press, London (1982)
Djelloul, K.: Decomposable theories. J. Theory and Practice of Logic Programming (to appear)
Frühwirth, T.: Theory and Practice of Constraint Handling Rules. J. Logic Programming 37(1-3), 95–138 (1998)
Frühwirth, T.: Parallelizing union-find in Constraint Handling Rules using confluence. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 113–127. Springer, Heidelberg (2005)
Frühwirth, T., Abdennadher, S.: Essentials of Constraint Programming. Springer, Heidelberg (2003)
Herbrand, J.: Recherches sur la théorie de la demonstration. PhD thesis, Université de Paris, France (1930)
Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)
Maher, M.J.: Complete axiomatizations of the algebras of finite, rational, and infinite trees. In: LICS 1988, pp. 348–357, Los Alamitos (CA), USA (1988)
Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)
Meister, M., Frühwirth, T.: Complexity of the CHR rational tree equation solver. In: CHR 2006, Report CW, vol. 452, pp. 77–92. K.U. Leuven, Belgium (2006)
Paterson, M.S., Wegman, M.N.: Linear unification. J. Computer and System Sciences 16(2), 158–167 (1978)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Schrijvers, T., Frühwirth, T.: Optimal union-find in Constraint Handling Rules. J. Theory and Practice of Logic Programming 6(1&2), 213–224 (2006)
Schrijvers, T., et al.: Constraint Handling Rules (CHR) web page (2007), http://www.cs.kuleuven.ac.be/~dtai/projects/CHR/
Tarjan, R.E., Van Leeuwen, J.: Worst-case analysis of set union algorithms. J. ACM 31(2), 245–281 (1984)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meister, M., Djelloul, K., Frühwirth, T. (2007). Complexity of a CHR Solver for Existentially Quantified Conjunctions of Equations over Trees. In: Azevedo, F., Barahona, P., Fages, F., Rossi, F. (eds) Recent Advances in Constraints. CSCLP 2006. Lecture Notes in Computer Science(), vol 4651. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73817-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-73817-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73816-9
Online ISBN: 978-3-540-73817-6
eBook Packages: Computer ScienceComputer Science (R0)