Abstract
We are interested in the expressiveness of constraints represented by general first order formulae, with equality as unique relational symbol and functional symbols taken from an infinite set F. The chosen domain is the set of trees whose nodes, in possibly infinite number, are labeled by elements of F. The operation linked to each element f of F is the mapping (a 1 ,...,a n ) → b, where b is the tree whose initial node is labeled f and whose sequence of daughters is a 1 ,...,a n .
We first consider constraints involving long alternated sequences of quantifiers ∃∀∃∀.... We show how to express winning positions of two-person games with such constraints and apply our results to two examples.
We then construct a family of strongly expressive constraints, inspired by a constructive proof of a complexity result by Pawel Mielniczuk. This family involves the huge number α(k), obtained by evaluating top down a power tower of 2’s, of height k. With elements of this family, of sizes at most proportional to k, we define a finite tree having α(k) nodes, and we express the result of a Prolog machine executing at most α(k) instructions.
By replacing the Prolog machine by a Turing machine we rediscover the following result of Sergei Vorobyov: the complexity of an algorithm, deciding whether a constraint without free variables is true, cannot be bounded above by a function obtained by finite composition of elementary functions including exponentiation.
Finally, taking advantage of the fact that we have at our disposal an algorithm for solving such constraints in all their generality, we produce a set of benchmarks for separating feasible examples from purely speculative ones. Among others we solve constraints involving alternated sequences of more than 160 quantifiers.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Benhamou F., P. Bouvier, A. Colmerauer, H. Garetta, B. Giletta, J. L. Massat, G. A. Narboni, S. N’Dong, R. Pasero, J. F. Pique, Touraïvane, M. Van Caneghem and E. Vétillard, Le manuel de Prolog IV. PrologIA, Marseille, June 1996.
Clark K.L., Negation as failure, in Logic and Databases, edited by H. Gallaire and J. Minker, Plenum Press, New York, pp. 293–322, 1978.
Colmerauer A., Prolog and Infinite Trees, in Logic Programming, K. L. Clark and S. A.. Tarnlund editors, Academic Press, New York, pp. 231–251, 1982.
Colmerauer A., Henry Kanoui and Michel Van Caneghem, Prolog, theoretical principles and current trends, in Technology and Science of Informatics, North Oxford Academic, vol. 2, no 4, August 1983. English version of the journal TSI, AFCET-Bordas, where the paper appears under the title: Prolog, bases théoriques et développements actuels.
Colmerauer A., Equations and Inequations on Finite and Infinite Trees, in Proceeding of the International Conference on Fifth Generation Computer Systems (FCGS-84), ICOT, Tokyo, pp. 85–99, 1984.
Colmerauer A., An Introduction to Prolog III, Communications of the ACM, 33(7): 68–90, 1990.
Coupet-Grimal S. and O. Ridoux, On the use of advanced logic programming features in computational linguistics. The Journal of Logic Programming, 24(1–2), pages 121–159.
Courcelle B., Fundamental Properties of Infinite Trees, Theoretical Computer Science, 25(2), pp. 95–169, March 1983.
Courcelle B., Equivalences and Transformations of Regular Systems-Applications to Program Schemes and Grammars, Theoretical Computer Science, 42, pp. 1–122, 1986.
Dao T. B. H., Résolution de contraintes du premier ordre dans la théorie des arbres fini ou infinis, Neuvièmes Journées Francophones de Programmation Logique et Programmation par Contraintes (JFPLC’2000), Marseille, June 2000, proceedings to be published by Hermes Science Publications.
Huet G., Résolution d’équations dans les langages d’ordre 1,2,...,ω., Thèse d’Etat, Université Paris 7, 1976.
Maher M. J., Complete Axiomatization of the Algebra of Finite, Rational and Infinite Trees, Technical report, IBM-T. J.Watson Research Center, 1988.
Mielniczuk P., Basic Theory of Feature Trees, submitted to Journal of Symbolic Computation, also available at http://www.tcs.uni.wroc.pl/~mielni.
Vorobyov S., An Improved Lower Bound for the Elementary Theories of Trees, Proceeding of the 13th International Conference on Automated Deduction (CADE’96). Springer Lecture Notes in Artificial Intelligence, vol 1104, pp. 275–287, New Brunswick, NJ, July/August, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Colmerauer, A., Dao, TBH. (2000). Expressiveness of Full First Order Constraints in the Algebra of Finite or Infinite Trees. In: Dechter, R. (eds) Principles and Practice of Constraint Programming – CP 2000. CP 2000. Lecture Notes in Computer Science, vol 1894. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45349-0_14
Download citation
DOI: https://doi.org/10.1007/3-540-45349-0_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41053-9
Online ISBN: 978-3-540-45349-9
eBook Packages: Springer Book Archive