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


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
input 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,\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 {\ga \vd_{\Phi,\of{x}{A}}\ald([t/x]D)=[t/x]D'}{\gfald(\PIXA D)=\PIXA D'}{\ald\Pi}\vsk
    \ianc{\ga\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{}{\ga\vdf\alg(\top)=\top}{\alg\top}\qquad  %% CHECK!!
  \ianc{}{\ga\vdf\alg(\bot)=\bot}{\alg\bot}\vsk
  \ianc{\GG\vdf^{\!Q}\mnota(\cD)=\cD_{\neg}}
{\ga\vdf\alg(Q)
  =\cD_{\neg}\Imp Q}{\alg At}\vsk
\ianc{}{\cdot;\top_Q\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([x'/x]G)=[x'/x]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 correspondent 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}

% \begin{Lemma}
% \label{le:defnot}
% Let $\ga\vdf\mnota(\cD)=\cD_{\neg}$. Then $D\in def(q,\ga)$ iff $D\in
% def(q,\GG;(\cD\And\cD_{\neg})$.
% \end{Lemma}
% \begin{proof}
% A straightforward induction on the structure of $D$.
% \end{proof}

% We call a clause or a goal \emph{positive} if it contains no
% occurrence of a negative literal.

% \begin{Theorem}[Positive Conservativity]
% \label{thm:conservaug}
% If $G$ is positive, then $\ga\vdf G$ iff $\ga\vdf\alg(G)$.
% \end{Theorem}

% \begin{proof}
% We generalize this...
% \end{proof}



\subsection{Contexts Schema}

\label{sec:runtime}
\newcommand{\yd}{\stackrel{\tiny{D}}{\Longrightarrow}}
\newcommand{\yg}{\stackrel{\tiny{G}}{\Longrightarrow}}

\begin{figure}[htbp]
  \label{fig:schema}

\[
\begin{array}{c}
  \ianc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{\ga\vd X\yg\ga}{\yg At} \vsk
  \ibnc{ \GG;(\cD\And D)\vd G\yg S_1}{D\yd S_2}{ \ga \vd D\Imp  G\yg S_1\mid S_2}{ \yg\Imp}\vsk
  \ianc{(\GG,\xoa);\cD\vd G\yg S}{ \ga\vd\PIXA G\yg S}{ \yg\Pi}\vsk
 \ibnc{ \ga \vd G_1 \yg S_1}{\ga\vd G_2\yg S_2}
    { \ga\vd G_{1}\And G_{2}  \yg S_1\mid S_2}{ \yg\And}\vsk
 \ibnc{ \ga \vd G_1 \yg S_1}{\ga\vd G_2\yg S_2}
    { \ga\vd G_{1}\Or G_{2}  \yg S_1\mid S_2}{ \yg\Or}\vsk
\vsk
  \ianc{X\in\{\top,\perp\}}{X\yd \cdot;\top}{\yd At} \vsk
  \ianc{\cdot;\top\vd G\yg S_1} {(G\Imp  Q)\yd S_1}{ \yd\Imp}\vsk
% \ibnc{\cdot;\top\vd G\yg S_1}{D\yd S_2} {(G\Imp  D)\yd S_1\mid S_2}{ \yd\Imp}\vsk
% for more general G\Imp D
  \ianc{ D\yd S}{ \PIXA D\yd S}{ \yd\Pi}\vsk
 \ibnc{ D_1 \yd S_1}{D_2\yd S_2}
    { D_{1} \And D_{2}  \yd S_1\mid S_2}{ \yd\And}\vsk
 \ibnc{ D_1 \yd S_1}{D_2\yd S_2}
    { D_{1} \tensor D_{2}  \yd S_1\mid S_2}{ \yd\tensor}
 \end{array}
\]
  \caption{Schema context}
\end{figure}

\begin{Example}
\beq
def(copy)&\yd & \cdot;\top_{cp}\mid x\oftp exp,y\oftp exp;cp\ x\ y\And
(\PI{E'}{exp} \neg copy\ E'\ y\If x\neqd E')\And\\
&& (\PI{F'}{exp} \neg copy\ x\ F'\If y\neqd F')
\eneq
\end{Example}



\subsection{Call Graph}

\renewcommand{\ga}{Q}
\newcommand{\call}{\succ}

\[
\begin{array}{c} 
  \ianc{}{Q\vd Q'\yg Q\call Q'}{\yg\call}\qquad
 \ianc{X\in\{\top,\perp\}\mbox{ or (dis)eq}}{\ga\vd X\yg\cdot}{\yg At} \vsk
  \ibnc{Q\vd Q'\yg Q\call Q'}{Q'\vd Q''\yg Q'\call Q''}{Q\vd Q'\yg
  Q\call Q''}{\yg Cut}\vsk
  \ibnc{ Q\vd G\yg R_1}{D\yd R_2}{ \ga \vd D\Imp  G\yg R_1, R_2}{ \yg\Imp}\vsk
  \ianc{\ga\vd G\yg R}{ \ga\vd\PIXA G\yg R}{ \yg\Pi}\qquad
  \ianc{\ga\vd G\yg R}{ \ga\vd\exa G\yg R}{ \yg\Pi}\vsk
 \ibnc{ \ga \vd G_1 \yg R_1}{\ga\vd G_2\yg R_2}
    { \ga\vd G_{1}\And G_{2}  \yg R_1, R_2}{ \yg\And}\vsk
 \ibnc{ \ga \vd G_1 \yg R_1}{\ga\vd G_2\yg R_2}
    { \ga\vd G_{1}\Or G_{2}  \yg R_1, R_2}{ \yg\Or}\vsk
\vsk
  \ianc{}{\top\yd \cdot}{\yd \top} \qquad
  \ianc{}{\perp\yd \cdot}{\yd \perp} \vsk
  \ianc{Q\vd G\yg R} {(G\Imp  Q)\yd R}{ \yd\Imp}\qquad
  \ianc{ D\yd R}{ \PIXA D\yd R}{ \yd\Pi}\vsk
 \ibnc{ D_1 \yd R_1}{D_2\yd R_2}
    { D_{1} \And D_{2}  \yd R_1, R_2}{ \yd\And}\vsk
 \ibnc{ D_1 \yd R_1}{D_2\yd R_2}
    { D_{1} \tensor D_{2}  \yd R_1, R_2}{ \yd\tensor}
 \end{array}
\]

\begin{Example}
$$(a\If (b\If d)\Imp c)\And (c\If b)\yd a\call c,c\call b, b\call d,
a\call b, a\call d, c\call d$$
where the last three elements are obtained thru the Cut rule.
\end{Example}



