\chapter{Clause Complementation}
\label{ch:cc}

In this chapter we introduce the source language and its uniform proofs
system. Before formalizing the restriction to terminating programs, we
establish the fundamental notion of context schema. This allows to
enforce the \emph{Regular World Assumption} (RWA), on which clause
complementation is built. Finally, we discuss how to give an
operational semantics to our system.
\renewcommand{\SP}{}
\renewcommand{\SM}{}
\renewcommand{\IP}{}
\renewcommand{\IM}{}
%\newcommand{\semic}{::}
\newcommand{\semic}{}
\renewcommand{\tensor}{\Or}
\renewcommand{\emp}{\cdot;\top}
\section{The Logic}
\label{sec:logic}

We will use the following slightly unusual source language.
 Again, we fix a signature $\Sigma$ in advance
which would otherwise clutter the presentation; let $\vM,\vN$ be
sequences of \emph{simple} terms:
\[ \begin{array}{rrcl}
\mbox{\textit{Atoms}}& Q & \bnfas & q\ \vM \bnfalt \neg q\ \vM \\
\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\bnfalt\\%\exa G\\
\mbox{\textit{Clauses}}& D & \bnfas & \top\bnfalt\perp\bnfalt Q\bnfalt D \If
G\bnfalt D_{1}\And D_{2}\bnfalt D_{1}\tensor D_{2}\bnfalt\PIXA D
\end{array}
\]
First and foremost, we restrict ourselves to clauses of at \emph{most}
third-order, that is we allow HHF which only make Horn assumptions.
This simplifies the presentation of the complement algorithm, but it
is not an unsurmountable obstacle; we comment on this and other
restrictions in the Conclusions (Chapter~\ref{ch:end}). Differently
form standard presentation of HHF, we do not allow existential goals.
This rules out open queries and local variables, as well as  spares us from the heavy machinery of
\emph{mixed prefixes}~\cite{Miller92jsc}.  On the other hand, we allow
disjunction between clauses, equality and inequality. While
disjunction among clauses will be eliminated, inequalities will
survive, although they will always be solvable at run-time by a simple
syntactic check, as we will see in due time (Section~\ref{sec:ref}).
 % (in)equalities containing parameters will
% not. 
 This  simplifies their treatment  in type-theoretic languages such as \emph{Twelf},
where, in general,  (in)equalities should be viewed as types inhabited
by appropriate proof terms. 
% However, since (in)equalities will be treated exclusively as
% \emph{constraints}, we will not need a complicated treatment such as in
% Martin-L\"of's type theory.
The tokens $\top,\perp$ may be decorated with a predicate symbol, as
explained in Subsection~\ref{ssec:top} and Definition~\ref{def:defq}.
Finally, we remark that `$\neg$' is \emph{not} a connective, but a
name constructor for atomic formulae.

\[ \begin{array}{rrcl}
\mbox{\textit{Parameter Contexts}}& \GG & \bnfas &\cdot\bnfalt\GG, \xoa\\ 
\mbox{\textit{Assumptions}}& \cD & \bnfas &\top\bnfalt\cD\And D
\end{array}
\]
We call a pair of concrete context and assumption $\GG;\cD$, such that
all parameters occurring in $\cD$ are mentioned in $\GG$, 
 a \emph{(run-time) context}. We make the
usual conventions on contexts, in particular we
avoid mentioning the leading $\cdot$ and $\top$ elements.
% \begin{Definition}[$\defp(q,D)$]
% \label{def:defq}
% \[\begin{array}{rclr}
% \defp(q,\top) & = & \top_q\\ 
% \defp(q,\perp) & = &  \perp \\
% \defp(q,Q\If G) & = &  Q\If G&\mbox{if } Q\equiv q\ \vM \\
% \defp(q,Q\If G) & = &  \top&\mbox{otherwise} \\
% \defp(q,\PI{x}{A} D) &= &  \PIXA \defp(q,D) \\
% \defp(q,D_1\And D_2) & = &  \defp(q,D_1)\And \defp(q,D_2) \\
% \defp(q,D_1\tensor D_2) & = & \defp(q,D_1)\tensor \defp(q,D_2)
% \end{array}\]
% \end{Definition}

% If $D=\cP$, \ie the underlying program (seen as a conjunction of
% clauses), we call $\defp(q,\cP)$ the \emph{static} definition of $q$. If
% $D$ is a conjunction of run-time assumptions, we call the latter the
% \emph{dynamic} definition of $q$.  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$ denotes the universal definition for $q$.  
We use the notation $D\inn\cP\And\cD$ to indicate that $D$ is a
top-level conjunct in the $\cP$ or in $\cD$.


% We will also need to establish when a clause belongs to a definition;
% this can be established as follows:

\smallskip We now introduce the uniform proofs judgments for
provability and denial in Figure \ref{fig:sf} and for immediate
implication and denial in Figure \ref{fig:imm}. While the system for
denial is introduced for technical reasons, namely the proof of the
Exhaustivity Theorem~\ref{thm:exhau}, it is of independent interest,
since it provide evidence (that is proof terms) for non-provability.
A similar system was presented in~\cite{Harland91phd}, although in a
simplified setting without parametric judgments.  We remark that the
systems for denial will instead not be needed in the proof of exclusivity
(Theorem \ref{thm:exclu}).

Due to the presence of
`$ \tensor$' as a clause constructor, uniform proofs are \emph{not}
complete \wrt intuitionistic logic. We will remedy this situation in
Section \ref{ssec:tensor}. The rules are depicted (when possible) in
two columns where every row displays a positive rule and its negative
counterpart.
\[
\begin{array}{ll}
\ga\sp G & \mbox{Program $\cP$ and assumption $\cD$ uniformly entail
  $G$.}\\
\ga\fp G & \mbox{Program $\cP$  and assumption $\cD$ uniformly deny $G$.}\\
\ga\sp D \imm Q & \mbox{Clause  $D$ from  $\cP\And\cD$ immediately entails
  atom $Q$.}\\
\ga\fp D \imm Q & \mbox{Clause  $D$ from $\cP\And\cD$
  immediately denies atom $Q$.}
\end{array}
\]

\begin{figure}
\[
\begin{array}{c}
% |-
 \ianc{}{\ga\sp\top}{\vd\top}\qquad\ianc{}{\gna\fp \perp}{{\nprv}\perp}\vsk
\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{{\prv\eqd}}\qquad
\ianc{\vM \not = \vN}{\ga\fp \vM \eqd \vN}{{\nprv\eqd}}\vsk
\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{{\prv\neqd}}\qquad
\ianc{\vM  = \vN}{\ga\fp \vM \neqd \vN}{{\nprv\neqd}}\vsk
\ibnc{\ga\sp G_1}{\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{{\prv}\And}
\qquad
\ibnc{\ga\fp G_1}{\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{{\nprv}\Or}
\vsk
\ianc{\ga\sp G_1}{\ga\sp G_{1}\Or G_{2}}{{\prv\Or_1}}
\qquad
\ianc{\ga\fp G_1}{\ga\fp G_{1}\And G_{2}}{{\nprv\And_1}}\vsk
\ianc{\ga\sp G_2}{\ga\sp G_{1}\Or G_{2}}{{\prv\Or_2}}
\qquad
\ianc{\ga\fp G_2}{\ga\fp G_{1}\And G_{2}}{{\nprv\And_2}}
\vsk
%\ibnc{\GG\vd t\hastype A}{\ga\sp[t/x]G}{\ga\sp\exa G}{\vd\exists}
%\vsk
%\ibnc{\mbox{\rm for all $n$ }\GG\vd n\hastype A}{\gna\fp[n/x] G}{\gna\fp\exa G}{\nvd\exists}
%\vsk
% HORN --> HHF
 \ianc{\GG;(\cD\And D) \sp G}{\ga\sp D \Imp G}{{\prv} \Imp}
\qquad
\ianc{\GG;(\cD\And D )\fp G}{\ga\fp D \Imp G}{{\nprv} \Imp}
\vsk
\ianc{(\GG,y\oftp A);\cD\sp[y/x]G}{\ga\sp \PIXA G}{{\prv} \Pi^y}
\qquad
\ianc{(\GG,y\oftp A);\cD\fp[y/x]G}{\ga\fp \PIXA G}{{\nprv} \Pi^y}\vsk
%\ibnc{D\inn\cP\And\cD}{\ga\sp D\imm Q}{\ga\sp Q}{\vd\atm}
%\qquad
%\ibnc{\mbox{for every }D\inn\cP\And\cD}{\gna\fp D \nimm Q}{\ga\fp Q}{\nprv\atm}
 \ianc{ \ga\sp \cP\And\cD \imm Q}{\ga\sp Q}{{\vd {\rm atm }}}
 \qquad
 \ianc{ \gna\fp \cP\And\cD \nimm Q}{\ga\fp Q}{\nprv {\rm atm }}\vsk

\end{array}
\]
\caption{Provability and denial}
\label{fig:sf}
\end{figure}

\begin{figure}
%\boxarray{
\[
\begin{array}{c}
% immediate >>
\ianc{}{\ga\sp\perp\imm  Q}{\imm\perp}\qquad
\ianc{}{\ga\fp \top\nimm Q}{\notimm \top}\vsk
%\ianc{\vN = \vM}{\ga\sp q\ \vN \imm q\ \vM}{\imm\rm \atm}\qquad
%\ianc{\vN \neq \vM}{\ga\fp q\ \vN \nimm q\ \vM}{\notimm{\rm atm}}\vsk
\ibnc{ \GG\vd t\hastype A}{ \ga\sp  [t/x]D \imm
  Q}{\ga\sp \PIXA D \imm Q}{\imm\Pi}\vsk
\ibnc{\mbox{for all $n$ $\GG\vd n\hastype A$} }{ \ga\fp [n/x]D \nimm
  Q}{\ga\fp \PIXA D \nimm Q}{\notimm\Pi}\vsk
\ianc{\ga\sp D_{1}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{\imm{\And_1}}\qquad
\ianc{\ga\fp D_{1}\nimm Q}{\ga\fp D_{1}\tensor D_{2}\nimm
  Q}{\notimm{\tensor_1}}\vsk
\ianc{\ga\sp D_{2}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{\imm{\And_2}}\qquad
\ianc{\ga\fp D_{2}\nimm Q}{\ga\fp D_{1}\tensor D_{2}\nimm Q}{\notimm{\tensor_2}}\vsk
\ibnc{\ga\sp D_{1}\imm Q}{ \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor D_{2}\imm 
Q}{\imm\tensor}\vsk
\ibnc{\ga\fp D_{1}\nimm Q}{\ga\fp D_{2}\nimm Q}{\ga\fp D_{1}\And D_{2}\nimm
Q}{\notimm\And}\vsk
\ibnc{\ga\sp D\imm Q}{\ga\sp  G}{\ga\sp  D\If G \nimm 
  Q}{\imm\Imp}\vsk
\ianc{\ga\fp D\imm Q}{\ga\fp  D\If G \nimm 
  Q}{\notimm{\Imp_1}}\qquad
\ianc{\ga\fp G}{\ga\fp  D\If G \nimm 
  Q}{\notimm{\Imp_2}}
% \ibnc{\ga\sp\vN\eqd\vM}{\ga\sp G}{ \ga\sp ( q\  \vN\If G) \imm q\
%   \vM}{\imm\Imp}
% \vsk
% \ibnc{\ga\fp \vN\neqd\vM}{\fp G} {\ga\fp (q\ \vN\If G) \nimm q\ \vM}{\notimm{\Imp_2}}
% \vsk
% \ianc{\ga\fp \vN\eqd\vM}{\ga\fp (q\ \vN\If G) \nimm q\ \vM}{\notimm{\Imp_1}}
\end{array}
\]
\caption{Immediate entailment and denial}
\label{fig:imm}
\end{figure}

We briefly comment on the rules: the (in)equalities rules simply
mirror the object logic symbols $\eqd,\neqd$ in meta-level
(in)equality.  The denial rules for implication and universal
quantification reflect the operational semantics of unprovability that
we have discussed earlier.  Note that $\notimm\Pi$ 
%and $\nvd\exists$
is an  infinitary rule, due to the meta-linguistic extensional universal
quantification on all terms.  Rule $\notimm\Pi$ must be read as: for
every well-typed term $n$ in parameter context $\GG$, $\PIXA D$
immediately denies $Q$ if so does $[n/x]D$.
% Analogously for $\nvd\exists$. 
 Rules $\vd\Pi,\nvd\Pi$ are instead parametric in the
new eigenvariable, say $y$; the $()^y$ superscript reminds us of the
parameter condition on $y$, e.g.\ that $y$ does not occur free in
$\ga$ nor in $G$. We will use this notation in any other parametric
rule.

Differently from the latter, we will also use \emph{global}
eigenvariables, say $u$ (see for example rule $\yd\Pi$ in Figure
\ref{fig:topnormal}); this expresses the fact that in those rules the
relation holds for \emph{any} term; those parameters are therefore
analogous to logic variables. We will pervasively utilize this
notation; however, to avoid notational clutter, when possible we shall
not keep an explicit record of global parameters, but we agree to
implicitly gather them in a pool $\Phi$, which we can access when
needed, in particular to type-check substitutions, see
Section~\ref{sec:runtime}.


For the sake of conciseness we will often use in this thesis
the following rule schema, where $\cJ(X,R)$ is a judgment involving a
token $X$ ranging over a set $\cT$ and a relation $R$:
$$\ianc{X\in \cT}{\cJ(X,R)}{R\ X}$$

% \subsection{Substitutions}
% \label{subs:subst}

%%Since we have introduced meta-level extensional quantification we will
%% Given the mixed quantifier structure of HHF, we need to talk about
%% \emph{valid substitutions}:
%% %moreover, they ought to respein a framework
%% %where the universal quantifier is interpreted intensionally, 
%% soundness requires the latter not only to be well-typed, but also to
%% correctly deal with quantifier alternations, in so that substitution
%% terms for essentially existential variables must respect the eigenvariable
%% restriction brought in by parametric rules.
%% We do not develop the usual theory of well-typed substitutions; we
%% simply assume that $t$ can be given the type associated to $x$.

% We will need the notion of \emph{well-typed substitutions}:

% \[ \begin{array}{rrcl}
% \mbox{\textit{Substitutions}}& \sigma & \bnfas \epsilon\bnfalt \sigma,t/x
% \end{array}
%% Substitutions can be  well-typed as follows:
%% \beq
%% \ianc{}{\cdot\vd\epsilon\hastype\cdot}{\epsilon\cdot}\qquad
%% \ibnc{\GG\vd t\hastype
%%   A}{\GG\vd\sigma\hastype\Phi}{\GG\vd\sigma,t/x\hastype(\Phi,x\hastype
%%   A)}  {\sigma\Phi}
%% \eneq

% For $\sigma=\sigma',t/x$, we say that $x$ is \emph{defined} in $\s$.
% We require all variables defined in a substitution to be distinct: we
% use dom($\s$) for the set of variables defined in $\s$ and cod($\s$)
% for the variables occurring in the substituting terms. We assume them
% to be disjoint.  



%%\medskip


%% It is apparent that the non-monotonic nature of denial falsifies
%% weakening in general; there is one special case, though, which holds
%% and is required in the proof of Theorem \ref{thm:topnormalnvd}:

%% \begin{Lemma}[Negative $\top$-Weakening]
%% \label{le:vdweak}
%% \renewcommand{\ga}{ \Gamma;\q\cD }
%% \mbox{}
%% \ben
%% \item  If $\foq\ga\nvd \q G$, then
%% \ben
%% \item  $(\GG,\xoa);\q\cD\nvd\q G$.
%% \item  $\GG;(\cD\And \top)\nvd\q  G$.
%% \enen
%% \item If $\ga\nvd\q  D\imm\q  Q$, then 
%% \ben
%% \item $(\GG,\xoa);\cD\nvd\q  D\imm\q  Q$.
%% \item  $\GG;(\cD\And \top)\nvd\q  D\imm\q  Q$.
%% \enen
%% \enen
%% \end{Lemma}
%% \begin{proof}
%% A straightforward induction on the given derivations.
%% \end{proof}
%% \end{document}

\subsection{$\top$-Normalization}
\label{ssec:top}
\newcommand{\ygt}{\stackrel{\mbox{\tiny{$G^{\top}$}}}{\Longrightarrow}}
\newcommand{\ydt}{\stackrel{\mbox{\tiny{$D^{\top}$}}}{\Longrightarrow}}
\newcommand{\tend}[1]{ #1^{\top}}
\newcommand{\teng}[1]{ #1^{\top} }
% \newcommand{\teng}[1]{\mid #1 \mid_{G} }
% \newcommand{\tenx}[1]{\mid #1 \mid_{\Pi} }

 
We show in this section how to put every program in a normalized
format \wrt assumptions so that every goal in the scope of an
universal quantifier depends on some assumption, possibly the trivial
clause $\top$. This has also the effect of `localizing' the trivial
assumption to its atom, a property will be very useful while
performing augmentation, see Section \ref{sec:aug}.  % Some caution must
% be exercised to discriminate whether the universal quantifier
% contributes or not to the provability of the goal in its scope.
 
We first state some basic properties of provability.

\begin{Lemma}[Weakening]
\label{le:vdweak}
\mbox{}
\ben
\item  If $\ga\vd G$, then:
\ben
\item  $(\GG,\xoa);\cD\vd G$.
\item  $\GG;(\cD\And D)\vd G$.
\enen
\item If $\ga\vd D\imm Q$, then:
\ben
\item $(\GG,\xoa);\cD\vd D\imm Q$.
\item  $\GG;(\cD\And D')\vd D\imm Q$.
\enen
\enen
\end{Lemma}
\begin{proof}
  A straightforward mutual induction on the given derivations.
\end{proof}

In the proof of Theorem \ref{thm:topnormalvdrl} we will need the
following form of Strengthening:

\begin{Lemma}[$\top$-Strengthening]
\label{le:topstren}
\mbox{}
\ben
\item If $\GG;(\cD\And\top)\vd G$, then $\ga\vd G$.
\item If $\GG;(\cD\And\top)\vd D\imm Q$, then $\ga\vd D\imm Q$.
\enen
\end{Lemma}
\begin{proof}
  By an easy mutual induction on the structure of the given
  derivations.
\end{proof}


%\smallskip

Normalization is realized in Figure \ref{fig:topnormal} by the two
judgments $D\ydt\tend{D}$ and $\ga\vd G\ygt\teng{G}$. The only
interesting case is when we reach an atomic goal: if no parameter has
been introduced, the clause does not require any normalization. 
%  Similarly
% if $\cD$ is non-trivial. If $\GG$ is non-empty, there is the
% possibility that the type of the introduced parameter  is
% \emph{subordinate} \cite{Virga99phd} to the type of the atom
% considered. In this case there is no need for us to introduce the
% trivial assumption. 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$. Thus
% we $\top$-normalize $Q$ only when there is a parameter in the context
% which is relevant to $Q$.
If $\ga$ is non-empty, we adopt a brute-force approach and add the
trivial clause for \emph{every} predicate in the signature. This is
largely unnecessary, but it gives a very simple account of mutually
recursion, without an explicit appeal to a call graph. As a matter of
fact, we would really need to $\top$-normalize an 
 atom $Q$ with the trivial clause for every predicate that
is mutually recursive to $Q$ and such that the type of the parameter in the
context is not \emph{subordinate} \cite{Virga99phd} to the type of
$Q$.
% considered. In this case there is no need for us to introduce the
% trivial assumption.
On the other hand Theorems \ref{thm:topnormalvdlr} and
\ref{thm:topnormalvdrl} ensures, as obvious, that this program
transformation is harmless, since it preserves provability and
denial. Moreover, we will engineer the rule for clause complementation
so that the irrelevant $\top_q$ will be inactive. We will remove those
irrelevant augmentations in a final pass (Section~\ref{ssec:tensor}).


\begin{Example}
Consider the lambda clause in the \texttt{open} program:
\beq
oplam &: & \PI{ E}{ exp\Imp exp} open\ (lam\ E)  \\
& & \qquad\If  \PI {x } {exp} open\ (E\ x).
\eneq
%As $x\oftp exp$ is relevant to $open\oftp exp\Imp\prop$,
$oplam\ydt\tend{oplam}$, \ie
\beq
\tend{oplam}&:&  \PI{ E}{ exp\Imp exp} open\ (lam\ E)   \\
& & \qquad \If(\PI {x } {exp} \top_{open} \Imp open\ (E\ x)).
\eneq
Consider this fragment of code involving two  mutually recursive predicates:
\beq
qlam& : &   \PI{ E}{ exp\Imp exp} q\ (lam\ E)  \\
& & \qquad\If  \PI {x } {exp} p\ (E\ x).\\
papp & : & \PI{E_1}{exp}\PI{E_2}{exp} p\ (app\ E_1\ E_2)\\
& & \qquad\If q\ E_1\And p\ E_2.
\eneq
Then:
\beq
\tend{qlam}& : &   \PI{ E}{ exp\Imp exp} q\ (lam\ E)  \\
& & \qquad\If  (\PI {x } {exp} \top_p\And\top_q \Imp p\ (E\ x)).
\eneq
% Now consider $\Sigma = form,term\oftp type, all\oftp (term\Imp
% form)\Imp form,isd\oftp form\Imp\prop$ and the clause:
% \beq
% isdall & : & \PI{D}{term\Imp form} isd\ (all\ D)\\
% & & \qquad \If\PI{x}{term}  isd\ (D\ x).
% \eneq
% Here as $term\not\equiv form$, then $x\oftp term$ is \emph{not}
% relevant to $isd\oftp form\Imp\prop$ and $\tend{isdall}\ydt isdall$.
\end{Example}
In examples, we will not mention inactive $\top$ clauses.

\begin{figure}
\[
\begin{array}{c}
  \ianc{X\in\{\top,\perp\}\mbox{ or (dis)eq}}{\ga\vd
  X\ygt X}{\ygt X}\vsk
\ianc{}{\emp\vd Q\ygt Q}{\ygt\atm\mbox{-emp}}\qquad
%\ianc{\cD\not\equiv\top}{\ga\vd Q\ygt Q}{\atm\cD\mbox{ non-emp}}\vsk
\ianc{}{\ga\vd Q\ygt (\BAnd_{p\in\Sigma}\top_p\Imp
  Q)}{\ygt\atm}\vsk
%\ianc{\mbox{not }x\ R^i q}{(\GG,\xoa);\top\vd Q\ygt
%  Q}{\atm x\not R^i q}\vsk
\ibnc{ \GG;(\cD\And D)\vd G\ygt \teng{G}}{D\ydt \tend{D}}{ \ga \vd
  D\Imp G\ygt \tend{D}\Imp \teng{G}}{ \ygt\Imp}\vsk
\ianc{(\GG,y\oftp A);\cD\vd[y/x] G\ygt  [y/x]\teng{G}}{ \ga\vd\PIXA
  G\ygt \PIXA\teng{G}}{ \ygt\Pi^y}\vsk 
%\ianc{\GG;\cD\vd[u/x] G\ygt [u/x]\teng{G}}{ \ga\vd\exa G\ygt \exa\teng{G}}{ \ygt\exists^u}\vsk 
\ibnc{ \ga \vd G_1 \ygt  \teng{G}_1}{\ga\vd G_2\ygt \teng{G}_2} { \ga\vd G_{1}\And
  G_{2} \ygt \teng{G}_1\And \teng{G}_2}{ \ygt\And}\vsk 
\ibnc{ \ga \vd G_1 \ygt \teng{G}_1}{\ga\vd G_2\ygt \teng{G}_2} { \ga\vd
  G_{1}\Or G_{2} \ygt \teng{G}_1\Or \teng{G}_2}{ \ygt\Or}\vsk 

% \ianc{}{\top\ydt \cdot;\top}{\ydt \top} \qquad
 % \ianc{}{\perp\ydt \cdot;\top}{\ydt \perp} \vsk
\ianc{X\in\{Q,\top,\perp\} }{X\ydt X}{\ydt X} \vsk
%  \ianc{\cdot;\top\vd G\ygt \cS} {(G\Imp Q)\ydt \cS}{ \ydt\Imp} Q\If G syntax
  \ibnc{\cdot;\top\vd G\ygt \teng{G}}{D\ydt \tend{D}} {(G\Imp  D)\ydt \teng{G}\Imp \tend{D}}{ \ydt\Imp}\vsk
  \ianc{ [u/x]D\ydt [u/x]\tend{D}}{ \PIXA D\ydt \PIXA\tend{D}}{ \ydt\Pi^u}\vsk 
\ibnc{ D_1 \ydt \tend{D}_1}{D_2\ydt \tend{D}_2} { D_{1} \And D_{2} \ydt
  \tend{D}_1\And \tend{D}_2}{ \ydt\And}\qquad
\ibnc{ D_1 \ydt \tend{D}_1}{D_2\ydt \tend{D}_2} { D_{1} \tensor D_{2} \ydt
  \tend{D}_1\tensor \tend{D}_2}{ \ydt\tensor}
  \end{array}
\]
  \caption{$\top$-Normalization}
  \label{fig:topnormal}
\end{figure}

\smallskip
We start by showing that this transformation preserves run-time
provability. We extend the notion of \emph{application} of a
substitution, notation $[t/x]F$, to a formula $F$. More in general, we denote
with $[\theta] F$ the application of $\theta$ to $F$.  We will also
need an operation of composition, say $\s_1\cdot\s_2$, such that
$[\s_1\cdot\s_2]F=[\s_2]([\s_1] F)$.

\begin{Theorem}
\label{thm:topnormalvdlr}
Let $\GG';\cD'\vd G\ygt G^{\top}$, $D\ydt \tend{D}$, $\cD\ydt \tend{\cD}$
and $\GG\vd\q\hastype\Phi$.
 \renewcommand{\q}{[ \theta ]}
\newcommand{\gad}{\GG;\q\tend{\cD}} \renewcommand{\ga}{\GG;\q\cD}
 \ben
\item  If $\ga\vd \q G$,  then $\gad\vd\q\teng{ G}$.
\item  If  $\ga\vd\q  D\imm\q Q$,  then $\gad\vd\q\tend{ D}\imm\q Q$.
\enen
\end{Theorem}

\begin{proof}
\renewcommand{\q}{[ \theta ]}
\newcommand{\gad}{\GG;\q\tend{\cD}}
\renewcommand{\ga}{\GG;\q\cD}
By mutual induction on the structure of the derivation of
$\gamma::\ga\vd\q G$  and inversion on $\gamma'::\GG';\cD'\vd G\ygt\teng{G}$
together  with $\delta ::\ga\vd\q D\imm\q Q$ and inversion on 
$\delta'::D\ydt \tend{D}$. We sketch only some cases:
\bit
\itc 
$\gamma$ ends in $\vd\atm$ and $\gamma'$ is $\ygt
X,\ygt\atm\mbox{-emp}$: trivial.
\itc
$\gamma$ ends in $\vd\atm$ and $\gamma'$ ends in $\ygt\atm$:
\btab
$\ga\vd\q Q$\bh
$\ga\vd \q(\cP\And\cD)\imm\q Q$\bs
%$ D\ydt\tend{D}$\bh
$\gad\vd\q \tend{\cP\And\cD}\imm\q Q$\bi $2$\\
$\GG;(\q\tend{\cD}\And (\BAnd_{p\in\Sigma}\top_p))\vd\q\tend{\cP\And\cD}\imm\q
Q$\` By repeated Weakening\\ 
$\GG;(\q\tend{\cD}\And (\BAnd_{p\in\Sigma}\top_p))\vd\q Q$\` By rule $\vd\atm$\\
$\gad\vd(\BAnd_{p\in\Sigma}\top_p)\Imp\q Q$\br $\vd\Imp$\\
$\ga\vd\teng{\q Q}$\br $\ygt\atm$
\etab
The other cases follows immediately by IH $1$ and $2$.
% \itc
% $\gamma$ ends in $\vd\atm$ and $\gamma'$ is $(\atm\cD\mbox{
%   non-emp}),(\atm\mbox{ non-rel})$: by IH $2$.
\enit
\end{proof}
Now, the converse:
\begin{Theorem}
\label{thm:topnormalvdrl}
Let $\GG';\cD'\vd G\ygt G^{\top}$, $D\ydt \tend{D}$, $\cD\ydt \tend{\cD}$
and $\GG\vd\q\hastype\Phi$.

\renewcommand{\q}{[ \theta ]}
\renewcommand{\ga}{\GG;\q\cD}
\newcommand{\gad}{\GG;\q\tend{\cD}}
\ben
\item   If $\gad\vd\q \teng{G}$, then $\ga\vd \q G$.
\item   If $\gad\vd\q\tend{D}\imm\q Q$, then $\ga\vd\q  D\imm\q Q$.
\enen
\end{Theorem}
\begin{proof}
\renewcommand{\q}{[ \theta ]}
\renewcommand{\ga}{\GG;\q\cD}
\newcommand{\gad}{\GG;\q\tend{\cD}}
By mutual induction on the structure of $\gamma::\gad\vd\q\teng{ G}$ and
$\delta::\gad\vd\q\tend{ D}\imm\q Q$,  as above but using $\top$-Strengthening
(Lemma \ref{le:topstren}) in place of Weakening. 
\end{proof}

An analogous result can be proven \wrt failure; the latter would
require $\top$-Weakening and Strengthening \wrt the (immediate) denial
relation. On the other hand, the above result will suffice, if we restrict to
terminating programs as we will do in Section~\ref{sec:termination}. 
First, we need to establish a theory of \emph{context schemata}
