\chapter{Elimination of Negation in Clauses}
\label{ch:hornelim}

The transformational approach to negation in normal programs has a
somewhat long history, see \cite{Naish86} for a survey of the early
80's.  The idea was to implement negation using inequalities, so that
the complement of any predicate occurring negatively in a
program  is synthesized  to obtain an equivalent definite
program.  This was first proposed in \cite{Sato84}.

\section{The Completion}
\label{sec:what}
At the risk of being trivial, let us start by asking naively what the
complement of a program should be; if we see the latter as a
set of (possibly mutually recursive) predicate definitions, its
negation would be the set of the negation of those
definitions. Thus, let us concentrate on a program definition as our
target and consider the simplest case, \ie that of a single clause
$q(0)$ on the signature of numerals. Our first instinct would be to
use the \mnot\ algorithm and by computing $\mnot(0)= s(X)$ assert
$\PI{X}{nat}\neg q(s(X))$; this is indeed the right thing to do, but
we need to justify it formally. We can look at the definition $q(0)$
as a degenerate case (that is with trivial condition) of
\emph{inductive} definition; an equivalent formulation would be:
$$\PI{X}{nat} q(X)\If X\eqd 0.$$
for an object-logic equality symbol `$\eqd$', which simply expresses
the condition 
$X\eqd 0$ for atoms to be in the inductive definition of $q$. The next
step is to enforce the minimality condition by saying that the latter
is the only way to belong to the definition. One way to achieve that
is by exchanging the $\If$ connective into a biconditional $\BImp$:
$$\PI{X}{nat} q(X)\BImp X\eqd 0.$$
This is in a nutshell Clark's very
fortunate idea of the \emph{completion} of a program \cite{Cla78}.
What is left is describing how to interpret the equality relation;
this is accomplished by the so-called Clark's equality theory, that is
the axioms of free equality: namely, the usual equality axioms including 
congruence, plus the axioms for finite trees. Indeed, this theory is the 
axiomatic and proof-theoretic rendering of the unification algorithm,
for a proof see for example St\"{a}rk's thesis
\cite{Staerk92}. For instance, the following is free equality over numerals:
\[
\begin{array}{rllr}
%(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}
 \]
The last axiom is the Domain Closure Axiom \cite{Mancarella88}, which
is required to give a complete axiomatization of finite trees over
\emph{finite} signatures.
Since we will not consider unification so far, we will keep 
this relation uninterpreted; thus those axioms do not play any role,
which is handy, as it allows us to dispense with the issue of the
compatibility of DCA with  dynamic extensions on the signature.

\smallskip Of course, definitions are usually more interesting than a
simple clause, so let's step to next simplest example, even numbers:
\[
\begin{array}{l}
even(0).\\
even(s(s(Y))) \If even(Y).
\end{array}
\]
To turn this code into a minimal inductive definition, we need to
normalize the conjunction of clauses, a process described for
example in \cite{Apt94}. The net result is the axiom:
$$\forall x. even(x) \Bimp x = 0 \Or \exists y . x =ss(y) \And
even(y)$$

One way to obtain the complement definition, that is {\tt odd}, would
be to reason classically on the completed program by taking the
contrapositive of the completion. Let me offer the following rational
reconstruction. We may  use rewrite rules to achieve conversion
into negation normal form (nnf) and  into disjunctive normal
form (dnf), plus some more massage to preserve the original positive
bindings in clauses. Once this is done, we need a way to solve the
possibly universally quantified dis-equalities we have created.  A call
of the disunification algorithm described in Section \ref{sec:disunif}
(\texttt{disunify}($\dots$)) is enough to obtain a solved form, from
which we can recover the intended negated program. This is best
explained in Figure~\ref{fig:comp_even}, which uses the subcomputation of
$\forall y:z \neq 0 \And z \neq s(s(y))$, detailed in
Example~\ref{ex:num}.

\begin{figure}
\[
\begin{array}{l}
\forall x\, . \, even(x) \Bimp x = 0 \Or \exists y \, . \, x =s(s(y)) \And even(y)\\
 \quad \lead_{cp}\\
\quad \quad\forall x\, . \, \neg even(x) \Bimp \neg ( x = 0 \Or \exists y \, . \, 
x =s(s(y)) \And even(y))\\
\quad \lead_{nnf}\\
\quad\quad \forall x\, . \, \neg even(x) \Bimp x \neq 0 \And (\forall y \, . \, 
x  \neq s(s(y)) \Or \neg even(y))\\
\quad\lead_{lift}\\
\quad\quad\forall x\, . \, \neg even(x) \Bimp x \neq 0 \And 
\forall y \, . \, x  
\neq s(s(y)) \Or (\exists y\, . \,  x =s(s(y))  \And \neg even(y))\\
\quad\lead_{dnf}\\
\quad\quad\forall x\, . \, \neg even(x) \Bimp (x \neq 0 \And \forall y \, . \, x  
\neq s(s(y))) \Or (x \neq 0 \And \exists y\, . \,  x =s(s(y))  \And \neg 
even(y))\\
\quad\lead_{disunify(x \neq 0 \And \forall y : x  \neq s(s(y)))}\\
\quad\quad\forall x\, . \, \neg even(x) \Bimp x = s(0) \Or (x \neq 0 \And 
\exists y\, . \,  x 
=s(s(y))  \And \neg even(y))\\
\quad\lead_{disunify(x \neq 0 \And \exists y : x  = 
s(s(y)))}\\
%\footnote{M3,Cls(T)}\\
\quad\quad\forall x\, . \, \neg even(x) \Bimp x = s(0) \Or (\exists y\, . \,  x 
=s(s(y))  \And \neg even(y))\\
\quad\lead_{prettyp}\\
\end{array}
\]
\[
\begin{array}{l}
odd(s(0)).\\
odd(s(s(Y))) \If odd(Y).
\end{array}
\]
\caption{Synthesis of the predicate {\tt odd} }
\label{fig:comp_even}
\end{figure}

% \smallskip
% This was pretty much suggested in the early 80's by Sato \& Tamaki in
% \cite{Sato84}. In this seminal paper they isolate what is essentially
% still the right framework: locally stratified many-sorted programs,
% with no local variables.  The authors informally showed that the
% finite failure set of such a coincides with the success set of the
% transformed program. They did not offer an explicit mechanism to
% handle inequalities, but relied on the intuitive semantics of
% `non-unifiable', thus incurring in the fallacy of allowing
% non-left linear clauses.  This was fixed in \cite{Lassez87}, as we
% have seen, in the general context of explicit representation of
% generalization and refined in \cite{Lassez91}; there it is shown that
% such an algorithm may simplify those constraints into a solved form,
% but also that this elimination is not achievable in general.

Following this drift, an extensive project started in Pisa under
the name of \emph{intensional negation}
\cite{Barbuti87,Mancarella88,Bar90,Brogi90,Mancarella90,Bruscoli93}.
In particular \cite{Bar90} computes the set-theoretic complement of
the terms in the negative predicate compiling away the inequalities.
The authors restrict to a class of left-linear non-stratified program
called \emph{flat}, where all predicates are defined by a single
clause (and hence we have no disjunction in the completion) and such
that if a head contains non-variable terms, the body must be a single
literal. With some painful source-to-source transformations, programs
can be turned in and out of this format. Thanks to this, the
transformation of the completion delineated above yields only
disequation of the form $x\neq t$, which the \mnot\ algorithm can
solve.

If we discard for the moment the problematic issue of local variables,
\ie variables that appear in the body but not in the head of a clause
(as they turn out to become universally quantified in an extensional
sense during the completion transformation), this seems at first sight
fairly convincing. On the other hand, managing control of
disunification and rewrite rules requires some ingenuity as the
following example shows:

\begin{Example} Consider the usual program for membership in 
lists:
\[
\begin{array}{l}
member(X,X.XS). \\
member(X,Y.YS)\If member(X,YS). 
\end{array}
\]
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

The synthesis of its negation is depicted in Figure~\ref{fig:member}.
Not only disunification is more complex, as there are a few choices of
variables where the Explosion rule can be applied, but propositional
transformations are difficult to direct as well.
\end{Example}
\begin{figure}[p]
\[\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)$}. 
 &{ nonmember(X,Y.YS)\If  X \nq Y, nonmember(X,YS)}. 
\end{array} \]
\caption{Synthesis of the {\tt nonmember} predicate}
\label{fig:member}
\end{figure}

Working with flat programs is not a real alternative, since some form
of partial evaluation is needed to recover some structure in the
target program. In fact, the more mature version presented in
\cite{Bruscoli93} embraces the constraint \lp approach. We will
instead give a completely deterministic algorithm to compute the
negation of programs. This is based on solving the relative complement
problem by pairing term complement with unification and is proven
correct by Corollary \ref{co:boolean}; that is, we do not need full
disunification as we can solve, for example $x \neq 0 \And \forall y :
x \neq s(s(y))$ by computing $\mnot(0)\cap\mnot(s(s(Y))$.

There is one further, more basic difficulty with the
completion-based approaches; they use transformations that are
intrinsically classical and turn out to  preserve the operational semantics,
only because in Horn logic classical and intuitionistic provability
coincide.  We discuss this issue further in Section \ref{sec:completion}.
We will instead lift the boolean operations we have introduced on
(simple) terms to clauses (programs) and we shall prove that they still satisfies
the usual boolean rules; in particular we will verify that clause
complementation fulfills exclusivity and exhaustivity. This
high-level `boolean' language will eventually be compiled into a
version of HHF 
%augmented with Herbrand constraints 
that is amenable of
a complete uniform proof search strategy. We offer an informal
discussion next (Section \ref{sec:intro5}).

% There have been several partial solutions to the above problem: 
% \cite{Sato84} proposes to use a more general fold/unfold transformation 
% system.  In \cite{Bar90} instead it is proposed to compute the 
% set-theoretic complement of the terms in the negative predicate 
% compiling away the inequalities. Later, \cite{Bruscoli94}, a CLP
% approach is adopted, where universally quantified  (dis)equations are
% created and later hopefully solved by the constraint solving
% module. If we stick to the pure Herbrand universe the rules for
% \emph{disunification}, \cite{Comon91}, in particular
% those dealing to universal quantification elimination can be
% adopted. This may pose serious questions of control as discussed in
% Section \ref{sec:related}.





% \subsection{Comparison}
% \label{comparison}
% The original 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 
% \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  the 
% flat version of the usual $7$-literals naive {\em reverse} program
% explodes in a $27$ literals program

% 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}:
% 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))$,
%  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^*})
% \]
% 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.

% \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}{lcrr}
% neven(x) &\Bimp &neven1(x) \And neven2(x) \\
% neven1(x)& \Bimp &\exists z. x = s(z)  & \mbox{ from} \; x\neq 0 \\
% neven2(x)& \Bimp x=0 &\Or x = s(0) \Or\\
%  & & \exists z . x= s(s(z)) \And 
% neven(z)  & \mbox{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}
% \]
% \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 infeasible.} 
% 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.
















