\documentclass{rtaloop}
\rtalabel{contex-unification}
\begin{document}
\begin{problem}%
{Hubert Comon, Manfred Schmidt-Schau\ss, Jordi Levy}
{\cite{Comon:rr699}, \cite{Schauss:rr94-12}, \cite{Levy:rta96}}%
{September 1991, 1994, July 1996}
\begin{abstract}
Are {\em context unification} and
{\em linear second order unification} decidable?
\end{abstract}
{\em Context unification} and {\em linear second order unification}
are closely related, they both generalize string unification
(which is known to be decidable, \cite{Makanin:77})
and are special cases of second order unification
(which is know to be undecidable, \cite{Goldfarb:tcs81}).
Context unification (\cite{Comon:rr699}, \cite{Schauss:rr94-12}) is
unification of first-order terms with context variables that range
over terms with one hole.
Linear Second Order Unification is second-order unification where
the domain of functions is restricted to $\lambda$-terms with exactly
one occurrence of any bound variable (there can be several bound variables
in contrast to context unification allowing for just one hole)
Applications are
\begin{itemize}
\item solving membership constraints in completion of contraint rewriting
(\cite{Comon98ajsc})
\item solving constraints occurring in Distributive Unification
(\rtaref{distributivity}, \cite{schmidt-schauss:jsc97})
\item Extended Critical Pairs in Bi-Rewriting Systems
(\cite{LevyAgust:jsc96})
\item Semantics of ellipses in natural language
(\cite{Niehren:cade97})
\item One-Step Rewriting constraints
(\cite{Niehren:cade97})
\end{itemize}
Some special cases have been solved:
\begin{itemize}
\item Hubert Comon \cite{Comon98bjsc} solved a special case where
any occurrence of the same context variable is always applied
to the same term,
\item Manfred Schmidt-Schau{\ss} \cite{Schauss:rr94-12} (see also
\cite{schmidt-schauss:jsc97}) solved the case of so-called
{\em stratified} context unification, where for any occurrence
of the same second-order variable the string of
second-order variables from this occurrence to the root of the
containing term is the same,
\item Jordi Levy \cite{Levy:rta96} (see also \cite{Niehren:cade97})
showed that linear-second order
unification is decidable when any variable has at most two
occurrences.
\item Manfred Schmidt-Schau{\ss} and Klaus Schulz \cite{Schauss:cade99}
showed that solvability is decidable for systems of
context equations containing only two context variables (having
an arbitrary number of occurrences in the system) and an
arbitray number of first-order variables.
\end{itemize}
Progress towards a decidability proof along the lines of Makanin's proof for
string-unification has been reported in~\cite{schmidt-schauss:rta98}. Levy and
Villaret \cite{Levy:rta00} show how to reduce linear second-order unification
to context unification plus membership predicates in regular tree languages,
and discuss a possible way of showing decidability of the latter.
\cite{levy02rta} shows that it is sufficient, both for linear 2nd-order and
for context unification, to consider signatures consisting of an arbitrary
number of constants and one binary function symbol. \nocite{Schauss:cisrep99}
\end{problem}
\end{document}