\section{Terminating Programs}
\label{sec:termination}

% \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. The notion of termination that
we adopt is the very strong \emph{universal} one, as it is known in
logic programming~\cite{DeSchreye94}. 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$]''.  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$, call it $[R]$.  We say
that $\cP$ is \emph{terminating}, denoted $\cP\da$, whenever $[R]$ is
well-founded.

%%%%%%% WITH GLOBAL PARAMETERS %%%%%%%%%%%%
\begin{figure}
\[
\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 [u/x] G\yg R}{ \GG\vd \exa G\yg R,G\less \exa G}{ \yg\exists^u}\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 [u/x]D\yd R}{ \GG\vd\PIXA D\yd R}{ \yd\Pi^u}\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} If \texttt{even} defines the even number,
  \texttt{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}

Finally\added, we define when a \emph{schema} is terminating:
\beq
\ianc{}{\ecs\da}{\ecs\da}\qquad
\ibnc{\GG\vd \cD\da}{\cS\da}{\cS\mbar\GG;\some{\Phi}\cD\da}{\mbar\da}
\eneq 
Since $\Phi$ ranges over $FV(\cD)\sla \GG$, we verify the termination
of $\cD$ in the $\GG$ context.

\begin{Lemma}
\label{le:termrel}
\mbox{}
\begin{enumerate}
\item If $\GG\vd \cD\yd R$, $D\inn\cD$ and $\GG\vd D\yd R'$,
  then $R'\subseteq R$.
\item If $\GG\vd G\yg R$, $G'\less G$ and  $\GG\vd G'\yg R'$,
  then $R'\subseteq R$.
\end{enumerate}
\end{Lemma}
\begin{proof}
By a straightforward mutual induction on the structure of $\GG\vd D\yd
R'$ and $\GG\vd G'\yg R'$.
\end{proof}

\begin{Corollary}
\label{co:termrel}
If $\GG\vd\cD\da$ and $D\inn\cD$, then $\GG\vd D\da$.
\end{Corollary}
\begin{proof}
  By definition, $\GG\vd\cD\da$ if $\GG\vd\cD\yd R$ and $[R]$ is
  well-founded; by Lemma \ref{le:termrel} $\GG\vd D\yd R'$, and
  $R'\subseteq R$. Thus $[R']$ is well-founded, and $D\da$.
\end{proof}


\begin{Lemma}
\label{le:termdsat}
Let  $\cS\da$. If $\ga\inss$ and $D\inn\cD$, then $D\da$.
\end{Lemma}
\begin{proof}
  By induction on the structure of $\cS\da$, using Corollary
  \ref{co:termrel}.
\end{proof}

\smallskip
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 recall that $\fp$ is the denial relation introduced in
Figure \ref{fig:sf} and \ref{fig:imm}.

\begin{Theorem}[Termination]
\label{thm:termination}
Let $\cP\da$ and  $\cS\da$ be a  schema such that
$\dsat\cP$ and $\ga\inss$: for any ground $G$, if not $\ga\sp G$, then
$ \gna\fp G$.
% Let $\cP\da$ and  $\cS\da$ be a  schema such that
% $\dsat\cP$ and $\ga\inss$: for any ground $G$, either  $\ga\sp G$ or
% $ \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 For every $D\inn \cP\And\cD$, 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$: we start with $2$.
Since $D$ is an
instance of a terminating clause either from the program or the
run-time context,  by stability and Corollary \ref{le:termdsat}, it is
terminating as well.
\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$. By termination of $D_1\If G_1$, 
$ G_1\less D_1$, hence we can apply the IH to $G_1$:
%By termination   
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  $\imm\Imp_2$
\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 $\imm\Imp_1$
\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 \br $\imm\Imp_1$
\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 $G=\top$: trivially true. 
\itc $G=\perp$: 
\[\ianc{}{\ga\fp\perp}{\nvd\perp}\]
\itc $G=Q$:
either $\ga\sp D\imm Q$ or for every $D$ not  $\ga\sp D\imm Q$:
\ben
\item %1
\btab
$\ga\sp D \imm Q$\ba
$\ga\sp Q$\br
\etab
\item %2
\btab
Not $\ga\sp D \imm Q$ for every $D$\ba
$\ga\fp D \imm Q$\bi $2$\\
$\gna\fp  Q$\br
\etab
\enen
\itc $G=G_1\And G_2$: %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 $G= G_1\Or G_2$:
% 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 $G=\exa G'$: %exa keep
% 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\sp[t/x] 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 $G=\PIXA G'$: %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;\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;\cD\fp\PIXA G'$\br
\etab
\enen
\itc $G=D'\Imp G'$: %\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}

