HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Termination.Order

An Abstract domain of relative sizes, i.e., differences between size of formal function parameter and function argument in recursive call; used in the termination checker.

  • 1 type
  • 1 class
  • 17 values
  • PackageAgda-2.7.0.1
  • Exports19
  • LanguageHaskell2010
  • LicenceMIT
  • SourceOrder.hs

Structural orderings

19 declarations
datadata Order
#

In the paper referred to above, there is an order R with Unknown <= Le <= Lt.

This is generalized to Unknown <= 'Decr k' where Decr 1 replaces Lt and Decr 0 replaces Le. A negative decrease means an increase. The generalization allows the termination checker to record an increase by 1 which can be compensated by a following decrease by 2 which results in an overall decrease.

However, the termination checker of the paper itself terminates because there are only finitely many different call-matrices. To maintain termination of the terminator we set a cutoff point which determines how high the termination checker can count. This value should be set by a global or file-wise option.

See Call for more information.

TODO: document orders which are call-matrices themselves.

Constructors

  • Decr !Bool !Int

    Decrease of callee argument wrt. caller parameter.

    The Bool indicates whether the decrease (if any) is usable. In any chain, there needs to be one usable decrease. Unusable decreases come from SIZELT constraints which are not in inductive pattern match or a coinductive copattern match. See issue #2331.

    UPDATE: Andreas, 2017-07-26: Feature #2331 is unsound due to size quantification in terms. While the infrastructure for usable/unusable decrease remains in place, no unusable decreases are generated by TermCheck.

  • Unknown

    No relation, infinite increase, or increase beyond termination depth.

  • Mat !(Matrix Int Order)

    Matrix-shaped order, currently UNUSED.

Instances11Eq, Ord, Show, Pretty, PartialOrd, CallComb, …
  • Eq OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order
  • Ord OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order
  • Show OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order
  • Pretty CallMatrixDefined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
  • Pretty OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order
  • PartialOrd OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order

    Information order: Unknown is least information. The more we decrease, the more information we have.

    When having comparable call-matrices, we keep the lesser one. Call graph completion works toward losing the good calls, tending towards Unknown (the least information).

  • CallComb CallMatrixDefined in Agda-2.7.0.1 · Agda.Termination.CallMatrix

    Call matrix multiplication.

    f --(m1)--> g --(m2)--> h is combined to f --(m2 mul m1)--> h

    Note the reversed order of multiplication: The matrix c1 of the second call g-->h in the sequence f-->g-->h is multiplied with the matrix c2 of the first call.

    Preconditions: m1 has dimensions ar(g) × ar(f). m2 has dimensions ar(h) × ar(g).

    Postcondition: m1 >*< m2 has dimensions ar(h) × ar(f).

  • HasZero OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order
  • NotWorse CallMatrixDefined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
  • NotWorse OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order

    It does not get worse then `increase'. If we are still decreasing, it can get worse: less decreasing.

  • Diagonal (CallMatrixAug cinfo) OrderDefined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
valuedecr :: IP "cutoff" CutOff => Bool -> Int -> Order
#

Smart constructor for Decr k :: Order which cuts off too big values.

Possible values for k: - ?cutoff <= k <= ?cutoff + 1.

valuesupremum :: IP "cutoff" CutOff => [Order] -> Order
#

The supremum of a (possibly empty) list of Orders. More information (i.e., more decrease) is bigger. Unknown is no information, thus, smallest.

valueorderSemiring :: IP "cutoff" CutOff => Semiring Order
#

We use a record for semiring instead of a type class since implicit arguments cannot occur in instance constraints, like instance (?cutoff :: Int) => SemiRing Order.

valuele :: Order
#

le, lt, decreasing, unknown: for backwards compatibility, and for external use.

valueisDecr :: Order -> Bool
#

Matrix-shaped order is decreasing if any diagonal element is decreasing.

classclass NotWorse a where
#

A partial order, aimed at deciding whether a call graph gets worse during the completion.

Methods

Instances4NotWorse
  • NotWorse CallMatrixDefined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
  • NotWorse OrderDefined in Agda-2.7.0.1 · Agda.Termination.Order

    It does not get worse then `increase'. If we are still decreasing, it can get worse: less decreasing.

  • NotWorse (CallMatrixAug cinfo)Defined in Agda-2.7.0.1 · Agda.Termination.CallMatrix
  • (Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o)Defined in Agda-2.7.0.1 · Agda.Termination.Order

    We assume the matrices have the same dimension.