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

In this chapter we introduce the source language and its uniform proof
system. After 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}


We will use the following slightly unusual source language\ednote{Say
  here third-order?}: 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}
\]
Differently form standard presentation of HHF, we allow disjunction
between clauses, equality and inequality. While disjunction among
clauses will be eliminated, (in)equalities containing parameters will
not. This means that in type-theoretic languages such as \emph{Twelf}
they need to 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$ and $\perp$ may be
decorated with a predicate symbol, as explained in in
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_q \\
\defp(q,Q\If G) & = &  Q\If G&\mbox{if } Q\equiv q\ \vM \\
\defp(q,Q\If G) & = &  \top_q&\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_q$ denotes the universal definition for $q$.  
 We use the notation $D\in\defp(q,\cP\And\cD)$
to indicate that $D$ is a top-level conjunct in the definition of $q$.


% 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}. 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.  We remark that the systems for denial will not be needed
in the proof of exclusivity (Theorem \ref{thm:exclu}).
\[
\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  $\defp(q,\cP\And\cD)$ immediately entails
  atom $Q$.}\\
\ga\fp D \imm Q & \mbox{Clause  $D$ from $\defp(q,\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
\ianc{\ga\sp\defp(Q,\cP\And\cD)\imm Q}{\ga\sp Q}{\vd\atm}
\qquad
\ianc{\gna\fp\defp(Q,\cP\And\cD) \nimm Q}{\ga\fp Q}{\nprv\atm}
% \ianc{ \ga\sp \defp(Q,\cP\And\cD) \imm Q}{\ga\sp Q}{{\vd {\rm atm }}}
% \qquad
% \ianc{ \gna\fp \defp(Q,\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.
Note that $\notimm\Pi$ and $\nvd\exists$ are infinitary rules, 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 rules $\yd\Pi$ and
$\yg\exists$ in Figure \ref{fig:topnormal}); this expresses the fact
that in those rules the relation holds for \emph{any} term and are
therefore analogous to logic variables. We will pervasively utilize
this notation and to avoid notational clutter, we shall not keep an
explicit record, but we agree to implicitly gather them in a pool
$\Phi$, which we can access when needed.

The denial rules for implication and universal quantification reflect
the operational semantics of unprovability that we have discussed
earlier. 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
have to introduce \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$.

\[ \begin{array}{rrcl}
\mbox{\textit{Substitutions}}& \sigma & \bnfas \epsilon\bnfalt \sigma,t/x
\end{array}
\]
Substitutions can be  well-typed as follows:
\beq
\ianc{}{\GG\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
The judgment $\GG\vd \sigma$ formalizes that $\sigma$ is a valid
substitution \wrt $\GG$, where  $par(t)$ denotes the set of parameters occurring
in $t$:
\beq
\ianc{}{\GG\vd\epsilon}{\epsilon}\qquad
\ibnc{par(t)\subseteq\GG}{\GG\vd\sigma}{\GG\vd\sigma,t/x}{\sigma}
\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.  Notation: $[t/x]E$ denotes the
substitution of $x$ with $t$ in an well-formed expression $E$. More in
general we denote with $[\sigma] E$ the application of $\sigma$ to $E$. 
We will also need an operation of composition, say $\s_1\cdot\s_2$,
such that $[\s_1\cdot\s_2]E=[\s_2]([\s_1] E)$.

%\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}

\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\yd\tend{D}$ and $\ga\vd G\yg\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$.

\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\yd\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
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}\yd isdall$.
\end{Example}


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

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

We start by showing that this transformation preserves run-time
provability.

\begin{Theorem}
\label{thm:topnormalvdlr}
Let $\GG';\cD'\vd G\yg G^{\top}$, $D\yd \tend{D}$, $\cD\yd \tend{\cD}$ and $\GG\vd\q$:
\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\yg\teng{G}$
together  with $\delta ::\ga\vd\q D\imm\q Q$ and inversion on 
$\delta'::D\yd \tend{D}$. We sketch only some cases:
\bit
\itc 
$\gamma$ ends in $\vd\atm$ and $\gamma'$ is $\yg
X,(\atm\GG\mbox{ emp})$: trivial.
\itc
$\gamma$ ends in $\vd\atm$ and $\gamma'$ ends in $\atm\mbox{ rel}$:
\btab
$\ga\vd\q Q$\bh
%$D\in \cP\And\q\cD$ and
 $\ga\vd\q D\imm\q Q$\bs
$ D\yd\tend{D}$\bh
$\gad\vd\q \tend{D}\imm\q Q$\bi $2$\\
$\GG;(\q\tend{\cD}\And \top_q)\vd\q\tend{D}\imm\q Q$\` By Weakening\\
$\GG;(\q\tend{\cD}\And \top_q)\vd\q Q$\` By rule $\vd\atm$\\
$\gad\vd\top_q\Imp\q Q$\br $\vd\Imp$\\
$\ga\vd\teng{\q Q}$\br $\atm\top\mbox{ rel}$
\etab
\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\yg G^{\top}$, $D\yd \tend{D}$, $\cD\yd \tend{\cD}$ and $\GG\vd\q$:
\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 do next.



\section{Terminating Programs}

% \begin{Definition}
% \label{def:goalorder}
% Given a second-order program $\cP$, define the binary relation
% $G_1\less G_2$ as the smallest stable relation, \ie such that
% $G_1\less G_2$ entails $\sigma G_1\less\sigma G_2$ for any
% substitution $\sigma$, which satisfies the following rules:
% \newcommand{\induce}{\stackrel{\less}{\Longrightarrow}}

% \[
% \begin{array}{c}
% \ianc{}{G_1\less G_1\And G_2}{\less\And_1}\qquad
% \ianc{}{G_2\less G_1\And G_2}{\less\And_2}\vsk
% \ianc{}{G_1\less G_1\Or G_2}{\less\Or_1}\qquad
% \ianc{}{G_2\less G_1\Or G_2}{\less\Or_2}\vsk
% \ianc{}{[t/x]G\less \exa G}{\less\exists}\qquad
% \ianc{}{[y/x]G\less \PIXA G}{\less\Pi^y}\vsk
% \ianc{}{G\less D\Imp G}{\less\Imp}\qquad
% \ianc{ (Q\If G)\induce G\less Q}{G\less Q}{\less\atm}\vsk


% \ianc{D_1\induce G\less Q}{D_1\And D_2\induce G\less Q}{\induce\And_1}\qquad
% \ianc{D_2\induce G\less Q}{D_1\And D_2\induce G\less Q}{\induce\And_2}\vsk
% \mbox{No clause for } \top\vsk
% \ibnc{D_1\induce G\less Q}{D_2\induce G\less Q}{D_1\tensor D_2\induce
%   G\less Q}{\induce\tensor}\vsk
% \ianc{\mbox{for every }G}{\perp_Q\induce G\less Q}{\induce\perp}\qquad
% \ianc{D\induce G\less Q}{\PIXA D\induce G\less Q}{\induce\Pi}
% \end{array}
% \]
% We say that $\cP$ is \emph{terminating} whenever the transitive
% closure of the above relation is well-founded.
% \end{Definition}

% \begin{Example}
%   You can check that $\defp(even)\induce even(X)\less even(ss(X))$.
%   Furthermore the relation is well-founded as it can be proven say by
%   induction on $X$. Instead $\PI{X}{nat}p\ s(X)\Imp p\ s(X)$ is not
%   terminating as the subgoal relation contains the infinite chain $p\ 
%   s^n(0)\less p\ s^n(0)\less\dots$ for every $n\in nat$.
% \end{Example}


We now introduce terminating programs.  This is abstractly achieved by
means of a relation between goals or between goals and clause heads,
namely `$\less$', with the intended meaning of ``$G_1$ ($G$) can arise
as a subgoal of $G_2$ ($D$ resp.\ )''.  Intuitively, a program
terminates if it yields an ordering relation which admits no infinite
descending chains. This is defined in Figure \ref{fig:termgraph}.  We
do not commit here to actual ways to verify the latter property. This
issue is explored, in the \ho setting, for example in
\cite{Rohwedder96esop}.  More formally:

\[ \begin{array}{rrcl}
\mbox{\textit{Ordering}}& R & \bnfas &\cdot \bnfalt R, G\less D\bnfalt R, G_1\less G_2 \\
\end{array}\]


Let $\cP\yd R$ and take the stable (that is, closed under
substitutions) and transitive closure of $R$.  We
say that $\cP$ is \emph{terminating} whenever the former is
well-founded.


\begin{figure}[htbp]
\[
\begin{array}{c} 
%  \ianc{}{ Q\yg Q'}{\yg\call}\qquad
 \ianc{X\in\{Q,\top,\perp\}\mbox{ or (dis)eq}}{ \GG\vd X\yg\cdot}{\yg X} \vsk
 % \ibnc{ Q'\yg Q\call Q'}{Q'\vd Q''\yg Q'\call Q''}{ Q'\yg
 % Q\call Q''}{\yg Cut}\vsk
  \ibnc{ \GG\vd   G\yg R_1}{\GG\vd D\yd R_2}{ \GG\vd  D\Imp  G\yg R_1, R_2,G\less D\Imp
  G}{ \yg\Imp}\vsk
  \ianc{ \GG,y\oftp A\vd  G\yg R}{ \GG\vd \PIXA G\yg R,[y/x]G\less \PIXA G}{ \yg\Pi^y}\vsk
  \ianc{ \GG\vd  G\yg R}{ \GG\vd \exa G\yg R,G\less \exa G}{ \yg\exists}\vsk
%  \ianc{ G\yg R}{ \exa G\yg R,[t/x]G\less \exa G}{ \yg\exists}\vsk
 \ibnc{ \GG\vd   G_1 \yg R_1}{ \GG\vd G_2\yg R_2}
    { \GG\vd  G_{1}\And G_{2}  \yg R_1, R_2,G_1\less G_1\And G_2,G_2\less
  G_1\And G_2}{ \yg\And}\vsk
 \ibnc{ \GG\vd   G_1 \yg R_1}{ \GG\vd G_2\yg R_2}
    { \GG\vd  G_{1}\Or G_{2}  \yg R_1, R_2,G_1\less G_1\Or G_2,G_2\less
  G_1\Or G_2,}{ \yg\Or}\vsk
\vsk
  \ianc{X\in\{Q,\top,\perp\}}{\GG\vd X\yd \cdot}{\yd X} \vsk
%  \ianc{}{\perp\yd \cdot}{\yd \perp} \vsk
  \ibnc{\GG\vd D\yd R_1}{ \GG\vd   G\yg R_2} {\GG\vd(G\Imp  D)\yd R_1,R_2,G\less D}{ \yd\Imp}\vsk
  \ianc{ \GG\vd D\yd R}{ \GG\vd\PIXA D\yd R}{ \yd\Pi}\vsk
 \ibnc{ \GG\vd D_1 \yd R_1}{\GG\vd D_2\yd R_2}
    { \GG\vd D_{1} \And D_{2}  \yd R_1, R_2}{ \yd\And}\vsk
 \ibnc{ \GG\vd D_1 \yd R_1}{\GG\vd D_2\yd R_2}
    { \GG\vd D_{1} \tensor D_{2}  \yd R_1, R_2}{ \yd\tensor}
 \end{array}
\]
\caption{Generation of the Subgoal Relation}
  \label{fig:termgraph}
\end{figure}

\begin{Example}
  $\cdot\vd\defp(even)\yd even( X) \less even (s( s( X)))$.  Furthermore the
  closure of this relation is well-founded as it can be proven say by
  induction on $X$. Consider instead the following:
  \[
  \begin{array}{l}
    \PI{E}{exp}\PI{M}{nat} \\
    p\ (lam\ E) \ M\\
    \qquad \If(\PI{x}{exp}(\PI{N}{nat} p\  x\ (s\ N)\If p\ x\ (s\ N))\Imp
    p\ (E\ x) \ M).
  \end{array}
  \]
  The clause is not terminating as the subgoal relation contains the
  pair\\
  $[y/x](p\ x\ s(N)\less p\ x\ s(N))$ which yields an infinite
  descending chain $(p\ y\ (s\ 0))\less (p\ y\ (s\ 0))\less\dots$.
\end{Example}

We can now prove that if a program is terminating, a non-proof of any
ground $G$ is a \emph{denial} of $G$; we are going to reason
classically that either there is a proof of $G$, or there is not such
a proof. We remark that $\fp$ is the denial relation introduced in
Figure \ref{fig:sf} and \ref{fig:imm}.

\begin{Theorem}[Termination]
\label{thm:termination}
Assume $\cP$ is terminating: for any ground $G$, if not $\ga\sp G$,
then $ \gna\fp G$.
\end{Theorem}

\begin{proof}
\renewcommand{\ga}{\Gamma;\cD }
\renewcommand{\gna}{ \Gamma;\cD }
\renewcommand{\ba}{\` Subcase\\}
We generalize this to:  let $D$ be a ground instance of $ \defp(q,\cP\And\cD)$:
\ben
\item
If not $   \ga\sp  G$, then  $  \gna\fp  G$.
\item
If not $  \ga\sp   D \imm  Q$,
then  $  \gna\fp   D \imm    Q$.
\enen
We proceed by mutual induction on the goal ordering induced by $\cP$
terminating and on the structure of   $D$:
\bit
\itc $D=\perp$: trivial.
\itc $D=\top$. 
$$\ianc{}{\gna\fp\top\imm  Q}{\nimm\top}$$
\itc $D=D_1\If G_1$. Either $ \ga\sp  G_1$ or not $ \ga\sp  G_1$ and
$\ga\sp D_1\imm Q$ or not $\ga\sp D_1\imm Q$. Since $D_1\If G_1$ is an
instance of a terminating clause,  by stability, it is terminating as well:
%By termination   $ G_1\less D_1$; 
there are four sub-cases:
\ben
\item %1
\btab
$\ga\sp G_1$\ba
$\ga\sp D_1\imm Q$\ba
$\ga\sp  D_1 \If  G_1\imm  Q $\br $\imm\Imp$\\
\etab
\item %2.
\btab
Not  $  \gna\sp   G_1$\ba
 $  \gna\fp   G_1$\bi $1$\\
$\ga\sp D_1\imm  Q$\ba
$\gna\fp  D_1 \If   G_1\imm    Q $\br\\
\etab
\item %3.
\btab
$\ga\sp  G_1$\ba
Not $\ga\sp  D_1\imm  Q$\ba
$\ga\fp  D_1\imm  Q$\bi $2$\\
$\gna\fp   D_1 \If   G_1\imm   Q$\br\\
\etab
\item %4 
\btab
Not $\gna\sp   G_1$\ba
Not $\gna\sp  D_1\imm Q$\ba
$\gna\fp  D_1\imm Q$\bi $2$\\
$\gna\fp   D_1 \If   G_1\imm   Q$\br\\
\etab
\enen
\itc %imm\tensor
$D=D_1\tensor D_2$.
\ben
\item %1
\btab
 $\ga\sp  D_1\imm Q$ \ba
$\ga\sp  D_2\imm Q$\ba
$\ga\sp  D_1\tensor  D_2\imm  Q$\br $\imm\tensor$\\
\etab
\item %2
\btab
 $\ga\sp  D_1\imm  Q$ \ba
Not $\gna\sp   D_2 \imm   Q$\ba
$\gna\fp   D_2 \imm   Q$\bi $2$\\
$\gna\fp   D_1\tensor   D_2 \imm   Q$\br \\
\etab
\item %3
\btab
 $\ga\sp  D_2\imm  Q$ \ba
Not $\gna\fp   D_1 \imm   Q$\ba
$\gna\fp   D_1 \imm   Q$\bi $2$\\
$\gna\fp   D_1\tensor   D_2 \imm   Q$\br \\
\etab
\item %4
\btab
Not $\gna\sp   D_1 \imm   Q$\ba
Not $\gna\sp   D_2 \imm   Q$\ba
$\gna\fp   D_1 \imm   Q$\bi $2$\\
$\gna\fp   D_2 \imm    Q$\bi $2$\\
$\gna\fp   D_1\tensor   D_2 \imm   Q$\br 
\etab
\enen
\itc%And
$D=D_1\And D_2$. 
\ben
\item %1
\btab
$\ga\sp  D_1\imm Q$ \ba
$\ga\sp  D_2\imm Q$\ba
$\ga\sp D_1\And D_2\imm  Q$\br $\imm\And$
\etab
\item %2
\btab
$\ga\sp D_1\imm  Q$ \ba
Not $\gna\sp    D_2 \imm    Q$\ba
$\gna\fp    D_2 \imm    Q$\bi $2$\\
$\ga\sp  D_1\And D_2\imm Q$\br
\etab
\item %3
\btab
 $\ga\sp  D_2\imm Q$ \ba
Not $\gna\sp   D_1 \imm   Q$\ba
$\gna\fp   D_1 \imm   Q$\bi $2$\\
$\ga\sp D_1\And D_2\imm  Q$\br
\etab
\item %4
\btab
Not $\gna\sp   D_1 \imm    Q$\ba
$\gna\fp   D_1 \imm    Q$\bi $2$\\
Not $\gna\sp   D_2 \imm    Q$\ba
$\gna\fp   D_2 \imm    Q$\bi $2$\\
$\gna\fp  D_1\And D_2 \imm    Q$\br
\etab
\enen
\itc %\Pi imm
$D=\PIXA D'$.  For some  ground $\GG\vd t\hastype A$, $\GG;\cD
\sp [t/x] D'\imm Q$ or for all ground $t$, not  $\ga\sp[t/x] D'\imm Q$:
\ben
\item %1
\btab
$\GG; \cD\sp [ t/x] D'\imm  Q$\ba
$\GG; \cD\sp \PIXA D'\imm   Q$\br $\imm\Pi$
\etab
\item %2
\btab
For all $t$ ground not $\GG;\cD\sp [t/x] D'\imm  Q$\ba
For all $t$ ground $\GG;\cD\fp [t/x] D'\imm  Q$\bi $2$\\
$\GG;\cD\fp  \PI{x}{A} D'\imm  Q$\br
\etab
\enen
%start \vd G
\itc 
\[\ianc{}{\ga\fp\perp}{\nvd\perp}\]
\itc
Either $\ga\sp\defp(q,\cP\And\cD)\imm Q$ or not  $\ga\sp\defp(q,\cP\And\cD)\imm Q$:
\ben
\item %1
\btab
$\ga\sp \defp(q,\cP\And\cD) \imm Q$\ba
$\ga\sp Q$\br
\etab
\item %2
\btab
Not $\ga\sp \defp(q,\cP\And\cD) \imm Q$\ba
$\ga\fp \defp(q,\cP\And\cD) \imm Q$\bi $2$\\
$\gna\fp  Q$\br
\etab
\enen
\itc Either $\ga\sp G_1$ or not $\ga\sp G_1$ and either $\ga\sp G_2$ or not $\ga\sp G_2$:
\ben
\item % 1
\btab
$\ga\sp  G_1$\ba
$\ga\sp  G_2$\ba
$\ga\sp  G_1\And G_2$\br
\etab
\item %2
\btab
$\ga\sp  G_1$\ba
Not $\gna\sp  G_2 $\ba
$\gna\fp  G_2 $\bi $1$\\
$\gna\fp  G_1\And G_2 $\br
\etab
\item %3
\btab
$\ga\sp  G_2$\ba
Not $\gna\sp  G_1 $\ba
$\gna\fp  G_1 $\bi $1$\\
$\gna\fp  G_1\And G_2 $\br
\etab
\item %4
\btab
Not $\gna\sp  G_1 $\ba
$\gna\fp  G_1 $\bi $1$\\
Not $\gna\sp  G_2 $\ba
$\gna\fp  G_2 $\bi $1$\\
$\gna\fp  G_1\And G_2 $\br
\etab
\enen
 %or
\itc Either $\ga\sp G_1$ or not $\ga\sp G_1$ and either $\ga\sp G_2$ or not $\ga\sp G_2$:
 $\gna\fp  G_2 $:
\ben
\item % 1
\btab
$\ga\sp  G_1$\ba
$\ga\sp  G_2$\ba
$\ga\sp  G_1\Or G_2$\br
\etab
\item %2
\btab
$\ga\sp  G_1$\ba
Not $\gna\sp  G_2 $\ba
$\gna\fp  G_2 $\bi $1$\\
$\ga\sp  G_2\Or G_1$\br
\etab
\item %3
\btab
$\ga\sp  G_2$\ba
Not $\gna\sp  G_1 $\ba
$\gna\fp  G_1 $\bi $1$\\
$\ga\sp   G_2\Or G_1$\br
\etab
\item %4
\btab
Not $\gna\sp   G_1 $\ba
$\gna\fp   G_1 $\bi $1$\\
Not $\gna\sp   G_2 $\ba
$\gna\fp  G_2 $\bi $1$\\
$\gna\fp  G_1\Or G_2 $\br

\etab
\enen
\itc %exa
Either for some ground $\GG\vd t\hastype A$, $\GG; \cD\sp[t/x] G$
or for all $t$  not  $\GG; \cD\sp[t/x] G$:
\ben
\item %1
\btab
$\GG\vd t\hastype A$\bh
$\GG; \cD[t/x]\sp G$\ba
$\ga\sp \exa G$\br 
\etab
\item 
\btab
For all ground $t$ not  $\GG; \cD\sp[t/x] G$\ba
$\GG;\cD\fp [t/x]G$\bi $1$\\
$\GG;\cD\fp \exa G$\br
\etab
\enen
\itc %PIXA G
For a new parameter $y$, $(\GG,y\oftp A);\cD\sp[y/x] G$
or not  $(\GG,y\oftp A);\cD\sp[y/x] G $:
\ben
\item %1
\btab
$(\GG,y\oftp A);\cD\sp[y/x]  G$\ba
$\GG;[ y/x]\cD\sp \PIXA G$\br
\etab
\item %2 
\btab
Not $(\GG,y\oftp A);\cD\sp[y/x] G$\ba
$(\GG,y\oftp A);\cD\sp[y/x] G$\bi $1$\\
$\GG;[,y/x]\cD\fp\PIXA G$\br
\etab
\enen
\itc %\Imp
$\GG;(\cD\And D) \sp G$ or not $\GG;( \cD\And 
D)\sp  G$:
\ben
\item %1
\btab
 $\GG;(\cD\And D)\sp G$\ba
$\ga\sp D\Imp  G$\br
\etab
\item % 2
\btab
Not  $\GG;( \cD\And  D)\sp  G$\ba
 $\GG;( \cD\And  D)\fp  G$\bi $1$\\
$\gna\fp  D\Imp  G$\br\etab
\enen 
\itc The (dis)equality case follows immediately from the decidability of the $\eqd,\neqd $
 rules.
\enit% main bit
\end{proof}

