\section{Complement Problems 
%and Elimination of Negation in Term Algebrae
}
\label{el-rel}  

Complement problems and elimination of negation are not restricted to 
\lp, but have some other relevant application in theoretic computer 
science.  Let me refer to \cite{Las91} and \cite{Com91} for issues 
impossible to detail here and for references, keeping in mind that 
this is just a scratch on the surface of the applications of 
disunification.
\smallskip
In fact, complement problems and variants of the prototypical {\em 
uncover} algorithm. proposed in \cite{Las87} as a first attempt to 
solve the former, have been studied and tentatively applied in several 
ways:
\begin{itemize}
\item
In a functional programming framework, to determine, modulo pattern 
matching, whether the program clauses describing a function are 
exhaustive and disjunct, even further to produce a non-ambiguous set 
of patterns.  Moreover it is possible to take advantage of the given 
sequential application of the rules to provide an improved compiled 
code.  Indeed, if, say, the second rule applies, it means the first 
one does not: hence the terms reducible by the second rule are in the 
complement of the LHS of the first.
\item
The connection of complementation to the notion of {\em ground 
reducibility} in term rewriting systems makes it a candidate as a 
checker for {\em sufficiently completeness} \cite{GH78} of an 
algebraic (equational) specification.  If the latter fails to be 
complete, the transformation rules my lead to recover the missing 
cases---hence the motto in \cite{Thi84}:
\begin{quote}
``Stop losing sleep over incomplete specifications''
\end{quote}
  Here we are looking for counter-examples: if a function is not 
sufficiently complete, there is a term, built from the constructors 
in the signature, which is different from any LHS, thus irreducible 
(see Example~\ref{ex:mod2}).
\item
In term rewriting systems describing infinite transition systems,
the complement of a LHS returns the states from which no transition 
is achievable, providing thusly a tool for the temporal analysis of 
communicating processes.
\item
In machine learning, a concept can be captured by a term with some 
(finite) exceptions: the computation of this structure, which is a 
relative complement, coincides with the search for an explicit 
representation of the cited concept.
\item
Finally, applications to inductive theorem proving under the slogan 
{\em inductionless induction} or \emph{proof by consistency} 
\cite{Com91b} are under scrutiny.  This is connected to the idea of 
the so-called \emph{inductive reducibility} property.  Roughly, given 
a rewrite system, a term $t$ is inductively irreducible, \ie its set 
of irreducible instances is obtained by computing the complement of 
the latter into the LHS of the system.
 \end {itemize}

\section{Term Complement as Disunification}

We address in this section the issue of how to express the (relative) 
complement problem on terms as an equational problem \cite{Las87} 
\cite{Com91}.  This is the basis to solve complement problems with 
disunification, as we will see in \ref{dis}.  An open term $t$ can be 
seen as the intensional representation of its ground instances, say 
$\| t \|$.  According to this set-theoretic interpretation, the {\em 
complement} of $t$ is the set of ground terms which are not instances 
of $t$, \ie are not in $\| t \|$.  It is natural to generalize this to 
the notion of {\em relative} complement; this corresponds to compute a 
suitable representation of all the ground instances of a given 
(finite) set of terms which are not instances of another given one, in 
symbols: \[ \| t_1 \mdots t_n \| - \| u_1 \mdots u_m \| \] where dots 
represent (set theoretic) union\footnote{Another equivalent notation 
found in the literature is $ t_1 \Or \cdots \Or t_n \setminus u_1 \Or 
\cdots \Or u_m$ \cite{Las87}, or a mixture of the two.}.  More 
properly \[ \| t_1 \mdots t_n \| =_{Def} \bigcup^{n}_{i=1} \|t_i\| \] 
% We will assume that any sequence $\| t_1 \mdots t_n \| $ is without 
% repetition modulo subsumption, \ie every element is incomparable with 
% everyone else under the subsumption ordering.  
Let $FV(t_1 \mdots t_n) 
= \vx$ disjoint from $FV(u_1 \mdots u_m) = \vy$.  Then the relative 
complement problem can be expressed by the following restricted format 
of equational problem, where the $z_i$'s are free.  \[ \exists \vx 
\forall \vy : \BAnd^{n}_{i=1} z_i = t_i \And \bigwedge^{m}_{i=1} z_i 
\nq u_{i} \] With no loss of generality we will take $n=1$: indeed: \[ 
\| t_1 \mdots t_n \| - \| u_1 \mdots u_m \| = \bigcup^{n}_{i=1}(\|t_i 
\| - \| u_1 \mdots u_m \| ) \] which corresponds to \[ 
\BAnd^{n}_{i=1}(\exists \vx_i \forall \vy : z = t_i \And 
\bigwedge^{m}_{j=1} z_i \nq u_{j}) \]

\begin{Examplen}
\beq
\label{ex:mod2}
ss0 & \Lmap & 0\\
y+0 & \Lmap & y\\
0+y & \Lmap & y\\
y+y & \Lmap & 0 \eneq 
These rules define integer addition modulo $2$.  
The question of sufficient completeness (in this case yielding a 
positive answer) can be expressed by the following problem (which 
intuitively leads to $\bot$):
\[
\exists x_1x_2\forall y : (z= x_1 + x_2) \And (z \nq ss0)\And (z \nq 
y+0)\And (z \nq 0+y)\And (z \nq y+y)
\]
which corresponds to
\[
\| x_1 + x_2\| - \|ss0,0+y,y+0,y+y \|
\]
\end{Examplen}

Then, since a variable stands for the universe of discourse, a {\em 
complement problem} is representable merely by $ \| z\| - \| u_1 
\mdots u_m \|$, i.e.\ a simpler ($\exists$-degenerate) case of 
equational problem
\[ 
\forall \vy : \bigwedge\limits^{m}_{i=1} z \nq u_{i}
\]
Thus a disunification algorithm over finite trees will solve 
complement problems, eventually providing values for free 
variables.

\section{Barbuti's {\em \mnot}}
\label{bnot}

We present the {\em \mnot} algorithm for first-order terms that 
specializes \cite{Las87} and is at the heart of Barbuti et al.'s 
approach \cite{Bar90}.  We present it in a many-sorted framework, 
differently from the original version\footnote{Note anyway that the 
related notion of {\em covering} presented in \cite{Bro90} is indeed 
many-sorted.}.

\begin{Definition}
Consider a many-sorted finitary signature $\Sigma$ and a linear term 
$t: \tau$ .  We define $\mnot(t)$ by structural induction, where we 
suppose that $t_i$ has type $\tau_i$:
\[ \begin{array} {lll}
\mnot(x : \tau) & =  & \emptyset: \tau \\
\mnot(f(\tn) : \tau) & = & \\
 & \{g(\zp) : \tau \mid  \mbox{for all $g \in \Sigma$ distinct from } 
f\} \cup \mbox{} 
\\
% & \{f(x_1 \mdots x_{i-1},\vs,x_{i+1}, \dots,x_n) : \tau \mid  s \in 
% \mnot(t_i) : \tau_i, i \in [1,n] \}
& \{f(x_1 \mdots x_{i-1},s,x_{i+1}, \dots,x_n) : \tau \mid s\in\mnot(t_{i}), i \in [1,n] \}
\end{array} \]
\end{Definition} 
Standard Prolog is not typed: this means that the uni-sorted version 
of this function tends to produce a lot of irrelevant outcomes (this 
has some analogy with the problems raised in in \cite{Foo88}).  For 
example, the result of $\mnot(0)$ in the (informal) signature of lists 
of numerals contains not only $\{s(x)\}$ as expected, but also $\{nil, 
0.nil \ldots \}$.  This may tend to increase dramatically with the 
size of the signature.  On the other hand, fixing $$\Sigma = \{0 : nat 
, nil : nlist , s : nat \Imp nat, cons : nat \Imp nlist \Imp nlist 
\}$$ For instance $\mnot(s(x).nil)$ yields only the desired 
 $\{nil,0.nil,y.z.xs\}$.
Moreover, more refined type theories, as dependent types and\slash 
or subsorts will further constrain the evaluation of $\mnot$.
\smallskip
It is possible to prove the set-theoretic correctness of the 
algorithm. 

\begin{Ppn}
$s \in \mnot(t)$ iff $s \not\in\| t \|$
\end{Ppn}
\begin{proof}
See proof of Proposition \ref{ppn:part}.
\end{proof}

% 
% \begin{Ppn}
% If $s \in \mnot(t)$ then $ \| s \| \not\subseteq \| t \|$
% \end{Ppn}
% \begin{proof}
% By induction on $t$.
% \begin{itemize}
% \item Basis: trivially true.
% \item
% Step: let $t \equiv f(\tn)$. Proceed by absurdum:
% \begin{enumerate}
% \item
% $s \equiv g(\zp)$: hence $\| g(\zp) \| \not\subseteq \| f(\tn) \|$ 
% by the $Clh$ axiom.
% \item
% $s \equiv f(x_1 \mdots x_{i-1},\vt,x_{i+1}, \dots,x_n)$. Apply the 
% inductive hypothesis to $\vt$.
% \end{enumerate}
% \end{itemize}
% \end{proof}
The model-theoretic correctness and the usability \wrt the 
transformation technique of the $\mnot$ procedure is guaranteed by the 
following result: %\begin{sloppypar}
\begin{Theorem}[\cite{Bar90}]
\label{t:bar}
Let $\vt$ be linear, $\mnot(\vt) = \{ \vt^c_1 \mdots 
\vt^c_n\}$ and $\vx$ a tuple of fresh variables.  Then
$E_{\Sigma T\cup DCA} \models \forall \vx(\forall(\vx \neq \vt) 
\Bimp \BOr^n_{i=1} \exists (\vx =\vt^c_i))$.
\end{Theorem}
%\end{sloppypar}
% This equivalence is crucial, inasmuch it allows to substitute a 
% complement problems with a set of positive terms.  This is actually 
% nothing more than a Corollary of Theorem \ref{thm:LM}, that we discuss 
% now.  
% % Reconsidering Example~\ref{eqb: odd},
% Considering the equational problem $\forall y: z \neq 0 \And z \neq 
% s(s(y))$ you would expect first to compute $\mnot(0) = \{s(x)\}$, then 
% $\mnot(s(s(y))) = \{0,s(0)\}$ and eventually somehow `anding' the result 
% to come up with the expected outcome $s(0)$.  This computation is 
% instead executed sequentially inside the transformation technique, as 
% discussed in Section~\ref{comparison}, and for some good reasons.  It 
% is worthwhile to imagine the semantics of the `anding' operation.  
% Intuitively, this would consist of some kind of set intersection with 
% unification.  This accordingly suggests a framework similar to the 
% lattice of first-order terms ordered by subsumption \cite{Las88} and 
% modified to take into account disjunction of terms (intensional 
% representation) as urelements.  
% %\include{lattice}
% Well, it turns out that this is not so immediate, due exactly to some 
% undesirable features of the $\mnot$ operator.  In other words, 
% intensional representation of terms are not closed under 
% complementation.
This equivalence is crucial, inasmuch it allows to substitute a 
complement problems with a set of positive terms.  This is actually 
nothing more than a Corollary of Theorem \ref{thm:LM}, that we discuss 
now.  Moreover it shows why the linearity requirement cannot be 
dropped.  The \mnot algorithm aims to behave as a complementation 
operator.  This accordingly suggests a framework similar to the 
lattice of first-order terms ordered by subsumption \cite{Las88} and 
modified to take into account disjunction of terms (intensional 
representation) as urelements.  Well, it turns out that this is not
immediately achievable, due exactly to some undesirable features of the $\mnot$ 
operator.  In other words, intensional representation of terms are not 
closed under complementation.  One canonical example is as follows: 

\begin{Examplen}
Consider the signature $\{a:i, f: i \Imp i \Imp i\}$: intuitively the 
complement of $f(y,y)$ should look something like:
\begin{equation}
\label{fxx}
\| z \| - \|f(y,y)\|  =  \{a\} \cup \{ f(x,z) \mid x \nq z \}
\end{equation}
Instead, the $\mnot$---as well as the {\em uncover\/}---algorithm 
incorrectly yields:
\[
\mnot(f(y,y)) \stackrel{?}{=} \{a\} 
\]
\end{Examplen}
In fact, Lassez \& Marriot \cite{Las87} have shown that the latter 
is correct only for {\em linear} terms: complement of non-linear 
ones do not have a straightforward finite representation.  This can be 
seen as the question whether an equational problem correspondent to a 
complement problem has always an unification solved form.  For 
instance $\mnot(s(0)) = 0 \Or ssy$, yet $z\nq s(0)$ may be considered 
irreducible, being already a solved form with constraints.  The key 
problem is then if it is possible to rephrase $z\nq s(0)$ into a 
unification problem, \ie if the relative complement $\| t\| - \| t_1 
\mdots t_m \|$, denoted ${\cal P}_{t;t_1 \mdots t_n}$ can be turned in 
an equivalent unification problem $\cal U$, so that ${\cal U} 
\approx_{\Sigma(T)} {\cal P}_{t;t_1 \mdots t_n}$.  This is answered 
by:
\begin{Theorem}[\cite{Las87}] 
\label{thm:LM}
There is an explicit representations of $\| t\| -
\|t_1\mdots t_n\|$ iff the signature is finite and $t_1\mdots t_n$
are unrestricted \wrt $t$. In particular, let $\q_i$ be the mgu of 
$t$ and $t_i$: then there is a $\cal U$ so that ${\cal U} 
\approx_{\Sigma(T)} {\cal P}_{t;t_1 \mdots t_n}$ iff there is $\phi_i 
t$ such that $\| \phi_i t\| =\|\q_i t\|$ and $\phi_i t$ is 
unrestricted \wrt $t$ for $i \in [1,n]$.
\end{Theorem}
%This has been further generalized by Comon \cite{Com89}.
% 
% \begin{Corollary}
% \label{claim:uncover}
% Let ${\cal U} \approx {\cal P}_{t;t_1 \mdots t_n}$ and let $\exists 
% \vx \forall \vy : \BAnd^{n}_{i=1} z_i = t_i \And 
% \bigwedge^{m}_{i=1} z_i \nq u_{i}$ rewrite to the unification 
% solved form $\exists \vx : P^*$. Then ${\cal S(U)= S}(\exists \vx : 
% P^*)$
% \end{Corollary}

% Again note that the reading of complement problems as equational 
% problems allows a uniform treatment of this kind of examples, 
% namely the former complement problem is equivalent to $\forall y : 
% z \nq f(y,y)$ which has the solved form $z = a \Or z = b \Or 
% \exists x_1,x_2 : z = f(x_1,x_2) \And x_1 \nq x_2$.


This constitutes further evidence of the opportunity of rephrasing 
unrestricted relative complements as disunification problems: one 
point is the ugliness of the original {\em uncover} algorithm 
\cite{Las87}.  The latter, in fact, is fairly complicated, somehow ad 
hoc, uncooperative to reasoning about it and overall difficult to 
generalize.  On the other hand, absorbing complements inside 
disunification offers a neat gain in term of elegance, declaratively, 
generalizability both to various type-theory and to more complicated 
syntax.  In summary it inherits all the advantages of a sound and fast 
developing subfield in equational studies.  More technically it nicely 
overcomes the difference between {\em linear} and {\em non-linear\/} 
terms in the difference between various solved forms.

% Hence the equivalence between {\em \mnot} and the appropriate 
% disunification problem follows from Corollary \ref{claim:uncover},
% semantically:
% 
% \begin{Corollary}
% For any ground term $s,  s \in \| \mnot(t) \| $ iff there exists $\q 
% \in {\cal S}(\forall \vy : z \nq t)$ such that $s \in  rng(\q)$.
% \end{Corollary}
% 
% Overloading the symbol `$\Or$', the proof-theoretic statement goes 
% like this:
% \begin{Corollary}
% \label{co: pt-equiv}
% $\mnot(t) = t_1 \Or \cdots \Or t_n$ iff\ $\forall \vy : z \nq t \Lmap^*
%  z = t_1 \Or \cdots \Or z = t_n$.
% \end{Corollary}
% 
% \medskip

As well known, the limitation in \ref{claim:uncover} seems to be 
almost immaterial in \lp thanks to the idea of {\em 
left-linearization} introduced by Plaisted and used by Stickel 
\cite{Pla88,Sti88} to avoid unnecessary occur checks testing.  It 
simply consists of allowing only heads with linear terms as argument 
and constraining equal occurrences in the body by a new predicate, say 
$eq$, whose definition is $eq(x,x)$.  As a matter of fact, this 
approach is less innocent as it looks at first sight, since it opens 
the road to transformation of the source program
%  and in particular it 
% sweeps under the rug the move to a touch of constraint 
% \lp
\footnote{This is particularly keen to \cite{Bar90} where the 
source program has a very restricted acceptable format (see 
Section~\ref{comparison}).  Moreover it is consistent with the 
development of the approach to CLP as in \cite{Bru93}.  A discussion 
can be found in \cite{Mom95}.}. What is worse, it entails an 
axiomatization if inequality which is parameterized by the signature, 
see \ref{dis}.

Anyway, this is not the only road that can be traveled. We may be 
using: 
\bit
\item
{\em Regular tree languages} to describe (unary) types 
\cite{Gec84,Pfe92b}.
\item
 {\em Constrained terms} \cite{Com88,Com91b}
\item
Complement operations based on  disunification.
\enit

Both the first and second approaches\footnote{which are not disjoint, 
if we wish to use as in \cite{Com91b} (order) sorted signatures, as 
the latter are identified with finite bottom-up tree automata, where 
the sorts are the states and the function symbols are the terminal 
alphabet.  More details in the cited report.} enjoy closure under 
complementation.  The last one seems to have the required amount of 
elegance and generality at the cost of an increased technical 
complexity.
