Problem #94
Originator: Gérard Huet [Hue76]
Date: 1979
Summary:
Is higherorder matching decidable?
Higherorder matching is the following problem:
Given a set of equations s_{i} = t_{i} between typed lambdaterms where
the t_{i} are ground, is there a substitution σ such that
σ s_{i} = t_{i} for all i. The order of the matching problem is
the maximal height of function arrows in the types of the terms. Is
higherorder matching decidable for arbitrary order? The problem has
nonelementary complexity [Vor97].
The following results are known:

Firstorder matching is, of course, decidable.
 Secondorder matching is decidable [Hue76].
 Thirdorder matching is decidable [Dow93].
 Fourthorder matching is decidable [Pad96] and
NEXPTIMEhard [Wie99].
The solutions can be described by a tree automaton [CJ97],
which gives an 2NEXPTIME upper bound.
 A restricted case of fifthorder matching has been shown decidable in
[Sch97].
 Linear higherorder matching is decidable and NPcomplete
[dG00].
More on the complexity of higherorder matching can be found in
[Wie99].
This problem is also listed as Problem #21 in the
TLCA list of open problems.
Remark
It has recently been announced [Sti06] that the
higherorder 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.
References

[CJ97]

Hubert Comon and Yan Jurski.
Higherorder 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.
SpringerVerlag.
 [dG00]

Philippe de Groote.
Linear higherorder matching is NPcomplete.
In Leo Bachmair, editor, Rewriting Techniques and
Applications, volume 1833 of Lecture Notes in Computer
Science, pages 127–140, Norwich, UK, July 2000.
SpringerVerlag.
 [Dow93]

Gilles Dowek.
Third order matching is decidable.
Annals of Pure and Applied Logic, 1993.
 [Hue76]

Gérard Huet.
Résolution d’équations dans les langages d’ordre
1,2,…,ω.
Thèse d’état, Université Paris 7, Paris, France, 1976.
 [Pad96]

Vincent Padovani.
Filtrage d’ordre supérieure.
Phd thesis, Université de Paris 7, Paris, France, 1996.
 [Sch97]

Aleksy Schubert.
Linear interpolation for the higherorder 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.
SpringerVerlag.
 [Sti06]

Colin Stirling.
A gametheoretic approach to deciding higherorder 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.
SpringerVerlag.
 [Vor97]

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.
 [Wie99]

Tomasz Wierzbicki.
Complexity of the higherorder 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.
SpringerVerlag.