[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #94

Originator: Gérard Huet [Hue76]
Date: 1979

Summary: Is higher-order matching decidable?

Higher-order matching is the following problem:

Given a set of equations si = ti between typed lambda-terms where the ti are ground, is there a substitution σ such that σ si = ti for all i. The order of the matching problem is the maximal height of function arrows in the types of the terms. Is higher-order matching decidable for arbitrary order? The problem has non-elementary complexity [Vor97].

The following results are known:

More on the complexity of higher-order matching can be found in [Wie99].

This problem is also listed as Problem #21 in the TLCA list of open problems.


It has recently been announced [Sti06] that the higher-order matching problem is decidable. However, the proof method only applies to the "classical" case of the problem, that is when all types are built from a single atom. Therefore, the problem remains open for the generalized case of types built from an arbitrary number of type variables.


Hubert Comon and Yan Jurski. Higher-order matching and tree automata. In M. Nielsen and Wolfgang Thomas, editors, Proceedings of the Conference on Computer Science Logic, volume 1414 of Lecture Notes in Computer Science, pages 157–176, Aarhus, Denmark, August 1997. Springer-Verlag.
Philippe de Groote. Linear higher-order matching is NP-complete. In Leo Bachmair, editor, Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 127–140, Norwich, UK, July 2000. Springer-Verlag.
Gilles Dowek. Third order matching is decidable. Annals of Pure and Applied Logic, 1993.
Gérard Huet. Résolution d’équations dans les langages d’ordre 1,2,…,ω. Thèse d’état, Université Paris 7, Paris, France, 1976.
Vincent Padovani. Filtrage d’ordre supérieure. Phd thesis, Université de Paris 7, Paris, France, 1996.
Aleksy Schubert. Linear interpolation for the higher-order matching problem. In Michel Bidoit and Max Dauchet, editors, Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 441–452, Lille, France, April 1997. Springer-Verlag.
Colin Stirling. A game-theoretic approach to deciding higher-order matching. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, ICALP (2), volume 4052 of Lecture Notes in Computer Science, pages 348–359, Venice, Italy, July 2006. Springer-Verlag.
Sergei Vorobyov. The "hardest" natural decidable theory. In Glynn Winskel, editor, Twelfth Symposium on Logic in Computer Science, pages 294–305, Warsaw, Poland, June 1997. IEEE.
Tomasz Wierzbicki. Complexity of the higher-order matching. In Harald Ganzinger, editor, 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 82–96, Trento, Italy, July 1999. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]