Abstract
We present effective criteria for first-order definability of regular tree languages. It is known that over words the absence of modulo counting (the “noncounting property”) characterizes the expressive power of first-order logic (McNaughton, Schützenberger), whereas non-counting regular tree languages exist which are not first-order definable. We present new conditions on regular tree languages (more precisely, on tree automata) which imply nondefinability in first-order logic. One method is based on tree homomorphisms which allow to deduce nondefinability of one tree language from nondefinability of another tree language. Additionly we introduce a structural property of tree automata (the socalled Λ-∨-patterns) which also causes tree languages to be undefinable in first-order logic. Finally, it is shown that this notion does not yet give a complete characterization of first-order logic over trees. The proofs rely on the method of Ehrenfeucht-Fraïssé games.
The present work was supported by EBRA Working Group 6317 “Algebraic and Syntactic Methods in Computer Science (ASMICS 2)” and by a fellowship of the EC program “Human, Capital and Mobility”.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J.R. Büchi, Finite automata, their algebras and grammars, D. Siefkes, ed. (Springer Verlag, New York, 1989).
J. Doner, Tree acceptors and some of their applications, Journal of Computer and System Sciences 4 (1970) 406–451.
H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic (Springer Verlag, New York, Berlin, Heidelberg, Tokyo, 1984).
A. Ehrenfeucht, An application of games to the completeness problem for formalized theories, Fundamenta Mathematicae 49 (1961) 129–141.
J. Engelfriet, Bottom-up and top-down tree transformations — a comparison, Mathematical Systems Theory 9 (1975) 198–231.
R. Fraiïssé, Sur quelques classifications des systèmes de relations, basés sur des isomorphismes restreints, Publications Scientifique de l'Université d'Alger, Série A 1 (1954) 35–182.
F.Gecség, M.Steinby, Tree Automata (Akadémiai Kiadó, Budapest, 1984).
U. Heuter, First-order properties of trees, star-free expressions and aperiodicity, RAIRO Theoretical Informatics and Applications 25 (1991) 125–145.
R. Ladner, Applications of model theoretic games to discrete linear orders and finite automata, Information and Control 33 (1977), 281–303.
R. McNaughton, S. Papert, Counter-free Automata (The M.I.T. Press, Cambridge, Massachusetts, 1971).
D. Perrin, Finite Automata, in: Handbook of Theoretical Computer Science, Vol. B, J.v. Leeuwen, ed. (Eisevier, Amsterdam, 1990) 3–57.
A. Potthoff, Modulo counting quantifiers over finite trees, TCS 126 (1994) 97–112.
A.Potthoff, Logische Klassifizierung regulärer Baumsprachen, (Dissertation, Kiel, 1994).
A.Potthoff, W.Thomas, Regular tree languages without unary symbols are starfree, in: 9th International Conference on Fundamentals of Computation Theory, Zoltán Ésik, ed., Lecture Notes in Computer Science 710 (1993) 396–405.
M.P. Schützenberger, On monoids having only trivial subgroups, Information and Control 8 (1965) 190–194.
M. Steinby, A theory of tree language varieties, in Tree automata and languages, M. Nivat, A. Podelski, eds., Studies in Computer Science and Artifical Intelligence Vol. 10 (Elsevier, Amsterdam, 1992) 57–81.
J.W. Thatcher, J.B. Wright, Generalized finite automata theory with an application to a decision problem of second-order logic, Mathematical Systems Theory 2 (1968) 57–81.
W. Thomas, Logical aspects in the study of tree languages, in: 9th Colloquium on Trees in Algebra and Programming, B. Courcelle, ed. (Cambridge University Press, Cambridge, 1984) 31–51.
W.Thomas, On the Ehrenfeucht-Fraïssé game in theoretical computer science, in: 18th Colloquium on Trees in Algebra and Programming, M.C.Gaudel, J.P.Jouannaud, eds., Lecture Notes in Computer Science 668 (1993) 559–568.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Potthoff, A. (1995). First-order logic on finite trees. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds) TAPSOFT '95: Theory and Practice of Software Development. CAAP 1995. Lecture Notes in Computer Science, vol 915. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59293-8_191
Download citation
DOI: https://doi.org/10.1007/3-540-59293-8_191
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59293-8
Online ISBN: 978-3-540-49233-7
eBook Packages: Springer Book Archive