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 non-terminating 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
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 instantion 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 98-distribution exactly as they were with only two minor adjustements. First, to accomodate 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 self-contained proofs, AProVE did not re-use 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 (==).
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 non-terminating from the total of 1272, termination can be shown for 81.68 percent of all start terms.