\section{Related Wok}
\label{sec:related}

Complement problems have some  relevant applications in theoretic computer 
science (see \cite{Comon91} for a list of references); for example in functional programming to 
produce non-ambiguous function definitions by patterns and to 
improve its compilation, in rewriting systems, to check whether an 
algebraic specification is sufficiently completeness,or to analyze 
communicating processes expressed by infinite transition systems, as well as 
in machine learning and inductive theorem proving. In \lp Kunen 
\cite{Kun87} used them to represent infinite set of answer to 
negative queries. An other approach is discussed in \ref{sec:appl}.

Lassez et Marriot \cite{Las87} proposed the seminal 
{\em uncover} algorithm  for computing relative 
complements and introduced the now familiar restriction to linear terms.
We here quote the definition of the $\mnot$ algorithm for the 
(singleton) complement problem given in \cite{Bar90} as an gentler
 introduction 
to our Definition \ref{def:compl}.

Consider a finite language $L$ and a linear term $t$.  
\[ \begin{array} {lll}
\mnot_L(x  ) & =   \emptyset  \\
\mnot_L(f(\tn)  ) & =  \\
 & \{g(\vx)   \mid  \mbox{for all $g \in \Sigma$ distinct from } 
f\} \cup \mbox{} 
\\
& \{f(z_1 \mdots z_{i-1},s,z_{i+1}, \dots,z_n) \mid 
s\in\mnot_L(t_{i}), i \in [1,n] \}
\end{array} \]

An alternative solution to the relative complement problem is 
\emph{disunification} (see \cite{Com91} for a survey and \cite{Lug95} for 
an extension to the simply-typed $\l$-calculus): here operations on 
sets of terms are translated into conjunctions or disjunctions of 
(dis)equations whose quantification status is also kept explicit.  
Non-deterministic application of a few dozens rules, some addressing 
identity on finite trees, other (dis)equality in general, eventually 
turns the given problem into a solved form.  Though a reduction to a 
significant subset of the disunification rules is likely to be 
attainable for complement problems, controls is a major problem.  We 
argue that using disunification for this purpose remains overkilling.  
Moreover the \ho case brings in additional complications, as 
dependencies, which are orthogonal to the hyper-logical structuring 
that disunification requires.

