Abstract
In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening proof of the selection problem originally established by Carayol and Serre using collapsible pushdown automata. The main idea is to start from an infinitary and colored relational semantics of the \(\lambda \,Y\)-calculus formulated in a companion paper, and to replace it by a finitary counterpart based on finite prime-algebraic lattices. Given a higher-order recursion scheme \(\mathcal {G}\), the finiteness of its interpretation in the resulting model enables us to associate to any MSO formula \(\varphi \) a higher-order recursion scheme \(\mathcal {G}_{\varphi }\) resolving the selection problem.
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
References
Bloom, S.L., Ésik, Z.: Fixed-point operations on CCC’s. Part I. Theor. Comput. Sci. 155(1), 1–38 (1996)
Carayol, A., Serre, O.: Collapsible pushdown automata and labeled recursion schemes: equivalence, safety and effective selection. In: LICS 2012. pp. 165–174. IEEE Computer Society (2012)
Coppo, M., Dezani-Ciancaglini, M., Honsell, F., Longo, G.: Extended Type Structures and Filter Lambda Models. In: Lolli, G., Longo, G., Marcja, A. (eds.) Logic Colloquium 82, pp. 241–262. North-Holland, Amsterdam (1984)
Grellois, C., Melliès, P.-A.: An infinitary model of linear logic. In: Pitts, A. (ed.) FOSSACS 2015. LNCS, vol. 9034, pp. 41–55. Springer, Heidelberg (2015)
Grellois, C., Melliès, P.A.: Relational semantics of linear logic and higher-order model-checking. http://arxiv.org/abs/1501.04789. (accepted at CSL 2015)
Haddad, A.: Shape-preserving transformations of higher-order recursion schemes. Ph.D. thesis, Université Paris Diderot (2013)
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)
Melliès, P.A.: Categorical semantics of linear logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthses 27. pp. 1–196. Soci Mathmatique de France (2009)
Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90 (2006)
Salvati, S., Walukiewicz, I.: A model for behavioural properties of higher-order programs (2015). https://hal.archives-ouvertes.fr/hal-01145494
Terui, K.: Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In: Tiwari, A. (ed.) RTA 2012. LIPIcs, vol. 15, pp. 323–338. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Wadern (2012)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grellois, C., Melliès, PA. (2015). Finitary Semantics of Linear Logic and Higher-Order Model-Checking. In: Italiano, G., Pighizzini, G., Sannella, D. (eds) Mathematical Foundations of Computer Science 2015. MFCS 2015. Lecture Notes in Computer Science(), vol 9234. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48057-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-662-48057-1_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48056-4
Online ISBN: 978-3-662-48057-1
eBook Packages: Computer ScienceComputer Science (R0)