% \begin{chapter}
% \label{ch: fo-dis}

This chapter (III) gives a smooth introduction to first-order 
disunification: we 
then show how to cast complement problems as disunification. 
Thirdly we integrate the latter into (essentially) Sato \& Tamaki's
transformation technique. Finally, we deal with the problem of local 
variables and the related issue of extensional quantification.

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

Indeed, 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{Background on First-Order (Dis)Unification}

For the sake of this chapter the underlying logical framework is 
implicitly many-sorted.  We will disclose the relevant (simple) 
typing only when it is difficult to infer from the context.  We 
assume thusly that we deal with well-typed objects and rules which 
preserve this property.  We proceed this way for pedagogical reasons 
only: it would be rather time-consuming to detail each typing in all 
its glory since it will eventually subsumed by the \ho framework.  
Moreover we will not work modulo some (quotient of a) locally free 
$\Sigma$-algebra, but with the standard model, the closed term model, 
more known to the \lp people as the {\em Herbrand Universe}.  See 
\cite{Com89,Com91} for a presentation respectively modulo many-sorted 
and $\Sigma$-algebrae.

\smallskip
Let $E_{\Sigma T}$ be the following formulation of  $CET$, {\em 
Clark's equational 
theory}, (\cite{Cla78,Kun87}), that is the equality axioms including 
congruence (Cng), plus the axioms for finite trees\footnote{We 
identify terms and finite trees as usual---the formal definition 
appears in~\ref{defs}.}, also called freeness (or distinctness 
axioms): for all operators in a signature $\Sigma$, $Dec$ enforces 
injectivity,
$Clh$ maintains that (the interpretation of) different symbols for 
function yields different values. $Ock$ should remind of the occur 
check in the actual unification algorithm. Indeed this theory is the 
axiomatic and proof-theoretic rendering of the latter algorithm, so 
that Clark's Lemma below is referred to as the Unification Lemma.
We assume the notational conventions introduced earlier.
\begin{Def}
\[
\begin{array}{llr}
(Ref): & \forall(x=x)\\
(Sym): & \forall(x=y \Imp y=x)\\
(Trn): & \forall(x=y \And y =z \Imp x=z)\\
(Cng): & \forall(\xn  = \ol{y_n} \Imp f(\xn) = f(\ol{y_n}))
 & \mbox {for   all }   f \in \Sigma\\
(Dec): & \forall(f(\xn) = f(\ol{y_n}) \Imp \xn = \ol{y_n}) & 
\mbox{for all }   f \in \Sigma\\
(Clh): & \forall(f(\xn) \nq g(\ym)) & \mbox{for distinct }  f,g \in 
\Sigma 
%\ \mbox{ of the same target type}
\\
(Ock): & \forall(x \nq t[x]) & \mbox{if $x$  occurs  properly  in}  \
t[x]
\end{array}
 \]
Additionally, define $E_{\Sigma T \cup DCA}$ (shortened
in $E_{\Sigma T^*}$ or $CET^*$) as the previous axioms 
plus
\beq
(DCA): & \forall x(\bigvee\limits_{f \in \Sigma}
\exists \vy (x=f(\vy))) 
\eneq
\end{Def}



\begin{Theorem}[Kunen \cite{Kun87}, Maher \cite{Mah88}]
\label{EFT:complete}
If $\Sigma$ is infinite then $E_{\Sigma T}$ is a complete theory 
(for arbitrary sentences); 
moreover it is a complete axiomatization of the algebra $T(\Sigma) 
$ of finite trees.
%---the Herbrand Universe. 
If $\Sigma$ is finite and not trivial (\ie it 
contains at least a constant and a function symbol) the same holds
for $E_{\Sigma T\cup DCA}$.
\end{Theorem}

In fact,  $E_{\Sigma T}$ (or $E_{\Sigma T\cup DCA}$)  are 
$\aleph_0$-categorical: the term model (for non-trivial signatures 
again) is countable, no model is finite  as enforced by $Clh$ and 
$Dec$ and every other 
denumerable model is isomorphic due to $Ock$ (or $Ock$ and 
$DCA$)---see for example Theorem 1 in \cite{Man88}). Thus 
completeness of the theory follows by the Los-Vaught theorem.


\begin{Theorem}
[Mal'cev] $E_{\Sigma T}$ has no finite axiomatization.
\end{Theorem}


It seems again that the crux of the matter lies in the cardinality of
the signature, which is in turn related to the universal query 
problem \pageref{uqp}. Finite signatures require the $DCA$.

The former results are actually corollaries of a theorem by Mal'cev 
that states that 
$E_{\Sigma T}$ is a complete axiomatization of the class of locally 
free algebrae, \ie 
 those whose finitely generated subalgebrae are free (this is why 
the finite trees axioms are called freeness axioms) and that there is
a finite axiomatization of this class. Maher has extended it to 
finite signatures, rational and infinite trees.

%Thus if you want to show completeness of a model of $E_{\Sigma 
%T}$ you show it is locally free. 

\begin{Examplen}
\label{ex:nat}
The algebra ${\cal N} = \la N, 0, s \ra$ of naturals is locally free:
$E_{\cal N^*}$ contains

\[
\begin{array}{llr}
%(Cng): & \forall x,y (x  = y \Imp s(x) = s(y))\\
(Dec): & \forall x,y ,s(x) = s(y) \Imp x  = y\\
(Clh): & \forall x. 0 \nq s(x)\\
(Ock): & \forall x. x \nq t[x] & \mbox{if $x$  occurs  properly  in}  
\
t[x]\\
(DCA): & \forall x. x=0 \Or
\exists y.  x=s(y) 
\end{array}
 \]

$Clh$ says that $0$ is not a successor, $Dec$ that the latter is a 
one-one 
mapping, $DCA$ that every non-zero is a successor and the schema 
$Ock$ 
that there are no loops, i.e.\ there are no isolated elements.  Note 
that this signature is the prototypical case  where there is an 
axiomatic redundancy, since every instance of $Clh$ is an instance of 
$Ock$.  This is to be compared with the usual axiomatization of the 
numerals. Here the role of $Ock$ is held by $Clh$ and induction, or 
by the stronger infinitary version of DCA:
\[
\begin{array}{llr}
(DCA^\omega): & \forall x. x=0 \Or x=s(0) \Or \dots 
\end{array}
 \]
\end{Examplen}

It must be remarked that this formulation of the axioms is not the 
most economical one, not only due to the formulation of 
equality but \wrt the $Ock$ axiom. In certain circumstances 
(instances) the latter encompasses the $Clh$ axiom (see for instance 
 Example~\ref{ex:nat}). Indeed, the logical statement of the occur 
check is more ample that its operational reading. While it is 
clear that the axiom should hold only when the left hand side ought to 
be only renamable to a  variable, it 
is not clear (to me) whether this is first-order expressible at 
all\footnote{ELABORATE}: It may then be argued that the more elegant 
framework is then rational trees. This does not seem to be the case 
when disunification is concerned, see \cite{Com89}. Anyway, we 
conclude by mentioning the unique solution axiom for rational trees, 
which replaces $Ock$, yielding the axioms $E_{\Sigma RT}$:
\beq
US: & \exists x\forall y : x =t[x] \And (y = t[y] \Imp x =y ) &\mbox{for 
non-trivial }\, t
\eneq

 \smallskip

From Theorem~\ref{EFT:complete} Clark's lemma follows 
immediately:
\begin{Lemma} [Clark 1978]
Let $s$ and $t$ be two terms in $T(\Sigma)$:
\begin{enumerate}
\item if they are unifiable, $E_{\Sigma T} \prv \exists (s=t)$
\item if not $E_{\Sigma T}\prv \forall(s \not = t)$
\end{enumerate}
\end{Lemma}

\noindent
{\bf Note:} The lemma holds for any signature, finite or infinite, 
\ie it is independent from the $DCA$. The direct syntactic proof, 
based on the Martelli-Montanari's 
rewrite system, uses only
reflexivity\footnote{This was, I think, first observed in 
passing in \cite{Pfe91a} where the author was refining the MM 
approach to a meta-logic for unification.} for 1.\ , congruence plus 
axioms 
for finite trees for 2.\ ---the negative result. This contrasts with 
Lloyd's proof w.r.t.\ Robinson algorithm \cite{Llo87}. 

\smallskip

\begin{proof}
Let $S$ be $\{s=t\}$ and consider the MM-rules augmented with the 
failure cases (rewriting into $\perp$).
\begin{Claim}
\mbox{} 
\begin{enumerate}
\item
 If $S \Lmap^*_{\cal MM} S^*$ and the latter is in unification solved 
form, then
$E_{\Sigma T} \prv \exists (s=t)$
\item
If $S \Lmap^*_{\cal MM} \bot $, then $E_{\Sigma T} \prv \forall (s 
\neq t)$.
\end{enumerate}
\end{Claim}
By induction on the number of rewrite steps. 
\end{proof}


A very similar, though independent,   proof (Unification Lemma) can 
be found in \cite{SH93}. Here the author, following \cite{Sa92},  
gives a neat sequent-style formulation of free equality, which is 
easily seen provably equivalent to $CET$. Furthermore he 
demonstrates  cut-elimination for equality formulae. We will 
implicitly use the latter property when dealing with axiomatic 
$CET$ in the context of other cut-free (or normalized) systems.

\smallskip

A syntactic proof of Theorem~\ref{EFT:complete} can be achieved by 
quantifier elimination \cite{Mah88}. This may become handy in the 
\ho case, where model-theoretic arguments are less available. On the 
other hand this result
can be obtained from the completeness and termination (and 
solvability, \ie the fact that solved forms have solutions, see 
\ref{def:sost-as-sol})
of disunification, as proved for instance in 
\cite{Com89}\footnote{Actually this directly concerns $\Sigma 
2$-equational formulae but it can easily be extended to arbitrary 
ones, which is another form, though more limited, of quantifiers 
elimination.}. Moreover
the aforementioned proof is achieved  \wrt a many-sorted language.
Since we will be actively interested in designing set of rules for 
disunification in the higher-order setting, we will consider 
Theorem~\ref{EFT:complete} as a corollary of future termination and 
completeness proofs.

Finally, we mention that it is possible to extend the results to 
rationale and infinite trees, as 
in the cited papers.


\section{Equational Problems and Disunification}
\label{disunif}
Disunification is devoted to solving {\bf arbitrary} first order 
formulae
whose only predicate symbol is equality, call them {\em equational 
formulae}.  The definition of what a {\em solution} is differs on the 
application at hand. We may be interested only in the overall 
validity 
or in the possible assignments that make the formula valid. 

\subsection{Related Work}

From an historic perspective this field became defined when it was 
realized by Martelli \& Montanari (if not by Herbrand) that 
\fo-unification can be seen as a transformation on set of equations. 
On the other hand the work of 
Mal'cev \cite{Mal71} on the decidability and complete axiomability of 
the theory of equational algebrae is clearly an ancestor.

The definition of Prolog-II introduced disequation. Indeed Colmerauer 
\cite{Col84} showed them to have solutions in the algebra of rational 
trees.
Next
Lassez et Marriot \cite{Las87} proposed the seminal (although 
awkward) {\em uncover} algorithm  for computing relative 
complements.
% of linear first-order terms
%\footnote{Definition in chapter 1, discussion in~\ref{bnot}.} 
As we will see, those problems are systems of disequation with 
universally quantified variables.

Kirchner and Lescanne first unified those previous papers in the 
framework of equational problems and proposed a set of 
transformational rules, though without a completeness proof
\cite{Kir87}.

Maher introduced the unification community to Mal'cev's results 
\cite{Mah88}. Comon and Lescanne were the first one to present an adequate set of 
rules \cite{Com88,CL89} and the former surveyed the field \cite{Com91}.
Now this has become a fast growing 
area in its own which
is impossible to review here: extension of disunification in 
order-sorted signatures is under research as well as in the presence 
of specific equational theories, inequalities   and symbolic 
constraints. We will be
presenting only what is required for our ultimate goal. 

\subsection{A Preliminary Account of Disunification}
How to go on to derive a disunification procedure can therefore vary 
from the syntax and semantics we are concerned with, but 
nevertheless it entails the following steps:
\bit
\item
Provide a set of axioms $\cal T$ that hold in the model we consider
\item
Design a set of rules $\cal R$ for the transformation of equational 
formulae that can be proven correct w.r.t.\ $\cal T$
\item
Design a control $C$ on $\cal R$ such that the application of rules 
satisfying $\cal R$ terminates: irreducible formulae are in solved 
form and have the same set of solutions of the original problem
\item
If arbitrary formulae are allowed and solved form are trivially 
decidable, this entails the decidability and completeness of $\cal T$.
\enit

The simplest example is unification of finite (first-order) trees: 
\bit
\item
 $\cal T$ is $E_{\Sigma T}$
\item $\cal R$ are, say, the MM rules; correctness corresponds to the 
preservation of solutions under rule application, or it can be 
refined into the content of Clark's lemma
\item
 Solved forms yield idempotent substitutions (see definition 
\ref{sf}) and control restricts the application of variable 
elimination. Completeness (of the theory) is established for example 
as in \cite{Mah88}.
\enit

We now list some standard definition that will be useful in the 
sequel.

\begin{Def} [Equational Formula] An {\em Equational formula} is an 
arbitrary first(higher)-order formula, such that $`='$ (resp.\ 
$`=_{\beta\eta}'$) is its only predicate symbol.
\end{Def}

 For instance, an {\em unification problem} \label{unifprob} is 
equivalent to a finite disjunction of equations. 

\begin{Def}
[System] A {\em system} $P$ is defined by the following grammar
\[
P::= \top \mid \bot \mid s=t \mid s\neq t \mid P_1 \And P_2 \mid 
P_1 \Or P_2
\]
\end{Def}
It is convenient to choose a normal form for the former notions. Thus 
we will consider equational formulae to be prenex, where the matrix 
is in conjunctive normal form. Other normal forms work equally well, 
provided they are induced by a canonical rewrite system. See 
Section~\ref{bnf} for more details.
\begin{sloppy}
\begin{Def} [Equational Problem]
An {\em equational problem} $\cal E$ is a $\Sigma_2$-equational 
formula, \ie it has the form 
$\exists \xn \forall \ym : P$, where $P$ is a system.
\end{Def}
\end{sloppy}
Equational problems are also known as {\em elementary formulae} 
\cite{Com91}, but we find this terminology misleading. 

We will try to use consistently
$\xn,\ym,\zp$  respectively for existential, universal and 
free---sometimes called the unknown of the 
problem---variables\footnote{I am affording myself the luxury of 
having both 
free and existential variables to be consistent with the 
literature.}. These classes are assumed to be disjoint.
It will also be convenient to employ $\wr$  for either a free or an 
existentially quantified variable.

\begin{Def}[Solutions]
\label{def:sost-as-sol}
A {\em solution} $\s$ of an equational problem $\cal E$ is a {\bf 
closed} 
substitution (from the term algebra) such that $FV({\cal E}) 
\subseteq Dom(\s)$ which satisfies the following
requirements:
\bit
\item
If $\cal E$ is $\top$, there are no requirements
\item
If $\cal E$ is $\bot$ then no substitution can be a solution
\item
If $\cal E$ is $s=t$, then $\s s$ and $\s t$ are identical
\item
If $\cal E$ is $s\neq t$, then $\s s$ and $\s t$ are different
\item
If $\cal E$ is a disjunction $d_1 \Or \cdots \Or d_n$, then there is 
some
$i$ such that $\s_{\mid FV(d_i)}$ is a solution of $d_i$
\item
If $\cal E$ is a conjunction $c_1 \And \cdots \And c_n$, then for all
$i$  $\s_{\mid FV(c_i)}$ is a solution of $c_i$
\item
If $\cal E$ is $\exists \xn \forall \ym : P$, then there is a closed 
substitution $\q_n$ such that for all closed substitutions $\rho_m$, 
$\s$ is a solution of $\q_n \rho_m P$.
\enit
\end{Def}
Again, this definition can be made parametric to any $\Sigma$-algebra 
$\cal A$, taking as $\cal A$-solutions the set of $\cal 
A$-assignments for the given unknown that satisfy the previous 
conditions. 
Let ${\cal S(E)}$ be the set of solutions for an equational problem 
$\cal E$:
we write ${\cal E}_1 \approx_{\cal A} {\cal E}_1 $ for a 
$\Sigma$-algebra $\cal A$ whenever ${\cal S(E}_1) = {\cal S(E}_2)$. 
If $\phi \approx_{\cal A}  \top$, we write ${\cal A} \models \phi$. 
%Finally, for the \ho case, insert the right equality. 

\begin{Def}
. A rule $R$ is {\em sound} ---no new solution---if
\[ \cal E \Lmap_R E' \Rightarrow S(E') \subseteq S(E) \]
It is {\em preserving} ---no lost solution---if 
\[ \cal E \Lmap_R E' \Rightarrow S(E) \subseteq S(E') \]
A rule is {\em correct} if it is both sound and preserving.
\end{Def}

We can think of a rule as a $4$-tuple $\la L, R, SC, C \ra$, where to
the left and right hand side we add a set $SC$ of side conditions to 
guarantee correctness and completeness and some control conditions 
$C$ to help with 
termination. When not concerned with the latter, we will not 
mention it, simplifying the exposition of the rules. 

Rules are chosen so to transform a problem in an equivalent 
presentation, called a {\em solved form} as a solution can be easily 
extracted from it. More explicitly:
\begin{Def} [Completeness]
A set of rules {\bf S} for solving equational formulae is {\em 
complete} \wrt a notion of solved form $\Sigma$---usually a subset of 
the former---if for any $\cal E$ there is a family  ${ \cal F}_i$ in 
$\Sigma$-normal form such that the latter are obtained by the former 
by application of the rules in {\bf S} and the union of the solution 
of the ${\cal F}_i$ is the set of solutions of $\cal E$.
\end{Def}
Several types of solved forms
can be considered depending on the application see \cite{Com91}.  We 
give the most 
useful to our purposes, in decreasing order of generality.

\begin{Def}  [Solved Forms]
\label{sf}
An equational problem $\cal E$ is in {\em parameterless} solved form 
if it 
contains no universal quantifiers. It is a {\em solved form with 
constraints\/}\footnote{Usually called in the literature a {\em 
definition with constraints}.} if it has the form
\[ \exists \vx : \BAnd\limits^m_{i=1} z_i = t_i \And 
\BAnd\limits^n_{j=1} z'_j \neq s_j \] 
\noindent
where 
$\vx = FV(t_1 \mdots t_m) \cup FV(s_1 \mdots s_n)$ and 
the free variables $z_1\mdots z_m$ occur only once in the 
system---note: this does not apply to the unknown $z'_1\mdots z'_n$.
A {\em unification} solved form is a solved form with constraints 
where no disequation occurs.
\end{Def}

For our purposes the latter two will be relevant\footnote{Please see 
\ref{tech} for some technical remarks on the operational use of solved 
form, especially solved form with constraints.}. Indeed unification 
solved form is the prototypical basis for any more complex solved 
form, like {\em basic formulae} \cite{Com91}, {\em simple formulae} 
\cite{Mah88}, {\em standard formulae} \cite{Mal71}, 
{\em substitutions with exceptions} \cite{Bur88} and so on.

\medskip

The disunification rewrite rules are divided in three big chunks:
\bit
\item
Equality rules, \ie rules which are correct for any equational algebra
\item 
Rules for finite trees over a infinite signature
\item 
Rules for finite trees over a finite signature.
\enit
We delay the presentation of the complete set of rules with 
proviso, control and notational conventions to the \ho case.  We 
just mention that the first group contains {\bf R}eplacement, 
{\bf U}niversal Quantifier {\bf E}limination, {\bf E}xistential 
quantifier {\bf E}limination  and {\bf E}limination of {\bf 
D}isjunctions.
The second batch  contain {\bf C}lash, {\bf D}ecomposition, {\bf 
O}ccur check. The third section would contain rules which are sensitive 
to the cardinality of the signature. Here we mention only
the {\bf E}xplosion rule, which is clearly motivated by the $DCA$.

We list below the rules relevant to the following examples in their 
barest form, \ie with only soundness and no termination condition:
\begin{figure}[h] 
\label{fig:fo-disunif}
\[
\begin{array} {lllll}
R & : & w=t \And P[w] & \Lmap & w=t \And [t/w]P\\
M1 & : & w=t \And w\not=u & \Lmap & w=t \And t\not = u\\
UE1 & : & \forall \vy,y : P \And y \neq t & \Lmap & \bot\\
% % UE2 & : & \forall \vy,y   : P \Or y \neq t & \Lmap & \forall \vy  : 
% [t/y] P\footnote{Used?}
% \\
Clh(T) & : & f(\tn) \nq g(\sm) & \Lmap & \top\\
Clh(F) & : & f(\tn) = g(\sm) & \Lmap & \bot\\
Dec1 & : & f(\tn) \neq f(\un) & \Lmap & \BOr\limits^{n}_{i=1} t_i \neq 
u_i\\
Dec2 & : & f(\tn) = f(\un) & \Lmap & \ANrd\limits^{n}_{i=1} t_i = 
u_i\\
E & : & \forall \vy : P & \Lmap & \BOr\limits_{f \in \Sigma} (\exists 
\vx \forall \vy : P \And w  = f(\vx))
\end{array}
\]
In {\bf R} $w \not \in Var(t)$, in {\bf E}, $P$ contains a 
(dis)equation with LHS $w$ and RHS $u$, where the latter is not a 
variable and contains a parameter.
\caption{Some disunification rules with minimal proviso}
\end{figure}
\begin{sloppypar}

A useful variant, with similar proviso, found in \cite{Com91b} which 
has a leading role in \ho disunification is:
\[
\begin{array} {lllll}
EEx & : &\exists \vx,x : P[x\nq t] &\Lmap &\BOr\limits_{f \in \Sigma} (\exists 
\vx\vw : P(x:=f(\vw))
\end{array}
\]
We mention the following completeness results \cite{Com89}: 
the rules Replacement, Clash, Decomposition, Occur Check, Universality 
of Parameters, Explosion and Elimination of Disjunctions are complete for definitions with 
constraints, while  the {\em uncover} algorithm is complete for 
unification solved form w.r.t.\ linear terms.
\end{sloppypar}

\subsubsection{Working with Normal Forms}
\label{bnf}
As a matter of fact, there is some latitude in designing a complete 
set of rules. This depends on several factors: the algebra under 
consideration\footnote{This will be immaterial to us, as we 
restrict to finite trees.}, the notion of solved form in question, 
the 
closeness to an algorithmic version and the usage of a normal form 
for equational problems. 

Addressing the latter, it is a well-known
phenomenon in rewriting systems that sometimes an applicable rule 
is disabled when the 
problem is brought to normal form. This is why completion algorithms 
are used. There are basically two 
approaches:
\bit
\item[(1)]
Work modulo Boolean relations without formalizing the context 
where rules are applied
\item[(2)]
Electing to keep the problem in a normal form.
\enit

The first approach allows to formulate fewer rules and in a more 
declarative fashion. The other is closer to an algorithm: it entails 
some Boolean
 normalization after each application of our rules, \ie
 we are implicitly working on the equivalence classes induced by 
such a (canonical) rewrite system. Hence the rules are tailored to 
the normal form in question and tend 
to multiply: for instance we may need this additional rule for 
decomposition, fit to conjunctive normal form.
\beq
Dec3 : P \And (f(\tn) = f(\un) \Or Q) & \Lmap & P \And \BAnd 
\limits^{n}_{i=1} (t_i  = u_i \Or Q)
\eneq

Yet this is just half of the story: even normal form cannot avoid 
wiring in some subset of Boolean pattern matching. For example 
$M1$
is applicable to, say, $\forall y:  z \nq s(y) \And z = 0$ only 
modulo 
commutativity of conjunction. Let us be more precise: if you are 
working with a normal form like cnf or dnf, the only remaining 
relations we have to deal with are  only associativity and 
commutativity of \And and \Or\footnote{This naturally leads to the 
question of AC-disunification, partially answered in \cite{CLu9?}.}: 
% CL89 p377
On the other hand even the liberal approach of (1) 
cannot evade taking care of Boolean simplification steps like 
absorption of neuter elements.
Moreover there is the issue of some quantifier manipulation; for 
instance suppression of empty quantification (resp.\ universal and 
existential) can be performed by some explicit rule \cite{Com89} 
like 
{\bf E}limination of {\bf P}arameters and {\bf C}leaning, or can be 
pushed into a wider notion of normal form.  The latter could then 
include prenexing operations as additional 
rewrite steps. In summary in this chapter we will compromise, 
following
approach (1) in the formulation of the rules and furthermore 
suppressing mention of logical 
simplification steps. Moreover we will apply an implicit type 
discipline in the examples, skipping the rules for many-sorted 
manipulations.

  On the other hand, we now list in Figure~\ref{fig:cnf}
 the rules which form a canonical system for commutativity, 
associativity and symmetry of quantifier free equational formulae 
leading to conjunctive normal form.
\begin{figure}
\label{fig:cnf}
\beq
s=s \Lmap \top  & &
\Not (s=t) \Lmap s\nq t\\
s\nq s \Lmap \bot  & &
(\phi\And \psi)\Or \chi \Lmap(\phi \Or \psi)\And (\psi \Or \chi)\\
\phi \And \phi \Lmap \phi  & &
\phi \Or \phi \Lmap \phi\\
\phi \And \top \Lmap \phi  & &
\phi \Or \top \Lmap \top\\
\phi \And \bot \Lmap \bot  & &
\phi \Or \bot \Lmap \phi\\
\Not \top \Lmap \bot  & &
\Not \bot \Lmap \top\\
\Not\Not \phi \Lmap  \phi  & &
\Not(\phi \And \psi)\Lmap \Not \phi \Or \Not \psi\\
\Not(\phi \Or \psi)\Lmap \Not \phi \And \Not \psi  & &
\phi \And (\phi \Or \psi) \Lmap \phi
\eneq
\caption{Rules for normalization}
\end{figure}

We add the rules for empty quantification\footnote{Although they seems 
pretty innocuous, they will no longer be valid in the dependent-type 
case, due to the possibility of empty types: in fact those rules 
entails a non empty domain to be applicable.}.  Remember that 
normalization applies to formulae already in prenex form.  More 
importantly remember that the rules are intended solely for equational 
problems, otherwise more complex quantifiers alternation might create 
dependencies, whose provisos would invalidate the rules.  Comon gives 
additional rules to lift everything to arbitrary equational formulae.

\beq
\forall\vy,y:\phi \Lmap \forall\vy: \phi  & y \not\in FV(\phi)  & (UC)\\
\exists\vx:\phi \Lmap  \phi  & x \not\in FV(\phi) & (EC_{1})\\
\exists\vx,x: x=t \And \phi \Lmap \exists\vx: \phi  & x \not\in 
FV(\phi,t) & (EC_{2})
\eneq

Though it may not be visible at first, the two existential rules 
differ, since $x$ occurs in the second problem, but the equation is 
trivially satisfiable.

\smallskip To be precise, though, we should show that the composition 
of the two sets still induces a quotient, notwithstanding the latter 
is a \ho rewrite system, see \cite{Bre88}.

\subsection{Term Complement as Disunification}

We now address how to express the (relative) complement problem 
on terms
as an equational problem \cite{Las87} \cite{Com91}. 
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 \| \]
\noindent
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\| \]

\noindent
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 \| ) \]

\noindent
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 positive) 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\footnote{Unfortunately the algorithm typically does not 
preserve the $\Pi_1$-format, see the Explosion rule.}.

\medskip

We now give an example of disunification on the numerals signature,
which shall be required in the synthesis of the {\tt odd} program. It 
consists in  solving 
\begin{eqnarray}
\label{eqb: odd}
\forall y:z \neq 0 \And  z \neq ssy
\end{eqnarray}
The intuitive solution of (\ref{eqb: odd}) is $z = s(0)$, \ie 
according to Definition~\ref{def:sost-as-sol} the substitution 
$[s(0)/z]$.  We will use the rules in Figure~\ref{fig:fo-disunif} and 
gloss over normalization steps as elimination of trivial 
(dis)equations .  Branches stemming from the explosion rule are 
numbered and pursued separately (keeping in mind that they form a 
disjunction, \ie a finitely branching tree from a search standpoint).  
$R(x)$ denote application of the rule $R$ on variable $x$.  Sometimes 
we use the more informative notation $R(s=t)$.

\begin{Examplen}
\label{ex:num}
\[ \begin{array} {ll}
\fbox{$\forall y: z \neq 0 \And z \neq ssy$}\\
\Lmap_{E(z)(1,2)}\\
& (1) \ \forall y: z \neq 0 \And z \neq ssy \And z=0\\
\Lmap_{M1(z)}\\
& \forall y: 0 \neq 0 \And 0 \neq ssy \And z=0\\
\Lmap ^*_{Clh(F)} \fbox{$\bot$}\\
& (2) \ \exists x \forall y: z \neq 0 \And z \neq ssy \And z=sx\\
\Lmap_{M1(z)}\\
& \exists x   \forall y: sx \neq 0 \And sx \neq ssy \And z=sx\\
\Lmap^*_{Dec,Clh(T)}\\
& \exists x \forall y: x \neq sy \And z=sx\\
\Lmap_{E(x)(2.1,2.2)}\\
&(2.1) \ \exists  x \forall y: x \neq sy \And z=sx 
\And x =0\\
\Lmap_{M1(z)}\\
&  \exists  x \forall y: 0 \neq sy \And z=s(0) 
\And x =0\\
\Lmap^*_{Clh(T)} \fbox{$z=s(0)$}\\
& (2.2)  \ \exists x_1 x \forall y: x \neq sy \And z=sx \And x 
=sx_1 \\
\Lmap^*_{M1(x),Dec1} \\
\exists x_1 x \forall y: x_{1} \neq y \And z=sx \And x 
=sx_1 \\
\Lmap^*_{UE_1(y)} \\
&  \fbox{$\bot$}
\end{array} \]
\end{Examplen}

Formally speaking, our problem has  the unification solved form
$\exists x : z = s(0) \And x = 0$, but we project away the value for 
the unknown 
$z$ which we are interested in\footnote{It is not clear yet when 
projection may get troublesome. Furthermore it could be interesting 
to understand if it is possible to implement the rewriting in a lazy 
way so as to stop when content with the values for the unknown even 
before reaching the required solved form.}.

Note in the derivation the following typical pattern: application of 
an explosion is 
performed as a last resort \wrt the elected solved form ---for 
instance, it can be prioritized to eliminate parameters---and 
immediately accompanied by a replacement of the exploded variable.
This may lead to formulate a derived rule combining the 
above\footnote{It may seem, at first sight, that we substitute $w$
 which could be free in $P$ with $x$ 
which is bound by $\exists$, so that there is a capture:  actually, 
the 
proviso on {\bf E} requires $w$ to be already existential.}:
\[
\begin{array} {llll}
E+R_{(w = f(\vx))}  : & \forall \vy : P & \Lmap & 
[f(\vx)/w](\BOr\limits_{f \in \Sigma} \exists \vx \forall \vy : 
P
%[w=t[\vy]]) 
\And w = f(\vx))
\end{array}
\]

\subsubsection{Barbuti's {\em Not}}
\label{bnot}

Compare with the {\em Not} 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{Def}
Consider a many-sorted finitary signature $\Sigma$. We 
define $Not(t: \tau)$ by structural induction, where we suppose that 
$t_i$ has type $\tau_i$:

\[ \begin{array} {lll}
Not(x : \tau) & =  \emptyset: \tau \\
Not(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 
% Not(t_i) : \tau_i, i \in [1,n] \}
& \{f(x_1 \mdots x_{i-1},Not(t_i),x_{i+1}, \dots,x_n) : \tau \mid 
\tau_i, i \in [1,n] \}
\end{array} \]
\end{Def} 
 
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 $Not(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 $Not(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 $Not$.

\smallskip
It is possible to prove the set-theoretic correctness of the 
algorithm. 

\begin{Ppn}
$s \in Not(t)$ iff $s \not\in\| t \|$
\end{Ppn}
\begin{proof}
By induction on $t$.  We prove only the if-direction, the converse 
being analogous.
\begin{itemize}
\item Basis: $s\in Not(x:\tau) \Bimp s \in \eset$ which trivially 
entails the conclusion
\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}


\begin{Ppn}
If $s \in Not(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 $Not$ procedure is 
guaranteed by the following result:
%\begin{sloppypar}
\begin{Theorem}[Barbuti \cite{Bar90}]
\label{t:bar}
Let $\vt$ be linear, $Not(\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},  \ie the  
equational problem $\forall y: z \neq 0 \And z 
\neq s(s(y))$  you would expect first to
 compute $Not(0) = \{s(x)\}$, then $Not(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. 
This is pursued in section 
\ref{lattice}. 
%\include{lattice}
Well, it turns out that this is not so immediate, due exactly to some 
undesirable features of the $Not$ operator. In other words, 
intensional representation of terms
are not closed under complementation. One canonical example is as 
follows: consider the 
signature $\{a:i, b: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,b\} \cup \{ f(t,s) \mid t \nq s \}
\end{equation}.

Instead, the $Not$---as well as the {\em uncover\/}---algorithm 
wrongly outputs:
\[
Not(f(y,y))= \{a,b\} 
\]

In fact,  Lassez \& 
Marriot \cite{Las87} have shown that the latter are correct only for 
{\em 
linear} terms: complement of non-linear ones do not have a 
straightforward finite representation. 

This is in our terms the question whether an equational problem 
correspondent to a complement problem has always an unification 
solved form. 
For instance $Not(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\| - \| u_1 \mdots u_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 
complements as 
disunification problems: one point is the ugliness of the 
original {\em uncover} algorithm \cite{Las87} for intensional 
complements. The latter, in fact, is fairly complicated, somehow ad 
hoc, uncooperative to reasoning about it and overall difficult to 
generalize\footnote{To moderate this criticism let me mention a 
efficient parallel version of the aforementioned algorithm 
\cite{Kup88}}. 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 Not} and the appropriate 
disunification problem follows from Corollary \ref~{claim:uncover},
semantically:

\begin{Corollary}
For any ground term $s,  s \in \| Not(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}
$Not(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}.}.

Anyway, this is not the only road that can be traveled. We may be 
using: 
\bit
\item
{\em Regular tree languages} to describe types 
\cite{Gec84,Pfe92b}.
\item
 {\em Constrained terms} \cite{Com88,Com91b}
\item
Full-fledged disunification (hopefully some neat subset of the rules).
\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 right amount of 
elegance and generality to suit our purposes.

We elaborate a little the second proposal as \ho \lp  languages are
naturally seen as CLP and, irrelatively, there is a connection with
the characterization of answer sets initiated in \cite{Kun87}. 
Moreover, a different kind of constraints will come up in ome 
formulation of disunification over simple types \cite{Lug94}.
The idea consists of 
promoting constraints as in (\ref{fxx}) to first class objects; 
representations (intensional terms) have the form $\| t \& c 
\|$ where $c$ is a 
constraint in a suitable language\footnote{We avoid considering sorts 
constraints as in \cite{Com91b} as they are foreign to our basic 
philosophy of \emph{prescriptive } typing il \lp.}. More specifically, constraints are 
conjunctions of non-trivial disequations on the free variables of the 
constrained term. Thus the relative complement 
\[
\| t \And d \| -\| s_1 \And c_1 \mdots s_n \And c_n\|
\]
is expressed by the equational formula:

\[
\exists \vx \forall \vy: z = t \And d \And \Not (z=s_1 \And c_1) \And 
\dots \And \Not (z=s_n \And c_n)
\]
\noindent
or, in a more suggestive format
\[
\exists \vx \forall \vy: z = t \And d \And ( z= s_1 \Imp \Not c_1) 
\And \dots \And  (z = s_n \Imp \Not c_n)
\]

Therefore, Example~\ref{fxx} is denoted by

\[
\forall y_1,y_2: z =f(y_1,y_2) \Imp y_1 \not = y_2
\]

Comon showed that the class of finite union of constrained terms is 
closed under complementation. Moreover, constrained terms are 
necessary to express the complement of an infinite set of ground 
terms in anothoter one, which 
would otherwise require an infinitary notation.  Besides, we can 
envision\footnote{Wishful thinking at this stage: numeric constraints 
are not accounted for in the formalism.} an extension
of this formalism to more expressive constraints, say inequalities. 

\begin{Examplen} [Constrained terms]
The set of  odd numbers can be  
represented by both (1) and (2)
\begin{eqnarray}
& \exists x \forall y : z = s(x) \And z \neq 0 \And z \neq s^{2n}(y) 
\And 0 \leq n\\
& \| s(z) \| - \|0, s^{2n}(y) \mid 0 \leq n\|
\end{eqnarray}
\noindent
or, with the obvious (I mean introducing abbreviations for the 
relative equational formulae)
%\footnote{TO ME: predicates defined as fix 
%point of equational formulae?}  
abuse of notation, define the odd numbers 
which are not prime and not included between say $99$ and $999$.
\begin{eqnarray*}
& \exists \vx \forall \vy : odd(z) \And \neg prime(z) \And \neg 
included(99,z, 999) \\
& \| odd(z) \| - \| prime(z), included(99,z,999) \|
\end{eqnarray*}
\end{Examplen}
\subsubesction{Solving Arbitrary Equational Formulae}

Notwithstanding our interest concerns mainly $\Sigma-2$-formulae$, \ie 
equational problem,and the rules are tailored only for the latter ,
 since $CET$ is decidable,  you may wonder how to solve arbitrary 
 equational formulae. The good old nethod is quantifier elimination, 
 as in \cite{Mah88}, but only up to $\Sigma-2$-formulae$. This makes 
 isd pretty simple. Suppose we have a formula $\cP = 
 \vec{Q}\forall\ldots\exists\ldots P$. Then its set of solutions is 
 equal to the complement of the set of solutions of $not(\cP)$. 
 Iterate this procedure and you get a prenex (or the negation) of an 
 equational problen which can be solved by disunification. Rather 
 than detailing the procedure we show how to solve into $\top$
the $DCA(nat)$. We will pretty informal.
\[
 \forall y. y=0 \Or\exists x. y=s(x) \Lmaps_{\rm prenex} 
 \forall y \exists x: y=0 \Or  y=s(x) \Lmaps_{\rm neg}
  \exists y \forall x: \not y=0 \And  \not y=s(x) \Lmaps^{*}_{E,Clh,Dec} 
  \Bot
  \Lmaps_{\rm neg} \Top
\]


\section{Putting it together}

We show, through some standard examples,  how, given a  
negation-closed horn program\footnote{We call  {\em negation-closed} 
a horn program 
such that it is closed under complementation, \ie it is equivalent to 
one whose complementation  is 
still horn. Non-negation closed programs are treated in 
Section~\ref{local}, when 
dealing with universal quantification},  we synthesize its 
complement: the transformation uses some logical equivalences on 
the completion:
moreover the operational semantics is preserved 
as well, in the sense that the success set of the transformed program 
coincides with the {\em finite} failure set of the source one. This 
equivalence requirement will probably prove on the practical side to 
be too stringent: only programs that can be shown to be decision 
procedures, say through static mode analysis, will be guaranteed to 
have a complement. For the rest, the responsibility will reside on 
the user (see the discussion in the Introduction).

First the simplest example. 

\subsection{Even Example}
Consider our favorite program:

\[
\begin{tt}
\begin{tabular}{l}
even(0).\\
even(s(s(Y))) :- even(Y)
\end{tabular}
\end{tt}
\]

Form the completion of the program {\em comp(even)} and massage it so 
as to derive its complement {\tt odd} as in Figure~ \ref{comp_even}:
\begin{figure}
\label{comp_even}
\[
\begin{array}{l}
\forall x. even(x) \Bimp x = 0 \Or \exists y . x =ss(y) \And even(y)\\
 \quad \lead_{cp}\\
\quad \quad\forall x. \neg even(x) \Bimp \neg ( x = 0 \Or \exists y . 
x =ss(y) \And even(y))\\
\quad \lead_{nnf}\\
\quad\quad \forall x. \neg even(x) \Bimp x \neq 0 \And (\forall y . 
x  
\neq ss(y) \Or \neg even(y))\\
\quad\lead_{lift}\\
\quad\quad\forall x. \neg even(x) \Bimp x \neq 0 \And \forall y . x  
\neq ss(y) \Or (\exists y.  x =ss(y)  \And \neg even(y))\\
\quad\lead_{dnf}\\
\quad\quad\forall x. \neg even(x) \Bimp (x \neq 0 \And \forall y . x  
\neq ss(y)) \Or (x \neq 0 \And \exists y.  x =ss(y)  \And \neg 
even(y))\\
\quad\lead_{disunify(x \neq 0 \And \forall y : x  \neq ss(y))}\\
\quad\quad\forall x. \neg even(x) \Bimp x = s(0) \Or (x \neq 0 \And 
\exists y.  x 
=ss(y)  \And \neg even(y))\\
\quad\lead_{disunify(x \neq 0 \And \exists y : x  = 
ss(y))}\footnote{M3,Cls(T)}\\
\quad\quad\forall x. \neg even(x) \Bimp x = s(0) \Or (\exists y.  x 
=ss(y)  \And \neg even(y))\\

\quad\lead_{prettyp}\\
\end{array}
\]
\[
\begin{tt}
\begin{tabular}{l}
odd(s(0)).\\
odd(s(s(Y))) :- odd(Y).
\end{tabular}
\end{tt}
\]
\caption{{\tt odd} example}
\end{figure}


Clearly most of the label on the $\lead$ rewrite relation are 
self-explanatory. It is nevertheless worthwhile to state specifically 
the {\em 
lift} equivalence in its generality. Recall that $\ym$ are the new 
variables renaming the definiendum, while $\xn$ are now the local 
ones. If $k =0$ then the rewriting is the identity, since the RHS 
converts to false.


\begin{Def} {Lift}
\beq
\lefteqn {\forall \ym (\forall \xn ( \ym \nq \overline{t_m}[\xn] \Or  
\BOr\limits^{k}_{i=1} \neg p_i[\xn])) \Bimp }\\
& & \forall \xn (\ym \nq \overline{t_m}[\xn]) \Or
\BOr\limits^{k}_{i=1} \exists \xn (\ym = \overline{t_m}[\xn] \And 
\neg p_i[\xn])) \ )
\eneq
\end{Def}


\begin{Remark} [Lift correctness]
The {\em lift} equivalence  follows classically from
$E_{\Sigma T}$ (and $E_{\Sigma RT}$). In particular the derivation 
employs congruence and 
decomposition axioms in each sense and classical 
manipulation of connectives and quantifiers\footnote{On the other 
hand, $CET$ is decidable, so why bother. Moreover, and we'll have much 
more to say about that, we can consider Nelson's logic \N as our 
meta-logic, since it allows the aforementioned manipulations without 
losing constructivity}. In particular it does not 
use $DCA$. 
%Question: are atomic extension of CET 
%decidable as well, \ie can we decide lift-like formulae? Atomic?
\end{Remark}

As we said earlier, the linearity condition guarantees that the 
disunification 
process ends in an unification solved form (Definition
\ref{sf}), but it is no 
restriction, as the next example shows. What we may end up with is 
a solved form with constraints, which in this case are 
simply disequations on the (many-sorted) Herbrand universe.

\begin{Examplen} Consider the usual program for membership in 
lists:
\[
\begin{tt}
\begin{tabular}{l}
member(X,X.XS). \\
member(X,Y.YS):- member(X,YS). 
\end{tabular}
\end{tt}
\]

Its completion is
\beq
\forall z, zs ( member(z,zs) & \Bimp  
	& \exists x,xs (zs = x.xs \And z = x) \Or  \mbox{} \\
		& & \exists x,y,ys (zs = y.ys \And z = x \And 
member(x,ys)))
\eneq

Now the transformation: note that we have to choose $zs$ rather 
then $z$ as the 
variable to explode in the same disjunct. In general it is not clear 
whether this choice that happens to be compelled in this 
circumstance by the side conditions of the rule can be supported by 
some kind of experimental heuristics\footnote{This naturally 
leads to a form of nested OR-parallelism, \cite{Kup88}, entailing
pursuing at the same times branches produced by 
explosion, as well as explosion on other variables.}. Remark anyway 
that the implicit type-discipline  considerably reduces 
this search.
The computation is reported in Figure~\ref{fig:member} tacitly 
restricting the solved form to 
contain only the appropriate variables\footnote{This may sweep 
under the rug a serious constraint projection problem, \ie which 
inequalities are to be taken into account for the final format. In 
this 
case they are the one for which linearity does not hold: is that 
heuristics or a satisfactory condition?}.

\begin{figure}[p]
\label{fig:member}
\[\begin{array} {ll} 
comp(member)\\
\lead_{cp}\\
\quad \forall z, zs (\neg member(z,zs) \Bimp 
	& \forall x,xs (zs \neq x.xs \Or z \neq x)  \And  \mbox {}\\
&   \forall x,y,ys (zs \neq y.ys \Or z \neq x \Or \neg member(x,ys))\\
\lead_{lift}\\
\quad \forall z, zs (\neg member(z,zs) \Bimp 
& \forall x,xs(zs \neq x.xs \Or z \neq x) \And \mbox {}\\
 & \forall x,y,ys (zs \neq y.ys \Or z \neq x) \Or \mbox{} \\
& \exists x,y,ys. (zs = y.ys \Or z = x) \And \neg member(x,ys)\\
\lead_{dnf}\\
\quad \forall z, zs (\neg member(z,zs) \Bimp 
& (d1) \ \forall x,y,xs,ys. (zs \neq x.xs \Or 
z \neq x) \And  (zs \neq y.ys \Or z \neq x) \\
& (d2) \ \forall x,xs, (zs \neq x.xs \Or z \neq x) \And \mbox{} \\
 & \exists x,y,ys. (zs = y.ys \And z = x) \And \neg member(x,ys)\\
(d1) \ \Lmap_{E+R(zs=nil)(1.1)}\\
%\quad 
& (d1.1)  \ \forall (nil \neq x.xs \Or 
z \neq x) \And  (nil \neq y.ys \Or z \neq x) \And zs=nil\\
\Lmap_{Cl(T)^*}\\
&  zs=nil \\
\lead_{prettyp} \\
% & \fbox{nonmember(X,nil)} \\
& {\tt nonmember(X,nil)} \\

(d1) \ \Lmap_{E+R(zs=w.ws)(1.2)}\\
& (d1.2) \ \exists w, ws\forall x,y,xs,ys. (w.ws \neq x.xs \Or 
z \neq x) \And  \mbox{}\\
&  (w.ws \neq y.ys \Or z \neq x) \And zs=w.ws\\
\Lmap_{UE2(x,y,xs,ys)}^* \\
% & \fbox{$\bot$} \\
& \fbox{$\exists w (w \nq z)$} \\
\lead_{prettyp} \\
& \la \ra\\
(d2) \lead_{disunify(\forall x,xs (zs \neq x.xs \Or z \neq x))}\\
 % (d2) \lead_{disunify(\exists y,ys . zs = y.ys \And z = x)}\\
\Lmap_{UE2(x,y,xs,ys)}^* \\
 % & z=x \And zs =y.ys \And x \neq y \\
& x \nq y\And \exists y,ys . zs = y.ys \And z = x \\
\Lmap_{norm} \\
 & \exists y,ys (zs = y.ys \And z \nq x)\\
\lead_{prettyp}\\
% &\fbox{$nonmember(X,Y.YS) \leftarrow X \nq Y, nonmember(X,YS)$}. 
 &{\tt nonmember(X,Y.YS) :- X \nq Y, nonmember(X,YS)}. 

\end{array} \]
\caption{Synthesis of the {\tt nonmember} predicate}
\end{figure}
Remark again that since the starting problem was nonlinear, the 
solved form contains a constraint.
\end{Examplen}
\subsubsection{Technicalities}
\label{tech}
There are two points that have to be specified about the interaction 
between disunification and the transformation procedure:
\bit
\item Compare the usage of variables in Example \ref{ex:num} (the 
disunification of $\forall y: z \neq 0 \And z \neq ssy$ to be plugged in into the \texttt{odd} example in 
Figure \ref{comp_even}. It could seem that while in the former 
treatment Explosion was correctly applied to the free variable $z$, in 
the latter Explosion is uncorrectly applied to $x$, which is universally 
quantified from the outside of the completion. Instead from the 
operational reading of logic programs, disunification must be 
considered in isolation: thus $x$ is free and can be soundly exploded
\item
On a similar vein, you may object to the solution of the \texttt{member} 
example in Figure \ref{fig:member} as $zs =nil \Or \exists y,ys (zs = y.ys \And z \nq x)$
as not matching our definition of \emph{solved form with constraints}, 
which does not allow disjunctions of these solved form\footnote{As 
remarked after Definition \ref{sf}, other notion of solved forms allow 
this.}.  Again the operational reading of logic programs comes to our 
rescue, since disjunctive solution yields disjunctive clauses, \ie 
different program clauses.
\enit
 
\subsection{In a Few Words} 

At this point we sum up the procedure: 
Let $p$ be  a $n$-ary predicate and suppose there are $m$
clauses of the form $p(\dots)$ in the underlying program, where the
$i-th$ clause has the following form:
\[
p(t_{i,1}[\vy] \mdots t_{i,n}[\vy]) \leftarrow
B_{i,1}[\vy] \mdots B_{i,k(i)}[\vy]
\]
for each $i$, \ie every clause in the definition, $k(i)$ denotes the 
number of literals therein, while all the variables occurring in the 
definition are taken from the set $\vy$.
Then its completion {\em comp(p)} is
\[
\forall \xn (p(\xn) \Bimp \BOr\limits^m_{i=1}
\exists \vy (\BAnd\limits^n_{j = 1} x_j=t_{i,j}[\vy] \And
\BAnd\limits^{k(i)}_{j=1} B_{i,j}[\vy]))
\]
which can be abbreviated in the definiens formula
\[
\forall \xn (p(\xn) \Bimp D[\vx])
\]

Then the procedure yielding the complement $p^c$ of the predicate 
definition $p$ is obtained thru the following transformation on the 
definiens formula:

\bit
\item 
contraposition (cp)
\item
 conversion into  negation normal form (nnf)
\item
 conversion into  disjunctive normal form (dnf)
\item
call of the disunification algorithm (disunify($\dots$))
\item
 lifting of the RHS: see above.
\end{itemize}


Finally prettypp renames negated atoms into positive ones and 
performs the inverse of the completion formation procedure, somehow 
projecting the constraints nicely. We do not consider it an official 
part of the  main transformation, but as a post-processing phase as 
completion formation is a pre-processing one.

The procedure can be iterated on every procedure which occurs 
negatively in the whole program, as necessary. It is clear that if 
two procedures are negatively mutually recursive, there is not much 
to do but rethinking the program. This is why we always assume local 
stratification \ref{d:strat}\footnote{If we want to play the game of 
completion consistency more deeply, there are slightly weaker 
conditions, see references in \cite{Apt95}.}.

 Following 
\cite{Sat84}, it can be shown that:
\begin{Ppn}[Sato \& Tamaki \ref{ST84}]
$P^c$ is the dual of a negation-closed $P$, \ie $F_P = M_{P^c}$.
\end{Ppn}

For the general case, you may want to try to follow the proof in 
\cite{Bar90}. A different proof can be found in \cite{Mom95}, as Proposition 5.10.

\subsection{Comparison}
\label{comparison}
Note the balance with Barbuti approach: there you start with a 
specific format in the source program called {\em flat}, which 
includes  left-linearization (e) and localization (d); 
this amounts to simplify the logical complexity of the completion 
formula and to permit to use the simpler $Not$ algorithm instead of 
full disunification. 
We here give their version of the process and reexamine some 
examples.
Let us be more specific: a {\em flat} definite program has the 
following format:
\[\begin{array}{llr}
(a) & eq(x,x)\\
(b) & p(\vx) \leftarrow q_1(\vx) \mdots q_n(\vx)\\
(c) & p(\vx) \leftarrow q_1(\vx) ;\dots ; q_n(\vx)\\
(d) &    p(\vx) \leftarrow q(\vx,\vy) \\
(e) & p(\vec{t}) \leftarrow q(\vec{t^*}) & var(\vec{t^*}) \subseteq 
var(\vec{t})
\end{array}\]
\noindent
where $\vec{t}$ is linear.  We gloss over the eight steps 
necessary for the transformation and the heuristics required to keep 
the size of the program manageable. The target program is logically 
equivalent to the source one: the main characteristics of the new 
program are as follows;
\bit 
\item all predicates are defined by a single clause 
%and hence we have no disjunction in the completion
\item
all clauses, but $eq(x,x)$ are linear
\item
if the body contains a local variable it must occur in a single atom 
as in (d)
\item
if a head contains non-variable terms, the body must be a single 
literal under proviso (e)
\item
if a body is a conjunction (disjunction) every element is positive 
and 
have the same variable of the head.
\enit

\begin{Examplen} 
\[
\begin{tt}
\begin{tabular} {lll}
member(Z,ZS) & :- & m1(Z,ZS) ; m2(Z,ZS).\\
m1(X,Y.XS) & :- & eq(X,Y).\\
m2(X,Y.YS) & :- & member(X,YS).\\
eq(X,X).
\end{tabular}
\end{tt}
\]
\end{Examplen}

Note that the {\em member} predicate is almost a best-case 
scenario, since it is already in the (e) format, so its flat version 
results only from left-linearization and folding. We give here the 
flat version of the naive {\em reverse} program to show how little 
of the original format is preserved.

\begin{Examplen}
\[
\begin{tt}
\begin{tabular} {lll} 
rev([],[]).\\
rev(X.XS,R) & :- & rev(XS,Tmp), \\
& & append(Tmp, [X], R).\\
append([], XS,XS).\\
append(X.XS,YS,X.ZS) & :- &  append(XS,YS,ZS).
\end{tabular} 
\end{tt}
\]
Next the flat versions, with the clauses for {\tt rev} annotated with 
the {em flat} condition:
\[
\begin{tt}
\begin{tabular} {llll} 
rev(ZS,YS) & :- & r1(ZS,YS); & (c)\\
& & r2(ZS,YS).\\
r1([],[]). & & & (e)\\
r2(X.XS,R) & :- & rr2(X,XS,R). & (e)\\
rr2(X,XS,R) & :- & rrr2(X,XS,R,Tmp). & (d)\\
rrr2(X,XS,R,Tmp) & :- & r21(X,XS,R,Tmp), & (b)\\
& & r22(X,XS,R,Tmp).\\
r21(X,XS,R,Tmp) & :- &  rev(XS,Tmp). & (e)\\
r21(X,XS,R,Tmp) & :- & append(Tmp,[X],R). & (e)\\
\\
append(X,Y,Z) & :- & append1(X,Y,Z);\\
			&  & append2(X,Y,Z).\\
append([],Y,Z) & :- & eq(Y,Z).\\
append2(X,Y,Z) & :- & append3(X,Y,Z),append4(X,Y,Z).\\
append3(X.Y,Z,V.W) & :- & eq(X,V)\\
append4(X.Y,Z,V.W) & :- & append(Y,Z,W).
\end{tabular} 
\end{tt}
\]
\end{Examplen}

Given the de-structuring due to the flat format, the constructed 
completion is simpler and stepwise built as imagined.

\[\begin{array}{lll}
(a) & \forall x,y .eq(x,y) \Bimp x=y\\
(b) & \forall \vx.p(\vx) \Bimp q_1(\vx) \And\cdots \And q_n(\vx)\\
(c) & \forall \vx.p(\vx) \Bimp q_1(\vx) \Or \cdots \Or q_n(\vx)\\
(d) &   \forall \vx. p(\vx) \Bimp \exists \vy. q(\vx,\vy) \\
(e) & \forall \vy .p(\vec{y}) \Bimp \exists \vx. \vy = \vec{t} \And 
q(\vec{t^*}) \end{array}\]

Then, it is negated  and lifted as 
expected. Using Theorem~\ref{t:bar} universal inequalities stemming 
from (e) are replaced with their solutions given by the $Not$ 
algorithm, yielding:
\[
\forall \vy p^c(\vy) \Bimp \BOr^n_{i=1} \exists \vx (\vy = 
\vec{t^c_i}) \Or . \exists \vx.\vy = \vec{t} \And q^c(\vec{t^*})
\]
\noindent
which eventually leads to $n$ facts $p^c(\vec{t^c_i})$ and a rule 
$p^c(\vt) :-q^c(\vec{t^*})$. To recover some sense in the resulting 
set of clauses, unfolding is used. It is worthwhile to stress again 
that the inequalities are computed `sequentially', \ie independently, 
due to 
the mentioned issue of the `conjunction' of intensional terms and 
that left-linearity is essential for the method to be applicable. 
Second, it is the unfolding which makes `parallel' the term 
complementation.

We do not dare to exemplify the method
on the {\tt rev} predicate, hence, back to the {\tt odd} one: 

\begin{Examplen} 
\[
\begin{tt}
\begin{tabular} {lll}
even(Z) & :-& even1(Z) ; even2(Z).\\
even1(s(0)).\\
even2(s(s(X))) & :-& even(X).
\end{tabular}
\end{tt}
\]

The negated completion is
\[
\begin{array}{lr}
neven(x) \Bimp neven1(x) \And neven2(x) \\
neven1(x) \Bimp \exists z. x = s(z)  & {\em from} \; x\neq 0 \\
neven2(x) \Bimp x=0 \Or x = s(0) \Or \exists z . x= s(s(z)) \And 
neven(z)  & {\em from} \; \forall z. x \neq s(s(z))
\end{array}
\]

Which eventually yield the clauses:
\[
\begin{tt}
\begin{tabular} {lll}
 neven(Z)  & :-&  neven1(Z), \\
		& & 	neven2(Z). \\
 neven1(s(X)). \\
 neven2(0). \\
 neven2(s(0)). \\
 neven2(s(s(X)))  & :-&  	neven(X). 
\end{tabular}
\end{tt}
\]

Only after partial evaluation our good old program reappears. Note 
that it is difficult to attach an operational, as well as 
declarative, 
meaning to the intermediate code.
\end{Examplen}

Unfortunately this is not the end of the story: it remains to deal 
with the transformation of $eq$, which, as it stands, cannot be 
addressed in the given framework. Yet, since 
this 
predicate is non-linear it requires an ad hoc treatment, namely for 
every type\footnote{An untyped approach would be unfeasible.} 
adding the clauses, for every argument position $1\leq i\leq n$:
\[
\begin{array} {lllr}
neq(g(\Xn), f(\Ym)). &  & & \mbox{for distinct $f$ and $g$}\\
neq(g(\Xn),g(\Yn)) & \leftarrow & neq(X_i,Y_i) & \mbox{for}\: i \in 
[1..n]
\end{array}
\]

Moreover, the instantiation to variables in open negative literals in 
what used to be the pre-transformation 
 queries is exactly yielded by the $neq$ predicate. Moreover its 
operational behavior is not satisfactory: consider the goal 
$neq(XS,X.XS)$. While it should succeed without bindings, it loops.
Clearly, the disunification approach allows a symmetric treatment. 
It is not a coincidence that more recent version of intensional 
negation are situated in a constraint framework \cite{Bru93}.
 
Finally the intermediate code for the {\tt member} predicate:
\[
\begin{tt}
\begin{tabular} {lll}
 nonmember(X,XS)  & :-&  nonmember1(X,XS) , nonmember2(X.XS). \\
 nonmember1(X,[]). \\
 nonmember1(X,Y.YS) & :-& neq-el(X,Y).\\
 nonmember2(X,[]). \\
 nonmember2(X,Y.YS)  & :-&  	nonmember(X,YS). \\
neq([],Z.ZS).\\
neq(Z.ZS,[]).\\
neq(X.XS,Y.YS) & :-& neq-el(X,Y),neq(XS,YS).
\end{tabular}
\end{tt}
\]

Again, partial evaluation with suspension (delaying) of $neq$ yields 
the well-known program. The notation `neq-el' alludes to the 
inequality theory induced by the type of the element of the list 
which has to be added.
\subsubsection{Costructive Negation}
\label{cn}
Disunification can provide a rational reconstruction and refinment of 
\emph{constructive negation} \cite{Cha88} \ref{cn-gen}, taking care of the messy 
treatment of inequalities in the former.  The key observation is 
that if $G$ is a goal and we consider the answer substitutions 
$\q_1,..., \q_n$ as an equational problem, $G \Bimp \exists)\q_1 \Or 
\dots \Or q_n$ is a logical consequence of the completed database.  
Therefore the constructive negation rule is simply $\Not G \Bimp \Not 
\forall(\q_1 \Or \dots \Or q_n)$, where the right-hand side can be 
simplified by disunification. For instance given the query $?- 
not(even(X))$, its positive version jields the answer $ 
X=0\Or \exists Y : X= ssY$, whose negation is the well-known 
equational problem $X\nq 0\And forall Y: X \nq ssY$: its solved form 
is hence $X=s(0)$, which we can regard as a more informative 
refinment of the answer constructive negation produces.

\subsubsection{Complementing Functions}

Naish

\section{The Trouble with Local Variables}
\label{local}
This section could also be entitled `What has universal 
quantification to 
do with the negation technique ?'


Answer: even starting with a Horn program, the transformed one
may contain universal quantification in the body, stemming from
local variables. Consider a program for (irreflexive) transitive 
closure of a relation, which keeps also track of the intermediate 
elements in the path construed, 
in the 
version of \cite{Bro90}\footnote{Why, you would ask, complicate 
one's life 
with a third argument: well the clue is: consider the (d) clause in 
flat 
programs.}:

\begin{Examplen}
\label{path}

\[\begin{tt}\begin{tabular} {llll} 
path(X,Y) & \Ift & path3(X,Y,ZS)\\
path3(X,Y,[]) &\Ift & edge(X,Y). \\
path3(X,Y,Z.ZS)& \Ift & edge(X,Z), path3(Z,Y,ZS). \\ 
\\
edge(a,b).\\
edge(b,c).\\
\end{tabular}\end{tt} \]

The complement of the program follows:

\[\begin{tt}
\begin{tabular} {lll} 
nonpath(X,Y) &\Ift &  all ZS. nonpath3(X,Y,ZS). \\
nonpath3(X,Y,[]) & \Ift & nonedge(X,Y).\\
nonpath3(X,Y,Z.ZS) & \Ift & nonedge(X,Z).\\
nonpath3(X,Y,Z.ZS) & \Ift & nonpath3(Z,Y,ZS). \\ 
\\
%nonedge(b,a).\\
%nonedge(a,a).\\
nonedge(a,c).\\
nonedge(b,b).\\
nonedge(X,a).\\
nonedge(c,b).\\
nonedge(c,c). % c,X may coincide with X,a on c,a
\end{tabular}\end{tt} \]
\end{Examplen}


This raises several important questions:
\begin{enumerate}
\item
What is the operational reading of universal quantification
in this setting 
\item
How it mingles with generic judgments (discussed in 
Section~\ref{uquant}) ?
\item
How can this be reflected in the theory of inductive definitions
\cite{Acz77} (discussed in~\ref{ind}) ?
\end{enumerate}
This section is devoted to addressing the first one. We  start 
asking the naive query $\If nonpath(c,c)$, with the intuitive reading 
that indeed it should succeed since the graph is irreflexive.  Thus 
the 
subgoal $\If \forall^e ZS. nonpath3(c,c,ZS)$ should eventually 
succeed.
Nevertheless a naive exhaustive search would loop, since there are 
infinite paths between $c $ and $c$ in the (cyclic) antigraph.

We thus turn to the literature \cite{Man88,Bro90,Har91a}.

\subsection{Logic Programming and Universal Quantification}
\label{uquant}

Similarly to  implication, several attempts
to allow universally quantification in  goals in a 
controlled way were proposed in the mid 80's (see NQ-Prolog
\cite{Gab84}, NI \cite{Gab86}, clausal intuitionistic logic
\cite{McC86})\footnote{The trend is still going on, see Gabbay's 
chapter `Elements of Algorithmic Proof' in \cite{Gab94}.}; They all showed, as far as I am concerned, 
an amazing amount  of technicalities, restrictions,
lack of clear operational semantics and mostly the absence
of a programming language significance, which is the original
sin of all dead languages\footnote{To alleviate this, I have to 
mention that the impetus to develop NQ-Prolog was the attempt
to formalize the British Nationality Act; yet this hardly qualifies
as a development of programming languages feature.}.

A possible source of misunderstanding was perhaps the confusion
between what we now know as the {\em intensional} \cite{Mil91b} 
vs.\ {\em extensional} \cite{Bar90} interpretation of $\forall$, as 
well as the implicit assumption
of the Closed World Assumption (CWA). This is connected with what 
has come to be known as the {\em universal query problem} 
\cite{Apt95,Kun87}, discussed in Chapter~\ref{defs}\footnote{This 
section must be updated: we need to consider also partial predicates 
\cite{Wag91}.}.
%\footnote{Note that we only introduce this distinction for 
%goals.}:

\begin{itemize}
\item
Extensional:\\
$\forall^e x. G$ holds if for all closed terms $t, [t/x]G$ 
holds
\item
Intensional:\\
$\forall^i x. G$ holds if for a new parameter $a, [a/x]G$ holds.
\end{itemize}

We will use the notation $\Pi$ for the latter, for reasons that will 
become apparent in the sequel. This dichotomy  is also characterized 
as the difference between the model and proof-theoretical approach.


There is a not so obvious relation\footnote{To be further discussed} 
with what we intend the domain
of computation to be (recall that in the \lp \, tradition this
is central to define the intended term model).

\begin{itemize}
\item
Closed Domain:\\
the signature is fixed once and for all as the one
underlying the program; this is enforced by the $DCA$, 
the  first-order approximation of the CWA

\item
Open Domain:\\
the signature is taken to be infinite; in operational
terms this means that it is free to expand during execution
 by parameters\footnote{I assume at this point that parameter 
introduction is consistent with $CET$. Everything should boil down to 
adding/dropping the $DCA$. Infinite languages and parameter 
introduction should be orthogonal.}.
\end{itemize}

This has some relevant model-theoretic consequences that
we may not pursue here (see Theorem 1 in \cite{Man88}). At the risk 
of being trivial we instead give the following:

\begin{Examplen}
\label{ex:psx}
Consider the ``program'' $q(a)$; the query $\forall^e x.q(x)$
follows logically from $P \cup DCA$ (in every normal model---this 
will be assumed from now on) and should accordingly succeed;
symmetrically $\Pi x.q(x)$ does not and it fails, as it should. Yet
take the slighter more complicated program:
\[\begin{array} {l}
 p(0)\\
 \forall x. p(s(x))
\end{array} \]
the query $\forall^e x.p(x)$ apparently fails to terminate even
it follows logically from $P \cup DCA$, yet every instance $p(s^n(0))$ 
is provable. The query $\Pi x.q(x)$ still fails.
\end{Examplen}


Before rushing to declaring the intensional approach the obvious 
winner, let me point out the following:
\begin{enumerate}
\item
It does not seem at the Horn level to be a problem of classical versus 
constructive logic; the above derivations exists in the minimal 
predicative calculus with equality\footnote{More precisely with the 
congruence axiom for the mentioned predicates, see the $M1$ rule in 
Section~\ref{disunif}.} and $DCA$.  For finite signatures, it would 
be  a 
showing of  sophisticated taste not to take $DCA$ as a constructive principle.  Infinite 
ones do not arise because they conflict with the Closed Domain 
Assumption.  Even OWA signatures stay finite \wrt terminating 
computations
\item
The issue of choice of domain is strongly linked to (constructive) 
negation: going back to the first example above: a query of the type 
$\If \exists x .  \Not q(x)$ could succeed in the Open Domain with 
answer something like $x \not =b$, for a new parameter $b$.  Yet it is 
not fair to consider constructive negation in the Open Domain as 
something already given\footnote{In CWA the only answer would be 
$x \not =a$ for the only element domain $\{a\}$: to be further 
discussed: the OWA answer interctr with the UQP.} .
\end{enumerate}


There is no contest that intentional quantification has proved to be 
a really novel and useful language feature: Miller has made a 
convincing case for its usage to implement local declarations and 
abstract data types
in $\lambda$Prolog; furthermore the $\Pi$ operator  in Elf is the 
cornerstone of allowing hypothetical and parametrical judgments. 
Nevertheless
it seems that the only reasonable interpretation of universal
quantification originating from local variables is an extensional 
one\footnote{This interpretation may also be useful in a Datalog 
sense \cite{Llo84,Llo86}.}. 
\begin{sloppy}
Coming back
to Example~\ref{path}, you may check that the intensional version
of $\If \Pi ZS. nonpath(X,Y,ZS)$ makes no sense.
\end{sloppy}
Note that we have so far  carefully avoided to discuss an interpreter 
for extensional quantification. This is not a coincidence. Barbuti's 
first solution is eminently operational, cryptic and 
incomplete too. Namely, for a predicate $q$ and its complement $q^c$, 
a query $\If \forall y q^c(x,y)$ succeeds 
whenever:
\begin{enumerate}
\item 
$\If q^c(x,y)$ is computed producing a candidate substitution $\q$
\item 
$\If q(\q x,z)$ fails finitely, for $z$ fresh.
\end{enumerate}
\begin{sloppy}
You may indeed check that the query $\If nonpath(c,c)$ succeeds, $\If 
nonpath(b,X)$ yield answers $X=a, X=b,X=b\ldots$ and $\If nonpath(a,c)$ fails.
\end{sloppy}
The idea seem to use the knowingly mistaken interpretation that \NF 
gives to quantifier in non-ground queries (see Introduction~\ref{}) 
to 
achieve the result. The source of incompleteness can be localized to 
the interaction between local variables and conjunction, namely the 
candidate substitution may be too general to yield the desired finite 
failure (see example at pp.\ 213--214 in \cite{Bar90}).  Indeed the 
procedure has to be further factorized as follows:
\bit
\item
If $\If q(\q x,z)$ has only finite failure derivations, then succeed
\item
otherwise further instantiate $\q x$ and go to the previous step.
\enit

This instantiation is achieved by a procedure  {\tt herbrand} which
enumerates the term model. Of course, when dealing with an infinite 
universe, the procedure always diverges, as admitted by the authors 
(pp.\ 226). Hence:
\begin{quote}
``\dots It is meaningless to talk about the finite failure of {\em 
SLDN}''
\end{quote}

Indeed, a clever usage of the $DCA$ may alleviate this problem as 
explained in \cite{Mom95} and reported in Section~\ref{mdca}.

Nevertheless,  we thus agree  w.r.t.\ regarding the overall 
unfeasibility of this approach, as unable to 
grant completeness. Therefore we
abandon this problematic generate-and-test
approach and turn to the refinement of  extensionality that goes 
under the name of {\em proof by case analysis}, shortened in 
$CASE$ \cite{Man88,Bro90}
(and somehow also  \cite{Har91a}), which is naturally suggested by 
the second program quoted in Example~\ref{ex:psx}.

\smallskip
$CASE$ is based on two pillars: the idea of   {\em term covering} 
\cite{Man88}, i.e.\ an intensional finite representation of all the 
ground instances of a term, and on the operational reading of an 
opportune instance of (an equivalent of) the $DCA$.

To give the idea away, the point is to prove a positive universal 
statement by proving a {\em finite} set of its instances which 
nevertheless constitute a {\em covering} of the original one.

We will next quote the model-theoretic results which support this new 
kind of rule. We will also mention the stronger completeness result 
that can be achieved for \SLD \ and \NF.
We stress again that the reference theory we are using is the 
completion of the program plus $CET$ enriched of the $DCA$. Moreover
the latter can be shown to be  a conservative extension of Clark's 
completion w.r.t.\ 
universal positive queries.
