| ||||

| ||||

Description | ||||

Termination checker, based on "A Predicative Analysis of Structural Recursion" by Andreas Abel and Thorsten Altenkirch (JFP'01). and "The Size-Change Principle for Program Termination" by Chin Soon Lee, Neil Jones, and Amir Ben-Amram (POPL'01). TODO: Note that we should also check that data type definitions are strictly positive. Furthermore, for inductive-recursive families we may need to do something more clever. | ||||

Synopsis | ||||

| ||||

Documentation | ||||

terminates :: (Ord meta, Monoid meta) => CallGraph meta -> Either meta () | ||||

TODO: This comment seems to be partly out of date.
cs
terminate. The call graph cs should have one entry (Call) per
recursive function application.
If termination can not be established, then problems contains an
indication of why termination cannot be established. See lexOrder
for further details.
Note that this function assumes that all data types are strictly positive. The termination criterion is taken from Jones et al. In the completed call graph, each idempotent call-matrix from a function to itself must have a decreasing argument. Idempotency is wrt. matrix multiplication. This criterion is strictly more liberal than searching for a lexicographic order (and easier to implement, but harder to justify). | ||||

tests :: IO Bool | ||||

Produced by Haddock version 2.4.2 |