Higher-Order Matching and Games

  • Colin Stirling
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


We provide a game-theoretic characterisation of higher-order matching. The idea is suggested by model checking games. We then show that some known decidable instances of matching can be uniformly proved decidable via the game-theoretic characterisation.


games higher-order matching typed lambda calculus 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1009–1062. North-Holland, Amsterdam (2001)CrossRefGoogle Scholar
  3. 3.
    Huet, G.: Rèsolution d’èquations dans les langages d’ordre 1, 2, . . . ω. Thèse de doctorat d’ètat, Universitè Paris VII (1976) Google Scholar
  4. 4.
    Loader, R.: Higher-order β-matching is undecidable. Logic Journal of the IGPL 11(1), 51–68 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Padovani, V.: Decidability of all minimal models. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 201–215. Springer, Heidelberg (1996)Google Scholar
  6. 6.
    Padovani, V.: Decidability of fourth-order matching. Mathematical Structures in Computer Science 10(3), 361–372 (2001)CrossRefMathSciNetGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Schmidt-Schauβ, M.: Decidability of arity-bounded higher-order matching. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 488–502. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Statman, R.: The typed λ-calculus is not elementary recursive. Theoretical Computer Science 9, 73–81 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, Heidelberg (2001)Google Scholar
  11. 11.
    Wierzbicki, T.: Complexity of higher-order matching. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 82–96. Springer, Heidelberg (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Colin Stirling
    • 1
  1. 1.School of InformaticsUniversity of Edinburgh 

Personalised recommendations