Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.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

- terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Either cinfo ()
- terminatesFilter :: (Monoid cinfo, ?cutoff :: CutOff) => (Node -> Bool) -> CallGraph cinfo -> Either cinfo ()
- endos :: [Call cinfo] -> [CallMatrixAug cinfo]
- idempotent :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool

# Documentation

terminates :: (Monoid cinfo, ?cutoff :: CutOff) => CallGraph cinfo -> Either cinfo () Source #

TODO: This comment seems to be partly out of date.

``terminates` cs` checks if the functions represented by `cs` terminate. The call graph `cs` should have one entry (`Call`) per recursive function application.

``Right` perms` is returned if the functions are size-change terminating.

If termination can not be established, then ``Left` problems` is returned instead. Here `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).

terminatesFilter :: (Monoid cinfo, ?cutoff :: CutOff) => (Node -> Bool) -> CallGraph cinfo -> Either cinfo () Source #

endos :: [Call cinfo] -> [CallMatrixAug cinfo] Source #

idempotent :: (?cutoff :: CutOff) => CallMatrixAug cinfo -> Bool Source #

A call `c` is idempotent if it is an endo (``source` == `target``) of order 1. (Endo-calls of higher orders are e.g. argument permutations). We can test idempotency by self-composition. Self-composition `c >*< c` should not make any parameter-argument relation worse.