\documentclass{article}
\usepackage{lcom}
\usepackage{latexsym}
\usepackage{cdsty}
% \usepackage{prooftree}
\def\zzctdrawdotedge{\drawdotedge{4pt}0}
\def\ctabutborderlr{1em}
\def\ctabutbordertb{1ex}
%\newcommand{\ald}{\mbox{aug$_{\mbox{\tiny {\textrm{D}}}}$}}
%\newcommand{\alg}{\mbox{aug$_{\mbox{\tiny {\textrm{G}}}}$}}
\newcommand{\xoa}{x\oftp A}
\newcommand{\eq}{\eqd}
\newcommand{\yield}{\Rightarrow}
\renewcommand{\neq}{\not\eqd}
\newcommand{\alg}{aug_{\mbox{\tiny \textrm{G}}}}
\newcommand{\ald}{aug_{\mbox{\tiny \textrm{D}}}}
\newcommand{\prop}{\mbox{\textbf{prop}}}
\newcommand{\gfald}{\prv_{\!\Phi}\ald} %changed
\newcommand{\gfalg}{\Gamma;\cD\prv_{\!\Phi}\alg}
%\newcommand{\mnot}{{\rm Not\ }}
\newcommand{\mmnot}{\neg}
\newcommand{\mnots}{{\rm Not^* }}
%\newcommand{\mnotd}{{\rm Not}_{\mbox{$D$} }}
%\newcommand{\mnotg}{{\rm Not}_{{\mbox{$G$} }}}
\newcommand{\mnota}{{\rm Not}_{\mbox{$\alpha$} }}
\newcommand{\mmnota}{\neg_{\mbox{$\alpha$}}}
\newcommand{\mnotd}{{\rm Not}_{\rm D}  }
\newcommand{\mnotg}{{\rm Not}_{\rm G}  }
\newcommand{\ag}{\alpha_{\rm G}  }
\newcommand{\ad}{\alpha_{\rm D}  }
\newcommand{\PP}{\cP^{+}}
\newcommand{\PM}{\cP^{-}}
\renewcommand{\sp}{\vd_{\cP}}
\newcommand{\spp}{\vd_{\PP}}
\newcommand{\snp}{\vd_{\PM}\mnotg}
\newcommand{\sn}{\vd_{\PM}}
\newcommand{\PIXA}{\Pi x\!:\!A.\,}
%\newcommand{\fpp}{\nvd_{\PP}}
%\newcommand{\fnp}{\nvd_{\PM}\mnotg }
%\newcommand{\fn}{\nvd_{\PM}}
%\newcommand{\fp}{\nvd_{\cP}}
\newcommand{\cA}{{\cal A}}
\newcommand{\tensor}{\oplus}
\newcommand{\ga}{ } %change!
\newcommand{\gna}{ }%change!
%\newcommand{\vN}{\vec{N}}
%\newcommand{\vM}{\vec{M}}
% \newcommand{\PA}{\mid \cP\cup\cA\mid_{\GG}}
\newcommand{\PA}{\mid \cP\mid}
\newcommand{\eqd}{\stackrel{\cdot}{=}}
\newcommand{\neqd}{\not\stackrel{\cdot}{=}}
%\newcommand{\pix}{\Pi^{\cal X}}
\newcommand{\imm}{>\!\!>}
%\newcommand{\nimm}{>\!<}
\newcommand{\IP}{{\cal I}^{+}}
\newcommand{\IM}{{\cal I}^{-}}
\newcommand{\SP}{{\cal S}^{+}}
\newcommand{\SM}{{\cal S}^{-}}
%\newcommand{\less}{\preceq}
\newcommand{\gf}{\Gamma\vd_{\!\Phi}^{\! Q}}
\newcommand{\vdf}{\vd_{\!\Phi}}

\begin{document}
\section{Clause Complementation}
\label{sec:alge}


Source language: Let $\vM,\vN$ be sequences of \emph{simple} terms:
\beq
% Q & \bnfas & q\ \vM \bnfalt \neg q\ \vM \bnfalt \vM \eqd \vN\bnfalt \vM \neqd 
% \vN\\
Q & \bnfas & q\ \vM \bnfalt \neg q\ \vM \\
G & \bnfas & Q \bnfalt G_{1}\And G_{2}\bnfalt G_{1}\Or G_{2}\bnfalt D\Imp G\bnfalt
\Pi x:A.G\bnfalt \vM \eqd \vN\bnfalt \vM \neqd \vN\bnfalt
\top\bnfalt \perp\\
D & \bnfas &  \Pi x:A. D\bnfalt Q \If G\bnfalt D_{1}\And D_{2}\bnfalt \top\bnfalt
D_{1}\tensor D_{2}\bnfalt \perp \\
% remove Q , since facts re Q \If\top
% \cP & \bnfas & \cdot\bnfalt D,\cP
\eneq


Note that `facts' are represented, in a standardized way, by $ Q\If
\top$. Remark also that $\mnot$ is \emph{not} a connective, but a name
constructor for atomic formulae.

We now introduce in Figure \ref{fig:notd} and \ref{fig:notg} the
rules for (static) clause and goal complemetation. 
We  collect essentially existential variables in a pool $\Phi$
left here, for the moment, implicit. $\Pi(Q\If \top)$ denotes the
universal closure of the free variables in $Q$.
In $\mnotg\Pi$ the asterisk reminds of the eigenvariable condition on
$a$.

Note that rule $\mnotd\Imp$ is where all the work is done: a set of
negative facts is built via $\mnot (\vM)$, whose fresh free variables
are universally closed and the negative counterpart of the source
clause is obtained via complementation of the body. The original
quantification is retained thanks to rule $\mnotd\Pi$.

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

\begin{figure}[htbp]
  \label{fig:notg}
    \[
    \begin{array}{c}
      \ianc{}{\mnotg (\top)  =  \perp}{\mnotg\top}\qquad
        \ianc{}{\mnotg (\perp)  =  \top}{\mnotg\perp}\vsk
      \ianc{}{\mnotg(\vM \eqd \vN)= \vM \neqd \vN}{\mnot\eqd}\vsk
      \ianc{}{\mnotg(\vM \neqd \vN)= \vM \eqd \vN}{\mnot\neqd}\vsk
        \ianc{}{\mnotg (Q) =  \neg Q}{\mnotg At}\vsk
          \ianc{\mnotg([a/x]G)=[a/x]G'}{\mnotg (\PI{x}{A}G)  =  \PI{x}{A}G'}{\mnotg\Pi^*}\vsk
        \ibnc{\mnotg (G_{1})= G_1'}{\mnotg (G_{2}= G_2')}{\mnotg
        ( G_{1}\And G_{2})=G_1'\Or G_2'}{\mnot\And}\vsk
       \ibnc{\mnotg (G_{1})= G_1'}{\mnotg (G_{2})= G_2'}{\mnotg
        ( G_{1}\Or G_{2})= G_1'\And G_2'}{\mnot\Or}\vsk
      \ianc{\mnotg(G) = G'}{\mnotg( D \Imp G) = D\Imp   G'}{\mnotg\Imp}
    \end{array}\]
    \caption{Goal Complementation: $\mnotg(G)=G'$}
    \label{fig:gcomp}
\end{figure}

% \begin{Definition}[Head]
% \label{def:head}
% \beq
% head(\top_q) & = & \{q\}\\
% head(\perp_q) & = & \{ q\} \\
% head(q\ \vM\If G) & = & \{ q\} \\
% head(\neg q\ \vM\If G) & = & \{ \neg q\} \\
% head(\PI{x}{A} D) & = & \{ head(D)\} \\
% head(D_1\And D_2) & = & \{ head(D_1),head(D_2)\} \\
% head(D_1\tensor D_2) & = &\{ head(D_1),head(D_2)\} 
% \eneq
% \end{Definition}
\begin{Definition}[$def(q,D)$]
\label{def:head}
\beq
def(q,\top) & = & \top_q\\
def(q,\perp) & = &  \perp_q \\
def(q,q\ \vM\If G) & = &  q\If G \\
def(q,q'\ \vM\If G) & = &  \top_q \\
def(q,\PI{x}{A} D) & = &  \PIXA def(q,D) \\
def(q,D_1\And D_2) & = &  def(q,D_1)\And def(q,D_2) \\
def(q,D_1\tensor D_2) & = & def(q,D_1)\tensor def(q,D_2) 
\eneq
\end{Definition}


If $D=\cP$, \ie the underlying program seen as a conjunction of
clauses, we call $def(q,\cP)$ the \emph{static} definition of $q$. When
there are no dynamic assumptions, we avoid mentioning $\cP$.  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 will omit the subscript in $\top_q$ and
$\perp_{q}$, when it can be inferred by the context.  We also
implicitely absorb all the irrelevant occurrences of $\top_q$.

\smallskip

If $D\in def(q)$, we call $ \mnotd (D)$ the \emph{D-candidates}.
Candidates represent the potential negative contribution of each
clause: the `factual' part $\mnotd(Q ) $ motivates failure due to
clash with the head of $D$; the remainder $\mnotg (G)$ expresses
failure in the body, if any.  Note that the latter only brings the
body into what we may call \emph{parametric negation normal form}, to
stress the distinction from classical negation normal form or even
from normal form in constructive logics as extension of intuitionism
with strong negation.  Candidates from each clause in the definition
of a predicate need to be considered simultaneously.  In fact, if an
atom is unprovable from its definition, then its negation must be provable
from every $D$-candidate; symmetrically if it succeeds
then its complement must be unprovable from at least one candidate.  This is
abstractly accomplished by the operator $\tensor$, which thus works
similarly to disjunction.  Note that the former is available uniquely
as a program constructor and can therefore be used only in the
focusing phase of deductions; this  allows to preserve the
uniformity property.  In a second time, when describing the
operational semantics of the system, we will show how to `compile away'
those disjunctions through an \ho equivalent   of the intersection operator
`\@' described in \cite{MP90,Bar90}.

\smallskip
Fixed a signature $\Sigma_{\cP}$ and given a program $\cP$:
\beq
\mnotd(def(q)) & = & \bigoplus_{D\in def(q)} \mnotd(D)\\
\mnotd(\cP) & = &  \BAnd_{q\in\Sigma_{\cP}} \mnotd (def(q))
\eneq

We abbreviate $\mnotd(def(q))$ in $def(\neg q)$.   If $\PP$ is the source program, we
use $\PM$ for $\mnotd (\PP)$.


\begin{Example}
Let $def(even)$ be
\[
even(0)\And \PI{X}{nat} even(ss(X))\If even(X).
\]
Then $def(\neg even)$ is:
\[
\begin{array}{l}
\PI{Z}{nat} \neg even(s(Z))\tensor\mbox{}\\
(\neg even(0)\And\neg even(s(0))
\And \PI{X}{nat}\neg even(ss(X))\If \neg even(X).
\end{array}
\]
\end{Example}

\input{theproof}

\section{Augmentation}
\label{sec:aug}
\newcommand{\mnotxi}{\mnot^x_i}
\newcommand{\mnotxij}{\mnot^x_{i,j}}


We for now restrict to programs with
\bit
\item
flat parameters:\ie parameters can occur is assumption only at the 
top-level, 
%or in the body of lambda: $$e_x \bnfas x\bnfalt\lx e_x$$
\item
no mutual recursion
\item
second-order terminating clauses with the simultaneous subterm ordering.
\enit


Judgments:
\bit
\item
$\gf\mnota(\cD)$:
Complementation of the dynamic definitions in $\cD$ \wrt an atom $Q$ and input terms $\Phi$.
\item
$\gf\mnota(D)$:   Complementation of assumption
  $D$.
\item
$\gf\mnot^x(D)$:   Complementation of assumption $D$ \wrt $x$.
\item
$\gf\mnotxi(D)$:   Complementation of assumption $D$ \wrt $x$ and
  position $i$.
\item
$\gfald(D)$:   Augmentation of clause $D$.
\item
$\gfalg(G)$:   Augmentation of goal $G$
\enit
where,
\begin{itemize}
\item $\GG$ is a list of  parameters.
\item $\cD$ is a conjuction of  assumption.
\item $\Phi$ is a list of  \emph{input} evars.
\end{itemize}

We can think of assumption complementation, \ie complementation of
clauses that are by definition parametric in some $x$, as standard clause
complementation \wrt $x$. Informally, for an atomic assumption, say $ q\ M_1\dots M_{i-1}\ x\
M_{i+1}\dots M_n$, its complement can be taken as $\mnotd( q_x\
M_1\dots M_{i-1}\ M_{i+1}\dots M_n)$. We have to exercise then some
care to reposition the parameter we have pivoted on. 

We present two definitions: the first (eager complementation) computes
complemetation of ground terms via the auxiliary judgment $\gf\mnotxij
(D) \yield D'$, while the second (lazy complemetation) always
introduces disequations, even when they are unsatisfiable:

\begin{Definition}[Eager Assumption Complementation]
  \label{def:nota}
Let 
for  $0\leq j\leq n$, 
$Z_j$ be a fresh logic variable of correct type: the judgement
$\gf\mnotxi(D)=D'$ is realized by the following rules:
  \[
  \begin{array}{c}
% \ianc{}{\gf\mnotxi(\bot)  \yield   \bot}{\mnotxi\bot}\qquad NOT CLAUSES
    \ianc{head(Q)=q, \Sigma(q)= \An\Imp \prop}
    {\gf\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
%\mbox{no case for $\GG=\cdot$}\footnote{\mbox{does not make sense,
%    since $x\in\GG$}}\vsk 

  \ianc{p\not\equiv head(Q)}{\gf\mnotxi(p\ \Mn\If G)= \top_q}{\mnotxi At-nmr}\vsk
 %  \ianc{M_i \mbox{ \ \textrm{closed}}}
%   {\GG,x\oftp A\vdf \mnotxi\ q(M_1\mdots  M_i\mdots M_m, x,\Nn) \yield 
%     \BAnd_{N\in\cdot\vd\mmnot M_i}\Pi(\neg q(M_1\mdots N\mdots M_m,
%     x,\Nn)\If\top) }{\mnotxi\mmnot}\vsk
%   \ianc{M_i
% \mbox{ \textrm{no case for $M_j$ local gvar}}\vsk
%{\gf\mnotxi  q(M_1\mdots  M_i\mdots M_m,
%      x,\Nn)\yield \top}{\mnotxi At\_else}\vsk
  \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
    {\gf\mnotxi(D_{1}\And D_{2})  =  D_{1}'\tensor D_{2}'}{\mnotxi\And}\vsk
    \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
    {\gf\mnotxi(D_{1}\tensor D_{2})  =  D_{1}'\And
    D_{2}'}{\mnotxi\tensor}\vsk
  \ianc {\gf \mnotxi(D)= D' }{\gf\mnotxi(\PI{y}{B} D)= \PI{y}{B} D'}{\mnotxi\Pi}\vsk
    \ibnc{\gf\mnotxij(q\ \Mn)=D'}{\gf\mnotg(G) =  G'}{\gf\mnotxi(q\ \Mn\If G )=
    D'\And\neg q\ \Mn \If G'}{\mnotxi\If}\vsk\vsk

    \ianc{ \exists j\oftp 1\leq j\leq n, j\not\equiv i\,.\,M_j\in\GG\cup\Phi
   }{\gf\mnotxij  (q\ \Mn)\yield
    \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\If M_j\neqd Z_j}{\mnotxij Atc}\vsk
     \ianc{\exists j\oftp 1\leq j\leq n, j\not\equiv i}
     {\gf\mnotxij  (q\ \Mn)\yield\BAnd_{N\in\mnot(M_j)}\Pi(
    %\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} 
       \neg q\ Z_1\dots\ N\ \dots\ x\ 
       \dots Z_n)\If\top_q}{\mnotxij At}
  \end{array}
  \]
where
$$\gf\mnotxij(D)=\BAnd D'\mid \gf\mnotxij(D)\yield D'$$
\end{Definition}

In the rule $\mnotxij At$ we choose a term $M_j$ in the source atom
  such that it is either an input term or another parameter, in a CLP
  style, we add the relative disequation. Otherwise we compute its
  complement with a call to $\mnot$. In particular, if $M_j$ is an
  essentially existential variable, its complement is empty and
  $\top_Q$ is returned.

\begin{Definition}[Lazy Assumption Complementation]
  \label{def:lazynota}
The judgement
$\gf\mnotxi(D)= D'$ is realized by the following rules:
  \[
  \begin{array}{c}
    \ianc{head(Q)=q, \Sigma(q)= \An\Imp \prop}
    {\gf\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
    \ibnc{1\leq j\leq n,j\not = i}{\mnotg(G)=G'}{\begin{array}{l}
\gf\mnotxi  (q\ \Mn\If G)=
    \BAnd\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\If M_j\neqd Z_j\\
    \mbox{}\And \neg q\ \Mn\If G'\end{array}}{\mnotxi At}\vsk
  \ianc{p\not\equiv head(Q)}{\gf\mnotxi(p\ \Mn\If G)= \top_q}{\mnotxi At-nmr}\vsk
  \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
    {\gf\mnotxi(D_{1}\And D_{2})  =  D_{1}'\tensor D_{2}'}{\mnotxi\And}\vsk
    \ibnc{\gf\mnotxi(D_1) =  D_1'}{\gf\mnotxi(D_2) =  D_2 '}
    {\gf\mnotxi(D_{1}\tensor D_{2})  =  D_{1}'\And
    D_{2}'}{\mnotxi\tensor}\vsk
  \ianc {\gf \mnotxi(D)= D' }{\gf\mnotxi(\PI{y}{B} D)= \PI{y}{B} D'}{\mnotxi\Pi}
  \end{array}
  \]
\end{Definition}

Note that if $M_j$ is essentially existential, we create a
unsatisfiable constraint which will simplify in $\perp$.
\smallskip

Now collect the result of complementing $D$ \wrt $x$ for \emph{every}
position:
\beq
\gf\mnot^x(D)=\BAnd \gf\mnotxi(D) \mbox{ for every 
  $i$ such that } x\in Q_{\mid_i}
\eneq
Moreover, we do the same for every parameter which is relevant to
the type of $q$:
\beq
\gf\mnota(D)=\BAnd \gf\mnot^x(D)\mbox{ for every 
$x\oftp A\in\GG$ such that}\\ \mbox{
if $\Sigma(q)=\An\Imp\
prop$, then there is a $i$ such that }A_i\equiv A 
\eneq
Finally
\beq
\gf\mnota(\cD) & = &  \BAnd\gf \mnota (def(q,\cD))
\eneq


We briefly comment on the rules:
 \begin{itemize}
\item
The rule $\mnotxi\top$ allows to build a new negative assumption \wrt $q,x,i$
in case one is not present in the source program. As we have no
information at all \wrt $q$, the most general negative assumption is added.
\item If instead the atomic assumption considered is different (and
  later non mutually recursive) to the pivot atom, the trivial clause
  is added.
\item The rest of the rules simply recur on the structure of the assumption.
 \end{itemize}

 Remark that there are three-layers: once we have collected the complement of an assumption
\wrt to $x$ and a given position $i$, we need to do the same for every
other position $x$ can occur in the atom we are complementing
with. Once this is done, we proceed to do it again \wrt every
parameter in $\GG$ whose type (for the time being only of base type)
can be used in building argument to the pivot atom. Recall if there
are no assumptions returned at all, by convention the result is
$\top_q$, \ie the empty conjunction.

\renewcommand{\ga}{\GG;\cD}


We now turn to the judgments to augment a program: $\gfald(D)$ merely
recurs on the structure of clauses collecting in $\Phi$ a list of
imput terms and then calls $\ga\vdf\alg(G)$. The latter traverses a goal
collecting parameters in $\GG$ and assumptions in $\cD$. When it
reaches an atom, either it stops, as no parameter has been introduced,
or it passes $Q,x,\GG,\cD,\Phi$ to assumption complementation.

\begin{figure}[htbp]
  \[
  \begin{array}{c}
    \ianc{}{\gfald(\bot)  =  \bot}{\ald\bot}\qquad
    \ianc{}{\gfald(\top)  =  \top}{\ald\top}\vsk
    \ibnc{\gfald(D_1) = D_1'}{\gfald(D_2) = D_2 '}
    {\gfald(D_{1}\And D_{2})  = D_{1}'\And D_{2}'}{\ald\And}\vsk
    \ibnc{\gfald(D_1) = D_1'}{\gfald(D_2) = D_2 '}
    {\gfald(D_{1}\tensor D_{2})  = D_{1}'\tensor
    D_{2}'}{\ald\tensor}\vsk
  \ianc { \vd_{\Phi,\of{x}{A}}\ald(D)}{\gfald(\PIXA D)=\PIXA D'}{\ald\Pi}\vsk
    \ianc{\cdot;\cdot\vdf\alg(G) = G_a}{\gfald(Q\If G )= Q \If G_a}{\ald\If}
  \end{array}
  \]
  \caption{Clause Augmentation: $\gfald(D) = D'$}
  \label{fig:augd}
\end{figure}
%\newcommand{\vA}{\vec{A}}
%\newcommand{\vE}{\vec{E}}



\begin{figure}
\label{fig:augg}

\[
\begin{array}{c}
  \ianc{\GG\vdf^{\!Q}\mnota(\cD)=\cD_{\neg}}
{\ga\vdf\alg(Q)
  =\cD_{\neg}\Imp Q}{\alg At}\vsk
\ianc{}{\cdot;\top\vdf\alg(Q)=Q}{\alg At^\cdot}\vsk
%   \ibnc{ A\less \Sigma(Q)}{\GG,\xoa\vdf\mmnota(q\ M_1\dots
%   x\dots M_n)=D_{\neg}}
% {(\GG,x\oftp A);\cdot\vdf\alg(q\ M_1\dots
%   E\ x\dots M_n)=
% D_{\neg}\Imp (q\ M_1\dots E\ x\dots M_n)}{\alg At-sub}\vsk
%  \ianc{ A\not\less \Sigma(Q)}{(\GG,x\oftp A);\cdot\vdf \alg(q\ M_1\dots E\ x\dots M_n)=(q\ M_1\dots E\ x\dots M_n)}{\alg At-nonsub}\vsk
  \ianc{\GG;(\cD\And D)\vdf\alg(G)=G'}{\ga\vdf\alg(D\Imp  G)=D\Imp G'}{\alg\Imp}\vsk
  \ianc{(\GG,x\oftp A);\cD\vdf\alg(G)=G'}{\ga\vdf\alg(\PIXA G)= \PIXA G'}{\alg\Pi}\vsk
 \ibnc{\ga\vdf\alg(G_1) = G_1'}{\ga\vdf\alg(G_2) = G_2 '}
    {\ga\vdf\alg(G_{1}\And G_{2})  = G_{1}'\And G_{2}'}{\alg\And}\vsk
    \ibnc{\ga\vdf\alg(G_1) = G_1'}{\ga\vdf\alg(G_2) = G_2 '}
    {\ga\vdf\alg(G_{1}\Or G_{2})  = G_{1}'\Or
    G_{2}'}{\alg\Or}\vsk
 %  \ianc{}{\ga\vdf\alg(\vM\eqd\vN)=\vM\eqd\vN}{\alg\eqd}\vsk
%   \ianc{}{\ga\vdf\alg(\vM\neqd\vN)=\vM\neqd\vN}{\alg\neqd}
\end{array}
\]
\caption{Goal Augmentation: $\ga\vdf\alg(G)= G_a$}
\end{figure}



\newcommand{\qqquad}{\qquad\qquad}

\begin{Example}
Consider the \texttt{copy} program on $\l$-terms:
\beq
cpapp &:& \PI{E_1,E_2,F_1,F_2}{exp}\\
& & copy\ (app\ E_{1}E_{2}) \ (app\ F_{1}F_{2})\\
&& \qquad\If  copy\ (E_{1}F_{1})\\ 
&& \qquad\If copy\ (E_{2}F_{2})\\
cplam &:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& & copy\ (lam\ E) \ (lam\ F)\\
& & \qquad\If \PI
{x}{ exp}\PI{y}{exp} copy\ (x\ y)\\
& & \qquad\qquad\Imp copy\ (E\ x) \ (F\ y)
\eneq
The augmentation procedure calls $x,y\oftp exp\vd^{\! cp\
  Ex\ Fy} \mnota( cp\ x\ y)$, glossing over the context $\Phi$ which
is not active in this case. First $x,y\oftp exp\vd^{\! cp\
  Ex\ Fy} \mnot^x_1(cp\ x\ y)= (\PI{E'}{exp} \neg copy\ E'\ y\If
x\neqd E')$, secondly $x,y\oftp exp\vd^{\! cp\
  Ex\ Fy} \mnot^y_2(cp\ x\ y)= (\PI{F'}{exp} \neg copy\ x\ F'\If
y\neqd F')$, yielding:
\beq
\ald(cplam)&:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& &  copy\ (lam\ E) \ (lam\ F)\If \\
& & \qquad \PI{x}{exp}\PI {y}{ exp}\\
& & \qquad (\PI{E'}{exp} \neg copy\ E'\ y\If x\neqd E')\And\\
& & \qquad (\PI{F'}{exp} \neg copy\ x\ F'\If y\neqd F')\Imp\\
&& \qquad\qquad
 copy\ (x\ y) \Imp copy\ (E\ x) \ (F\ y)
\eneq
while of course, $\ald(cpapp)=cpapp$, as enforced by $\alg At^\cdot$. If
we had a version of $copy$ without coloring, \ie
\beq
cplam' &:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& & copy\ (lam\ E) \ (lam\ F)\If\\
& & \qquad \PI
{x}{ exp}  copy\ (x\ x)\\
& & \qquad\qquad\Imp copy\ (E\ x) \ (F\ x)
\eneq
Then we would get the  two calls to $x\oftp exp\vd^{\! cp\
  Ex\ Fx} \mnot^x_1(cp\ x\ x)= (\PI{E'}{exp} \neg copy\ E'\ x\If
x\neqd E')$ and  $x\oftp exp\vd^{\! cp\
  Ex\ Fx} \mnot^x_2(cp\ x\ x)= (\PI{F'}{exp} \neg copy\ x\ F'\If
x\neqd F')$ and the augmented clause:
\beq
\ald(cplam')&:& \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
& &  copy\ (lam\ E) \ (lam\ F)\If \\
& & \qquad \PI{x}{exp}\\
& & \qquad (\PI{E'}{exp} \neg copy\ E'\ x\If x\neqd E')\And\\
& & \qquad (\PI{F'}{exp} \neg copy\ x\ F'\If x\neqd F')\Imp\\
&& \qquad\qquad
 copy\ (x\ x) \Imp copy\ (E\ x) \ (F\ x)
\eneq
Take the typing clause for lambda terms:
\beq
oflam &:&  \PI{E}{exp\Imp exp}\PI{T1,T2}{tp}\\
&& of\ lam(E) \ arrow(T1,T2)\If\\
& & \qquad \PI{x}{exp} of\ x\ T1 \Imp  of\ E\ x\,T2
\eneq
As $T1$ is an input term, the corrispondent diseqution is inserted:
\beq
\ald(oflam) &:& \PI{E}{exp\Imp exp}\PI{T1,T2}{tp}\\
&& of\ lam(E) \ arrow(T1,T2)\If\\
& & \qquad \PI{x}{exp} of\ x\ T1 \Imp\\
& &\qqquad (\PI{T}{tp} \neg of\ x\ T\If T\neqd T1)\Imp\\
&&\qqquad\qquad  of\ E\ x\,T2.
\eneq

Consider now a predicate to perform instantiation of a binding
operator ( in the pattern fragment):
\beq
inlam & : & \PI {E}{exp\Imp exp} \PI {F} {exp} \\
& & inst\ (lam\ E) \ F \If\\
& &  \qquad\PI {x}{exp} (\PI {T}{exp} copy\ x\ T)\\
& & \qqquad  \Imp copy\ (E\ x)  \ F
\eneq
The call to $x\oftp exp\vdf^{\!inst\ Ex\ F}\mnot^x_1 (\PI {T}{exp}
copy\ x\ T)$ fails as the complement of $T$ is empty [the
unsatisfiable clause $\PI{T}{exp}\PI{Z}{exp} \neg cp\ x\ Z\If Z\neqd
T$] and thus the
augmentation is trivial.


Let us see how rule $\mnotxi\top$ enters the picture: consider the
\texttt{open} program
\beq
oplam &: & \PI{ E}{ exp\Imp exp} open\ (lam\ E)  \If\\
& & \qquad  \PI {x } {exp\Imp exp} open\ (E\
x)
\eneq
The judgment
$x\oftp exp;\top_{open}\vdf\alg( open\ Ex)$
triggers the rule $\mnotxi\top$, as $\Sigma(open)=exp\Imp\prop$ and thus $x\oftp exp\vdf^{\!open\
  Ex}\mnot^x_1(\top_{open})= \neg open\ x$:
\beq
\ald(oplam)&:&  \PI{ E}{ exp\Imp exp} open\ (lam\ E) \If  \\
& & \qquad \PI {x } {exp\Imp exp} \neg open\ x \Imp open\ (E\ x)
\eneq


Now consider $\Sigma = form,term\hastype type, all\hastype (term\Imp
form)\Imp form$ and the clause:
\beq
isdall & : & \PI{D}{form} isd\ (all\ D)\If \PI{x}{term} isd\ (D\ x)
\eneq
Here as $term\not\equiv form$, then $\ald(isdall)=isdall$ 
\end{Example}

\end{document}
\subsection{Run-time contexts}
\label{sec:runtime}


\[
\begin{array}{c}
  \ianc{X\in\{Q,\top,\perp\}\mbox{ or dis(eq)}}{\ag(X)\yield \cdot;\top_q}{\ag At} \vsk
  \ianc{ \ag(G)\yield \GG;\cD}{ \ag(D\Imp  G)\yield (\GG,\xoa);\cD}{ \ag\Imp}\vsk
  \ianc{\vdf \ag(G)\yield \GG;\cD}{ \ag(\PIXA G)\yield (\GG,x\oftp A);\cD}{ \ag\Pi}\vsk
 \ianc{ \ag(G_i) \yield \GG;\cD}
    { \ag(G_{1}\And G_{2})  \yield \GG;\cD}{ \ag\And}\vsk
  \ianc{ \ag(G_i) \yield \GG;\cD}
    { \ag(G_{1}\Or G_{2})  \yield \GG;\cD}{ \ag\Or}\vsk
 \ianc{X\in\{Q,\top,\perp\}\mbox{ or dis(eq)}}{\ad(X)\yield \cdot;\top_q}{\ad At} \vsk
  \ianc{ \ad(G)\yield \GG;\cD}{ \ad(D\Imp  G)\yield (\GG,\xoa);\cD}{ \ad\Imp}\vsk
  \ianc{\vdf \ad(G)\yield \GG;\cD}{ \ad(\PIXA G)\yield (\GG,x\oftp A);\cD}{ \ad\Pi}\vsk
 \ianc{ \ad(D_i) \yield \GG;\cD}
    { \ad(D_{1}\And D_{2})  \yield \GG;\cD}{ \ad\And}\vsk
  \ianc{ \ad(D_i) \yield \GG;\cD}
    { \ad(D_{1}\tensor D_{2})  \yield \GG;\cD}{ \ad\tensor}\vsk
 \end{array}
\]
\end{document}


