\documentclass{rtaloop}
\rtalabel{ho-matching}


\begin{document}
\begin{problem}{G\'erard Huet}{\cite{Huet:these}}{1979}

\begin{abstract}
Is {\em higher-order matching} decidable?
\end{abstract}

Higher-order matching is the following problem:

Given a set of equations $s_i = t_i$ between typed lambda-terms where
the $t_i$ are ground, is there a substitution $\sigma$ such that
$\sigma 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
higher-order matching decidable for arbitrary order? The problem has
non-elementary complexity \cite{Vorobyov:lics97}.

The following results are known:
\begin{itemize}
\item
First-order matching is, of course, decidable.
\item
Second-order matching is decidable \cite{Huet:these}.
\item
Third-order matching is decidable \cite{Dowek:apal93}.
\item
Fourth-order matching is decidable \cite{Padovani:these} and
NEXPTIME-hard \cite{Wierzbicki:cade99}.
The solutions can be described by a tree automaton \cite{comon:csl97},
which gives an 2-NEXPTIME upper bound.
\item
A restricted case of fifth-order matching has been shown decidable in
\cite{Schubert:tapsoft97}. 
\item
Linear higher-order matching is decidable and NP-complete
\cite{deGroote:rta00}. 
\end{itemize}

More on the complexity of higher-order matching can be found in
\cite{Wierzbicki:cade99}. 

This problem is also listed as \emph{Problem \#21} in the
\ahref{http://tlca.di.unito.it/opltlca/}{TLCA list of open problems}.

\begin{remark}
  It has recently been announced \cite{stirling06icalp} 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.
\end{remark}

\end{problem}
\end{document}