Abstract
Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that t θ and u have the same normal form with respect to βη-equality: can t be pattern matched to u? The problem was conjectured to be decidable by Huet [4]. Loader showed that it is undecidable when β-equality is the same normal form by encoding λ-definability as matching [6].
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 subscriptionsReferences
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications. Draft Book (2002), http://l3ux02.univ-lille3.fr/tata/
Comon, H., Jurski, Y.: Higher-order matching and tree automata. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 157–176. Springer, Heidelberg (1998)
Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (ed.) Handbook of Automated Reasoning, vol. 2, pp. 1009–1062, North-Holland (2001)
Huet, G.: Rèsolution d’èquations dans les langages d’ordre 1, 2, ... ω. Thèse de doctorat d’ètat, Universitè Paris VII (1976)
Jung, A., Tiuryn, J.: A new characterisation of lambda definability. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 245–257. Springer, Heidelberg (1993)
Loader, R.: Higher-order β-matching is undecidable. Logic Journal of the IGPL 11(1), 51–68 (2003)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Procs LICS, pp. 81–90 (Longer version available from Ong’s web page) (2006)
Padovani, V.: Decidability of fourth-order matching. Mathematical Structures in Computer Science 10(3), 361–372 (2001)
Schubert, A.: Linear interpolation for the higher-order matching problem. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 441–452. Springer, Heidelberg (1997)
Stirling, C.: Modal and Temporal Properties of Processes. In: Texts in Computer Science, Springer, Heidelberg (2001)
Stirling, C.: Higher-order matching and games. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 119–134. Springer, Heidelberg (2005)
Stirling, C.: A game-theoretic approach to deciding higher-order matching. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 348–359. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stirling, C. (2007). Games, Automata and Matching. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-73595-3_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73594-6
Online ISBN: 978-3-540-73595-3
eBook Packages: Computer ScienceComputer Science (R0)