\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}