\section{Exclusivity}
\label{sec:excluproof}

We are now in the position to prove the main result of this Chapter,
namely that clause complementation satisfies the boolean rules of
negation, in the form of exclusivity and exhaustivity. We remark that
this holds due to the fact that context schemata allow to pose only
`well-behaved' goals. For example, consider the query $G\equiv\neg
even(0)\Imp even(s(s(0)))$, which is such that both $\emp\vd_{even} G$
and $\emp\vd_{\neg even} \mnotg(G)$ are provable. By definition of
schema satisfaction, this is not a legal query. Similarly, the
following counter-example to exhaustivity $\emp\vd_{even} \PI{x}{nat}
even(x)$ is not allowed. Moreover, the Context Preservation Theorems
(Theorem \ref{thm:poscntpres} and \ref{thm:negcntpres}) guarantees
that, from allowed run-time contexts and goals, only allowed subgoals
are generated.

We will need the following obvious fact:
\renewcommand{\vN}{\ol{N_n}}

\begin{Lemma}
\label{le:rigid}
If $\GG\vd M\hastype A$ and $M$ is rigid, so is every $N$ such that
$N\in(\GG\vd\mnot(M))$.
% If $\Pi(q\ \Mn)$ satisfies the rigidity condition, then for every
% $\GG$ and $\vN$ if $\vN\in\GG\vd\mnot(\Mn)$, then there exists $1\leq
% i\leq n$ such that $N_i$ is rigid.
% \end{Lemma}
\end{Lemma}
\begin{proof}
  By a straightforward induction on the structure of $\GG\vd\mnot(M)$.
\end{proof}




\renewcommand{\nn}[2]{(\BAnd_{x\in\dom(\GG)} \mnotr(q\ #1)\And (\BAnd_{1\leq
  i\leq n,xR^{i}q}\mnotxi(q\ #1))) \And \Pi( \neg q\ #1)\If #2}
\renewcommand{\ga}{\Gamma;\cD }
\renewcommand{\gna}{ \Gamma;\cD }
\renewcommand{\q}{}
\renewcommand{\s}{[\sigma]}
\renewcommand{\PP}{\cP}
\renewcommand{\PM}{\cP}
\renewcommand{\ex}{e_x}
\newcommand{\vnx}{ \ol{N_{\ex}^i}}
\renewcommand{\vM}{\ol{M_n}}
\newcommand{\vT}{\ol{T_n}}
\renewcommand{\vS}{\ol{S_n}}
\renewcommand{\sn}{\vd_{\cP}}
\renewcommand{\spp}{\vd_{\cP}}
\renewcommand{\sp}{\vd_{\cP}}
\renewcommand{\snp}{\vd_{\cP}\mnotg}
\renewcommand{\PIXA}{\PI{x}{a}}


We use $\ga\sn\mnotg (G)$ for $\GG\vd\mnotg(G) = G'$ and $\gna\sn G'$; also,
$\ga\sn\mnotd (D)\imm\neg Q$ for $\mnotd(D) = D'$ and $\gna\sn
D'\imm\neg Q$; similarly for $\mnota$. 
%  Recall that $D\inn
% \defp(q,\cP\And\cD)$ denotes that $D$ is a top-level conjunct in the
% static or dynamic definition of $q$. Similarly, $D\inn \defp(\neg
% q,\cP\And\cD)$ denotes that $D$ is a top-level disjunct in the static
% or dynamic definition of $\neg q$. 
We use $\cP$ to denote the
conjunction of a positive program $\cP^+$ and its negation
$\cP^-=\mnotd(\cP^+)$. 

% Finally, since by Corollary \ref{co:clocomp} a
% (run-time) context is closed under negation, $D'\inn \defp(\neg q,\cD)$
% iff $\GG\vd\mnota(D)=D'$ for $D\inn \defp( q,\cD)$.

\begin{Theorem}[Exclusivity] 
\label{thm:exclu}
Let $\models_{\!\csa}\ald(\PP)$ and $\ga\ins\csa$.  For every goals
such that $\ga\sla G \ins\csa$,  It is not the case that there is $\SP ::  \ga\spp G$ and there is $\SM
:: \gna\snp ( G)$. 
%it is not the case that both $\ga\spp G$ and $ \gna\snp (G)$.
\end{Theorem}
\begin{proof}
We generalize this to; 
\bit  %%%% main bit
% \item[\fbox{1}] It is not the case that there is $\SP ::  \ga\spp G$ and there is $\SM
% :: \gna\snp ( G)$. 
\item[\fbox{2.1}]
\input{twoone}
\item[\fbox{2.2}] %second case
  Let $D\inn \defp(q,\PP)$ and $D'\inn \defp( q,\cD)$. It is not the
  case that $\IP :: \ga\spp D \imm Q$ and $\IM :: \gna\sn
  \mnota(D')\imm \neg Q$.  By simultaneous induction on the structure
  of $\IP$ and $\IM$:
\input{twotwo}
\item[\fbox{2.3}] %third case
  Let $D\inn \defp(q,\cD)$ and $D'\inn \defp( q,\cP)$.  It is not the
  case that $\IP :: \ga\spp D \imm Q$ and $\IM :: \gna\sn
  \mnotd(D')\imm \neg Q$.  By simultaneous induction on the structure
  of $\IP$ and $\IM$. Note that by the restriction to complementable
  programs, some SPE $\ex$ occurs in $D$; we thus use the notation $\vnx$.
\input{twothree}
\item[\fbox{2.4}] %\fourth case
  Let $D\inn \defp(q,\cD)$ and $D'\inn \defp(q,\cD)$. 
  There are two main cases, according to whether $D$ and
  $D'$ belong to the same block (and in this case it suffices to
  consider $D\equiv D'$) or not:
\input{twofour}
 %end four cases
 %start \vd G
\item[\fbox{1}] By  induction on the structure of $\SP$.
\input{one}
\enit% main bit
\end{proof}

Note that the proof goes through as there is no `bad' interaction
between the static and dynamic definition of a predicate; namely in
sub-case $2.2$ there is no overlap between a clause from $\defp(q,\PP)$
and $\defp(\neg q,\cD)$ since in every atomic assumption there must be an
occurrence of a new parameter \emph{and} every term at the same
position in a program clause
head must be \emph{rigid}. Symmetrically for $2.3$. Sub-case $2.4$
holds 
% either because atoms in $\defp(q,\PP)$ and $\defp(\neg q,\cD)$ have a
% different pivot parameter or, if it the same, an appropriate
% disequation is inferred. 
%because an appropriate disequation is inferred; this approximates what
analogously to the first case $2.1$, which is based on term
exclusivity (Corollary \ref{le:part}). In the latter case, it suffices
to consider, for $D\inn \defp(q,\cP)$, only $\ga\spp D\imm Q$ and
$\ga\sn\mnotd(D)\imm\neg Q$, because the positive definition is a
conjunction, while the negative one is a disjunction; $2.4$ needs to
discriminate whether the two dynamic assumptions belong to the same
block: if so the same remark applies. If not, the (pivot)
eigenvariable condition ensures non-overlapping.

The condition for programs to require clause heads with rigid terms
%and assumptions with parameters only in head position 
may seem too restrictive; the natural way to relax it, 
requiring that only \emph{one} of those terms which
 occur in the same position of a parameter in each assumption needs to
 be rigid, turns out to be inconsistent; in fact, the property needs to be preserved in the negative program as well. Consider the following counterexample:
\beq
plam & : & p\ (lam\ E) \ (lam\ F)\If \PI{x}{exp} p\ (E\ x) \ (F\ x).\\
papp & : & p\ (app\ E_1\ E_2) \ F.
\eneq
Augmentation will insert the clause $\Pi(\neg p\ x\ H\And \neg p\ H'\ 
x)$, which now overlaps with $\neg$\texttt{papp}.  As a result both $p\ 
(lam(\lamb{x}{exp} app\ x\ x))\ (lam(\lamb{y}{exp}y))$ and its
negation are provable.

As we remarked earlier, the rigidity condition applies only to
predicate definitions which are mutually recursive to non-Horn ones.
Thus, any such program which uses a `catch-all' clause is those
positions is forbidden; nevertheless it is easy to avoid catch-all
clauses via explicit coercion or (sometimes) partial evaluation.
Finally, we remark that any other (decidable) condition which avoids
overlap between static and dynamic clauses will do; the one we have
proposed is statically checkable, certainly not `ad hoc' and has been
dictated by the practice of logical frameworks.
% The condition for programs to require clause heads with rigid terms
% %and assumptions with parameters only in head position 
% may seem too restrictive and we thus comment on it. As we remarked
% earlier, it applies only to predicate definitions which are mutually
% recursive to non-Horn ones; secondly, only one of those terms which
% occur in the same position of a parameter in each assumption needs to
% be rigid; more formally, if $q\ \Mn\If G$ is a HHF formula
% $q\ N^i_{\ex}$ is in  a schema $\cS$ for
% \emph{some} $1\leq i\leq n$, then only $M_i$ must be rigid. Thus, any
% HHF program which uses a `catch-all' clause is those positions is
% forbidden; nevertheless it is easy to avoid catch-all clauses via
% explicit coercion or partial evaluation.  Finally, we remark that any
% other (decidable) condition which avoids overlap between static and
% dynamic clauses will do; the one we have proposed is statically
% checkable, certainly not `ad hoc' and has been dictated by the
% practice of logical frameworks.






