Abstract
Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type hierarchy upon this interpretation of the base type gives a finite semantics for simply-typed lambda-trees.
A calculus based on this semantics is proven sound and complete. In particular, for regular infinite lambda-trees it is decidable whether a given automaton has a run or not. As regular lambda-trees are precisely recursion schemes, this decidability result holds for arbitrary recursion schemes of arbitrary level, without any syntactical restriction. This partially solves an open problem of Knapik, Niwinski and Urzyczyn.
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
Aehlig, K., Joachimski, F.: On continuous normalization. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 59–73. Springer, Heidelberg (2002)
Aehlig, K., Miranda, J.G.d., Ong, C.H.L.: The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 39–54. Springer, Heidelberg (2005)
Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF. Information and Computation 163(2), 285–408 (2000)
Knapik, T., Niwiński, D., Urzyczyn, P.: Deciding monadic theories of hyperalgebraic trees. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 253–267. Springer, Heidelberg (2001)
Knapik, T., Niwiński, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)
Knapik, T., Niwiński, D., Urzyczyn, P., Walukiewicz, I.: Unsafe grammars, panic automata, and decidability. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1450–1461. Springer, Heidelberg (2005)
Kreisel, G., Mints, G.E., Simpson, S.G.: The use of abstract language in elementary metamathematics: Some pedagogic examples. In: Parikh, R. (ed.)Logic Colloquium. Lecture Notes in Mathematics, vol. 453, pp. 38–131. Springer, Heidelberg (1975)
Mints, G.E.: Finite investigations of transfinite derivations. Journal of Soviet Mathematics, 10, 548–596 (1978); Translated from: Zap. Nauchn. Semin. LOMI 49 (1975); Cited after Grigori Mints. Selected papers in Proof Theory. Studies in Proof Theory. Bibliopolis (1992)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of the Twenty First Annual IEEE Symposium on Logic in Computer Science (LICS 2006) (to appear, 2006)
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141, 1–35 (1969)
Tait, W.W.: Intensional interpretations of functionals of finite type. The Journal of Symbolic Logic 32(2), 198–212 (1967)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aehlig, K. (2006). A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata. In: Ésik, Z. (eds) Computer Science Logic. CSL 2006. Lecture Notes in Computer Science, vol 4207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11874683_7
Download citation
DOI: https://doi.org/10.1007/11874683_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45458-8
Online ISBN: 978-3-540-45459-5
eBook Packages: Computer ScienceComputer Science (R0)