\documentclass[11pt]{article}
\usepackage{a4}
\usepackage{hevea}
\begin{document}
\setlength{\parskip}{6pt}
\setlength{\parindent}{0pt}

\section*{Context Unification}

\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{Comon:rr699}, \cite{Comon:icalp92})
\item solving constraints occurring in Distributive Unification
        (\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{Comon:rr699} 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.
\nocite{Schauss:cisrep99}

\bibliographystyle{alpha}
\bibliography{rewriting}

\end{document}
