HORIZON HASKELLDocslts/ghc-10.0.xfc4e5982026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · fc4e598 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.Termination.Termination

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

  • 2 types
  • 4 values
  • PackageAgda-2.8.0.2
  • Exports6
  • LanguageHaskell2010
  • LicenceMIT
  • SourceTermination.hs
datadata Terminates cinfo
#

Result of running the termination checker.

Constructors

  • Terminates

    Termination proved without considering guardedness.

  • TerminatesNot GuardednessHelps cinfo

    Termination could not be proven, witnessed by the supplied problematic call path. Guardedness could help, though.

datadata GuardednessHelps
#

Would termination go through with guardedness?

Constructors

Instances10Bounded, Enum, Eq, Show, Generic, NFData, …
valueterminates
  1. :: (Monoid cinfo, IP "cutoff" CutOff)
  2. => CallGraph cinfo
  3. -> Terminates cinfo
#

terminates cs checks if the functions represented by cs 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).

valueidempotent :: IP "cutoff" CutOff => CallMatrixAug cinfo -> Bool
#

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.