\documentstyle[jair,twoside,11pt,theapa]{article}
%\documentstyle[jair,twoside,11pt]{article}
\input epsf
\jairheading{4}{1996}{209-235}{1/96}{4/96}
\ShortHeadings{A Divergence Critic}
{Walsh}
\firstpageno{209}

\begin{document}

\newcommand{\w}[3]{\mbox{\wf{#1 \wh{#2} #3}}}
\newcommand{\wf}[1]{\mbox{\fbox{$#1$}}}
%\newcommand{\wfout}[1]{\fbox{$#1$}^{\uparrow}}
%\newcommand{\wfin}[1]{\fbox{$#1$}^{\downarrow}}
\newcommand{\wfout}[1]{\fbox{$#1$}}
\newcommand{\wfin}[1]{\fbox{$#1$}}
\newcommand{\wh}[1]{\mbox{$\underline{#1}$}}
\newcommand{\sink}[1]{\left\lfloor #1 \right\rfloor}

\newcommand{\eqref}[1]{(\ref{#1})}

\newcommand{\app}[2]{#1 \mbox{$\! \mbox{@} \!$} #2}
\newcommand{\cons}[2]{#1 \mbox{$\! :: \!$} #2}
\newcommand{\consnil}[1]{[#1]}
\newcommand{\nil}{[]}
\newcommand{\appd}[2]{app(#1,#2)}
\newcommand{\consd}[2]{cons(#1,#2)}
\newcommand{\consdnil}[1]{\consd{#1}{\nild}}
\newcommand{\nild}{nil}
%\newcommand{\appd}[2]{\mbox{\rm app}(#1,#2)}
%\newcommand{\consd}[2]{\mbox{\rm cons}(#1,#2)}
%\newcommand{\consdnil}[1]{\mbox{\rm cons}(#1,\nild)}
%\newcommand{\nild}{\mbox{\rm nil}}
\newcommand{\len}{\mbox{\it len}}
\newcommand{\rev}{\mbox{\it rev}}
\newcommand{\qrev}{\mbox{\it qrev}}
\newcommand{\xxx}{\mbox{\it x}}
\newcommand{\yyy}{\mbox{\it y}}
\newcommand{\zzz}{\mbox{\it z}}
\newcommand{\uuu}{\mbox{\it u}}
\newcommand{\vvv}{\mbox{\it v}}
\newcommand{\www}{\mbox{\it w}}
\newcommand{\aaa}{\mbox{\it a}}
\newcommand{\bbb}{\mbox{\it b}}
\newcommand{\ccc}{\mbox{\it c}}
\newcommand{\ddd}{\mbox{\it d}}
\newcommand{\eee}{\mbox{\it e}}
\newcommand{\fff}{\mbox{\it f}}
\newcommand{\ggg}{\mbox{\it g}}
\newcommand{\hhh}{\mbox{\it h}}
\newcommand{\lll}{\mbox{\it l}}
\newcommand{\nnn}{\mbox{\it n}}
\newcommand{\ttt}{\mbox{\it t}}
\newcommand{\sss}{\mbox{\it s}}
\newcommand{\rrr}{\mbox{\it r}}
\newcommand{\XXX}{\mbox{\it X}}
\newcommand{\YYY}{\mbox{\it Y}}
\newcommand{\ZZZ}{\mbox{\it Z}}
\newcommand{\UUU}{\mbox{\it U}}
\newcommand{\VVV}{\mbox{\it V}}
\newcommand{\WWW}{\mbox{\it W}}
\newcommand{\AAA}{\mbox{\it A}}
\newcommand{\BBB}{\mbox{\it B}}
\newcommand{\CCC}{\mbox{\it C}}
\newcommand{\DDD}{\mbox{\it D}}
\newcommand{\EEE}{\mbox{\it E}}
\newcommand{\FFF}{\mbox{\it F}}
\newcommand{\GGG}{\mbox{\it G}}
\newcommand{\HHH}{\mbox{\it H}}
\newcommand{\LLL}{\mbox{\it L}}
\newcommand{\NNN}{\mbox{\it N}}
\newcommand{\TTT}{\mbox{\it T}}
\newcommand{\SSS}{\mbox{\it S}}
\newcommand{\RRR}{\mbox{\it R}}

\newcommand{\sorted}{\mbox{\it sorted}}
\newcommand{\isort}{\mbox{\it isort}}
\newcommand{\insertd}{\mbox{\it insert}}
\newcommand{\rot}{\mbox{\it rot}}
\newcommand{\half}{\mbox{\it half}}
%\newcommand{\half}{\mbox{\rm half}}
%\newcommand{\rot}{\mbox{\rm rot}}
%\newcommand{\sorted}{\mbox{\rm sorted}}
%\newcommand{\isort}{\mbox{\rm isort}}
%\newcommand{\insertd}{\mbox{\rm insert}}
%\newcommand{\len}{\mbox{\rm len}}
%\newcommand{\rev}{\mbox{\rm rev}}
%\newcommand{\qrev}{\mbox{\rm qrev}}
%\newcommand{\aaa}{\mbox{\rm a}}
%\newcommand{\bbb}{\mbox{\rm b}}
%\newcommand{\ccc}{\mbox{\rm c}}
%\newcommand{\ddd}{\mbox{\rm d}}
%\newcommand{\eee}{\mbox{\rm e}}
%\newcommand{\fff}{\mbox{\rm f}}
%\newcommand{\ggg}{\mbox{\rm g}}
%\newcommand{\hhh}{\mbox{\rm h}}
%\newcommand{\lll}{\mbox{\rm l}}
%\newcommand{\nnn}{\mbox{\rm n}}
%\newcommand{\rrr}{\mbox{\rm r}}
%\newcommand{\sss}{\mbox{\rm s}}
%\newcommand{\ttt}{\mbox{\rm t}}
%\newcommand{\uuu}{\mbox{\rm u}}
%\newcommand{\vvv}{\mbox{\rm v}}
%\newcommand{\www}{\mbox{\rm w}}
%\newcommand{\xxx}{\mbox{\rm x}}
%\newcommand{\yyy}{\mbox{\rm y}}
%\newcommand{\zzz}{\mbox{\rm z}}


%\begin{document}
%\bibliographystyle{plain}

\title{A Divergence Critic for Inductive Proof}
\author{\name Toby Walsh \email toby@itc.it \\
\addr IRST, Location Pant\`{e} di Povo\\
I38100 Trento, ITALY}



\maketitle


\begin{abstract}
Inductive theorem provers often diverge. This paper describes a
simple critic, a computer program
which monitors the construction of inductive proofs
attempting to identify diverging
proof attempts. Divergence is
recognized by means of a ``difference matching'' procedure.
The critic then proposes lemmas and generalizations
which ``ripple'' these differences away
so that the proof can go through without divergence.
The critic enables the theorem prover
{\sc Spike} to prove many theorems completely automatically from
the definitions alone.
\end{abstract}


\section{Introduction}

Two key problems in inductive theorem proving are
proposing lemmas and generalizations. A prover's divergence
often suggests to the user an appropriate lemma or
generalization that will enable the proof to
go through without divergence. As a simple example, consider 
the theorem, 
\begin{eqnarray*}
\forall n \ . \ dbl(n) & = & n+n.
\end{eqnarray*}
This is part of a simple program verification
problem \cite{dershowitz1}.
Addition and doubling are defined recursively 
by means of the rewrite rules,
\begin{eqnarray*}
X + 0 & = &  X \\
X + s(Y) & = & s(X+Y) \\
dbl(0) & = & 0 \\
dbl(s(X)) & = & s(s(dbl(X))) 
\end{eqnarray*}
where $s(X)$ represents the successor of $X$ (that is, $X+1$).
I have adopted the {\sc Prolog} convention of writing meta-variables
like $X$ and $Y$ in upper case. 

The theorem prover {\sc Spike} \cite{rusi1} 
fails to prove this theorem. 
The proof attempt begins with a simple
one step induction on $x$. The base case is 
trivial. In the step case, 
the induction hypothesis is,
$$ dbl(x) = x + x $$
And the induction conclusion is,
$$ dbl(s(x))  = s(x)+s(x). $$
{To ease presentation,
variables in this paper are, as here, sometimes renamed 
from those introduced by {\sc Spike}. This has no effect
on the results as the prover and divergence
critic both alpha convert variable names where necessary.}
Rewriting the induction conclusion with the
recursive definitions of $dbl$ and $+$ gives,
$$ s(s(dbl(x))) = s(s(x) + x). $$
The outermost successor functions on either 
side of the equality are now cancelled, 
$$ s(dbl(x)) = s(x) + x. $$
The prover then fertilizes with the induction hypothesis
on the left hand side,
$$ s(x+x) = s(x) + x. $$
This equation cannot be simplified further so 
another induction is performed. Unfortunately, 
this generates the diverging sequence of subgoals,
\begin{eqnarray*}
s(x + x) & = & s(x)+x \\
s(s(x + x)) & = & s(s(x))+x \\
s(s(s(x + x))) & = & s(s(s(x)))+x \\
s(s(s(s(x + x)))) & = & s(s(s(s(x))))+x \\
s(s(s(s(s(x + x))))) & = & s(s(s(s(s(x)))))+x \\
& \vdots &
\end{eqnarray*}
The problem is that the prover repeatedly tries an induction
on $x$ but is unable to simplify the successor functions that this introduces
on the first argument position of 
$+$. The proof will go through without divergence if
we have the rewrite rule,
$$s(X) + Y = s(X+Y).$$
This rule ``ripples'' accumulating successor functions 
off the first argument position of
$+$. This rewrite rule is derived from
the lemma, 
$$\forall x,y \ . \ s(x) + y = s(x+y).$$
This is the commuted version of the recursive definition
of addition and is, coincidently, a generalization
of the first subgoal. This lemma can be proved without 
divergence as the induction variable, $y$ occurs just in the second
argument position of $+$. 

In this paper I describe a simple ``divergence critic'',
a computer program which attempts to automate this process.
The divergence critic identifies when a proof attempt is diverging
by means of a ``difference matching'' procedure.
The critic then proposes lemmas and generalizations
which hopefully allow the proof to go through without divergence.
Although the critic is designed to work with the prover {\sc Spike}, 
it should also work with other induction provers
\cite{divergence-critic}.
{\sc Spike} is a rewrite based
theorem prover for first order conditional theories.
It contains powerful rules for case analysis, simplification 
and implicit induction using the notion of a test set. 
Unfortunately, as is the case with other inductive
theorem provers, its attempts to prove many
theorems diverge without an appropriate generalization or the addition
of a suitable lemma.

In Section \ref{sec-rippling}, I describe difference
matching and rippling, the two key ideas at the heart of the
divergence critic. I then outline 
how difference matching identifies the accumulating term structure
which is causing divergence (Section \ref{sec-da}).
In Section \ref{sec-lemma} and
\ref{sec-transverse}, I show how lemmas are speculated which ``ripple'' 
this term structure out of the way. In Section \ref{sec-general},
I describe the heuristics used in generalizing these lemmas.
Finally, implementation and results are described
in Sections \ref{sec-implementation} and \ref{sec-results}. 

\section{Difference matching and rippling}
\label{sec-rippling}

Rippling 
is a powerful heuristic developed at Edinburgh for 
proving theorems involving explicit induction
\cite{pub567} 
and is implemented in the {\sc Clam} theorem prover \cite{Clam}.
In the step case of an inductive proof, the induction conclusion
typically differs from the induction hypothesis by the addition of
some constructors or destructors. 
Rippling uses annotations to mark these differences and
applies annotated rewrite rules to remove them.

As a simple example, consider again the theorem discussed in the
introduction. 
%{\sc Clam} proves this theorem using the 
%following explicit induction schema,
%\[ \frac{P(0) \ \ \ \ \ \ \ \ P(x) \vdash P(s(x))}{\forall n \ . \ P(n)} \]
In the step case, the induction hypothesis is,
\[ dbl(x) = x + x \]
And the induction conclusion is,
\[ dbl(s(x)) = s(x) + s(x). \]
If we ``difference match''
the induction conclusion against the
induction hypothesis  \cite{pub556}, 
we obtain the following annotated induction
conclusion,
\[ dbl(\wf{s(\wh{x})}) = \wf{s(\wh{x})} + \wf{s(\wh{x})}. \]
An annotation consists of a {\em wave-front}, a box with a {\em wave-hole}, an
underlined term. 
Wave-fronts
are always one functor thick
\cite{termination-rippling}. That is, every 
wave-front has one immediate subterm that is annotated with
a wave-hole. To make presentation simpler, we
display adjacent wave-fronts merged. Thus,
$\wf{s(s(\wh{x}))}$ is just syntactic sugar for
the annotated term, $\wf{s(\wh{\wf{s(\wh{x})}})}$.
Wave-fronts % \cite{pub567} 
can also include up and down arrows
to indicate whether they are moving towards the
top of the term tree or down towards the leaves. 
This extension can, however, be safely ignored here.

The {\em skeleton} of an annotated
term is formed by deleting everything that
appears in the wave-front but not in the wave-hole. 
The {\em erasure} of an annotated terms is formed by deleting
the annotations but not the terms they contain. In this case,
the skeleton of the annotated induction conclusion is identical to
the induction hypothesis, and 
the erasure of the annotated induction conclusion is 
the unannotated induction conclusion. 
Difference matching guarantees this; that is,
difference matching the induction conclusion with 
the induction hypothesis
annotates the induction conclusion so that its skeleton 
matches the induction hypothesis.

Formally, $r$ is a {\em difference
match} of $s$ with $t$ with substitution $\sigma$ iff
%\begin{eqnarray*}
$\sigma(skeleton(r)) = t$
% & \ {\rm and} \ & 
and 
$erase(r)=s$
%\end{eqnarray*}
where $skeleton(r)$ and $erase(r)$ build the skeleton and erasure of 
the annotated term $r$. 
Difference matching is not unitary. That is,
two terms can have more than one difference match. 
For example, both $\wf{s(\wh{s(x)})}$ and 
$s(\wf{s(\wh{x})})$ are difference matches of
$s(s(x))$ with $s(x)$. The number of difference matches
can be reduced if we compute just the
{\em maximal} difference match in which wave-fronts
are as high as possible in the term tree. A formal
definition of such a well founded ordering on annotated
terms has been given by Basin and Walsh (1994).
% \cite{termination-rippling}. 

The aim of rippling is to rewrite the annotated induction conclusion so that
the skeleton, the induction hypothesis, is preserved and
the differences, the wave-fronts are moved to harmless
places (for example, to the top of the term). If
this rewriting succeeds, we will then be able to appeal to the
induction hypothesis. 
To rewrite the annotated induction conclusion, we use 
the following annotated rewrite rules, or {\em wave rules}:
\begin{eqnarray}
dbl(\wf{s(\wh{X})}) & = & \wfout{s(s(\wh{dbl(X)}))} \label{dbl-rule} \\
X+\wfout{s(\wh{Y})} &=& \wfout{s(\wh{X +Y})} \label{plus2-rule} \\
\wfout{s(\wh{X})}+Y &=& \wfout{s(\wh{X +Y})} \label{plus1-rule} 
\end{eqnarray}
The first two of these annotated rewrite rules are derived from 
the recursive definitions of $dbl$ and $+$ whilst
the second is derived from the lemma proposed at
the end of the introduction. 
Each of these annotated rewrite 
rules preserves the 
skeleton of the term being 
rewritten, and moves the wave-fronts higher up the term
tree. Wave rules guarantee this: 
a wave rule is an annotated rewrite rule
with an identical skeleton on left and
right hand sides that moves wave-fronts
in a well founded direction like, for instance, to the
top of the term tree  \cite{termination-rippling}. 

Rippling on the left hand side of the annotated induction conclusion
using \eqref{dbl-rule} yields,
\[ \wf{s(s(\wh{dbl(x)}))} = \wf{s(\wh{x})} + \wf{s(\wh{x})}. \]
Then rippling on the right hand side with 
\eqref{plus2-rule} gives,
\[ \wf{s(s(\wh{dbl(x)}))} = \wf{s(\wh{\wf{s(\wh{x})} + x})}. \]
Finally rippling with \eqref{plus1-rule} on the right hand side yields,
\[ \wf{s(s(\wh{dbl(x)}))} = \wf{s(s(\wh{x + x}))}. \]
As the wave-fronts are at the top of each term,
we have successfully rippled both sides of the equality.
We can now appeal
to the induction hypothesis on the left hand side
giving,
\[ \wf{s(s(\wh{x+x}))} = \wf{s(s(\wh{x + x}))}. \]
This is a simple identity and the proof is complete. 
Note that to complete the proof, we needed to 
rewrite with a lemma, \eqref{plus1-rule}. 
The aim of the divergence critic described in this paper
is to propose such lemmas. 

Rippling has several desirable properties. It is highly goal
directed, manipulating just the differences between
the induction hypothesis and the induction conclusion. 
As the annotations restrict the application
of the rewrite rules, rippling also involves little or no search.
Difference matching and rippling have proved useful
in domains outside of explicit induction. For example,
they have been used to sum
series \cite{pub563} 
and to prove limit theorems \cite{limits}.
In the rest of the paper, I show that difference
matching and rippling are also useful in identifying
and correcting divergence in a prover that neither
uses explicit rules of induction nor uses
annotations to control rewriting. 

\section{Divergence Analysis}
\label{sec-da}

The initial problem is recognizing when the proof
is diverging. Various properties of rewrite rules have been identified which 
cause divergence like, 
for example, forwards and backwards crossed systems \cite{hermann1}.
However, these properties fail to capture all diverging
rewrite systems since the problem is, in general, undecidable. 
The divergence critic instead
studies the proof attempt looking
for patterns of divergence; no attempt is made to analyse the rewrite rules
themselves for structures which give rise to divergence. The advantage of this
approach is that the critic need not know the details of the rewrite
rules applied, nor the type of induction being performed,
nor the control structure used by the prover. The 
critic can thus recognise divergence patterns arising from
complex mutual or multiple inductions with little more difficulty than divergence
patterns arising from simple straightforward inductions. 
The disadvantage of this approach 
is that the critic can identify a ``divergence''
pattern when none exists. Fortunately, such cases appear to be rare, and
even when they occur, the critic usually suggests a lemma or generalization
which gives a shorter and more elegant proof (see Section \ref{sec-results}
for an example). 


% \section{An Example}
\label{sec-example}
To illustrate the ideas behind the critic's divergence
analysis, consider again the theorem from the introduction,
\begin{eqnarray*}
\forall n \ . \ dbl(n) & = & n + n .
\end{eqnarray*}
The divergence critic first partitions the 
sequence of equations which the prover attempts to prove by induction. 
This is necessary since several diverging sequences
may be interleaved in the prover's output. 
Several heuristics can be used to reduce the number of 
partitions considered. The most useful heuristic is parentage in which
the sequence is partitioned so that
each equation is derived from the
previous one. That is, the equations lie on 
a single branch of the proof tree. In particular, the base case and 
step case of an induction
are partitioned into different sequences. 
Other heuristics which can be used include:
the function and constant symbols which occur in one equation
occur in the next equation in the partition,
and the weights of the equations in a partition 
form a simple arithmetic progression.
In this case, there is
just a single open branch in the proof tree,
\begin{eqnarray*}
s(x + x) & = & s(x)+x \\
s(s(x + x)) & = & s(s(x))+x \\
s(s(s(x + x))) & = & s(s(s(x)))+x \\
%s(s(s(s(x + x)))) & = & s(s(s(s(x))))+x \\
% s(s(s(s(s(x + x))))) & = & s(s(s(s(s(x)))))+x \\
& \vdots &
\end{eqnarray*}

The critic then attempts to find 
the accumulating and nested term structure in each sequence which is 
causing divergence. In this case, successor
functions are accumulating on the first argument of +. 
To identify
this accumulating term structure, the critic uses difference
matching. Difference matching successive equations gives the annotated
sequence,
\begin{eqnarray*}
s(x + x) & = & s(x)+x \\
\wf{s(\wh{s(x + x)})} & = & \wf{s(\wh{s(x)})}+x \\
\wf{s(\wh{s(s(x + x))})} & = & \wf{s(\wh{s(s(x))})}+x \\
%\wf{s(\wh{s(s(s(x + x)))})} & = & \wf{s(\wh{s(s(s(x)))})}+x \\
%\wf{s(\wh{s(s(s(s(x + x))))})} & = & \wf{s(\wh{s(s(s(s(x))))})}+x \\
& \vdots & 
\end{eqnarray*}
This is the unique maximal difference match. 

The critic then tries to speculate a lemma which can be
used as a rewrite rule to move
the accumulating and nested term structure out of the way. 
In this case, the critic speculates
a rule for moving a successor function off the first argument of +.
That is, the rule,
$$ 
\wf{s(\wh{X})}+Y = \wf{s(\wh{X+Y})}.  $$
With this rule, {\sc Spike} is able to prove the $dbl$ theorem
without divergence. In addition, this rule is sufficiently
simple that it can be proved without assistance.
The heuristics used by the critic to perform this 
lemma speculation are
described in more detail in the next two sections.

The divergence analysis performed by the critic is
summarised in Figure 1.
\begin{figure}[htb]
%\begin{table}
\begin{center}
\fbox{
\begin{minipage}{4in}
{
\mbox{} 

\begin{enumerate}
\item There is a sequence of equations $s_i=t_i$ which
the prover attempts to prove by induction ($i$ = 0, 1 ...);
\item There exists (non trivial) $G, H$ such 
that for each $j$, the maximal difference match has
$s_{j}$ = $G(U_j)$, and $s_{j+1}=G(\wf{H(\wh{U_j})})$.
\end{enumerate}
%\begin{center}
%{\bf Preconditions to the divergence critic.}
%\end{center}
}
\end{minipage}
}
\caption{Preconditions to the divergence critic}
\end{center}
\end{figure}
In analysing the divergence, we consider
{\em all} the equations which the prover attempts to prove by induction.
This includes those equation where the induction proof succeeds as 
these can often suggest useful patterns. 
By ``non-trivial'' I wish to
exclude $\lambda \zzz \, .\, \zzz $, the identity
substitution. 
$H$ is thus the accumulating and nested term structure
that appears to be causing divergence.
For the $dbl$ example, $H$ is $\lambda \zzz \, .\, s(\zzz)$,
$G$ is $\lambda \zzz \, . \, \zzz + x$, and $U_0$ is $s(x)$.
Although $G$ and $H$ 
are second order variables, the second order nature of
the divergence analysis is limited. Indeed, the implementation
of the critic merely requires first order difference matching which is 
polynomial. For simplicity, 
the preconditions ignore the orientation of equations.
In addition, the preconditions can be easily generalised
to include multiple and nested annotations.
This allows the critic to recognise multiple sources of divergence
in the same equation. 
Techniques 
which identify accumulating term structure by most
specific generalization  \cite{dershowitz1}
cannot cope with divergence patterns that give
rise to nested annotations (see Section \ref{sec-related} for
more details).

The specification of the preconditions has left the length of sequence
undefined. If the sequence is of length 2, then the critic
is preemptive. That is, it will propose
a lemma just before another induction is attempted and 
divergence begins. Such a short sequence risks
identifying divergence when none exists.
On the other hand using a long sequence 
is expensive to test and allows the prover
to waste time on diverging
proof attempts. Empirically, a good compromise appears
to be to look for sequences of length 3. This is both
cheap to test and reliable.
To identify accumulating term structure, it appears to
be sufficient to use ground difference matching with
alpha conversion of variable names. There exists
a fast polynomial algorithm to perform such difference
matching based upon the ground difference matching
algorithm using dynamic programming
\cite{BasinWalshDu}. 
Since the skeleton
must be well typed (along with the erasure),
the algorithm is extended to
use sort information to prune 
potential difference matches.

\section{Lemma Speculation}
\label{sec-lemma}

One way of removing the accumulating and nested term structure
is to propose a {wave rule}
which moves this difference to the top of the term
leaving the skeleton unchanged.
We hope either that it will then cancel 
against wave-fronts on the other side of the equality
or that it will disappear in the process of being 
moved. For the $dbl$ theorem, 
after generalization (which is discussed in the next
section) the divergence pattern suggests
a rule of the form,
$$ \wf{s(\wh{X})}+Y = \wf{F(\wh{X+Y})} $$
where $F$ is a second order variable which
we need to instantiate. 
Instantiating $F$ is ultimately 
a difficult synthesis problem so we can only hope
to have heuristics that will work some of the time.
Two of the heuristics used by the divergence critic
to instantiate $F$ are {\em cancellation} and {\em petering out}. 

The cancellation heuristic uses difference
matching to identify term structure 
accumulating on the opposite side of the
sequence which would allow cancellation to
occur. Failing that, the cancellation heuristic
looks for suitable term structure
to cancel against in a new sequence (the original 
sequence is usually a divergence pattern of
a step case, whilst the new sequence
is usually a divergence pattern of a base
case). In the
$dbl$ example, successor functions accumulate
at the top of the left hand side of the diverging
equations,
\begin{eqnarray*}
s(x + x) & = & s(x)+x \\
\wf{s(\wh{s(x + x)})} & = & \wf{s(\wh{s(x)})}+x \\
\wf{s(\wh{s(s(x + x))})} & = & \wf{s(\wh{s(s(x))})}+x \\
%\wf{s(\wh{s(s(s(x + x)))})} & = & \wf{s(\wh{s(s(s(x)))})}+x \\
%\wf{s(\wh{s(s(s(s(x + x))))})} & = & \wf{s(\wh{s(s(s(s(x))))})}+x \\
& \vdots & 
\end{eqnarray*}
\noindent
This divergence pattern
suggests that $F$ should be instantiated to $\lambda \zzz \, . \, \sss(\zzz)$
to enable immediate cancellation.
Thus, as required, the cancellation heuristic suggests the rule,
$$ \wf{s(\wh{X})}+Y = \wf{s(\wh{X+Y})} . $$

The other heuristic used to instantiate
the right hand side of speculated lemmas 
is petering out. In moving the differences
up to the top of the term, they may disappear altogether. 
Consider, for example, the theorem,
$$ \forall l \ . \  \sorted(\isort(l)) = true $$
where \isort\ is insertion sort
and $\sorted$ is true iff a list is sorted into
order. These are defined by the conditional rewrite rules,
\begin{eqnarray*}
sorted(nil) & = & true \\
sorted(cons(X,nil)) & = & true \\
X<Y \rightarrow sorted(cons(X,cons(Y,Z))) & = & sorted(cons(Y,Z)) \\
isort(nil)& = & nil \\
isort(cons(X,Y)) & = & insert(X,isort(Y))
\end{eqnarray*}
where $insert(X,Z)$, which inserts the element $X$ into the
list $Z$ in order, and $X<Y$ are defined by the rewrite rules, 
\begin{eqnarray*}
0<X & = & true \\
s(X)<0 & = & false \\
s(X)<s(Y) & = & X<Y \\
insert(X,nil) & = & cons(X,nil) \\
X<Y \rightarrow insert(X,cons(Y,Z)) & = & cons(X,cons(Y,Z)) \\
\neg(X<Y) \rightarrow insert(X,cons(Y,Z)) & = & cons(Y,insert(X,Z)) \\
\end{eqnarray*}

Divergence analysis of {\sc Spike}'s attempt to prove this theorem 
suggests the need for a rule of the form,
%\begin{eqnarray*}
%\sorted(\wf{\insertd(\yyy,\wh{\xxx})}) & = & \sorted(\xxx)
%\end{eqnarray*}
$$ \sorted(\wf{\insertd(\YYY,\wh{\XXX})}) =  \wf{F(\wh{\sorted(\XXX)}} . $$
The petering out heuristic 
instantiates $F$ to the identity function $\lambda \zzz \, .\, \zzz$. This
gives the rule,
$$ \sorted(\wf{\insertd(\YYY,\wh{\XXX})}) =  \sorted(\XXX). $$
This rule allows the proof to go through without
divergence. 

As a more complex example, consider the theorem,
$$ \forall i, j, l \ . \ nth(i,nth(j,l)) = nth(j,nth(i,l)) $$
where $nth$ is defined by the rewrite rules,
\begin{eqnarray*}
nth(0,L) & = & L \\
nth(N,nil) & = & nil \\
nth(s(N),cons(H,T)) & = & nth(N,T).
\end{eqnarray*}
{\sc Spike}'s diverging attempt to prove this 
theorem generates the equations,
\begin{eqnarray*}
nth(s(i),nth(j,x)) & = & nth(s(j),nth(i,x)) \\
nth(s(s(i)),nth(j,cons(y,x))) & = & nth(s(j),nth(i,x)) \\
nth(s(s(s(i))),nth(j,cons(z,cons(y,x)))) & = & nth(s(j),nth(i,x)) \\
& \vdots & 
\end{eqnarray*}
Divergence analysis identifies
term structure accumulating in two different places,
\begin{eqnarray*}
nth(s(i),nth(j,x)) & = & nth(s(j),nth(i,x)) \\
nth(\wf{s(\wh{s(i)})},nth(j,\wf{cons(y,\wh{x})})) & = & nth(s(j),nth(i,x)) \\
nth(\wf{s(\wh{s(s(i))})},nth(j,\wf{cons(z,\wh{cons(y,x)})})) & = & nth(s(j),nth(i,x)) \\
& \vdots & 
\end{eqnarray*}
This is the unique maximal difference match.
This divergence pattern
suggests the need for a rewrite rule of the form,
$$ nth(\wf{s(\wh{I})},nth(J,\wf{cons(Y,\wh{X})})) = 
\wf{F(\wh{nth(I,nth(J,X))})}. $$
The petering out heuristic 
instantiates $F$ to the identity function $\lambda \zzz \, .\, \zzz$
giving the rule,
$$ nth(\wf{s(\wh{I})},nth(J,\wf{cons(Y,\wh{X})})) = 
nth(I,nth(J,X)). $$
This rule allows the proof to go through without
divergence. 


Since the erasure of the wave rule must be properly typed, sort information 
can be used to prune inappropriate instantiations for $F$. 
All speculated lemmas are therefore filtered through a type checker.
Speculated lemmas are also filtered through a conjecture disprover.
When a confluent set of rewrite rules exists for
ground terms, exhaustive normalization of some representative
set of ground instances of the equations is used to filter
out non-theorems. Alternatively,
the prover itself could be used to filter out non-theorems.
Unlike many other induction theorem provers, {\sc Spike} can
refute conjectures since its inference rules are 
refutationally complete for conditional theories in which
the axioms are ground convergent and defined functions
are completely defined over free constructors  \cite{rusi2}. 
Other techniques for
disproving conjectures are described by
Protzen (1992).
% \cite{protzen}.

The critic's lemma speculation is summarized in Figure 2
(using the same variable names as the preconditions).
\begin{figure}[htb]
\begin{center}
\fbox{
\begin{minipage}{4in}
{
\mbox{} 

\begin{enumerate}
\item The critic proposes a rule of the
form,
\begin{eqnarray*}
G(\wf{H(\wh{U_0})}) & = & \wf{F\wh{(G(U_0)})}
\end{eqnarray*}
\item $F$ is instantiated by the cancellation
or petering out heuristics;
\item Lemmas are filtered through a type checker and a conjecture
disprover;
\item If several lemmas are suggested, 
the critic deletes any that are subsumed.
\end{enumerate}
%\begin{center}
%{\bf Postconditions for the divergence critic.}
%\end{center}
}
\end{minipage}
}
\caption{Postconditions to the divergence critic}
\end{center}
\end{figure}
This specification
again uses second order variables in a limited
manner. First order difference matching is merely 
required to construct lemmas. As with the preconditions, 
the specification of the postconditions can be easily extended to deal
with multiple and nested wave-fronts (as in the
$nth(i,nth(j,l))=nth(j,nth(i,l))$ example).
Since the rules proposed by the critic move
the wave-fronts to top of the term, they
usually only introduce fresh divergence in the rare cases
that cancellation or fertilization fails. This is
unlikely since the cancellation and petering out
heuristics attempt to ensure {\em precisely}
that cancellation or fertilization
can take place. 

\section{Generalization}
\label{sec-general}

A major cause of divergence is the need to generalize.
Most of the lemmas proposed by the critic 
fix divergence, but attempting to prove
the lemmas themselves can cause fresh divergence. In addition,
several speculated lemmas can sometimes be replaced
by a single generalization. Generalized lemmas
also can lead to shorter, more elegant and natural proofs.
The critic therefore attempts to generalize the lemma
speculated, using the conjecture disprover to guard against
over-generalization. 

The main heuristic used for generalization is an extension of 
the primary term heuristic  \cite{aubinthesis}.
The {\em primary terms} are those terms encountered as
a term is explored from the root to the leaves 
ignoring non-recursive argument positions to functions. 
The same notion of recursive argument position is used
by the critic as defined by Bouhoula and Rusinowitch (1995a)
% \cite{rusi2}
and as used by {\sc Spike} for performing 
inductions. % \cite{rusi1}. 

Consider, for example, the theorem,
%\begin{eqnarray*}
%\len(\appd{\aaa}{\bbb}) & = & \len(\aaa)+\len(\bbb)
%\end{eqnarray*}
%$$\len(\appd{\aaa}{\bbb}) =  \len(\aaa)+\len(\bbb) $$
$$ \forall \aaa , \bbb \ . \ \len(\aaa)+\len(\bbb) = \len(\appd{\aaa}{\bbb}) $$
where + is again defined recursively on its second argument, 
and $len$ and $app$ are defined by means of the rewrite rules,
\begin{eqnarray*}
\len(\nild) & = & 0\\
\len(\consd{\HHH}{\TTT}) & = & \sss(\len(\TTT)) \\
\appd{\nild}{\TTT} & = & \TTT \\
\appd{\consd{\HHH}{\TTT}}{\RRR} & = & \consd{\HHH}{\appd{\TTT}{\RRR}}.
\end{eqnarray*}
This problem is taken from the {\sc Clam} library corpus \cite{Clam}.
{\sc Spike}'s attempt to prove this theorem
diverges. One of the sequences of equations generated is,
\begin{eqnarray*}
0+len(b) & = & len(b) \\
s(0)+len(b) & = & s(len(b)) \\
s(s(0))+len(b) & = & s(s(len(b))) \\
& \vdots &
\end{eqnarray*}
Difference matching identifies the term structure
causing divergence,
\begin{eqnarray*}
0+len(b) & = & len(b) \\
\wf{s(\wh{0})}+len(b) & = & \wf{s(\wh{len(b)})} \\
\wf{s(\wh{s(0)})}+len(b) & = & \wf{s(\wh{s(len(b))})} \\
& \vdots &
\end{eqnarray*}
This is the unique maximal difference match.
These annotations suggest the need for the wave rule,
$$\wf{\sss(\wh{0})}+\len(\BBB)  =
\wf{\sss(\wh{0+\len(\BBB)})}. $$
A set of candidate terms for
generalization is constructed by computing 
the intersection of the primary terms of the two sides of this rule.
In this case, the primary terms of the left hand side
are the set $\{ s(0)+\len(\BBB), \len(\BBB), \BBB\}$,
and the primary terms of the right hand side 
are the set $\{ s(0+\len(\BBB)), 0+\len(\BBB),\len(\BBB), \BBB\}$. 
The intersection of the primary terms
is thus the set $\{\len(\BBB),\BBB\}$. 
The critic picks members of the intersection
to generalize to new variables. 
Picking $\BBB$ justs gives an equivalent lemma up to renaming
of variables. Picking $\len(\BBB)$ gives the generalization,
$$ \wf{\sss(\wh{0})}+\YYY = 
\wf{\sss(\wh{0+\YYY})}. $$

The reason for considering just primary terms is that 
the recursive definitions typically provide wave rules for
removing term structure which accumulates at these positions.
In addition to primary terms, the divergence critic therefore 
also considers the positions of the wave-holes (but not
wave-fronts) in the skeleton of the lemma being
speculated. The motivation for this extension 
is that the speculated lemma will
allow accumulating term structure
to be moved from the wave-hole positions;
such positions are therefore also candidates for generalization.
Positions of the wave-fronts are not included since we
want to speculate a lemma that will move the term structure
at such positions. 

For instance, 
because of the wave-hole on the first argument of +
in the last example, 
$0$ is also
included in the intersection set of candidate terms for generalization.
Picking $0$ to generalize gives,
$$ \wf{\sss(\wh{\XXX})}+\YYY =  \wf{\sss(\wh{\XXX+\YYY})}. $$
The speculated lemma is now as general as is possible. This rule
allows the proof to go through without divergence. 

The critic also has a heuristic for merging
speculated lemmas. For instance, with the theorem $\sorted(\isort(\xxx))$,
the critic speculates several rules including,
\begin{eqnarray*}
\sorted(\wf{\insertd(0,\wh{\XXX})}) & = & \sorted(\XXX) \\
\sorted(\wf{\insertd(\sss(\YYY),\wh{\XXX})}) & = & \sorted(\XXX)
\end{eqnarray*}
As $\{0,\sss(\YYY)\}$ is a cover set
for the natural numbers, these two rules can be merged to
give,
%\begin{eqnarray*}
%\sorted(\wf{\insertd(\yyy,\wh{\xxx})}) & = & \sorted(\xxx)
%\end{eqnarray*}
$$ \sorted(\wf{\insertd(\YYY,\wh{\XXX})}) = \sorted(\XXX). $$


\section{Transverse Wave Rules}
\label{sec-transverse}

The lemmas speculated so far have moved accumulating
term structure directly to the top of the term where it is 
removed by cancellation or petering out. An alternative
way of removing accumulating term structure is to move 
it onto another argument position where: either
it can be removed
by matching with a ``sink'', a universally quantified variable in the
induction hypothesis; or it can be moved upwards by rewriting
with the recursive definitions.
Annotated rewrite rules which preserve the skeleton and
move wave-fronts across to other argument positions are called {\em
transverse} wave rules \cite{pub567}. 
Theorems involving functions with accumulators
provide a rich source of examples where such rewrite rules
prevent divergence. 

Consider, for example, a theorem about the 
correctness of tail recursive list reversal,
%\begin{eqnarray*}
%\qrev(\aaa,\bbb) & = & \appd{\rev(\aaa)}{\bbb}.
%\end{eqnarray*}
$$ \forall \aaa , \bbb \ . \ \qrev(\aaa,\bbb) = \appd{\rev(\aaa)}{\bbb} $$
where both $a$ and $b$ are universally 
quantified, $\rev$ is naive list reversal using
append, and $\qrev$ is tail recursive
list reversal building the reversed list on the
second argument position. These functions
are defined by the rewrite rules,
\begin{eqnarray*}
\rev(\nild) & = & \nild \\
\rev(\consd{\HHH}{\TTT}) & = & \appd{\rev(\TTT)}{\consd{\HHH}{\nild}} \\
\qrev(\nild,\RRR) & = & \RRR \\
\qrev(\consd{\HHH}{\TTT},\RRR) & = & \qrev(\TTT,\consd{\HHH}{\RRR}).
\end{eqnarray*}
{\sc Spike}'s attempt to prove this theorem 
diverges generating the following sequence of
equations which the prover attempts to show by induction,
\begin{eqnarray*}
\qrev(\aaa,\bbb) & = & \appd{\rev(\aaa)}{\bbb}  \\
\qrev(\aaa,{\consd{\ccc}{{\bbb}}}) & = & \appd{{\appd{{\rev(\aaa)}}{\consdnil{\ccc}}}}{\bbb} \\
\qrev(\aaa,{\consd{\ccc}{{\consd{\ddd}{\bbb}}}}) & = & 
\appd{{\appd{{\appd{\rev(\aaa)}{\consdnil{\ccc}}}}{\consdnil{\ddd}}}}{\bbb} \\
& \vdots & 
\end{eqnarray*}
Difference matching identifies 
the term structure accumulating within these equations
that is causing divergence,
\pagebreak
\begin{eqnarray*}
\qrev(\aaa,\bbb) & = & \appd{\rev(\aaa)}{\bbb}  \\
\qrev(\aaa,\wf{\consd{\ccc}{\wh{\bbb}}}) & = & \appd{\wf{\appd{\wh{\rev(\aaa)}}{\consdnil{\ccc}}}}{\bbb} \\
\qrev(\aaa,\wf{\consd{\ccc}{\wh{\consd{\ddd}{\bbb}}}}) & = & 
\appd{\wf{\appd{\wh{\appd{\rev(\aaa)}{\consdnil{\ccc}}}}{\consdnil{\ddd}}}}{\bbb} \\
& \vdots & 
\end{eqnarray*}
This is the unique maximal difference match. 
Rather than move
the accumulating term structure on the
right hand side of the equations to the top of the
term, it is much simpler to move the
accumulating term structure from the first 
onto the second argument of the outermost append. 
The critic therefore proposes a {transverse} wave rule,
which preserves the skeleton but moves the difference onto a different
argument position. In this example, this is a rule of the form,
%\begin{eqnarray*}
%\appd{\wf{\appd{\wh{\rev(\aaa)}}{\consdnil{\ccc}}}}{\bbb} & = & 
%\appd{\rev(\aaa)}{\wf{F({\wh{\bbb}})}} 
%\end{eqnarray*}
$$ \appd{\wf{\appd{\wh{\rev(\AAA)}}{\consdnil{\CCC}}}}{\BBB}  = 
\appd{\rev(\AAA)}{\wf{F({\wh{\BBB}})}}.  $$
In moving the difference onto another argument position,
the difference may change syntactically. The right hand side
of the lemma is therefore only partially determined. To instantiate $F$, 
the critic uses two heuristics: {\em fertilization} and
{\em simplification}. 

The fertilization heuristic
uses matching to find an instantiation for 
$F$ which enables immediate fertilization. In this case,
matching against the universally quantified
variable $b$ in the induction hypothesis suggests,
%\begin{eqnarray*}
%\appd{\wf{\appd{\wh{\rev(\aaa)}}{\consdnil{\ccc}}}}{\bbb} & = & 
%\appd{\rev(\aaa)}{\wf{\consd{\ccc}{\wh{\bbb}}}}  
%\end{eqnarray*}
$$ \appd{\wf{\appd{\wh{\rev(\AAA)}}{\consdnil{\CCC}}}}{\BBB} =  
\appd{\rev(\AAA)}{\wf{\consd{\CCC}{\wh{\BBB}}}}.  $$
Finally the critic generalizes the lemma using the 
same extended primary term heuristic as before 
({\it i.e.}, augmenting recursive positions
with wave-hole positions). This gives the rule,
%\begin{eqnarray*}
%\appd{\wf{\appd{\wh{\aaa}}{\consdnil{\ccc}}}}{\bbb} & = & 
%\appd{\aaa}{\wf{\consd{\ccc}{\wh{\bbb}}}}  
%\end{eqnarray*}
$$ \appd{\wf{\appd{\wh{\AAA}}{\consdnil{\CCC}}}}{\BBB}  = 
\appd{\AAA}{\wf{\consd{\CCC}{\wh{\BBB}}}}.   $$
This is exactly the rule needed by {\sc Spike} to complete the proof.
In addition, it is simple enough to be proved by itself 
without divergence; this is not true of the 
ungeneralized rule.

The other heuristic used to instantiate
the right hand side of the speculated 
lemma is the simplification heuristic. 
The heuristic uses regular matching to find an instantiation 
for $F$ which will enable the wave-front to be
simplified using one of the recursive definitions. 
Consider again the $dbl$ theorem from the introduction.
Divergence analysis identifies successor functions 
accumulating on the first argument position
of +. This accumulating term structure can either
be moved to the top of the term tree or alternatively
onto the second argument position of + using a transverse
wave rule of the form,
$$ \wf{s(\wh{X})}+Y = X+\wf{F(\wh{Y})} . $$
The right hand side of this transverse wave rule is 
instantiated by the simplification heuristic. 
The wave-front on the right hand side can be simplified by the
rewrite rule recursively defining +
if $F$ is instantiated by $\lambda z \, . \, s(z)$.
That is, if we have the rule,
$$ \wf{s(\wh{X})}+Y = X+\wf{s(\wh{Y})} . $$
This rule allows the proof to go through without
divergence.

Speculated transverse wave rules are generalized using the 
extended primary terms heuristic described in Section \ref{sec-general}.
The divergence critic also generalizes transverse wave
rules by means of an {\em equality} heuristic. This heuristic attempts to
cancel equal outermost functors where possible.
For example, consider the theorem,
%\begin{eqnarray*}
%\half(\xxx+\xxx)
%& = & \xxx
%\end{eqnarray*}
$$ \forall \xxx , \yyy \ . \ (\xxx+\yyy)-\xxx =  \yyy $$
where addition is defined recursively on 
its second argument position and
subtraction is defined by the rewrite rules,
\begin{eqnarray*}
X-0 & = & X \\
0-X & = & 0 \\
s(\XXX)-s(\YYY) & = & \XXX-\YYY.
\end{eqnarray*}
{\sc Spike}'s attempt to prove this theorem diverges
generating (amongst others) the goals,
\begin{eqnarray*}
(x+y)-x & = & y \\
(s(x)+y)-x & = & s(y) \\
(s(s(x))+y)-x & = & s(s(y)) \\
% (s(s(s(x)))+y)-x & = & s(s(s(y))) \\
& \vdots & 
\end{eqnarray*}
Divergence analysis identifies accumulating term structure
within these equations,
\begin{eqnarray*}
(x+y)-x & = & y \\
(\wf{s(\wh{x})}+y)-x & = & \wf{s(\wh{y})} \\
(\wf{s(\wh{s(x)})}+y)-x & = & \wf{s(\wh{s(y)})} \\
& \vdots & 
\end{eqnarray*}
This is the unique maximal difference match.
These annotations suggest the need for the transverse rule,
%\begin{eqnarray*}
%\half(\wf{\sss(\wh{\XXX})}+\YYY) & = & \half(\XXX+\wf{\sss(\wh{\YYY})})
%\end{eqnarray*}
$$ (\wf{s(\wh{X})}+Y)-X  =  (X+\wf{s(\wh{Y})})-X. $$
The equality heuristic deletes the equal outermost function,
$\lambda z \, . \, z - X$. This gives
the more general lemma,
%\begin{eqnarray*}
%\wf{\sss(\wh{\xxx})}+\yyy & = & \xxx+\wf{\sss(\wh{\yyy})}
%\end{eqnarray*}
$$ \wf{s(\wh{X})}+Y  =  X+\wf{s(\wh{Y})}. $$

All speculated lemmas are filtered through a type checker
to ensure that their erasure is well typed. 
Speculated lemmas are also filtered through a
conjecture disprover to guard against 
over-generalization.

The actions of the critic are summarized in Figure 3.
\begin{figure}[htb]
\begin{center}
\fbox{
\begin{minipage}{4in}
{
\mbox{} 

Preconditions:
\begin{enumerate}
\item There is a sequence of equations $s_i=t_i$ which
the prover attempts to prove by induction ($i$ = 0, 1 ...);
\item There exists (non trivial) $G, H$ such 
that for each $j$, the maximal difference match has
$s_{j} = G(U_j,Acc)$  and
$s_{j+1} = G(\wf{H(\wh{U_j})},Acc)$. 
\end{enumerate}
Postconditions:
\begin{enumerate}
\item The critic proposes a rule of the
form,
\begin{eqnarray*}
G(\wf{H(\wh{U_0})},Acc) & = & G(U_0,\wf{F(\wh{Acc})})
\end{eqnarray*}
\item $F$ is instantiated by the fertilization or simplification
heuristics;
\item The lemma is generalized using the (augmented) primary terms 
and equality heuristics;
\item Generalized lemmas are filtered through a 
type checker and a conjecture
disprover;
\item If several lemmas are suggested, 
the critic deletes any that are subsumed.
\end{enumerate}
}
\end{minipage}
}
\caption{Speculation of transverse wave rules.}
\end{center}
\end{figure}
The specification of preconditions and postconditions
again uses second order variables but in a limited
manner. The implementation merely requires
second order matching and first order difference matching.
The preconditions and postconditions can be easily generalised
to include multiple and nested annotations.
We could also speculate
hybrid wave rules which ripple part of 
the wave-front across and part of it up
the term tree. However, such
rules appear to be rare. In addition, 
such hybrid wave rules can often be decomposed 
into a pair of wave rules, one of which moves some
of the wave-fronts up the term tree, and 
another which moves the wave-fronts across. 


\section{Implementation}
\label{sec-implementation}

The divergence critic described in the previous sections has
been implemented in {\sc Prolog}. The system consists of 787
lines of code defining approximate 100 different
{\sc Prolog} predicates. More recently a cut down version has been
incorporated directly within the {\sc Spike} system 
which is written in {\sc Caml Light} \cite{Spike-manual}. 
The output of {\sc Spike} is parsed to generate input
to the critic. The input consists of: 
the equations which the prover attempts to prove
by induction; sort information (for the type checker
and difference matcher);
the recursive argument positions (for constructing
primary terms); and the rewrite rules defining
the theory (used by the conjecture disprover). 

Figure 1 gives the divergence critic's output on
the problem discussed in the introduction.
Either of the proposed lemmas when used as a rewrite rule is
adequate to fix divergence. In addition, the proposed 
lemmas are sufficiently simple to be proved 
automatically without introducing fresh divergence. 
The first lemma is a rewrite rule
for moving accumulating successor functions from 
the first argument position of + to the top of 
the term tree. 
The second lemma is a transverse wave rule
discussed in Section \ref{sec-transverse}
for moving accumulating successor functions from 
the first argument position of + to the second
argument position.

\begin{figure}
{
\hline
\begin{verbatim}

% compiling file /home/dream5/tw/work/Spike/diverge/data.double.x+x
% data.double.x+x compiled in module user, 0.233 sec 1,612 bytes

| ?- speculate.

  Equations input:
  double(x1)=x1+x1
  s(x1+x1)=s(x1)+x1
  s(s(x1+x1))=s(s(x1))+x1
  s(s(s(x1+x1)))=s(s(s(x1)))+x1

  Lemmas speculated:
  s(x1)+x1=s(x1+x1)
  s(x1)+x99=s(x1+x99)
  s(x99)+x1=s(x99+x1)
  s(x99)+x100=s(x99+x100)
  s(x1)+x1=x1+s(x1)
  s(x1)+x99=x1+s(x99)
  s(x99)+x1=x99+s(x1)  
  s(x99)+x100=x99+s(x100)

  Deleting lemmas subsumed:
  s(x1)+x99=s(x1+x99)
  s(x1)+x99=x1+s(x99)

  Merging remaining lemmas:
  s(x1)+x99=s(x1+x99)
  s(x1)+x99=x1+s(x99)

yes
| ?- 


\end{verbatim}
}
\hline
\caption{Example output of the divergence critic. }
\end{figure}


The critic is successful at identifying
divergence and proposing appropriate lemmas and generalizations
for a significant number of theorems. 
Divergence analysis is very quick on most examples. The divergence
pattern is recognized usually in less than a second. Most of
the time is spent looking for generalizations and refuting 
over-generalizations with the conjecture disprover.
This usually takes between 1 and 100 seconds. Additional heuristics 
for preventing over-generalization and a more efficient 
implementation of the conjecture disprover would speed up
the critic considerably. 

%\begin{figure}[h]
%\begin{verbatim}
%
%
%yes
%| ?- 
%
%\end{verbatim}
%\caption{More example output of the divergence critic.}
%\end{figure}


\section{Results}
\label{sec-results}

Table 1 lists 30 theorems that cause {\sc Spike}
to diverge and the lemmas speculated
by the divergence critic
after analysing the diverging proof attempts. 
These problems provide a representative
sample of the type of theorems for which the
cause of divergence can be identified and an appropriate
lemma or generalization speculated. 
Many of these problems
come from the {\sc Clam} library corpus. %\cite{Clam}.
Part of this table has appeared
before \cite{divergence-critic}.
Times are for the divergence critic to speculate the lemmas
and are for the average of 10 runs on a Sun
4 running {\sc Quintus} 3.1.1. 

\begin{table}
{
{\small
\begin{tabular}{|r|c|c|r|} \hline
No & Theorem & Lemmas speculated & Time/s \\ \hline \hline
1 & s(x)+x=s(x+x) & s(X)+Y=s(X+Y) & 7.8 \\
& & s(X)+Y=X+s(Y) & \\ \hline
2 & dbl(x)=x+x $\leftrightarrow$ & s(X)+Y=s(X+Y) & 8.2 \\
& $ \ \ \ \ $  dbl(0)=0, \ dbl(s(x))=s(s(dbl(x))) & s(X)+Y=X+s(Y) & \\ \hline
3 & len(\app{x}{y})=len(\app{y}{x}) & 
 len(\app{X}{(\cons{Z}{Y})})=s(len(\app{X}{Y})) & 3.6 \\
& &len(\app{X}{(\cons{Z}{Y})})=len(\app{(\cons{W}{X})}{Y}) & \\
\hline
4 & len(\app{x}{y})=len(x)+len(y) & s(X)+Y=s(X+Y)
& 7.2 \\ % \hline
& & s(X)+Y=X+s(Y) & \\ \hline
5 & len(\app{x}{x})=dbl(len(x)) &
len(\app{X}{(\cons{Z}{Y})})=s(len(\app{X}{Y})) & 11.6 \\
& & len(\app{X}{(\cons{W}{\cons{Z}{Y}})})=s(len(\app{X}{(\cons{W}{Y})})) &
\\ \hline
6 & even(x+x) &  even(s(s(X))+Y)=even(X+Y) & 5.4 \\ \hline
7 & odd(s(x)+x) & odd(s(s(X))+Y)=odd(X+Y) & 16.0 \\ \hline
8 & even\mbox{${}_m$}(x+x) &
even\mbox{${}_m$}(s(s(X))+Y)=even\mbox{${}_m$}(X+Y) & 28.4 \\
& & odd\mbox{${}_m$}(s(s(X))+Y)=odd\mbox{${}_m$}(X+Y) &  \\ \hline
9 & odd\mbox{${}_m$}(s(x)+x) &
even\mbox{${}_m$}(s(s(X))+Y)=even\mbox{${}_m$}(X+Y) & 65.5 \\
& & odd\mbox{${}_m$}(s(s(X))+Y)=odd\mbox{${}_m$}(X+Y) &  \\ \hline
10 & even\mbox{${}_m$}(x) $\rightarrow$ half(x)+half(x)=x &
s(X)+Y=s(X+Y) & 6.0 \\ % \hline
& & s(X)+Y=X+s(Y) & \\ \hline
11 & half(x+x)=x &  s(s(X))+Y=X+s(s(Y)) & 11.1 \\ 
& & half(s(s(X))+Y)=half(X+Y) & \\ \hline
12 & half(s(x)+x)=x &  s(s(X))+Y=X+s(s(Y)) & 31.0 \\ 
& & half(s(s(X))+Y)=half(X+Y) & \\ \hline
13 & rot(len(x),x)=x &
rot(len(X),\app{X}{\consnil{Y}})=\cons{Y}{rot(len(X),X)} & 2.4 \\ \hline
14 & len(rot(len(x),x))=len(x) &  
len(rot(X,\app{Z}{\consnil{Y}}))=s(len(rot(X,Z)))  & 4.8 \\ \hline
15 & rot(len(x),\app{x}{\consnil{y}})=\cons{y}{rot(len(x),x)} & 
\app{(\app{X}{\consnil{Y}})}{Z}=\app{X}{(\cons{Y}{Z})}& 86.3 \\
& &
rot(len(X),\app{(\app{X}{\consnil{Y}})}{Z})=\cons{Y}{rot(len(X),\app{X}{Z})}
&  \\ \hline
16 & len(rev(x))=len(x) & len(\app{X}{\consnil{Y}})=s(len(X)) & 2.0 \\ \hline
17 & rev(rev(x))=x & rev(\app{X}{\consnil{Y}})=\cons{Y}{rev(X)} & 1.2
\\ \hline 
18 & rev(\app{rev(x)}{\consnil{y}})=\cons{y}{x} &
 rev(\app{X}{\consnil{Y}})=\cons{Y}{rev(X)} & 16.0  \\  \hline
19 & rev(\app{rev(x)}{\consnil{y}})=\cons{y}{rev(rev(x))} &
rev(\app{X}{\consnil{Y}})=\cons{Y}{rev(X)}
& 18.6 \\ \hline
%15 & len(rev(\app{rev(x)}{\consnil{y}}))=s(len(x)) &
%len(\app{x}{\consnil{y}})=s(len(x)) & 1.7 \\ \hline
20 & len(rev(\app{x}{y}))=len(x)+len(y) &
len(\app{X}{\consnil{Y}})=s(len(X)) & 10.0 \\
& & s(X)+Y=s(X+Y)& \\ % \hline
& & s(X)+Y=X+s(Y)& \\ \hline
21 & len(qrev(x,\nil))=len(x) & len(qrev(X,\cons{Z}{Y}))=s(len(qrev(X,Y)))
& 2.2 \\ \hline
22 & qrev(x,y)=\app{rev(x)}{y} &
\app{(\app{X}{\consnil{Y}})}{Z}=\app{X}{(\cons{Y}{Z})} & 3.4 \\ \hline
23 & len(qrev(x,y))=len(x)+len(y) & s(X)+Y=s(X+Y)
& 12.0 \\ % \hline
& & s(X)+Y=X+s(Y) & \\ \hline
24 & qrev(qrev(x,\nil),\nil)=x &
qrev(qrev(X,{\consnil{Y}}),Z)=\cons{Y}{qrev(qrev(X,\nil),Z)} & 5.0 \\
\hline
25 & rev(qrev(x,\nil))=x & 
rev(qrev(X,\consnil{Y}))=\cons{Y}{rev(qrev(X,\nil))} & 5.8 \\ 
\hline
26 & qrev(rev(x),\nil)=x &
qrev(\app{X}{\consnil{Y}},Z)=\cons{Y}{qrev(X,Z)} & 5.2 \\ \hline
27 & nth(i,nth(j,x))=nth(j,nth(i,x)) & 
nth(s(I),nth(J,\cons{Y}{X}))=nth(I,nth(J,X)) & 7.4 \\ \hline
28 & nth(i,nth(j,nth(k,x)))=nth(k,nth(j,nth(i,x))) & 
nth(s(I),nth(J,\cons{Y}{X}))=nth(I,nth(J,X)) & 7.6 \\ \hline
29 & len(isort(x))=len(x) & len(insert(Y,X))=s(len(X)) & 2.0 \\ \hline
30 & sorted(isort(x)) & sorted(insert(Y,X))=sorted(X) & 114 \\
& & sorted(insert(Y,insert(Z,X)))=sorted(X) & \\ \hline
\end{tabular} 
}

\caption{Some lemmas speculated by the divergence critic.}

% \vspace{0.5em}

\noindent
{\bf Notes:} \cons{}{} is written for 
infix cons, \app{}{} for infix append, \nil\ for 
\nild, and \consnil{\xxx} for \consdnil{\xxx}. 
In addition, even is defined by a s(s(x)) recursion,
even$\mbox{}_{m}$ by a mutual recursion with
odd$\mbox{}_{m}$, and
rot($n,l$) rotates a list $l$ by $n$ elements.


}
\end{table}

{\sc Spike}'s proof attempt diverges on each example when given
the definitions alone. 
In each of the 30 cases,
the critic is quickly able to suggest a lemma which 
overcomes divergence. 
When multiple lemmas are proposed (with the exception of 20)
any one on its own is sufficient
to fix divergence. In every case (except 13 and 24)
the lemmas proposed are sufficiently simple to be proved 
automatically without introducing fresh divergence. 
In the majority of cases, the lemmas proposed are optimal;
that is, they are the simplest possible lemmas which 
fix divergence. In the cases when the lemma
is not optimal, they are usually only slightly more
complex than the simplest lemma which fixes divergence.
In many of the examples, other lemmas are conjectured
by the divergence analysis but these are quickly rejected by the
conjecture disprover. For example, in example 16, divergence
analysis and the petering out heuristic suggest the rule,
$$ \# \# \ \ \ \ \ \  len(\wf{app(\wh{X},cons(Y,nil))})=len(X) \ \ \ \ \ \ \# \# $$
However, this is refuted by exhaustive normalization
using any ground terms for $X$ and $Y$.
In this case, the cancellation heuristic identifies the required
lemma, 
$$  len(\wf{app(\wh{X},cons(Y,nil))})=\wf{s(\wh{len(X)})} . $$

Some of the examples deserve additional comment. 
In example 1,
the divergence critic identifies that successor functions
are accumulating on the first argument position of $+$.
The critic speculates a lemma for moving these successor functions
either to the top of the term (so that immediate cancellation
can occur) or onto to the second argument position (so that
simplification with the recursive definition of $+$ can occur).
The first lemma speculated is in fact a generalization
of the theorem being proved. 
Example 2 is a simple program verification
problem taken from Dershowitz and Pinchover (1990).
%\cite{dershowitz1}.
The forward direction of this
theorem was discussed in the introduction.
Similar divergence occurs as in example 1 and,
after generalization, the same lemmas are speculated.

Example 3 caused divergence in the beta-version of {\sc Spike}
available in the summer of 1994.
The proof rules in {\sc Spike} have since been strengthened and this
example no longer causes divergence in the current release.
The speculated
lemmas do, however, simplify the proof. 
Example 4 was used in the text to illustrate 
the generalization heuristics.
The second lemma in example 5 is 
perhaps a little surprising,
%$$ len(app(X,{(cons(W,\wf{\cons{Z}{\wh{Y}}}})})=\wf{s(\wh{len(\app{X}{(\cons{W}{Y})})})}. $$
 $$ len(app(X,(cons(W,\wf{cons(Z,\wh{Y})}))))=\wf{s(\wh{len(app(X,cons(W,Y)))})} . $$
Although it is more complex than the first lemma, it 
is nearly as good at fixing divergence. 

In example 6, the lemma proposed,
$$ even(\wf{s(s(\wh{X}))}+Y) = even(X+Y) $$ 
is not optimal. That is,
it is not the simplest
possible lemma that fixes divergence. To fix divergence,
we merely need one of the rules, $s(X)+Y=s(X+Y)$ or
$s(X)+Y=X+s(Y)$. Either of these will ripple the successor functions
accumulating on 
the first argument position of $+$. The divergence critic 
attempts to construct a lemma to ripple two successor functions 
across from the first to the second argument positions of 
$+$. Unfortunately, the critic fails to find an appropriate instantiation
for the right hand side of such a lemma.
The critic instead proposes a rule to move the two successor
functions up to the top of the term where the
wave-front can peter out. Example 7 is very similar
to example 6. 


Examples 8 to 10 demonstrate that the critic can 
cope with divergence in theories involving mutual recursion.
In example 8, {\sc Spike} attempts to prove by induction the equations,
\begin{eqnarray*}
even_m(x+x) & = & true \\
odd_m(s(x)+x) & = & true \\
even_m(s(s(x))+x) & = & true \\
odd_m(s(s(s(x)))+x) & = & true \\
even_m(s(s(s(s(x))))+x) & = & true \\
% odd_m(s(s(s(s(s(x)))))+x) & = & true \\
& \vdots &
\end{eqnarray*}
The critic identifies two inter-linking divergence
patterns,
%\begin{eqnarray*}
%even_m(x+x) & = & true \\
%even_m(\wf{s(s(\wh{x}))}+x) & = & true \\
%even_m(\wf{s(s(\wh{s(s(x))}))}+x) & = & true \\
%& \vdots &
%\end{eqnarray*}
%And,
%\begin{eqnarray*}
%odd_m(s(x)+x) & = & true \\
%odd_m(\wf{s(s(\wh{s(x)}))}+x) & = & true \\
%odd_m(\wf{s(s(\wh{s(s(s(x)))}))}+x) & = & true \\
%& \vdots &
%\end{eqnarray*}
\begin{eqnarray*}
even_m(x+x)  =  true & \ \ \ \ \ \ \ \ \ \ & odd_m(s(x)+x)  =  true  \\
even_m(\wf{s(s(\wh{x}))}+x) =  true & & odd_m(\wf{s(s(\wh{s(x)}))}+x) =  true  \\
even_m(\wf{s(s(\wh{s(s(x))}))}+x)  =  true & & odd_m(\wf{s(s(\wh{s(s(s(x)))}))}+x)  =  true \\
\vdots & & \vdots 
\end{eqnarray*}
The critic therefore proposes rules which ripple
this accumulating term structure up to the
top of the term where it peters out,
\begin{eqnarray*}
even_m(\wf{s(s(\wh{X}))}+Y) & = & even_m(X+Y) \\
odd_m(\wf{s(s(\wh{X}))}+Y) & = & odd_m(X+Y) 
\end{eqnarray*}
Just as in examples 6 and 7, these are not the
optimal rules for fixing divergence. 
Nevertheless, either of the
proposed rules fix divergence and both can
be proved without difficulty by {\sc Spike}.  
Example 9 is very similar to example 8.

Examples 10 to 12 require little comment. 
In example 13, the proposed lemma is too difficult to
be proved automatically. However, the divergence critic is 
able to identify the cause of this difficulty and propose
a lemma which allows the proof to go through
(example 15). In example 14, the speculated lemma is
not optimal. The simpler lemma speculated in example 13 would be 
adequate to prove this theorem without divergence. 
The speculated lemma is not optimal because the divergence
critic attempts to ripple the accumulating term structure
over two functors, $len$ and $rot$
to the top of the term tree. However, it is sufficient on 
this problem to ripple it up over just one functor, $rot$. 

Examples 16 to 19 are straightforward
and do not require discussion. 
In example 20, the critic identifies
two separate divergence patterns. To overcome divergence,
the first lemma plus one or other of the second and
third are therefore needed.
The first divergence pattern
occurs in the sequence of subgoals,
\begin{eqnarray*}
len(rev(x))  & = &  0+len(x) \\
len(\wf{app(\wh{rev(x)},cons(y,nil))})  & = &  \wf{s(\wh{0+len(x)})} \\
len(\wf{app(\wh{app(rev(x),cons(y,nil))},cons(z,nil))})  & = &  \wf{s(\wh{s(0+len(x))})} \\
& \vdots & 
\end{eqnarray*}
Term structure is accumulating on the 
second argument of append. Such term structure is removed
by the first rule,
\begin{eqnarray*}
len(\wf{app(\wh{X},cons(Y,nil))})  & = &  \wf{s(\wh{len(X)})}
\end{eqnarray*}
The second divergence pattern
occurs in the sequence of subgoals,
\begin{eqnarray*}
 s(x)+len(y) & = & s(x+len(y)) \\
 \wf{s(\wh{s(x)})}+len(y)  & = & \wf{s(\wh{s(x+len(y))})} \\
 \wf{s(\wh{s(s(x))})}+len(y)  & = &  \wf{s(\wh{s(s(x+len(y)))})} \\
& \vdots & 
\end{eqnarray*}
Term structure is accumulating on the
first argument of $+$. This is removed by one or other
of the second and third rules,
\begin{eqnarray*}
\wf{s(\wh{X})} + Y & = & \wf{s(\wh{X+Y})} \\
\wf{s(\wh{X})} + Y & = & X+\wf{s(\wh{Y})} 
\end{eqnarray*}


Examples 21 and 23 are reasonably straightforward.
The lemma speculated in example 22 is a special
case of the associativity of append. More powerful
generalization heuristics could have speculated 
the associativity of append. However, such heuristics
would also speculate more non-theorems. Further research
into the optimal strength of generalization heuristics
would be valuable.

Example 24 is the only disappointment; the 
lemma proposed fixes divergence but is too difficult to be proved
automatically, even with the assistance of the divergence
critic. 
See example 34 at the end of this section for more
details.
Example 25 is discussed in more detail in 
the related work in Section \ref{sec-related}
as it demonstrates the superiority of difference matching
over generalization techniques for divergence analysis.
Examples 26 to 28 require little discussion.
Finally, examples 29 and 30 demonstrate that the critic can
cope with divergence in moderately complex
theories containing conditional equations.

The results are very pleasing. Using the divergence critic,
the 30 theorems listed (with the exception
of 24) can all be proved from the definitions alone.
To provide an indication of the difficulty of these theorems, 
the {\sc Nqthm} system \cite{boyer1},
which is perhaps the best 
known explicit induction theorem prover, was unable to prove
more than half these theorems from the definitions alone. To be precise,
{\sc Nqthm} failed on 
5, 6, 7, 8, 9,
11, 12, 13, 14,
15, 18, 19, 21,
22, 24, 25, 26,
27 and 28.
Of course, with the addition of some simple lemmas, {\sc Nqthm}
is able to prove all these theorems. Indeed, in many cases, {\sc Nqthm} needs
the same lemmas as those proposed by the divergence critic and
required by {\sc Spike}.
This suggests that the divergence critic is not especially 
tied to the particular
prover used nor even to the implicit induction setting. 

To test this
hypothesis, I presented the output of a diverging proof attempt
from {\sc Nqthm} to the critic. I chose the commutativity of multiplication
as this is perhaps the simplest theorem which causes {\sc Nqthm}
to diverge. The critic proposed the lemma,
\begin{verbatim}
         (EQUAL (TIMES Y (ADD1 X)) (PLUS Y (TIMES Y X))))
\end{verbatim}
where {\tt TIMES} and {\tt PLUS} are primitives of {\sc Nqthm}'s logic
recursively defined on their first arguments. This is exactly
the lemma needed by {\sc Nqthm} to prove the
commutativity of multiplication. {\sc Nqthm} fails on many of the other
examples for similar reasons to {\sc Spike}, and
divergence analysis identifies an appropriate
lemma. This supports 
the suggestion that the divergence critic
is likely to be useful for a wide variety of provers.

The divergence critic has several limitations. 
Recognizing divergence is, in general, undecidable since
it reduces to the halting problem. The divergence critic will therefore 
sometimes fail to identify a diverging proof attempt. 
In addition, the critic will sometimes identify a ``divergence'' pattern when 
the proof attempt is not diverging. 
Even when divergence is correctly identified, the critic will sometimes
fail to speculate an appropriate lemma. Finally, the critic
only speculates wave-rules. Whilst many theories
contain a large number of wave-rules, and these are often
very useful for fixing divergence, other types of lemma
can be needed. 

Table 2 
lists four theorems on which the divergence critic
fails. These problems are representative
of the different ways in which the critic can fail.
The two main cause of failure are overlapping 
divergence patterns, 
and the inability of the heuristics
to speculate an appropriate right hand side for
a lemma. Again times are those to speculate lemmas
and not to find a proof of the theorem. 

{\small
\begin{table}
{\begin{tabular}{|r|c|c|r|} \hline
No & Theorem & Lemmas speculated & Time/s \\ \hline \hline
31 & s(x) $\times$ y=y+(x $\times$ y) & -- & n/a \\ \hline
32 & x $\times$ y=y $\times$ x & s(X)+Y=X+s(Y) & 8.0 \\ \hline
33 & x+(y+(z+(v+w))) = w+(x+(y+(z+v))) & s(X)+Y=s(X+Y) & 17.7 \\
   &               & s(X)+Y=X+s(Y) & \\ \hline
34 & qrev(qrev(x,{\consnil{y}}),z)=\cons{y}{qrev(qrev(x,\nil),z)} & 
qrev(Y,\cons{X}{Z})) = qrev(\cons{X}{Y},Z) & 9.6 \\
& &  qrev(qrev(X,\cons{Y}{Z}),W)=qrev(qrev(\cons{Y}{X},Z),W) & \\
& &  qrev(qrev(X,\cons{Y}{\consnil{Z}}),W)=\cons{Z}{qrev(qrev(X,\consnil{Y}),W)} & \\ \hline
\end{tabular}}

\caption{Some of the divergence critic's failures.}
\end{table}}

Example 31 is a commuted version of the recursive definition of 
multiplication
($\times$ is defined recursively on its 
second argument position). 
{\sc Spike}'s attempt to prove this theorem diverges,
generating the following
sequence of equations,
\begin{eqnarray*}
s(y) + (x+ (x \times y)) & = & s(y) + (y + (x \times y)) \\
s(s(y)) + (x + (x + (x\times  y))) & = & s(x) + (s(y) + (x + (x \times y)) \\
s(s(s(y))) + (x + (x + (x + (x \times y)))) & = & s(x) + (s(s(y)) + (x + (x + (x \times y)))) \\
& \vdots &
\end{eqnarray*}
Divergence analysis of the left hand sides of
these equations suggests the need for a rule of 
the form,
\begin{eqnarray*}
\wf{s(\wh{Y})} + \wf{(X+ \wh{Z})} & = & \wf{F(\wh{Y + Z})}
\end{eqnarray*}
Unfortunately the heuristics for lemma speculation are
not sufficiently strong to suggest a suitable
instantiation for $F$ (for example, $\lambda z \, . \, s(X + z)$). 
This lemma is rather complex and is the result of
two overlapping divergence patterns. If
the annotations are considered separately, 
they suggest the rules,
\begin{eqnarray*}
\wf{s(\wh{X})} + Y & = & \wf{s(\wh{X+Y})} \\
Y + \wf{(X+\wh{Z})} & = & \wf{X+\wh{(Y+Z)}} 
\end{eqnarray*}
With these two rules, {\sc Spike} finds a proof without difficulty.

Example 32 is the
commutativity of multiplication.
The divergence critic identifies a divergence
pattern and proposes the transverse wave rule,
\begin{eqnarray*}
\wf{s(\wh{X})}+Y & = & X+\wf{s(\wh{Y})}
\end{eqnarray*}
However, {\sc Spike} is unable to prove the
commutativity of multiplication with the
addition of this rule. The proof attempt is 
now somewhat simpler and contains the diverging 
sequence of equations,
\begin{eqnarray*}
x+(y+(x+(x*y))) & = & y+(x+(x+(x*y))) \\
x+(y+\wf{(x+\wh{(x+(x*y))})}) & = & y+\wf{(x+\wh{(x+(x+(x*y)))})} \\
x+(y+\wf{(x+\wh{(x+(x+(x*y)))})}) & = & y+\wf{(x+\wh{(x+(x+(x+(x*y))))})} \\
& \vdots & 
\end{eqnarray*}
Unfortunately the heuristics for instantiating the right hand side of
speculated lemmas are not 
strong enough to suggest the rule,
\begin{eqnarray*}
X+\wf{(Y+\wh{Z})} & = & \wf{Y+\wh{(X+Z)}}
\end{eqnarray*}
With this rule, {\sc Spike} finds a proof of the commutativity
of multiplication without difficulty. 
The difficulties in speculating this rule
arise because the wave-front is stuck in 
a similar position on both sides of the 
equality. There are few clues therefore to 
suggest how to ripple it up to the top of the
term tree. 

In example 33, the divergence critic proposes a lemma where one is not needed.
{\sc Spike} is able to find a proof of this theorem 
from the definitions alone using 16 inductions. Three of these inductions are 
on the equations,
\begin{eqnarray*}
0 + x & = & x \\
\wf{s(\wh{0})} + x & = & \wf{s(\wh{x})} \\
\wf{s(\wh{s(0)})} + x & = & \wf{s(\wh{s(x)})}
\end{eqnarray*}
This sequence of equations satisfies the divergence critic's
preconditions. The critic therefore proposes wave 
rules for moving accumulating successor functions
off the first argument position of $+$. Although the
proposed lemmas are not necessary, either give a much shorter
and simpler proof needing just 7 inductions. 

Example 34 is the lemma speculated in example 24. 
Divergence analysis of {\sc Spike}'s attempt to
prove this theorem identifies term structure accumulating on
the second (alias accumulator) argument of $qrev$. 
The first two lemmas proposed for removing this term
structure are of no use as they are subsumed by
the recursive definition of $qrev$. The third lemma also
fails to prevent divergence. This lemma simplifies
two element lists in the second argument position of $qrev$.
However, divergence will still occur as the prover
cannot simplify lists that occur in the
second argument position of $qrev$ which contain 3 or more elements. 
Divergence can be overcome if we 
introduce a derived function for appending onto
the end of a list. This can be used to simplify
terms in which a list of arbitrary size occurs on the second argument
position of $qrev$. For example, we can simplify with the rule,
$$
qrev(X,Y) = app(qrev(X,nil),Y)
$$
Unfortunately, append does
not occur in the specification of the theorem 
so it is difficult to find a heuristic that would speculate such
a rule. 


\section{Related Work}
\label{sec-related}

Critics for monitoring the construction of proofs were
first proposed 
by Ireland 
for the {\sc Clam} prover \cite{ireland1}. % \cite{Clam}.
In this framework, failure of one of the 
proof methods automatically invokes a critic. Various critics for 
explicit induction have been developed that
speculate missing lemmas, perform generalizations,
look for suitable case splits, {\it etc}. 
As rippling plays a central role in {\sc Clam}'s proof methods,
many of the heuristics are similar to those
described here \cite{rp613}. 
There are, however,
several significant differences. First, the divergence critic 
described here works in an implicit (and not an explicit) induction
setting.
Second, the divergence critic is not automatically invoked but must 
identify when the proof is failing. Third, the divergence
critic is less specialized. These last two differences reflect
the fact that critics in {\sc Clam} are usually associated
with the failure of a particular precondition to a heuristic. 
The same divergence pattern can, by comparison, arise for
many different reasons: the need to generalize variables apart, 
to generalize common subterms, to add a lemma, {\it etc.}
Fourth, the divergence critic must use difference
matching to annotate terms; in {\sc Clam}, terms
are usually already appropriately annotated. 
Finally, the divergence critic is less tightly coupled to the
the theorem prover's inference rules or heuristics. 
The critic can therefore exploit the strengths of the prover without
needing to reason about the complex rules or heuristics being used.
For instance, the divergence critic has no difficulty
identifying divergence in complex situations
like nested or mutual inductions. The critic
also benefits from the powerful simplification rules
used by {\sc Spike}. 


Divergence has been studied quite extensively
in completion procedures. Two of the main novelties of
the critic described here are the
use of difference matching 
to identify divergence, and the use of 
rippling in the speculation of lemmas to overcome divergence.
Dershowitz and Pinchover, by comparison, use
most specific generalization to identify
divergence patterns in the critical pairs
produced by completion \cite{dershowitz1}.
Kirchner uses generalization modulo 
an equivalence relation to recognise
such divergence patterns \cite{kirchner1}; 
meta-rules are then synthesized
to describe infinite families of rules with some common
structure. Thomas and Jantke use
generalization and inductive
inference to recognize divergence patterns and
to replace infinite sequences 
of critical pairs by a finite number of
generalizations \cite{thomas1}. 
Thomas and Watson 
use generalization to replace an infinite
set of rules by a finite complete set with an 
enriched signature  \cite{thomas2}. 

Generalization modulo an equivalence enables complex
divergence patters to be identified. However, it is in general
undecidable. Most specific generalization, by comparison,
is more limited. It cannot recognize 
divergence patterns which give nested wave-fronts like,
$$ \wf{s(\wh{\wf{s(\wh{x})}+x})}. $$
In addition, most specific generalization cannot identify
term structure in wave-holes. For example, consider the divergence
sequence of equations produced when {\sc Spike}
attempts to prove example 25 from Section \ref{sec-results},
\begin{eqnarray*}
\rev(\qrev(\xxx,\nild)) & = & \xxx \\
\rev(\qrev(\xxx,{\consd{\yyy}{{\nild}}})) & = & {\consd{\yyy}{{\xxx}}} \\
\rev(\qrev(\xxx,{\consd{\zzz}{{\consd{\yyy}{\nild}}}})) & = & {\consd{\zzz}{{\consd{\yyy}{\xxx}}}} \\
& \vdots & 
\end{eqnarray*}
Divergence analysis identifies
term structure accumulating within the accumulator argument
of $qrev$, 
\pagebreak
\begin{eqnarray*}
\rev(\qrev(\xxx,\nild)) & = & \xxx \\
\rev(\qrev(\xxx,\wf{\consd{\yyy}{\wh{\nild}}})) & = & \wf{\consd{\yyy}{\wh{\xxx}}} \\
\rev(\qrev(\xxx,\wf{\consd{\zzz}{\wh{\consd{\yyy}{\nild}}}})) & = & \wf{\consd{\zzz}{\wh{\consd{\yyy}{\xxx}}}} \\
& \vdots & 
\end{eqnarray*}
This annotated sequence is the unique maximal difference match.
These annotations suggest the need for the wave rule,
%\begin{eqnarray*}
%\rev(\qrev(\xxx,\consd{\yyy}{\nild})) & =& \consd{\yyy}{\rev(\qrev(\xxx,\nild))}
%\end{eqnarray*}
$$ \rev(\qrev(\XXX,\wf{\consd{\YYY}{\wh{\nild}}})) =
\wf{\consd{\YYY}{\wh{\rev(\qrev(\XXX,\nild))}}}. $$
This rule allows the proof to go through without divergence.
By comparison, most specific generalization seems to be unable
to identify this rule. 
The most specific generalization of the left hand side of 
this sequence gives the term $\rev(\qrev(\XXX,\ZZZ))$ (or, ignoring
the first term in the sequence,
$\rev(\qrev(\XXX,\consd{\YYY}{\ZZZ}))$).
Most specific generalization cannot, however,
identify the more useful pattern, 
$\rev(\qrev(\XXX,{\consd{\YYY}{{\nild}}}))$.

{\sc Nqthm}  %\cite{boyer1} 
contains a simple test for divergence based 
on subsumption. For instance, on example 13 of the last section, {\sc Nqthm} is
unable to simplify the following subgoal in the step case
of the proof, 
\begin{verbatim}
        (EQUAL (ROT (LENGTH X) (APPEND X (LIST Z)))
               (CONS Z (ROT (LENGTH X) X))))
\end{verbatim}
Note that this is the lemma speculated by the divergence critic.
{\sc Nqthm} generalizes {\tt (LENGTH X)} in this subgoal 
giving the false conjecture,
\begin{verbatim}
        (EQUAL (ROT Y (APPEND X (LIST Z)))
               (CONS Z (ROT Y X))))            
\end{verbatim}
After several more attempts at induction and generalization,
{\sc Nqthm} realizes the proof is diverging since a subgoal is 
subsumed by its parent. As the proof is therefore about to 
loop, {\sc Nqthm} gives up. No attempt is made to analyse
the failed proof attempt to identify where it started
to go wrong. In addition, subsumption is a very weak
test for divergence, much weaker than tests based
on difference matching or generalization. 
This subsumption test recognizes divergence on just a small number
of the failed examples in the last section.

\section{Conclusions}
\label{sec-conclusions}

I have described a
divergence critic, a computer program which attempts to identify diverging
proof attempts and to propose
lemmas and generalizations
which overcome the divergence.
The divergence critic has proved very successful; it enables the system 
{\sc Spike} to prove many theorems from
the definitions alone. The divergence critic's
success can be largely attributed to the power
of the rippling heuristic. This heuristic was originally 
developed for proofs using explicit induction but has
since found several other applications. 
Difference matching is used to 
identify accumulating term structure which is causing divergence.
Lemmas and generalizations are then proposed to ripple
this term structure out of the way. 
There are other types of divergence which 
could perhaps be recognized by the divergence critic. 
Further research is needed to
identify such divergence patterns, isolate their causes
and propose ways of fixing them.
This research may take advantage of the close
links between divergence patterns and particular
types of generalization. For instance, 
it may be possible to identify specific divergence patterns 
with the need to generalize common subterms in the
theorem being proved.

\section*{Acknowledgements}

This research was supported by a Human Capital and Mobility
Postdoctoral Fellowship. I wish to thank: Adel Bouhoula and
Michael Rusinowitch for their invaluable assistance with {\sc Spike};
Pierre Lescanne for inviting me to visit Nancy where
most of this research was performed; 
David Basin, Alan Bundy, Miki Hermann,
Andrew Ireland, and Michael Rusinowitch
for their comments and
questions; the reviewers for their comments
and suggestions; 
the members of the Eureca and Protheo groups
at INRIA; and the members of the DReaM group at Edinburgh
and the MRG groups in Trento and Genova.

\bibliographystyle{theapa}
%\bibliography{/afrodite1/modelli/toby/biblio/a-z,/afrodite1/modelli/toby/biblio/pub}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Aubin}{Aubin}{1976}]{aubinthesis}
Aubin, R. \BBOP1976\BBCP.
\newblock {\Bem Mechanizing Structural Induction}.
\newblock Ph.D.\ thesis, University of Edinburgh.

\bibitem[\protect\BCAY{Basin \BBA\ Walsh}{Basin \BBA\ Walsh}{1992}]{pub556}
Basin, D.\BBACOMMA\  \BBA\ Walsh, T. \BBOP1992\BBCP.
\newblock \BBOQ Difference matching\BBCQ\
\newblock In Kapur, D.\BED, {\Bem 11th Conference on Automated Deduction},
  \BPGS\ 295--309. Springer Verlag.
\newblock Lecture Notes in Computer Science No. 607. Also available from
  Edinburgh as DAI Research Paper 556.

\bibitem[\protect\BCAY{Basin \BBA\ Walsh}{Basin \BBA\
  Walsh}{1993}]{BasinWalshDu}
Basin, D.\BBACOMMA\  \BBA\ Walsh, T. \BBOP1993\BBCP.
\newblock \BBOQ Difference unification\BBCQ\
\newblock In {\Bem Proceedings of the 13th IJCAI}. International Joint
  Conference on Artificial Intelligence.
\newblock Also available as Technical Report MPI-I-92-247, Max-Planck-Institute
  f{\"u}r Informatik.

\bibitem[\protect\BCAY{Basin \BBA\ Walsh}{Basin \BBA\
  Walsh}{1994}]{termination-rippling}
Basin, D.\BBACOMMA\  \BBA\ Walsh, T. \BBOP1994\BBCP.
\newblock \BBOQ Termination orderings for rippling\BBCQ\
\newblock In Bundy, A.\BED, {\Bem 12th Conference on Automated Deduction},
  \BPGS\ 466--483. Springer Verlag.
\newblock Lecture Notes in Artificial Intelligence No. 814.

\bibitem[\protect\BCAY{Bouhoula, Kounalis, \BBA\ Rusinowitch}{Bouhoula
  et~al.}{1992}]{rusi1}
Bouhoula, A., Kounalis, E., \BBA\ Rusinowitch, M. \BBOP1992\BBCP.
\newblock \BBOQ Spike: A theorem-prover\BBCQ\
\newblock In {\Bem Proceedings of LPAR'92, Lecture Notes in Artificial
  Intelligence 624}. Springer-Verlag.

\bibitem[\protect\BCAY{Bouhoula \BBA\ Rusinowitch}{Bouhoula \BBA\
  Rusinowitch}{1995a}]{rusi2}
Bouhoula, A.\BBACOMMA\  \BBA\ Rusinowitch, M. \BBOP1995a\BBCP.
\newblock \BBOQ Implicit induction in conditional theories\BBCQ\
\newblock {\Bem Journal of Automated Reasoning}, {\Bem 14\/}(2), 189--235.

\bibitem[\protect\BCAY{Bouhoula \BBA\ Rusinowitch}{Bouhoula \BBA\
  Rusinowitch}{1995b}]{Spike-manual}
Bouhoula, A.\BBACOMMA\  \BBA\ Rusinowitch, M. \BBOP1995b\BBCP.
\newblock \BBOQ Spike user manual\BBCQ.
\newblock INRIA Lorraine and CRIN, 615 rue du Jardin Botanique,
  Villers-l\`{e}s-Nancy, France. Available from {\tt
  ftp://ftp.loria.fr/pub/loria/protheo/softwares/Spike/}.

\bibitem[\protect\BCAY{Boyer \BBA\ Moore}{Boyer \BBA\ Moore}{1979}]{boyer1}
Boyer, R.\BBACOMMA\  \BBA\ Moore, J. \BBOP1979\BBCP.
\newblock {\Bem A Computational Logic}.
\newblock Academic Press.
\newblock ACM monograph series.

\bibitem[\protect\BCAY{Bundy, Stevens, van Harmelen, Ireland, \BBA\
  Smaill}{Bundy et~al.}{1993}]{pub567}
Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., \BBA\ Smaill, A.
  \BBOP1993\BBCP.
\newblock \BBOQ Rippling: A heuristic for guiding inductive proofs\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 62}, 185--253.
\newblock Also available from Edinburgh as DAI Research Paper No. 567.

\bibitem[\protect\BCAY{Bundy, van Harmelen, Horn, \BBA\ Smaill}{Bundy
  et~al.}{1990}]{Clam}
Bundy, A., van Harmelen, F., Horn, C., \BBA\ Smaill, A. \BBOP1990\BBCP.
\newblock \BBOQ The {Oyster-Clam} system\BBCQ\
\newblock In Stickel, M.\BED, {\Bem 10th International Conference on Automated
  Deduction}, \BPGS\ 647--648. Springer-Verlag.
\newblock Lecture Notes in Artificial Intelligence No. 449.

\bibitem[\protect\BCAY{Dershowitz \BBA\ Pinchover}{Dershowitz \BBA\
  Pinchover}{1990}]{dershowitz1}
Dershowitz, N.\BBACOMMA\  \BBA\ Pinchover, E. \BBOP1990\BBCP.
\newblock \BBOQ {Inductive} {Synthesis} of {Equational} {Programs}\BBCQ\
\newblock In {\Bem Proceedings of the 8th National Conference on AI}, \BPGS\
  234--239. American Association for Artificial Intelligence.

\bibitem[\protect\BCAY{Hermann}{Hermann}{1989}]{hermann1}
Hermann, M. \BBOP1989\BBCP.
\newblock \BBOQ Crossed term rewriting systems\BBCQ\
\newblock CRIN report\ 89-R-003, Centre de {Recherche} en {Informatique} de
  {Nancy}.

\bibitem[\protect\BCAY{Ireland}{Ireland}{1992}]{ireland1}
Ireland, A. \BBOP1992\BBCP.
\newblock \BBOQ {The} {Use} of {Planning} {Critics} in {Mechanizing}
  {Inductive} {Proof}\BBCQ\
\newblock In {\Bem Proceedings of LPAR'92, Lecture Notes in Artificial
  Intelligence 624}. Springer-Verlag.
\newblock Also available as Research Report 592, Dept of AI, Edinburgh
  University.

\bibitem[\protect\BCAY{Ireland \BBA\ Bundy}{Ireland \BBA\ Bundy}{1992}]{rp613}
Ireland, A.\BBACOMMA\  \BBA\ Bundy, A. \BBOP1992\BBCP.
\newblock \BBOQ Using failure to guide inductive proof\BBCQ\
\newblock \BTR, Dept. of Artificial Intelligence, University of Edinburgh.
\newblock Available from Edinburgh as DAI Research Paper 613.

\bibitem[\protect\BCAY{Kirchner}{Kirchner}{1987}]{kirchner1}
Kirchner, H. \BBOP1987\BBCP.
\newblock \BBOQ Schematization of infinite sets of rewrite rules. {Application}
  to the divergence of completion processes\BBCQ\
\newblock In {\Bem Proceedings of RTA'87}, \BPGS\ 180--191.

\bibitem[\protect\BCAY{Protzen}{Protzen}{1992}]{protzen}
Protzen, M. \BBOP1992\BBCP.
\newblock \BBOQ Disproving conjectures\BBCQ\
\newblock In Kapur, D.\BED, {\Bem 11th Conference on Automated Deduction},
  \BPGS\ 340--354. Springer Verlag.
\newblock Lecture Notes in Computer Science No. 607.

\bibitem[\protect\BCAY{Thomas \BBA\ Jantke}{Thomas \BBA\
  Jantke}{1989}]{thomas1}
Thomas, M.\BBACOMMA\  \BBA\ Jantke, K. \BBOP1989\BBCP.
\newblock \BBOQ Inductive {Inference} for {Solving} {Divergence} in
  {Knuth-Bendix} {Completion}\BBCQ\
\newblock In {\Bem Proceedings of International Workshop AII'89}, \BPGS\
  288--303.

\bibitem[\protect\BCAY{Thomas \BBA\ Watson}{Thomas \BBA\
  Watson}{1993}]{thomas2}
Thomas, M.\BBACOMMA\  \BBA\ Watson, P. \BBOP1993\BBCP.
\newblock \BBOQ Solving divergence in {Knuth-Bendix} completion by enriching
  signatures\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 112}, 145--185.

\bibitem[\protect\BCAY{Walsh}{Walsh}{1994}]{divergence-critic}
Walsh, T. \BBOP1994\BBCP.
\newblock \BBOQ A divergence critic\BBCQ\
\newblock In Bundy, A.\BED, {\Bem 12th Conference on Automated Deduction},
  \BPGS\ 14--25. Springer Verlag.
\newblock Lecture Notes in Artificial Intelligence No. 814.

\bibitem[\protect\BCAY{Walsh, Nunes, \BBA\ Bundy}{Walsh et~al.}{1992}]{pub563}
Walsh, T., Nunes, A., \BBA\ Bundy, A. \BBOP1992\BBCP.
\newblock \BBOQ The use of proof plans to sum series\BBCQ\
\newblock In Kapur, D.\BED, {\Bem 11th Conference on Automated Deduction},
  \BPGS\ 325--339. Springer Verlag.
\newblock Lecture Notes in Computer Science No. 607. Also available from
  Edinburgh as DAI Research Paper 563.

\bibitem[\protect\BCAY{Yoshida, Bundy, Green, Walsh, \BBA\ Basin}{Yoshida
  et~al.}{1994}]{limits}
Yoshida, T., Bundy, A., Green, I., Walsh, T., \BBA\ Basin, D. \BBOP1994\BBCP.
\newblock \BBOQ Coloured rippling: the extension of a theorem proving
  heuristic\BBCQ\
\newblock In Cohn, A.\BED, {\Bem Proceedings of ECAI-94}, \BPGS\ 85--89.
John Wiley.
\newblock Also available from
  Edinburgh as DAI Research Paper 779.



\end{thebibliography}


\end{document}





