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:
-
First-order matching is, of course, decidable.
- Second-order matching is decidable [Hue76].
- Third-order matching is decidable [Dow93].
- Fourth-order matching is decidable [Pad96] and
NEXPTIME-hard [Wie99].
The solutions can be described by a tree automaton [CJ97],
which gives an 2-NEXPTIME upper bound.
- A restricted case of fifth-order matching has been shown decidable in
[Sch97].
- Linear higher-order matching is decidable and NP-complete
[dG00].
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.
Remark
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.
References
-
[CJ97]
-
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.
- [dG00]
-
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.
- [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 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.
- [Sti06]
-
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.
- [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 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.