\documentclass{rtaloop}
\rtalabel{Miller}


\begin{document}
\begin{problem}{Jean-Pierre Jouannaud}{}{April 1995}

\begin{abstract}
Is unification of patterns modulo any set of variable-preserving equations
decidable? 
\end{abstract}

Unification of patterns (\`{a} la \cite{miller91}) modulo associativity and
commutativity has been shown decidable \cite{boudet97cp}, repairing the
incomplete solution in \cite{QuianWangLNCS845}. Does it extend to equational
theories whose axioms have the same set of variables on left and right hand
side?

\begin{submitted}{Evelyne Contejean}{Mon Jan 12 15:20:45 MET 1998}

In his conference paper, Qian claimed that he has solved the problem of
unifying patterns a la Miller modulo AC, but in fact he never succeeded to
prove the completeness of his algorithm. Actually his algorithm is not
complete, since he uses a first-order unification algorithm for pure
AC-patterns as a black box. The problem was solved last year by Boudet and
Contejean \cite{boudet97cp}: the case of pure AC-patterns requieres is handled
in the same spirit as the first order case, by counting things, but
technically this is not exactly identical. In \cite{boudet97cp}, the proof of
completeness of the algorithm is given. I must admit that \cite{boudet97cp}
takes advantage of the paper of Qian, in particular, the remark that the
equations of the form
\[
\lambda x_1 ... x_n F(x_1,...,x_n) = 
\lambda x_1 ... x_n F(x_{\pi(1)},...,x_{\pi(n)})
\]
have an infinite set of solutions $\{\sigma_1,\sigma_2,...\}$ such that
$\sigma_{i+1}$ is strictly more general than $\sigma_i$. This leads to the
notion of constrained solution of a unification problem, and every unification
problem of patterns with AC symbols admits a finite complete set of
constrained unifiers, and the algorithm proposed in \cite{boudet97cp} computes
such a set.

\end{submitted}

\end{problem}
\end{document}