\section{Refinements}
\label{sec:ref}
\renewcommand{\q}{\theta}
\renewcommand{\s}{\sigma}

In the following sections we will move towards an operational
semantics for our language.


% \subsection{The Algebra of Clause Complementation}
% \label{ssec:ccalgebra}

% Similarly to what we did for term complementation, we show that we can
% organize  programs in a boolean algebra under $\la
% \And,\tensor,\mnotd,\top,\perp\ra$, generalizing the approach in \cite{MP90}.
% \bmeta fill in \emeta

\subsection{More on Termination}
\label{ssec:ccterm}

We prove that clause complementation preserve
termination, so that a negative program can be used as a decision
procedure if so is its positive counterpart. First some
preliminaries:
% call $[R]$ the stable and transitive closure of the
%subgoal ordering defined in Figure \ref{fig:termgraph}. 
define
$\mnot(R)$ as follows:
\beq
\mnot(\cdot) & = & \cdot\\
\mnot(R,G_1\less G_2) & = & \mnot(R),\mnotg(G_1)\less\mnotg(G_2)
\eneq
Observe that, by the restriction to clauses of the form $\Pi(Q\If G)$, it
is sufficient to consider only well-ordering on goals. It is clear that
negation is preserved under relation union, that is:
\beq
\mnot(R_1,R_2) & = & \mnot(R_1),\mnot(R_2)
\eneq
We will also need the following technical Lemma, stating that goal
complementation commutes with substitution:

\begin{Lemma}
\label{le:notgtheta}
Let $\GG\vd\q \hastype\Phi$. $\GG\vd_{\Phi}\mnotg([\q] G) =
\GG\vd_{\Phi}[\q] \mnotg(G)$.
\end{Lemma}
\begin{proof}
  By a simple induction on the structure of the derivation of
  $\GG\vd_{\Phi}\mnotg(G)$.
\end{proof}

\newcommand{\qq}{[\theta]}
%Next we show that
\begin{Lemma}
\label{le:notwf}
If $[R]$ is well-founded, so is $[\mnot(R)]$.
\end{Lemma}
\begin{proof}
  Suppose $[\mnot(R])$ is not well-founded. Then there is an infinite
  descending chain $\dots\less\qq G_i\less\dots\less\qq G_2\less\qq
  G_1$. By definition of $\mnot(R)$ there is  $G'_i$ such that
  $\mnotg(G'_i)=G_i$ and that $G'_i\less G'_{i-1}\in R$ for some
  $i\in\omega$. Since by Lemma \ref{le:notgtheta} $\mnotg([\q] G_i) =
  [\q] \mnotg(G_i)$, then $[R]$ allows an infinite descending chain
  $\dots\less\qq G'_i\less\dots\less\qq G'_2\less\qq G'_1$,
  impossible.
\end{proof}

\renewcommand{\glob}{[\rho]}
The final piece is to show that the relation induced by the complement
of a program is the complement of the relation induced by the program
itself.
\begin{Lemma}
\label{le:ccterm}
\mbox{}
\ben
\item If $\pi::\GG\vd D\yd R$ then $\mnotd(D)\yd\mnot(R)$.
\item If $\alpha::\GG\vd D\yd R$ then $\GG\vd\mnota(D)\yd\mnot(R)$.
\item If $\gamma::\GG\vd G\yg R$ then $\GG\vd\mnotg(G)\yg\mnot(R)$.
\enen
\end{Lemma}
\begin{proof}
By induction on the structure of the given derivations. We prove some
selected cases:
\bit
\itc $\pi::\top\yd \cdot$; $\mnotd(\top)=\perp\yd\cdot=\mnot(\cdot)$.
\itc $\pi$ ends in $\Pi(q\ \vM\If G)\yd R,\glob G\less\glob q\ \vM$, for a global substitution $\rho$:
\btab
$\cdot\vd \glob G\yg R$\bs
$\cdot\vd\mnotg(\glob G)\yg\mnot(R)$\bi $2$\\
$ \Pi(\neg q\ \vM\If\mnotg(
G))\yd\mnot(R),\mnot( G)\less  \neg q\ \vM$\br $\yd\Imp$\\
$\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg q\ \vN)\yd \cdot$\br $\yd\And$\\
$\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg q\ \vN) \And  \Pi(\neg q\ \vM\If\mnotg(
G))\yd\mnot(R),\mnot( G)\less  \neg q\ \vM$\br  $\yd\And$\\
$\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)) \And  \Pi(\neg q\ \vM\If\mnotg(
G))\yd\mnot(R),\mnot( G)\less  \mnotg(  q\ \vM)$\` By
rule $\mnotg\atm$\\
$\mnotd( \Pi(q\ \vM\If G)) \yd\mnot(R, G\less  \neg q\ \vM)$\` By
def.\ of $\mnot(R)$
\etab
\itc $\gamma::Q\yg \cdot$; $\mnotd(Q)=\neg Q\yd\cdot=\mnot(\cdot)$.
\itc $\gamma$ ends in $\GG\vd G_1\And G_2\yg R_1, R_2,G_1\less G_1\And G_2,G_2\less G_1\And G_2$:
\btab
$\GG\vd G_1 \yg R_1$ and $\GG\vd G_2\yg R_2$\bs
$\GG\vd \mnotg(G_1) \yg \mnot(R_1)$ and $\GG\vd \mnotg(G_2)\yg \mnotg(R_2)$\bi
$2$\\
$\GG\vd \mnot(G_1)\Or \mnotg(G_2)\yg \mnot( R_1), \mnot(R_2)$,\\
$\qquad\mnotg(G_1)\less \mnotg(G_1)\Or
\mnotg(G_2),\mnotg(G_2)\less \mnotg(G_1)\Or \mnotg(G_2)$\br\\
$\GG\vd\mnot(G_1\And G_2)\yg \mnot( R_1), \mnot(R_2),$\\
$\qquad\mnotg(G_1)\less \mnotg(G_1\And
G_2),\mnotg(G_2)\less \mnot(G_1\And G_2)$\br\\
$\GG\vd\mnot(G_1\And G_2)\yg \mnot( R_1, R_2,G_1\less G_1\And
G_2,G_2\less G_1\And G_2)$\` By union and def.\ of $\mnot(R)$
\etab
\enit
\end{proof}

\begin{Corollary}
  If $\cP$ is terminating, so is $\mnotd(\cP)$.
\end{Corollary}
\begin{proof}
  By definition, $\cP\da$  if $\cP\yd R$ and $[R]$ is
  well-founded: by Lemma \ref{le:ccterm} $\mnotd(\cP)\yd\mnot(R)$ and
  by Lemma \ref{le:notwf} $[\mnot(R)]$ is well-founded. Thus
  $\mnotd(\cP)\da$ .
\end{proof}


\subsection{Elimination of $\tensor$}
\renewcommand{\vN}{\vec{N}}
\label{ssec:tensor}

We now show how to eliminate the $\tensor$ operator preserving 
provability; this will recover uniformity in proof-search.  
We generalize the approach in 
\cite{Bar90}, where the operation was defined as follows:
for $m_1: Q_{1}\If G_{1}$ and  $m_2: Q_{2}\If G_{2}$:
\beq
m_1 \tensor m_2 & = &  \q(Q_{1}\If G_1\And G_2) \quad\mbox{{\rm where }} 
\q = mgu(Q_{1},Q_{2}) 
\eneq
As we remarked earlier, the $\tensor$ operator was introduced to
preserve the duality under negation between conjunction and
disjunction in clauses.  Its use, as a clause constructor, is limited
to clauses in the same predicate definition and therefore it can be
eliminated simulating unification in the definition.  Yet, the strict
\ho unification problem is quite complex and potentially even more so
complicated by the mixed quantifier structure of HHF, though this is
not the case for our language, which does not have existentials.
Moreover, we have already in our language
% parameter (dis)equations
%introduced by the augmentation procedure, as well as
variable-variable (dis)equations stemming from left-linearization and
normalization of input variables.  Finally, we have defined
unification of simple terms in Section~\ref{sec:sunif} as an
intersection operation. This has greatly simplified the presentation,
but does not immediately give us a notion of most general unifiers
seen as sets of substitutions. We thus choose to compile our source
into an intermediate language which makes unification problems
explicit as simple equational problems in the style of the unification
logic introduced in \cite{Pfenning91lf}.  We can perform unification
as constraint simplification as used in \emph{Elf}
\cite{Pfenning89lics} and \emph{Twelf} \cite{Schurmann98cade} in a
later stage that we do not describe here.

% \newcommand{\eprv}{\stackrel{\prv}{\sim}}
% \newcommand{\enprv}{\stackrel{\nprv}{\sim}}
% \smallskip

% We introduce a notion of \emph{operational equivalence} \wrt 
% provability.

% \begin{Definition}[Operational Equivalence]
% \label{def:opeq}
% We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent \wrt 
% provability}, denoted $\cP_{1}\eprv \cP_{2}$, iff, for any goal $G$ we 
% have $\ga\prv_{\cP_{1}} G$ iff $\ga\prv_{\cP_{2}} G$.

% \end{Definition}

We adapt the \emph{residuation} technique used in \cite{Pfenning94un}
to compile immediate implication into resolution.  We define the
judgment $D_{1}\tensor D_{2} \setminus D$ in Figure \ref{fig:otimes}
by simultaneous induction on  $D_{1}$ and $D_2$, with the intended meaning of
`$D_{1}\tensor D_{2}$ compiles to $D$'. %As usual, we implicitly add the 
%symmetric rules %to $\tensor\top,\tensor\Pi,\tensor\And$.  Note that
%residuation is undefined for clauses with different heads; yet we
%could make the judgment total by agreeing to compile them to $\top$.

% \begin{Lemma}
% \label{le:imm-eq}
% The following are valid rules of inference:
% $$\ianc{\ga\sp q\ \vN_{1}\imm Q\quad \vN_{1}\eqd \vN_{2}}{\ga\sp q\ \vN_{2}\imm Q}{\imm\eqd}
% \qquad
% \ianc{\gna\fp q\ \vN_{1}\nimm Q\quad \vN_{1}\neqd \vN_{2}}{\ga\fp q\ \vN_{2}\nimm Q}{\imm\neqd}
% $$
% \end{Lemma}
% \begin{proof}
% It will be trivial once we specify the equality rules.
% \end{proof}


\begin{figure}
\[
\begin{array}{c}
\ianc{}{\top\tensor D \setminus \top}{\tensor\top D}\qquad
\ianc{}{D\tensor\top \setminus \top}{\tensor D \top }\vsk
\ianc{}{\perp\tensor D \setminus D}{\tensor\perp D}\qquad
\ianc{}{D\tensor\perp \setminus D}{\tensor D \perp }
\vsk
\ianc{}{\Pi(q\ \vN_{1}\If G_{1})\tensor  \Pi(q\ \vN_{2}\If G_{2}) \setminus
\Pi(q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And G_{2})}{\tensor{\rm 
At}\atm}\vsk
\ianc{q\not\equiv q'}{\Pi(q\ \vN_{1}\If G_{1})\tensor  \Pi(q'\
  \vN_{2}\If G_{2}) \setminus\top}{\tensor{\rm At}\atm\not\equiv}\vsk 
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\tensor D'_{1})\tensor D_{2}\setminus D\tensor
  D'}{\tensor\tensor L}
\qquad
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{(D_{1}\And D'_{1})\tensor D_{2}\setminus D\And D'}{\tensor\And L}
\vsk
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{D_2\tensor (D_{1}\tensor D'_{1})\setminus D\tensor
  D'}{\tensor\tensor R}
\qquad
\ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D_{2}\setminus D'}
{D_2\tensor (D_{1}\And D'_{1})\setminus D\And D'}{\tensor\And R}
\end{array}
\]
\caption{$\tensor$-Elimination: $D_{1}\tensor D_{2}\setminus D$}
\label{fig:otimes}
\end{figure}

% \ibnc{\Pi(q\ \vN\If G)\tensor D_{1}\setminus D}{\Pi(q\ \vN\If
%   G)\tensor D_{2}\setminus D'} 
% {\Pi(q\ \vN\If G)\tensor (D_{1}\tensor D_{2})\setminus D\tensor
%   D'}{\tensor\atm\tensor}
% \vsk
% \ibnc{\Pi(q\ \vN\If G)\tensor D_{1}\setminus D}{\Pi(q\ \vN\If
%   G)\tensor D_{2}\setminus D'} 
% {\Pi(q\ \vN\If G)\tensor (D_{1}\And D_{2})\setminus D\And
%   D'}{\tensor\atm\And}
% \vsk

%  \ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D'_{2}\setminus D'}
%  {(D_{1}\And D'_{1})\tensor (D_{2}\tensor D'_2)\setminus D\tensor D'}{\tensor\And\Or}
% \vsk
%  \ibnc{D_{1}\tensor D_{2}\setminus D}{ D'_{1}\tensor D'_{2}\setminus D'}
%  {(D_{1}\tensor D'_{1})\tensor (D_{2}\tensor D'_2)\setminus D\tensor D'}{\tensor\And\Or}

%\input{ot}
% \begin{figure}
% \[
% \begin{array}{c}
% \ianc{}{\top\tensor D \setminus \top}{\tensor\top}
% \vsk
% \ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
% q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And G_{2}}{\tensor{\rm 
% atm}}\vsk
% \qquad
% \ianc{([u/x] D_{1})\tensor D_{2}\setminus[u/x]D}{(\PIXA D_{1})\tensor 
% D_{2}\setminus \PIXA  D}{\tensor\Pi}\vsk
% \ianc{D_{1}\tensor D_{2}\setminus D\quad D'_{1}\tensor D_{2}\setminus D'}
% {(D_{1}\And D'_{1})\tensor D_{2}\setminus D\And D'}{\tensor\And}
% \end{array}
% \]
% \caption{$\tensor$-Elimination: $D_{1}\tensor D_{2}\setminus D$}
% \label{fig:otimes}
% \end{figure}

\begin{Example}
\label{ex:closedatensor}
Continuing Example \ref{ex:closed},
recall that:
\beq
\lefteqn{\mnotd(cloz)=}\\
& & \PI{F}{exp}\neg closed\ (lam\ F)\And (\PI{F_1,F_2}{exp}
\neg closed\ (app\ F_{1} \ F_{2})).\\
\lefteqn{\mnotd(clolam)=}\\
&& \neg closed\ z\And  \PI{F_1,F_2}{exp}\neg closed\
               (app\ F_{1} \ F_{2})\And  \\ 
&& \PI{E}{exp} \neg closed\ (lam\ E) \If \PI {x } {exp}\ (closed\ x \Imp \neg closed\ 
 (E\ x)).
\eneq
Removing trivially unsatisfiable clauses, the computation of  $\mnotd (cloz) \tensor \mnotd (clolam)\setminus D$ results in:
\[\begin{array}{l}
% \PI{F}{exp}\neg closed\ (lam\ F)\If (lam\ F)\eqd z\And\mbox{}\\
% \PI{F,F_1,F_2}{exp}\neg closed\ (lam\ F)\If (lam\ F)\eqd (app\ F_1\
% F_2)\And\mbox{}\\
\PI{E}{exp}\neg closed\ (lam\ E) \If (\PI {x } {exp}\ closed\ x \Imp
 \neg closed\ (E\ x))\And\mbox{}\\
% \PI{F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2})\If (app\ F_{1} \
% F_{2})\eqd z\And\mbox{}\\
% \PI{F,F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2})\If (app\ F_{1} \
% F_{2})\eqd (lam\ F)\And\mbox{}\\
 \PI{F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2}).
\end{array}\]
%Note that only the third and last clause are satisfiable.
Going back to the \texttt{linx} example:
\beq
\lefteqn{ \mnotd(linxx)\tensor\mnotd(linxap1)=}\\
  && (\neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\And \neg linx(\lx lam( \ly (E\ x\
y))))\tensor\mbox{}\\ 
  && (\neg linx(\lx x)\And  \neg linx(\lx lam( \ly (E\ x\ y)))\And\neg
  linx(\lx app\ (E_1\ x) \ (E_2\ x^1) )\\ 
&& \mbox{}\And\neg linx(\lx app\ (E_1\ x) \ (E_2\ x^0) )\If\neg linx(\lx
E_1\ x))
\eneq
$\mnotd(linxx)\tensor\mnotd(linxap1)\sla D$, where
\beq 
 \lefteqn{D=}\\
&& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^1)) \And\mbox{}\\ 
&&
\neg linx(\lx app\ (E_1\ x) \ (E_2\ x^0))\If  \neg linx(\lx E_1\ x)
\And\mbox{}
\\ && \neg linx(\lx lam(\ly E\ x\ y)).
\eneq
\end{Example}

\smallskip
The following lemma guarantees that compilation preserves run-time immediate 
entailment:

\begin{Lemma}
\label{le:te-tim}
Let $ D_{1}\tensor D_{2}\setminus D$: for every ground substitution
$\GG\vd\theta\hastype \Phi$,  $\ga\vd [\q](D_1\tensor D_{2})
\imm Q$ iff $\ga\vd [\q]D\imm Q$.
\end{Lemma}
\begin{proof}
($\Imp$). By induction on the structure of $\pi:: D_{1}\tensor
D_{2}\setminus D$. 
\bit
\itc $\pi$ ends in $\tensor\top D,\tensor\atm\atm\not\equiv$: trivially true.
\itc $\pi$ ends in $ \tensor\perp D,\tensor\atm\perp$: immediate.
\itc
$$\pi=\ianc{}{\Pi(q\ \vN_{1}\If G_{1})\tensor  \Pi(q\ \vN_{2}\If
  G_{2}) \setminus 
\Pi(q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And G_{2})}{\tensor{\rm 
atm}}$$
\btab
$\ga\sp[\q] (\Pi(q\ \vN_{1}\If G_{1})\tensor \Pi(q\ \vN_{2}\If G_{2}))\imm q\ \vN$\bh
$\ga\sp [\q](\Pi(q\ \vN_{1}\If 
G_{1}))\imm q\ \vN$ and $[\q]( \Pi(q\ \vN_{2}\If G_{2}))\imm q\ \vN$\bv
$\ga\sp[\q\cdot \s_1]\vN_1\eqd \vN$ and $\ga\sp[\q\cdot \s_1] G_1$\bv
 $\ga\sp[\q\cdot\s_2]\vN_2\eqd\vN$ and $\ga\sp[\q\cdot\s_2] G_2$\bv
$\ga\sp [\q\cdot\s_1]\vN_1\eqd[\q\cdot\s_2]\vN_2$\`By replacement\\
$\ga\sp[\q\cdot\s_1\cdot\s_2] \vN_1\eqd[\q\cdot\s_1\cdot\s_2]\vN_2\And
[\q\cdot\s_1\cdot\s_2] G_1\And 
[\q\cdot\s_1\cdot\s_2] G_2$\\ \`By composition of ground substitution\\
 $\ga\sp [\q](\Pi(q\ \vN_{1}\If (\vN_{1}\eqd \vN_{2}) \And G_{1}\And 
G_{2}))\imm q\ \vN$\br
\etab
\itc $\pi$ ends in $\tensor\atm\And,\tensor\atm\tensor,\tensor\And,\tensor\tensor$: by an immediate
appeal to the IH.
% Case: 
% $$\ianc{([t/x] D_{1})\tensor D_{2}\setminus [t/x]D}{(\PIXA D_{1})\tensor 
% D_{2}\setminus \PIXA  D}\tensor\Pi}$$
% By inversion $([t/x] D_{1})\tensor D_{2} \setminus[t/x]D$ and $\ga\sp 
% [t/x]D\imm Q$ which is equivalent by IH to $\ga\sp [t/x]D_{1}\tensor 
% D_{2}\imm Q$ iff $\ga\sp [t/x]D_{1}\imm Q$ and $\ga\sp D_{2}\imm Q$ 
% iff $\ga\sp (\PIXA D_{1})\tensor D_{2}\imm Q$.
\enit
($\If$): similarly.
\end{proof}
We remark that, using again terminating programs, the above Lemma
covers immediate denial as well.
% The following guarantees that compilation preserves 
% Note that we have to take into account the meta-level universal 
% quantification on terms brought in by the $I^{\nprv}_{\Pi}$ rule.

% \begin{Lemma}
% \label{le:te-nimm}
% For all $\q, \ \q D_{1}\tensor D_{2}\setminus D$ and $\q D\nimm Q$ iff 
% $\q D_{1}\tensor D_{2} \nimm Q$.  
% \end{Lemma}
% \begin{proof}
% By induction on $D_{1}$.  We avoid mentioning substitutions when they 
% are immaterial and show only some significant cases in the $\Imp$ 
% direction, the converse following the same lines.
% \bit
% \item
% Case:
% $$\ianc{}{\top\tensor D \setminus \top}\tensor\top}$$
% $\ga\sp\top\nimm Q$ obviously entails   $\ga\sp\top\tensor D\nimm Q$.
% \item
% Case:
% $$\ianc{}{(q\ \vN_{1}\If G_{1})\tensor  (q\ \vN_{2}\If G_{2}) \setminus
% q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}}\tensor{\rm 
% atm}}$$
% Assume $\ga\fp q\ \vN_{1}\If \vN_{1}\eqd \vN_{2} \And G_{1}\And 
% G_{2}\nimm Q$.  Then either $\ga\fp q\ \vN_{1}\nimm Q$ or $\ga\fp 
% \vN_{1}\eqd \vN_{2} \And G_{1}\And G_{2}$. The first case entails
% $\ga\fp q\ \vN_{1}\nimm Q$ or $\ga\fp G_{1}$ which implies 
% $\ga\fp q\ \vN_{1}\If G_{1}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. The 
% second horn splits into three sub-cases:
% \ben
% \item
% $\vN_{1}\neqd \vN_{2}$. By Lemma \ref{le:imm-eq} $\ga\fp q\ 
% \vN_{2}\nimm Q$ which implies $\ga\fp q\ \vN_{2}\If G_{2}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
% \item
% $\ga\fp G_{2}$ implies $\ga\fp q\ \vN_{2}\If G_{2}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
% \item
% $\ga\fp G_{1}$ implies $\ga\fp q\ \vN_{1}\If G_{1}\nimm Q$ and finally 
% $\ga\fp q\ \vN_{1}\If G_{1}\tensor q\ \vN_{2}\If G_{2}\nimm Q$. 
% \enen
% \item
% Case:
% $$\ianc{([t/x] D_{1})\tensor D_{2}\setminus [t/x] D}{(\PIXA D_{1})\tensor 
% D_{2}\setminus \PIXA  D}\tensor\Pi}$$
% From $([t/x] D_{1})\tensor D_{2}\setminus [t/x] D$ and $\ga\sp \q 
% D\nimm Q$ by IH we infer $\ga\sp \q D\tensor D_{2}\nimm Q$, 
% equivalent to $\ga\sp \q D\nimm Q$ or $ D_{2}\nimm Q$ which implies 
% $(\PIXA D_{1})\tensor D_{2}\nimm Q$. 
% \enit
% \end{proof}
\newcommand{\ted}[1]{ (#1)^{\tensor_D} }
\newcommand{\teg}[1]{ (#1)^{\tensor_G} }
\newcommand{\PT}{\tensor\cP}

We now extend the effect of the above compilation on a program:
\begin{Definition}
\label{def:tensorpro}
\[\begin{array}{rcll}
 \ted{\top} & = & \top\\
\ted{\perp} & = & \perp\\
\ted{\Pi(Q\If G)} & = & \Pi(Q\If \teg{G})\\
\ted{ D_{1}\And D_{2} } & = & \ted{D_{1}}\And \ted{D_{2}} \\
%\ted{\PI{x}{A} D} & = & \PIXA  \ted{D} \\
\ted{D_{1}\tensor D_{2}} & = &  D  
& \mbox{\textrm{where }} \ted{D_{1}}\tensor \ted{D_{2}} \setminus D\\
\teg{X} & = & X & X\in\{\top,\perp,Q,\mbox{(dis)eq}\}\\
\teg{G_1\And G_2} & = & \teg{G_1}\And \teg{G_2}\\
\teg{G_1\Or G_2} & = & \teg{G_1}\Or \teg{G_2}\\
\teg{D\Imp G} & = & \ted{D}\Imp\teg{G}\\
\teg{\PIXA G} & = & \PIXA\teg{G}\\
%\teg{\exa G} & = & \exa\teg{G}
\end{array}\]
\end{Definition}

\newcommand{\td}[1]{ (#1)^{\tensor} }
\begin{Theorem}[Elimination of $\tensor$]
\label{thm:te-imm}
For every ground substitution
$\GG\vd\theta\hastype \Phi$
\ben
\item
 $\cS :: \ga\sp[\q] G$ iff $\td{\cS}) :: \GG;\ted{[\q]\cD}\sp\teg{ [\q]G}$;
\item
 ${\cal I} :: \ga\sp[\q] D \imm Q$ iff $\td{\cal I} ::
 \GG;\ted{[\q]\cD}\sp \ted{[\q]D} \imm Q$.
\enen
\end{Theorem}
\begin{proof}
($\Imp$). By a straightforward mutual induction on the structure of the given
derivations: we show the crucial case.
\bit
\itc $\td{\cal I}$ ends in $\imm\tensor$:
\btab
$\ga\sp [\q] D_1\imm Q$ and $\ga\sp  [\q]D_2\imm Q$\bs
$\GG;\ted{ [\q]\cD}\sp \ted{ [\q]D_1}\imm Q$ and $\GG;\ted{
  [\q]\cD}\sp \ted{ [\q]D_2}\imm Q$\bi $2$\\
$\GG;\ted{ [\q]\cD}\sp\ted{ [\q]D_1}\tensor \ted{ [\q]D_2}\imm Q$\br $\imm\tensor$\\
$\GG;\ted{ [\q]\cD}\sp [\q]\ted{D_1\tensor D_2}\imm Q$\` By Lemma
\ref{le:te-tim} 
\etab
\enit
($\If$). Similarly.
\end{proof}
The same remark \wrt termination applies.
%\begin{Proposition}
% \label{ppn:te-nimm}
% $\cP \enprv \PT$.
% \end{Proposition}
% \begin{proof}
% We need to show $\ga\nprv_{\cP} G$ iff $\ga\nprv_{\PT} G$. We 
% generalize this to:
% \ben
% \item
% $\SM :: \ga\fp G$ iff $\tensor \SM :: \ga\nprv_{\PT} G$;
% \item
% For every $\q$, $\IM :: \ga\fp \q(def(Q)) \nimm Q$ iff $\tensor \IM :: \ga\nprv_{\PT} 
% \q(def(Q)) \nimm Q$.
% \enen
% The proof is a straightforward mutual induction on the structure of the 
% derivation using Lemma \ref{le:te-nimm}.
% \end{proof}

% From the above propositions, we have the soundness and completeness 
% of the compilation:

% \begin{Corollary}
% \label{co:te-ti}
% $\cP \sim \PT$.
% \end{Corollary}

% \subsection{Constraints Simplification}
% \label{sec:simplify}
% \ednote{CHANGE}
% In this section we hint on how to bring clauses stemming from
% complementation into their final format by simplifying, whenever
% possible, the (dis)equations introduced by the $\mnota\Imp$ rule. In our
% language, two forms of disequations cannot be immediately solved and
% must be postponed as constraints:
% \begin{enumerate}
% \item Shallow parameter expression/existential variable disequations.
% \item Rigid term/existential variable disequations, stemming from
%   left-linearization.
% \end{enumerate}

% What can be solved instead is:
% \begin{itemize}
% \item Unification equations introduced by $\tensor$-elimination.
% %\item The rest of existential variable-rigid term disequations by
%  % computing the complement of the latter.
% %\item Unsatisfiable variable-variable disequations, by removal.
% %\item Removing useless augmentation clauses brought in by subordination.
% \end{itemize}

\bigskip

We finish up this Chapter by completing our two running example, where in a
final pass we have also: 
\begin{itemize}
\item Renamed negative predicates with more suggestive names.
\item Removed irrelevant occurrences of $\top$.
%\item Remove failing clauses, \ie with $\perp$ in the body.
\item Hidden the irrelevant augmentation in the final negative clause.
\item  Brought clauses to the `core'  languages syntax, as in LF.
\end{itemize}



\begin{Example}
\label{ex:closedfinal} 
Concluding Example \ref{ex:closed} and \ref{ex:closedatensor} the final
definition of $\neg$\texttt{closed} is:
\beq
oplam &: & \PI{ E}{exp} open\ (lam\ E)  \If \PI {x } {exp}\ open\ (E\ x).\\
opap1 &: & \PI{ E_{1},E_{2}}{exp} open\ (app\ E_{1} \ E_{2}) \If open\
E_1.\\
opap2 &: & \PI{ E_{1},E_{2}}{exp} open\ (app\ E_{1} \ E_{2}) \If open\ E_{2}.
\eneq
where we have
% solved all equations, which are in this case trivial
%<ground-ground checks,  
hidden the irrelevant assumption $closed\ x$ in \texttt{oplam} and renamed `$\neg$\texttt{closed}' into \texttt{open}.
\end{Example}

\begin{Example}
\label{ex:linearfinal} 
The final definition of \texttt{$\neg$linear} and in turn \texttt{$\neg$linx} is:

\beq
\neg linapp1 & : & \neg linear(app\ F\ G)\If \neg linear(F).\\
\neg linapp2 & : & \neg linear(app\ F\ G)\If  \neg linear(G).\\
\neg linlam1& : & \neg linear(lam\ \lx E\ x)\If \neg linx( \lx E\ x).\\
\neg linlam2& : & \neg linear(lam\ \lx E\ x)\\
&&\qquad\If (\PI{y}{exp} (\neg linx(\lx y)\And linear(y))\Imp\neg  linear(E\ y)).\\
\neg linxap1& :& \neg linx(\lx app\ (F\ x^1) \ (G\ x^1)).\\
\neg linxap2& : & \neg linx(\lx app\ (F\ x^0) \ (G\ x)^0).\\
\neg linxap3& : & \neg linx(\lx app\ (F\ x^1) \ (G\ x^0))\If \neg linx(\lx
 F\ x^1).\\ 
 \neg linxap4& : & \neg linx(\lx app\ (F\ x^0) \ (G\ x^1))\If \neg linx(\lx G\ x^1).\\ 
\neg linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\If\\
& & \qquad(\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ y)).
\eneq


% \neg linapp1 & : & \neg linear(app\ E_1\ E_2)\If \neg linear(E_1).\\
% \neg linapp2 & : & \neg linear(app\ E_1\ E_2)\If  \neg linear(E_2).\\
% \neg linlam1& : & \neg linear(lam\ \lx E\ x)\If \neg linx( \lx E\ x)\\.
% \neg linlam2& : & \neg linear(lam\ \lx E\ x)\If (\PI{y}{exp} (\neg linx(\lx y)\And linear(y))\Imp\neg  linear(E\ y)).\\
% % \neg linx1& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If strict(E_2\ x).\\
% % \neg linx2& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If
% % strict(E_1\ x).\\
% \neg linxap0& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x^1)).\\
% \neg linxap1& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^1))\If \neg linx(\lx
%  E_1\ x).\\ 
%  \neg linxap2& : & \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x))\If \neg linx(\lx E_2\ x).\\ 
% \neg linxap3& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If  \neg
% linx(\lx E_1)\And \neg linx(\lx  E_2\ x).\\
% \neg linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\If\\
% & & \qquad(\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ y)).
% \eneq
\end{Example}

\section{Summary}

In this Chapter we have given a complement algorithm for a significant
fragment of third order Hereditary Harrop Formulae, by adapting the idea
of \emph{elimination} of negation introduced in \cite{Sato84} for Horn
logic.  This has the neat effect that negation and its problems are
\emph{eliminated}, \ie we avoid any extension to the (meta) language.
This has entailed finding a middle ground between the Closed World
Assumption usually associated with negation and the Open World
Assumption typical of \lf s. Our solution is to restrict the set of
programs we deem deniable in a novel way, so as to enforce a
\emph{Regular Word Assumption} (RWA): we define a class of programs
whose dynamic assumptions extend the current database in a specific
regular way.  Technically, this regularity under
dynamic extension is calibrated so as to ensure that static and
dynamic clauses never \emph{overlap}. This property extends to the
negative program; in a sense, we maintain a distinction between static
and dynamic information, but at a much finer level, \ie \emph{inside}
the definition of a predicate. The resulting fragment is very rich, as
it captures the essence of the usage of hypothetical and parametric
judgments in a \lf; namely, that they are intrinsically combined to
represent \emph{scoping} constructs in the object language.


