\section{Complementable Clauses}

%\renewcommand{\vdf}{\GG\vd} ???
\renewcommand{\vdf}{}
\newcommand{\vda}{\vd}

\renewcommand{\ex}{e_x}

We restrict ourselves to programs with:
\bit
\item \emph{Complementable} clauses as defined in Figure~\ref{fig:compl}.
\item Rules of the form $\Pi(Q\If G)$, such that every (input) term in
  $Q$ is rigid.
\item Parameters of base type and occurring only in \emph{head}
  position, called \emph{Shallow Parameter Expressions}:
\[ \begin{array}{rrcl}
\mbox{\textit{SPE}}& e_x &  \bnfas & x\hastype a\bnfalt\lx e_x
\end{array}
\]
\enit

We do not formalize here the former assumptions on terms; note that
the rigidity restriction applies only to predicates mutually recursive
to non-Horn ones -- see the comment at the
end of the proof of Theorem~\ref{thm:exclu}. 
We do give a definition of complementable clause in Figure~\ref{fig:compl}.

\newcommand{\compg}[1]{\ga\vd #1 \mbox{ compl}}
\newcommand{\compd}[1]{\ga\vd #1 \mbox{ compl}}
\begin{figure}
\bca
  \ianc{X\in\{\top,\perp\}\mbox{ or (dis)eq}}{ \compg{ X}}{cg\ X}%\qquad 
%\ianc{}{\emp\vd Q\mbox{ compl}}{\atm\emp}
\vsk
\ianc{}{\GG;\top\vd Q \mbox{ compl}}{cg\atm}\vsk
\ianc{\mbox{\textrm{for all }}D\inn\cD: \,\dom(\GG)\cap par(D)\not=\eset}{\compg{Q}}{cg\atm\cap}\vsk
\ibnc{ \GG;(\cD\And D)\vd G \mbox{ compl}}{\compd{D}}{  \compg{D\Imp G}}{cg \Imp}\vsk
\ianc{(\GG,y\oftp a);\cD\vd[y/x] G  \mbox{ compl}}{\ga\vd \PI{x}{a}G\mbox{ compl}}{cg \Pi^y}\vsk 
\ibnc{   \compg{G_1}}{  \compg{G_2}} {  \compg{G_1\And G_2}}{cg \And}\vsk 
\ibnc{ \compg{G_1}}{ \compg{G_2}} { \compg{G_1\Or G_2}}{cg
  \Or}\vsk
 
\ianc{X\in\{\top,\perp\} }{\compd{X}}{cd\ X} \vsk
  \ibnc{\compd{D}}{\ga\vd G \mbox{ compl}} {\compd{D\If G}}{ cd\If}\vsk
  \ianc{ \compd{[u/x]D}}{ \compd{\PIXA D}}{cd \Pi^u}\vsk 
\ibnc{ \compd{D_1}}{\compd{D_2}} {  \compd{D_1\And D_2}}{cd \And}\vsk
\ibnc{\compd{D_1}}{ \compd{D_2}} {  \compd{D_1\tensor D_2}}{cd \tensor}
\eca
  \caption{Complementable clause and goal: $\compd{D}$ and $\compg{G}$}
  \label{fig:compl}
\end{figure}


\begin{Example}
The clause encoding the introduction rule for implication in
natural deduction from Example \ref{ex:nd} is \emph{not} complementable:
\beq
impi & : & nd(A\ imp\ B)\If (nd(A) \Imp nd(B)).
\eneq
On the other hand, the following  is allowed by rule $cg\atm$:
\beq
oplam^{\top}&:&  \PI{ E}{ exp\Imp exp} open\ (lam\ E)  \\
& & \qquad\If( \PI {x } {exp} \top_{open} \Imp open\ (E\ x)).
\eneq
% The same rule  promotes the following:
% \beq
% isdall & : & \PI{D}{term\Imp form} isd\ (all\ D)\If \\
% & & \qquad \PI{x}{term}  isd\ (D\ x).
% \eneq
\end{Example}

\renewcommand{\PIXA}{\PI{x}{a}} %base type parameters
The restriction on goals and clauses yields this revised grammar:
\[ \begin{array}{rrcl}
\mbox{\textit{Clauses}}& D & \bnfas & \top\bnfalt\perp\bnfalt \Pi(Q \If
G)\bnfalt D_{1}\And D_{2}\bnfalt D_{1}\tensor D_{2}\\%\bnfalt\PIXA D\\
\mbox{\textit{Goals}}& G & \bnfas & Q \bnfalt \top\bnfalt \perp\bnfalt
\vM \eqd \vN\bnfalt \vM \neqd \vN\bnfalt\\
& & & G_{1}\And G_{2}\bnfalt
G_{1}\Or G_{2}\bnfalt D\Imp G\bnfalt\PIXA G
\end{array}\]

We use $\Pi(Q\If G)$ as a normal form for `rules', where the
quantifier bounds every free variable in $Q\If G$. This has the
technical advantage to provide a handle for both the head of a clause
and the set of all its free variables at the same time, which will be
crucial to describe the complement algorithm.
In particular,  `facts' are
represented by $ \Pi(Q)\If \top$, although in
examples we will omit to mention the body.  We accordingly specialize
the immediate implication and denial rules as follows:

\[\begin{array}{c}
\ibnc{\GG\vd\sigma\hastype
  FV(\vN)\sla\dom(\GG)\qquad\ga\sp[\s]\vN\eqd\vM}{\ga\sp[\s] G} 
{ \ga\sp \Pi( q\  \vN\If G) \imm q\  \vM}{\imm\Imp}
\vsk
\ianc{\mbox{for all $\q$ } \GG\vd\q\hastype FV(\vN)\sla\dom(\GG)\qquad\ga\fp
  [\q]\vN\eqd\vM}{\ga\fp \Pi(q\ \vN\If G) \nimm q\
  \vM}{\not\imm{\Imp_1}} 
\vsk
\ibnc{\GG\vd\sigma\hastype FV(\vN)\sla\dom(\GG)\qquad\ga\fp
  [\s]\vN\neqd\vM}{\ga\fp[\s] G} {\ga\fp \Pi(q\ \vN\If G) \nimm q\
  \vM}{\not\imm{\Imp_2}} 
\end{array}\]

We remark that the `guards' in the immediate denial rules are
constructed so as to make the positive and negative judgment mutually
independent. Thus $\not\imm\Imp_1$ says that a clause $\Pi(q\ \vN\If
G)$ denies a goal $q\ \vM$ if for all well-typed substitutions $\q$
$[\q]\vN$ and $\vM$ clashes. Rule $\not\imm\Imp_2$ instead attributes
denial with the same conclusion due to `failure' in the body.
% If we use $\Pi(D)$ to denote the
% universal closure of (all) the free variables in $D$, 

Clause complementation is taken \emph{definition-wise}. We cluster a
program in a conjunction of possibly mutually recursive predicate
definitions. We accomplish this with the following:

\begin{Definition}[$\GG\vd\defp(q,D)$]
\label{def:defq}
\[\begin{array}{rclr}
\GG\vd\defp(q,\top) & = & \top_q\\ 
\GG\vd\defp(q,\perp) & = &  \perp_q \\
\GG\vd\defp(q,\Pi(Q\If G)) & = &  \Pi(Q\If G)&\mbox{if } Q\equiv q\ \vM \\
\GG\vd\defp(q,\Pi(Q\If G)) & = &  \top_q&\mbox{otherwise} \\
%\GG\vd\defp(q,\PI{x}{A} D) &= &  \PIXA \GG\vd\defp(q,D) \\
\GG\vd\defp(q,D_1\And D_2) & = &  \GG\vd\defp(q,D_1)\And \GG\vd\defp(q,D_2) \\
\GG\vd\defp(q,D_1\tensor D_2) & = & \GG\vd\defp(q,D_1)\tensor \GG\vd\defp(q,D_2)
\end{array}\]
\end{Definition}

If $D=\cP$, \ie the underlying program (seen as a conjunction of
clauses), we call $\cdot\vd\defp(q,\cP)$ the \emph{static} definition
of $q$ and if $\ga$ is a conjunction of a run-time context, we call
the latter the \emph{dynamic} definition of $q$.  We avoid mentioning
the parameter context when it can be inferred from the context. As a
special case, an undefined predicate $q$, \ie a predicate which occurs
in a body of a clause but not as a head is represented by the empty
conjunction $\top_q$.  Conversely $\perp_q$ denotes the universal
definition for $q$.  We agree to consider $\top_q$ ($\perp_q$ resp.~)
as the zero (one) element for conjunction and disjunction and
implicitly apply the appropriate absorption operations; for example:
$$\top_q\And\Pi(q\ \vM\If G) = \Pi(q\ \vM\If G)$$
We overload the
notation $D\inn\cD$ in the case $D\inn\GG\vd\defp(q,\cP\And\cD)$ to
indicate the relation that satisfies the following rules: \beq
\ianc{
%%% D\in \{ \top,\perp,\Pi(Q \If G)\}
} {
D\inn D}{} \qquad
\ibnc{D_1\inn\cD}{D_2\inn\cD}{D_1\And D_2\inn \cD}{} \qquad
\ibnc{D_1\inn\cD}{D_2\inn\cD}{D_1\tensor D_2\inn \cD}{} \eneq The
immediate implication and denial judgments is specialized as obvious:
\[
\begin{array}{ll}
\ga\sp D \imm Q & \mbox{Clause  $D$ from  $\GG\vd\defp(q,\cP\And\cD)$ immediately entails  atom $Q$.}\\
\ga\fp D \imm Q & \mbox{Clause  $D$ from $\GG\vd\defp(q,\cP\And\cD)$
  immediately denies atom $Q$.}
\end{array}
\]
In particular, the `\atm' rules are: 
\beq 
\ibnc{D\inn  \defp(Q,\cP\And\cD)}{\block{\GG};\block{\cD}\sp D \imm Q}
{\ga\sp Q}{\vd\atm}
\vsk 
\ibnc{D\inn  \defp(Q,\cP\And\cD)}{\block{\GG};\block{\cD}\fp  D \nimm Q}{\ga\fp
  Q}{\nprv\atm}
\eneq

Accordingly, we also specialized the rule for schema satisfaction:
we use $\rho$ to denote a \emph{global}
substitution, e.g.\ such that $\dom(\rho)$ is a set of  new global parameters.

\newcommand{\glob}{[\rho]}

\[\begin{array}{c}
\ianc
%\dsat\glob Q 
{\cdot;\top\sla\glob G\inss} 
{ \dsat \Pi( Q\If G) \imm q\  \vM}{\dsat\Imp^{\rho}}
\end{array}\]
It is clear that all the above rules are  derived rules of inference, as
can be proven by a straightforward induction on the number of
free variables in $\vN$.
% \begin{Lemma}
% \label{le:derivs}

%$$
%\ianc{\mbox{for some $\GG\vd t\hastype A$}}{ \ga\sp  [t/x]D \imm
 % Q}{\ga\sp \PIXA D \imm Q}{\imm\Pi}
%\ibnc{\GG\vd\s}{\ga\sp\s\vN\eqd\vM}{\ga\sp\Pi(q\
%  \vN\If \top)\imm  q\ \vM}{\Pi\s\imm}
%$$
% \end{Lemma}
% \begin{proof}

%\end{proof}




\subsection{Normalization of Input Variables }
\label{ssec:inputnormal}
\newcommand{\lgf}{\Lambda;\Phi;\Gamma\vd}
\newcommand{\fg}{\Phi;\Gamma\vd}
\newcommand{\mapd}{\stackrel{\mbox{\tiny{$D$}}}{\mapsto}}
\newcommand{\mapg}{\stackrel{\mbox{\tiny{$G$}}}{\mapsto}}

We present in Figure \ref{fig:inputterm} the rules for normalization
of input variables. Since we are currently working with the
restriction to ground goals, those are all the variables which are
universally quantified in the head of a clause. When they occur
positively in dynamic assumptions, they will carry some instantiation.
It helps to simplify the presentation of the clause complementation
algorithm if we forbid this kind of occurrence. The idea it to replace
every positive occurrence of an input variable in an assumption with a
new (local) universal variable, which is then constrained to be equal
to the input ones.

\begin{Example}
\label{ex:ivnorm}
Consider the typing clause for lambda terms:
\beq
oflam &:&  \PI{E}{exp\Imp exp}\PI{T_1,T_2}{tp}\\
&& of\ (lam\ E) \ (arrow\ T_1\ T_2)\\
& & \qquad\If( \PI{x}{exp} of\ x\ T_1 \Imp  of\ (E\ x) \ T_2).
\eneq
As $T_1$ is an input term occurring positively in the assumption `$ of\
x\ T_1$', normalization of input variables  inserts a new variable $T$
and constrains it to be equal to $T_1$:
\beq
oflam' &:& \PI{E}{exp\Imp exp}\PI{T_1,T_2}{tp}\\
&& of\ (lam\ E) \ (arrow\ T_1\ T_2)\\
& &\qquad\qquad (\PI{T}{tp}  of\ x\ T\If T\eqd T_1)\Imp\\
&&\qquad\qquad\qquad  of\ (E\ x) \ T_2).
\eneq
\end{Example}

This procedure is realized by the judgments:
\begin{itemize}
\item $D\mapd D'$: clause normalization.
\item $\GG\vd_{\Phi} G\mapg G'$: goal normalization.
\item $\fg D\mapsto D'$: assumption normalization \wrt global
  parameters in $\Phi$.
\item $\lgf M\mapsto M',E$: term $M$ normalizes to term $M'$ returning
  a conjunction of equations $E$ \wrt  bound ($\GG$), global ($\Phi$) and
existential ($\Lambda$) variables.
\end{itemize}

The first three judgments simply recur on the structure of clauses, goal
and assumptions, keeping track of bound, global and
existential  variables in assumptions, until we normalize
an assumption $\Pi (Q\If G)$: here we descend in every term by
introducing new local existential variable and binding them to the
global one via an equation $E$. For the sake of conciseness, we do this
for the simply-typed fragment; the generalization to the strict one is
immediate. In rule $\mapd\If^{\rho}$ we introduce in the global
context all the global parameters in the domain of $\rho$ with the
appropriate typing.

\begin{figure}
\newcommand{\vdfg}{\vd_{\Phi}}
\renewcommand{\glob}{[\rho]}
  \[
  \begin{array}{c}
    \ibnc{D_1\mapd D_1'}{D_2\mapd D_2'}
    {D_{1}\And D_{2}\mapd D_{1}'\And D_{2}'}{\mapd\And}\qquad
    \ibnc{D_1\mapd D_1'}{D_2\mapd D_2 '}
    {D_{1}\tensor D_{2}\mapd D_{1}'\tensor
    D_{2}'}{\mapd\tensor}\vsk
    \ianc{X\in\{ \top,\perp\}}{X\mapd  X}{\mapd X}\qquad
 \ianc{\cdot\vd_{\dom(\rho)}\glob G\mapg \glob G'}{\Pi(Q\If G) 
 \mapd\Pi(Q \If G')}{\mapd\If^{\rho}}
\vsk\vsk
  \ianc{X\in\{ \top,\perp, Q\} \mbox{ or  (dis)eq}}{\GG\vdfg X\mapg
    X}{\mapg X}\qquad
  \ianc{(\GG,y\oftp A);\cD\vdfg [y/x]G\mapg [y/x]G'}{\GG\vdfg \PIXA
  G\mapg  \PIXA G'}{\mapg\Pi^y}\vsk
  \ibnc{\fg D\mapsto D'}
{\GG;\cD\And D\vdfg G\mapg G'}{\GG\vdfg (D\Imp  G)\mapg (D'\Imp
  G')}{\mapg\Imp}\vsk
 \ibnc{\GG\vdfg G_1\mapg  G_1'}{\GG\vdfg G_2\mapg  G_2 '}
    {\GG\vdfg G_{1}\And G_{2}\mapg  G_{1}'\And G_{2}'}{\mapg\And}\qquad
    \ibnc{\GG\vdfg G_1\mapg  G_1'}{\GG\vdfg G_2\mapg   G_2 '}
    {\GG\vdfg G_{1}\Or G_{2}\mapg  G_{1}'\Or
    G_{2}'}{\mapg\Or}\vsk\vsk
  \ianc{\Lambda=FV(\Mn)\setminus\dom(\GG\cup\Phi)\qquad \lgf M_1\mapsto
    M_1',E_1\cdots \lgf M_n\mapsto M_n',E_n}{\fg\Pi(q\ \Mn\If G)\mapsto
    \Pi(q\ \ol{M'_n}\If E_1\And\dots\And E_n\And G)}{\mapsto\Imp}\vsk 
 \ianc{X\in\{ \top,\perp\}}{\fg X\mapsto X}{\mapsto X}\vsk
    \ibnc{\fg D_1\mapsto D_1'}{\fg D_2\mapsto D_2'}
    {\fg D_{1}\And D_{2}  \mapsto D_{1}'\And D_{2}'}{\mapsto\And}\qquad
    \ibnc{\fg D_1\mapsto D_1'}{\fg D_2\mapsto D_2 '}
    {\fg D_{1}\tensor D_{2}  \mapsto D_{1}'\tensor
    D_{2}'}{\mapsto\tensor}  \vsk\vsk
  \ianc{}{\Lambda;\Phi;(\GG,\xoa)\vd x\mapsto x,\top}{bv}\qquad
    \ianc{Z \mbox{ new}}{\Lambda;(\Phi,u\oftp A);\GG\vd u\mapsto Z,
    Z\eqd u}{iv}\qquad
    \ianc{}{(\Lambda,\xoa);\Phi;\GG\vd x\mapsto x,\top}{lv}\vsk
  \ibnc{\lgf M_1\mapsto M'_1,E_1}{\lgf M_2\mapsto M'_2,E_2}{\lgf M_1\
    M_2\mapsto M_1'\ M_2', E_1\And E_2}{App}\qquad
  \ianc{\Lambda;\Phi;(\Gamma,\xoa)\vd M\mapsto M', E}{\lgf\lamb{x}{A}
    M\mapsto \lamb{x}{A}M', E}{\l}
  \end{array}
  \]
  \caption{Clause, goal, assumption and term normalization}
  \label{fig:inputterm}
\end{figure}


It is clear, although very tedious, to verify that this transformation
preserves provability and denial:

\begin{Lemma}
\label{le:termmap}
Assume $\lgf M\mapsto M',E$; for every ground $N$, every $\ga$,
$\ga\vd M \eqd N$ iff $\ga\vd (M'\eqd  N)\And E$.
\end{Lemma}
\begin{proof}
By a straightforward induction on the structure of $\lgf M\mapsto M',E$.
\end{proof}

 \newcommand{\qb}{[ \theta ]}


% \begin{Lemma}
% \label{le:dmap}
% Let $\GG\vd\q\hastype\Phi$ and $\fg D\mapsto D'$. For every $\cD$, it holds
% $\GG;\qb\cD\vd \qb D\imm Q$ iff $\GG;\qb\cD\vd \qb D'\imm Q$.
% \end{Lemma}
% \begin{proof}
%   By a straightforward induction on the structure of $\fg D\mapsto D'$,
%   using Lemma \ref{le:termap}.
% \end{proof}

\begin{Theorem}
\label{thm:termap}
Let $\GG\vd\q\hastype\Phi$, $\fg \cD\mapsto \cD'$, $D\mapd D'$ and $\GG\vd_{\Phi} G\mapg G'$:
\begin{enumerate}
\item $\GG;\qb\cD\vd \qb D\imm Q$ iff $\GG;\qb\cD'\vd \qb D'\imm Q$.
\item $\GG;\qb\cD\vd \qb G$ iff $\GG;\qb\cD'\vd \qb G'$.
\end{enumerate}
\end{Theorem}

\begin{proof}
  By a straightforward mutual induction on the
  structure of the given derivations,
%%$D\mapd D'$ and $\GG\vd_{\Phi} G\mapg G'$
  using Lemma \ref{le:termmap}.
\end{proof}


\section{The Clause Complement Algorithm}
\label{sec:cc}

We now introduce in Figure \ref{fig:notclause} and Figure
\ref{fig:notass} the rules for \emph{static} and \emph{dynamic clause
  complementation}.  Consider a rule $\Pi(q\ \vM\If G)$; its
complement must contain a `factual' part motivating failure due to
clash with the head; the remainder $\mnotg (G)$ expresses failure in
the body, if any.  Clause complementation must discriminate whether
this rule belongs to the static or dynamic definition of a predicate.
In the first case all the relevant information is already present in
the head of the clause and we can, without further ado, use the term
complementation algorithm described in Chapter \ref{ch:relcomp}. This
is accomplished by the rule $\mnotd\Imp$, where a set of negative
facts is built via term complementation $\mnot (\vM)$ applied in the
empty context to the (vector of) terms in the clause head; namely
$\BAnd_{\vN\in\cdot\vd\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top)$;
%, whose fresh free variables are universally closed;
moreover the negative counterpart of the source clause is obtained via
complementation of the body.  The Partition Lemma
(Corollary~\ref{le:part}) guarantees the soundness and completeness of
this case.
%The original quantification is retained thanks to rule $\mnotd\Pi$.

\begin{figure}
    \[
    \begin{array}{c}
           \ianc{}{\vdf\mnotd (\top)  =       \perp}{\mnotd\top}\qquad
        \ianc{}{\vdf\mnotd (\perp)  =  \top}{\mnotd\perp}\vsk
    \ianc{\cdot\vd\mnotg(G) =  G'}{\vdf\mnotd( \Pi(q\ \vM\If G)) =
      \BAnd_{\vN\in\cdot\vd\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top) \And \Pi
      ( \neg q\ \vM\If G')}{\mnotd\If}\vsk\vsk
%         \ianc{\vdf\mnotd( D)=D'}{\vdf\mnotd (\PI{x}{A}D)  =  \PI{x}{A}D'}{\mnotd\Pi}\vsk
        \ibnc{\vdf\mnotd (D_{1})= D_1'}{\vdf\mnotd (D_{2})= D_2'}{\vdf\mnotd
        ( D_{1}\And D_{2})=D_1'\tensor D_2'}{\mnot\And}\vsk
       \ibnc{\vdf\mnotd (D_{1})= D_1'}{\vdf\mnotd (D_{2})= D_2'}{\vdf\mnotd
        ( D_{1}\tensor D_{2})=D_1'\And D_2'}{\mnot\tensor}
      \end{array}\]
    \caption{Clause complementation: $\vdf\mnotd(D)=D'$}
  \label{fig:notclause}
\end{figure}
\smallskip

\emph{Assumption} complementation is realized by the judgment $\gf\mnota(D)$,
which can be seen as a type directed \emph{parameter-conscious}
version of clause complementation.  In a first approximation, we can
think of complementation of assumptions, which are by definition
parametric in some $x$, as static clause complementation \wrt $x$.
Informally, for an atomic assumption, say $ q\ M_1\dots M_{i-1}\ \ex\ 
M_{i+1}\dots M_n$, its complement can be taken as $\mnotd( q_{\ex}\ 
M_1\dots M_{i-1}\ M_{i+1}\dots M_n)$, for a shallow parameter
expression $\ex$.  This is accomplished in two main
phases: first, $\ex$ is propagated in every position $1\leq j\leq n$
holding a rigid term of compatible type, but different from $\ex$
itself. This alone builds an element in the complement set. Secondly,
%provided every $M_i$ is not a parameter expression. In this case,
the idea is to can apply term complementation `around' $\ex$. In
particular, if $M_j$ is a variable, by normalization of input
variables, it must be a local one and term complement does not
contribute anything as expected. If $M_j$ is a parameter expression or
a compound term, we simply take the term complement of the former
term, with the notable difference of passing the current parameter
context to term complement. 

However, not all parameters are born alike; in many situations, a
parametric judgment is used simply to descend into a scoping
construct, while the parameter itself does not play a role \wrt
provability and denial. Consider, for example, the following program
that checks whether a universal formula is a $D$-clause: 
\beq
form,term& \hastype & type.\\
all& \hastype & (term\Imp form)\Imp form).\\
isd& \hastype & form\Imp\prop\\
isdall & : & \PI{D}{term\Imp form} isd\ (all\ D)\\
& & \qquad \If\PI{x}{term} isd\ (D\ x).  
\eneq
This phenomenon is known in the literature under the name of
\emph{subordination} and has been extensively studies in the dependent
typed context \cite{Virga99phd}. In the simply typed setting, this
relation collapses to  merely checking whether the type of the
parameters is equal to the target type of some argument of the
predicate. More formally, 
we say that $x\oftp A$ is \emph{relevant to $Q$} if $head(Q)\equiv q$,
$\Sigma(q)=A_{1}\mdots A_{n}\Imp \prop$ and for some $1\leq i\leq n$
it holds that $\mbox{target} (A_i)\equiv A$; we denote this with
$\xrq$. In the above example, as $term\not\equiv
form$, then $x\hastype term$ is \emph{not} relevant to $isd\hastype
form\Imp\prop$.
Wrt.\ clause complementation, if the parameter $x$ is \emph{not}
relevant to $q$, we do not need to build 
complementary facts out of it, although they would not impact
soundness, \ie Exclusivity (Theorem \ref{thm:exclu}).

\input{notass}
% \begin{figure}
% \renewcommand{\ga}{\GG\vd}
%     \[
%     \begin{array}{c}
%        \ianc{}{\GG\vda\mnota (\perp)  =  \top}{\mnota\perp}\vsk
%  \ianc{}{\GG\vd\mnota (\top_q)  = \BAnd_{x\in
%  dom(\GG)}(\BAnd_{xR^{i}q}\mnotxi(\top_q))}{\mnota\top}\vsk\\ 
% %       \ianc{}{\GG\vda\mnota (\top_q)  = \BAnd_{x\in dom(\GG)}^{x\in
% %          Q_{\mid_i}}\mnotxi(\top_q)}{\mnota\top}\vsk\vsk
% %           \ianc{\vdf\mnotg(G) = G'}{\GG\vda\mnota( Q\If G) =\BAnd_{x\in dom(\GG)}^{x\in
% %          Q_{\mid_i}}\mnotxi(Q) \And ( \neg Q\If
% % G')}{\mnota\If}\vsk\vsk

%            \ianc{\GG\vd\mnotg(G) = G'}{\GG\vd\mnota( Q\If G) =(\BAnd_{x\in
%            dom(\GG)}\BAnd_{xR^{i}q}\mnotxi(Q)) \And \Pi( \neg Q\If
%            G')}{\mnota\If}\vsk\vsk
% %    \ianc{\GG\vda\mnota([u/x] D)=[u/x]D'}{\GG\vda\mnota (\PI{x}{A}D)  =  \PI{x}{A}D'}{\mnota\Pi^u}\vsk
%         \ibnc{\GG\vda\mnota (D_{1})= D_1'}{\GG\vda\mnota (D_{2})= D_2'}{\GG\vda\mnota
%         ( D_{1}\And D_{2})=D_1'\tensor D_2'}{\mnot\And}\vsk
%        \ibnc{\GG\vda\mnota (D_{1})= D_1'}{\GG\vda\mnota (D_{2})= D_2'}{\GG\vda\mnota
%         ( D_{1}\tensor D_{2})=D_1'\And D_2'}{\mnot\tensor}
% \vsk\vsk
% \ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\cdot\vd sh(x,A_i)=\ex}
% {\gfq\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\  \ol{Z^i_{\ex}}\If \top}{\mnotxi\top}\vsk
%  \ianc{
% %\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop\qquad 
% M_i\equiv\ex}
% %{\cdot\vd       sh(x,A_i)=\ex}
% {\gfq\mnotxi  (q\ \Mn)=
%     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%      \neg q\ \ol{Z^i_{\ex}}\If M_j\neqd Z_j)}{\mnotxi\atm}
% \vsk\vsk
% \ianc{}{\gvd sh(x,a)=x}{\ex\atm}
% \qquad
% \ianc{\GG,y\oftp A\vd sh(x,B)=\ex}{\GG\vd sh(x,A\Imp B)=\lamb{y}{A}\ex}{\ex\Imp^y}
% % \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi(\top_q)  =
% %       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
% %       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
% %     \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi  (q\ \Mn)=
% %     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
% %      \neg q\ \ol{Z^i_x}\If M_j\neqd Z_j)}{\mnotxi\atm}
%  \end{array}\]
%     \caption{Old Assumption complementation: $\GG\vda\mnota(D)=D'$}
%   \label{fig:notass2}
% \end{figure}

% \bmeta Note the restriction to flat parameters\emeta
% We abbreviate $q\ M_1\dots M_{i-1} \ x\ M_{1+1}\dots M_{n}$ in $q \ 
% \ol{M_{x}^{i}}$.  Whenever we use this notation we will always assume
% that the type of $x$ is relevant to $Q$.
% For every $x\hastype A\in\GG$ relevant to $Q$ and for every $i$
% such that $x\in Q_{\mid_i}$, define:
% \beq
% \gf\mnota(D)=\BAnd D'\mid \gfq\mnotxi(D)=D'\eneq
% and
% \[
% \begin{array}{c}
% \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
%       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
%     \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop
% %\ga\vd\mnotg(G)=G'
% }{\begin{array}{l}
% \gfq\mnotxi  (q\ \Mn)=
%     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%      \neg q\ \ol{Z^i_x}\If M_j\neqd Z_j)
% %    \mbox{}\And (\neg q\ \Mn\If G')
%    \end{array}}{\mnotxi\atm}
%     \end{array}
%     \]
We concentrate on rules $\mnota\top$ and $\mnota\Imp$.
The notation $\zi$ is an abbreviation for\\
$ Z_1\dots Z_{i-1}\ \ex\ Z_{i+1}\dots Z_n$, where the $Z$'s are fresh
logic variables; similarly for $\zij$. The main loop goes as follows:

\begin{itemize}
    \item Choose a parameter $x\oftp a\in\GG$.
    \item Propagate $\ex$ in every `odd' position.
    \item Locate a type $A_i$ such that $x$ is relevant to $Q$ at $i$:
      \begin{itemize}
      \item Complement $D$ \wrt $x$ and $i$.
      \item Repeat for every relevant position $i$.
      \end{itemize}
    \item Repeat for every  $x$.
%    \item Special case: if no $x$ is relevant, the trivial program is
%      returned.
\end{itemize}


% The judgment is not optimized since if $M_j$ is
% essentially existential, an unsatisfiable clause is built; moreover,
% if it is a ground term, we add a disequation, rather then computing
% the term complement. We can perform constraint simplification in a
% separated phase, see Section \ref{sec:simplify}.
Rule $\mnota\Imp$ is the most complicated one: fixed a parameter $x$,
there are two ways in which an atomic assumption $q\ M_1\dots
M_{i-1}\ \ex\ M_{i+1}\dots M_n$, needs to be complemented. First, any
atom with same head with a term  $N_j\equiv\ex$ for $i\not=j$ is in the complement of the
former. Moreover, since they do differ in one coordinate, we may as
well leave open every other term. This is encoded in rule $\mnotr$. Of
course, we have to make sure that $N_j$ is not flex and that the type
is appropriate. Since $x$ is passed as a parameter, the $\GG\vd
sh(x,A)$ judgment builds a shallow parameter expression as required by
the type of the position in $q$ where it ought to occur.

Secondly, we have to take into account the case $M_i\equiv\ex$: here
we can build a set of complementary facts by pivoting on $\ex$ and
making another position different.
% by discriminating on $M_j$.
% If the latter is another SPE (rule $\mnotxi\GG$) the best we can do
% introduce a disequation; the SPE, say $e_y$ is replaced by a new
% local existential variable say $Z$ and the correspondent disequation
% $Z\neqd e_y$ is added to the body, while as before the rest of the
% term is left open, keeping $\ex$ as a pivot.
%  If on the other hand $M_j$ is a constructor or a flex term (rule $\mnotxi$),
Luckily, we can achieve this via a call to term complementation and
build a set of complementary facts similarly to clause
complementation.  The difference is that we pass to term
complementation, as a context, the set of parametric bound variables.
Finally, both processes are repeated for every $M_i$.

Notice the different treatment of the trivial clause $\top$ by rules
$\mnotd\top$ and $\mnota\top$: if no parameter has been assumed, then
$\top$ truly stands for the empty predicate definition and its
complement is the universal definition $\perp$.
% Notice that in this case,
%by definition of allowed program, $\cD$ must be empty as well. 
If, on the other side $\GG$ is \emph{not} empty, it means that
$\top_q$ has been introduced during the $\top$-normalization
preprocessing phase and has been localized to the predicate $q$.  Here
we need to construct a new negative assumption \wrt $q,x,i$ in case
$\top_q$ is the only dynamic definition of $q$. As $\top_q$ carries no
information at all concerning $q$, the most general negative
assumption is added. This is accomplished again by rule $\mnotr$,
where we make the convention to view $\top_q$ as a degenerate case of
$q\ \Mn$ where the sequence $\Mn$ is empty (and thus the condition
trivially satisfied).



\smallskip The remaining (common) rules for static and dynamic clause
complementation simply recur on the program respecting the duality of
conjunction and disjunction \wrt negation.  This a somewhat delicate
point and therefore we discuss it in some details.  Intuitively, negative
clauses stemming from the complement of the definition of
a predicate need to be considered simultaneously.  In fact, if an goal
is unprovable from its definition, then its negation must be provable
from the complement of each clause of its definition; symmetrically if
it is provable, then its negation must be unprovable from the
complement of at least one.  What we have described coincides the
operational semantics of an operator, which works exactly as
disjunction.  This is arguably at odd with the commonly held
goal-oriented interpretation of the sequent calculus as uniform
proofs, since case analysis makes the latter incomplete \wrt minimal
logic (but see \cite{Nadathur95lics} for ways to incorporate the
former in the framework of uniform proofs).
%First,
%we remark that the $\tensor$ is available uniquely as a program
%constructor and can therefore be used only in the focusing phase of
%deductions; i
In Section \ref{ssec:tensor} we will show how to
`compile away' all occurrences of $\tensor$ in clauses. This is an \ho
equivalent of the intersection operator `@' described in \cite{Bar90} and 
 will restore completeness of uniform proofs
\smallskip

Goal complementation, that is the judgment $ \mnotg(G)$ depicted in
Figure \ref{fig:notgoal} is straightforward, since it only brings the
body into a normalized format; namely, in what we may call
\emph{parametric negation normal form}, to stress the distinction from
classical negation normal form or even from negation normal form in
constructive logics as extension of intuitionism with strong negation
\cite{Nelson49}.  This re-iterates the problem with strong negation we
have hinted in Section \ref{sec:completion}; negation is pushed inward
but jumps over parametric-hypothetical judgments to respect the
operational interpretation of unprovability.

\newcommand{\gavd}{\GG\vd}
\begin{figure}
    \[
    \begin{array}{c}
      \ianc{}{\gavd\mnotg (\top)  =  \perp}{\mnotg\top}\qquad
        \ianc{}{\gavd\mnotg (\perp)  =  \top}{\mnotg\perp}\vsk
      \ianc{}{\gavd\mnotg(\vM \eqd \vN)= (\vM \neqd \vN)}{\mnot\eqd}\qquad
      \ianc{}{\gavd\mnotg(\vM \neqd \vN)= (\vM \eqd \vN)}{\mnot\neqd}\vsk
        \ianc{}{\gavd\mnotg (Q) =  \neg Q}{\mnotg At}\vsk
      \ianc{\GG,y\oftp a \vd\mnotg([y/x]G)=[y/x]G'}{\gavd\mnotg
        (\PI{x}{a}G)  =  \PI{x}{a}G'}{\mnotg\Pi^y}\vsk
        \ibnc{\gavd\mnotg (G_{1})= G_1'}{\gavd\mnotg (G_{2})= G_2'}{\gavd\mnotg
        ( G_{1}\And G_{2})=G_1'\Or G_2'}{\mnot\And}\vsk
       \ibnc{\gavd\mnotg (G_{1})= G_1'}{\gavd\mnotg (G_{2})= G_2'}{\gavd\mnotg
        ( G_{1}\Or G_{2})= G_1'\And G_2'}{\mnot\Or}\vsk
      \ianc{\gavd\mnotg(G) = G'}{\gavd\mnotg( D \Imp G) = D\Imp   G'}{\mnotg\Imp}
    \end{array}\]
    \caption{Goal complementation: $\gavd\mnotg(G)=G'$}
  \label{fig:notgoal}
\end{figure}

%This is why we need the \emph{augmentation} procedure described in the
%next Section (\ref{sec:aug}).

\smallskip
As a final remark, we note again that we must take the  complementation of a
program, seen as a conjunction,
\emph{predicate definition-wise} rather that \emph{clause-wise}. In
fact, it would be incorrect to simply negate a program as it would
introduce disjunctions rather than conjunction among predicate
definitions. The same remark applies to the `dynamic' program $\cD$. Formally,
given a fixed signature $\Sigma_{\cP}$ and  a program $\cP$:
\beq
\mnotd(\cP) & = &  \BAnd_{q\in\Sigma_{\cP}} \mnotd (\defp(q,\cP))
\eneq
Similarly for a (possibly run-time) context\fixed\ $\GG;\cD$:
\beq
\GG\vd\mnota(\cD) & = &  \BAnd_{q\in\Sigma_{\cP}} \GG\vd\mnota (\defp(q,\cD))
\eneq

Note that if $\ga$ is a run-time context, it consists of a conjunction
of blocks, \ie it has the form
$\GG'',\block{\GG'};\cD''\And\block{\cD'}$; in this case the
definition of $q$ consists of the conjunction of the definition for
\emph{every} block, namely:
$\GG'\vd\defp(q,\cD')\And\GG''\vd\defp(q,\cD'')$.  We abbreviate
$\mnotd(\defp(q))$ in $\defp(\neg q)$.  If $\cP^+$ is the source
program, we use $\cP^-$ for $\mnotd (\cP^+)$.

\smallskip Finally, we provide an example, which, even though is
somewhat a special case of the general procedure,  assumption
complementation being trivial,  it helps to clarify 
the rules for clause and goal complementation in isolation.
  We refer to the next
Section (\ref{sec:aug}) for more complex examples. We use
$\PI{F_1,F_2}{A} X$ as an abbreviation of
$\PI{F_1}{A}\PI{F_2}{A} X$.

\begin{Example}
\label{ex:closed}
A $\l$-expression is \emph{closed} if it has no occurrence of free
variables; let $z\hastype exp$ be a constant:
\beq
cloz & : & closed\ z.\\
clolam &: & \PI{E}{exp}closed\ (lam\ E) \If (\PI {x } {exp}\ (closed\ x 
\Imp closed\ (E\ x).)\\
cloapp &: & \PI{ E_{1}}{exp}\PI{E_{2}}{exp} closed\ (app\ E_{1} \ E_{2}) \If 
closed\ E_1 \And closed\ E_{2}.\\
\eneq

Now, $\defp(closed)= cloz\And clolam\And cloapp$. Note that $x\oftp
exp\vd \mnota(closed\ x)= \top$. Therefore:
 \beq \defp(\neg
closed)& =& \mnotd (cloz) \Or \mnotd (clolam) \Or \mnotd
(cloapp)
\eneq
where:
\beq
\mnotd (cloz) 
%& = &\mnotd (closed\ z)\\
            & = &\BAnd_{ N\in\cdot\vd\mnot(z)}\neg \Pi(closed\ N)\\
            & = &( \PI{F}{exp}\neg closed\ (lam\ F))\And
            \PI{F_1,F_2}{exp} \neg closed\ (app\ F_{1} \ F_{2}).
\vsk
\mnotd (clolam) 
%& = &\mnotd (closed\ lam\ E) \And
%\neg closed\ (lam\ E) \If \mnotg (\PI {x } {exp}\ (closed\ x \Imp closed\ 
%(E\ x))\\
              & = &\BAnd_{N\in\cdot\vd\mnot (lam\ E)}\Pi(\neg closed\ N)\And\\
&&
\PI{E}{exp}\neg closed\ (lam\ E) \If \mnotg (\PI {x } {exp}\ (closed\
x \Imp closed\  
(E\ x))\\
              & = &\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)).
\vsk
\mnotd (cloapp) 
%& = & \mnotd (closed\ (app\ E_1\ E_{2}))\And\\
%& & \PI{ E_{1}}{exp}\PI{E_{2}}{exp} 
%\neg  closed\ (app\ E_{1} E_{2}) \If \mnotg(closed\ E_1 \And closed\ 
%E_{2})\\
              & = & \BAnd_{N\in\cdot\vd\mnot  (app\ E_1\ E_2))} \neg
              \Pi(closed\ N)\And\\
& & \PI{E_1,E_2}{exp} \neg closed\ (app\ E_{1}\ E_{2}) \If \mnotg(closed\ E_1 \And 
closed\ E_{2})\\
              & = & \neg closed\ z\And (\PI{F}{exp}\neg closed (lam\
              F))\And\\
&& \PI{E_1,E_2}{exp}  \neg closed\ (app\ E_{1}\  E_{2}) \If
\neg closed\ E_1 \Or \neg closed\ E_{2}.
\eneq
\end{Example}

If you want to see the definition simplified, please skip to Example
\ref{ex:closedatensor} and the final result in Example  \ref{ex:closedfinal}.


