| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.Termination.Termination
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).
Synopsis
- data Terminates cinfo
- = Terminates
- | TerminatesNot cinfo
- terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Terminates cinfo
- terminatesFilter :: (Monoid cinfo, ?cutoff :: CutOff) => (Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
- terminationCounterexample :: (?cutoff :: CutOff) => (Node -> Bool) -> CallGraph cinfo -> Terminates cinfo
- idempotentEndos :: (?cutoff :: CutOff) => CallGraph cinfo -> [CallMatrixAug cinfo]
Documentation
data Terminates cinfo Source #
Result of running the termination checker.
Constructors
| Terminates | Termination proved without considering guardedness. |
| TerminatesNot cinfo | Termination could not be proven, witnessed by the supplied problematic call path. |
terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Terminates cinfo Source #
terminates cscs
terminate. The call graph cs should have one entry (Call) per
recursive function application.
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).
Arguments
| :: (Monoid cinfo, ?cutoff :: CutOff) | |
| => (Node -> Bool) | Only consider calls whose source and target satisfy this predicate. |
| -> CallGraph cinfo | Callgraph augmented with |
| -> Terminates cinfo | A bad call path of type |
While no counterexample to termination is found, complete the given call graph step-by-step.
terminationCounterexample Source #
Arguments
| :: (?cutoff :: CutOff) | |
| => (Node -> Bool) | Only consider calls whose source and target satisfy this predicate. |
| -> CallGraph cinfo | Callgraph augmented with |
| -> Terminates cinfo | A bad call path of type |
Does the given callgraph contain a counterexample to termination?
idempotentEndos :: (?cutoff :: CutOff) => CallGraph cinfo -> [CallMatrixAug cinfo] Source #
Get all idempotent call-matrixes of loops in the call graph.