Abstract
We show that the monadic second-order theory of any infinite tree generated by a higher-order grammar of level 2 subject to a certain syntactic restriction is decidable. By this we extend the result of Courcelle [6] that the MSO theory of a tree generated by a grammar of level 1 (algebraic) is decidable. To this end, we develop a technique of representing infinite trees by infinite λ-terms, in such a way that the MSO theory of a tree can be interpreted in the MSO theory of a λ-term.
Partly supported by KBN Grant 8 T11C 027 16.
Partly supported by KBN Grant 8 T11C 035 14.
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.
References
A. Arnold and D. Niwiński. Rudiments of μ-calculus. Elsevier, 2001.
A. Asperti, V. Danos, C. Laneve, and L. Regnier. Paths in the lambda-calculus. In Proc. 9th IEEE Symp. on Logic in Comput. Sci., pages 426–436, 1994.
A. Asperti and S. Guerrini. The optimal implementation of functional programming languages. In Cambridge Tracts in Theoretical Computer Science, volume 45. Cambridge University Press, 1998.
A. Berarducci and M. Dezani-Ciancaglini. Infinite lambda-calculus and types. Theoret. Comput. Sci., 212:29–75, 1999.
D. Caucal. On infinite transition graphs having a decidable monadic second-order theory. In F. M. auf der Heide and B. Monien, editors, 23th International Colloquium on Automata Languages and Programming, LNCS 1099, pages 194–205, 1996. A long version will appear in TCS.
B. Courcelle. The monadic second-order theory of graphs IX: Machines and their behaviours. Theoretical Comput. Sci., 151:125–162, 1995.
W. Damm. The IO-and OI-hierarchies. Theoretical Comput. Sci., 20(2):95–208, 1982.
H. Hungar. Model checking and higher-order recursion. In L. P. M. Kuty lowski and T. Wierzbicki, editors, Mathematical Foundations of Computer Science 1999, LNCS 1672, pages 149–159, 1999.
J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinitary lambda calculus. Theoret. Comput. Sci., 175:93–125, 1997.
T. Knapik, D. Niwiński, and P. Urzyczyn. Deciding monadic theories of hyperal-gebraic trees, 2001. http://www.univ-reunion.fr/~knapik/publications/
O. Kupferman and M. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In Computer Aided Verification, Proc. 12th Int. Conference, Lecture Notes in Computer Science. Springer-Verlag, 2000.
D. Niwiński. Fixed points characterization of infinite behaviour of finite state systems. Theoretical Comput. Sci., 189:1–69, 1997.
M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Soc, 141:1–35, 1969.
Z. Splawski and P. Urzyczyn. Type fixpoints: iteration vs. recursion. In Proc. 4th ICPF, pages 102–113. ACM, 1999.
W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3, pages 389–455. Springer-Verlag, 1997.
I. Walukiewicz. Monadic second-order logic on tree-like structures. In C. Puech and R. Reischuk, editors, Proc. STACS’ 96, pages 401–414. Lect. Notes Comput. Sci. 1046, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Knapik, T., Niwiński, D., Urzyczyn, P. (2001). Deciding Monadic Theories of Hyperalgebraic Trees. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_21
Download citation
DOI: https://doi.org/10.1007/3-540-45413-6_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41960-0
Online ISBN: 978-3-540-45413-7
eBook Packages: Springer Book Archive