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

Agda.Termination.Order

Contents

Description

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.

Synopsis

# Structural orderings

data Order Source #

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

 Mat !(Matrix Int Order) Matrix-shaped order, currently UNUSED.

Instances

 Source # Methods(==) :: Order -> Order -> Bool #(/=) :: Order -> Order -> Bool # Source # Methods(<) :: Order -> Order -> Bool #(<=) :: Order -> Order -> Bool #(>) :: Order -> Order -> Bool #(>=) :: Order -> Order -> Bool #max :: Order -> Order -> Order #min :: Order -> Order -> Order # Source # MethodsshowsPrec :: Int -> Order -> ShowS #show :: Order -> String #showList :: [Order] -> ShowS # Source # Methodsshrink :: Order -> [Order] # # Methodsshrink :: CallMatrix -> [CallMatrix] # Source # Methodscoarbitrary :: Order -> Gen b -> Gen b # Source # Methods Source # Methods Source # 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). Methods Source # Methods Source # It does not get worse then increase'. If we are still decreasing, it can get worse: less decreasing. Methods Source # Call matrix multiplication.f --(m1)--> g --(m2)--> h is combined to f --(m2 mul m1)--> hNote 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). Methods Source # Methods Diagonal (CallMatrixAug cinfo) Order Source # Methodsdiagonal :: CallMatrixAug cinfo -> [Order] Source # Ord i => NotWorse (Matrix i Order) Source # We assume the matrices have the same dimension. Methods

decr :: (?cutoff :: CutOff) => Int -> Order Source #

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

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

Raw increase which does not cut off.

Raw decrease which does not cut off.

(.*.) :: (?cutoff :: CutOff) => Order -> Order -> Order Source #

Multiplication of Orders. (Corresponds to sequential composition.)

supremum :: (?cutoff :: CutOff) => [Order] -> Order Source #

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

infimum :: (?cutoff :: CutOff) => [Order] -> Order Source #

The infimum of a (non empty) list of Orders. Unknown is the least element, thus, dominant.

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

Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.

collapseO :: (?cutoff :: CutOff) => Order -> Order Source #

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

class NotWorse a where Source #

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

Minimal complete definition

notWorse

Methods

notWorse :: a -> a -> Bool Source #

Instances

 Source # It does not get worse then increase'. If we are still decreasing, it can get worse: less decreasing. Methods NotWorse (CallMatrixAug cinfo) Source # MethodsnotWorse :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool Source # Source # Methods Ord i => NotWorse (Matrix i Order) Source # We assume the matrices have the same dimension. Methods