Our approach proves termination
of a given start term.
The use of a start term is necessary, since a term like "take 10 [(0::Int)..]"
terminates in Haskell, although it contains nonterminating functions.
Here, the term "[(0::Int)..]" evaluates to an infinite list of integers
and, thus, it obviously does not terminate.
This behavior is a fundamental consequence of the lazy evaluation strategy
of Haskell.
In the following we present an overview of the implementation
of our approach as well as an extensive experimental evaluation.
In the second step, the termination graph is constructed. Its nodes are terms and its edges essentially correspond to evaluation steps in Haskell. When a term cannot be evaluated further, this is either due to a constructor expected in a rule pattern, a type class instance that must be selected, or because a function does not have enough arguments. In the former cases, all possible instances are generated and the evaluation is continued. In the latter case, the term is expanded by applying it to fresh variables until the number of required arguments is reached. When the current term is an instance of a term already present in the graph, an instantiation edge is drawn between these two, where the substituted terms remain to be evaluated.
Each strongly connected component of the graph corresponds to a DP problem (P,R) where P is built from the instantiation edges and R contains all rules for the functions used in the matching substitution. The finiteness of the resulting DP problems is analyzed by the DP Framework implemented in the AProVE system. If finiteness can be shown, all instances of the start term are terminating using the Haskell evaluation strategy.
For a more detailed description including proofs for all theorems and lemmas
we refer to our paper. For
details on the simplification and on strategies for constructing termination
graphs consult the diploma thesis of Stephan
Swiderski (in German) and the diploma thesis of Matthias Raffelsieper.
We used the modules from Hugs 98distribution exactly as they were with only two minor adjustments. First, to accommodate for the differences between the module system of the Haskell implementation in AProVE and the module system of Hugs 98, we made trivial adjustments to the import statements. Second, we supply implementations for the primitive functions declared but not implemented in the Hugs 98 Prelude, e.g., primPlusInt :: Int > Int > Int, primMinusInt :: Int > Int > Int, and so on. The source files that we used for our analysis can be found here:
We first try to prove termination of a start term in its most general form. If the type of the start term has a class context, then afterwards we also try to prove termination of all variants of the start term where type variables with class constraints are replaced by actual type instances. The reason is that by regarding all instances we get a finer analysis for those cases where the most general form of the start term does not terminate (or cannot be shown terminating).
To avoid redundancy, for equivalent type instances we only analyzed one instance. For the class Integral we only considered Int, as in our implementation Int is unbounded and therefore equivalent to Integer, the other instance of Integral. The instances Float and Double are also equivalent in our implementation. Thus, we only considered the Float instances. Additionally, in our implementation we do not yet support derived instances of the classes Read and Ix.
In order to obtain selfcontained proofs, AProVE did not reuse previously computed termination properties of functions from libraries. This implies that for all functions used by the start term, termination has to be shown anew.
For example the proof for the start term elem :: Eq a => a > [a] > Bool indirectly contains also the proof for the start term (==) :: Eq a => a > a > Bool , because the function elem depends on the function (==).
Status  FiniteMap  List  Monad  Prelude  Queue  Total  

YES  258  80.37%  168  96.55%  69  86.25%  499  72.10%  5  100.00%  999  78.54% 
MAYBE  0  0%  4  2.29%  11  13.75%  42  6.06%  0  0.00%  57  4.48% 
TIMEOUT  63  19.62%  2  1.14%  0  0.00%  140  20.23%  0  0.00%  205  16.12% 
NO  0  0.00%  0  0.00%  0  0.00%  11  1.58%  0  0.00%  11  0.85% 
TOTAL  321  100.00%  174  100.00%  80  100.00%  692  100.00%  5  100.00%  1272  100.00% 
Overall, we can conclude that our approach allows for a powerful termination analysis
of Haskell programs. When subtracting the 49 start terms
that are known to be nonterminating from the total of 1272,
termination can be shown for 81.68 percent of all start terms.
Definition 2.4 (HTermination). The set of Hterminating ground terms is the smallest set
of ground terms t such that t is Hterminating if the following three
conditions hold for t:

data Foo = Bar  L (Foo > Foo)
app :: Foo > Foo > Foo
app (L f) x = f x
omega = L (\x > app x x)
app
omega
app omega
app omega x
app omega omega
since both
app omega x
and omega
are Hterminating and a
term t is considered to be
Hterminating iff t σ is Hterminating
for all substitutions σ with Hterminating ground terms.
But AProVE can actually prove its
nontermination (AProVE also features a prover of nontermination for Haskell,
which however is not very powerful). Indeed, the term app omega omega
is nonterminating in Haskell, as witnessed by the following infinite evaluation:
app omega omega →_{H}
app (L (\x > app x x)) omega →_{H}
(\x > app x x) omega →_{H}
app omega omega →_{H}
...
omega
should be regarded as being
Hterminating or not. Both possibilities lead to a contradiction:
omega
is considered to be Hterminating, then app x x
is not Hterminating. The reason is that otherwise, app omega omega
would also be
Hterminating, but that is impossible, because it has an infinite evaluation. Thus, app x x
is not Hterminating. But then, \x > app x x
is also not Hterminating and
thus, L (\x > app x x)
is not Hterminating either. In other words:
Htermination of omega
implies nonHtermination of omega
.
omega
is considered to be nonHterminating, then
there is no instantiation with Hterminating terms such that
app x x
has an infinite evaluation. Hence,
app x x
is Hterminating. But then, \x > app x x
is also Hterminating and
thus, L (\x > app x x)
is Hterminating as well. In other words:
nonHtermination of omega
implies Htermination of omega
.
Definition 2.4 (HTermination). The set of Hterminating ground terms is the smallest set
of ground terms t such that:
