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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Termination.Order

Contents

- Structural orderings

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

- data Order
  - = Decr !Bool !Int
  - | Unknown
  - | Mat !(Matrix Int Order)
- decr :: (?cutoff :: CutOff) => Bool -> Int -> Order
- increase :: Int -> Order -> Order
- decrease :: Int -> Order -> Order
- setUsability :: Bool -> Order -> Order
- (.*.) :: (?cutoff :: CutOff) => Order -> Order -> Order
- supremum :: (?cutoff :: CutOff) => [Order] -> Order
- infimum :: (?cutoff :: CutOff) => [Order] -> Order
- orderSemiring :: (?cutoff :: CutOff) => Semiring Order
- le :: Order
- lt :: Order
- unknown :: Order
- orderMat :: Matrix Int Order -> Order
- collapseO :: (?cutoff :: CutOff) => Order -> Order
- nonIncreasing :: Order -> Bool
- decreasing :: Order -> Bool
- isDecr :: Order -> Bool
- class NotWorse a where
  - notWorse :: a -> a -> Bool
- isOrder :: (?cutoff :: CutOff) => Order -> Bool

# 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

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.

#### Instances

Instances details

CallComb CallMatrix Source #

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

Instance details Defined in Agda.Termination.CallMatrix Methods (>*<) :: CallMatrix -> CallMatrix -> CallMatrix Source #
NotWorse CallMatrix Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods notWorse :: CallMatrix -> CallMatrix -> Bool Source #
NotWorse Order Source # | It does not get worse then ``increase'`. If we are still decreasing, it can get worse: less decreasing.
Instance details Defined in Agda.Termination.Order Methods notWorse :: Order -> Order -> Bool Source #
HasZero Order Source # |
Instance details Defined in Agda.Termination.Order Methods zeroElement :: Order Source #
PartialOrd Order 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).
Instance details Defined in Agda.Termination.Order Methods comparable :: Comparable Order Source #
Pretty CallMatrix Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods pretty :: CallMatrix -> Doc Source # prettyPrec :: Int -> CallMatrix -> Doc Source # prettyList :: [CallMatrix] -> Doc Source #
Pretty Order Source # |
Instance details Defined in Agda.Termination.Order Methods pretty :: Order -> Doc Source # prettyPrec :: Int -> Order -> Doc Source # prettyList :: [Order] -> Doc Source #
Show Order Source # |
Instance details Defined in Agda.Termination.Order Methods showsPrec :: Int -> Order -> ShowS Source # show :: Order -> String Source # showList :: [Order] -> ShowS Source #
Eq Order Source # |
Instance details Defined in Agda.Termination.Order Methods (==) :: Order -> Order -> Bool Source # (/=) :: Order -> Order -> Bool Source #
Ord Order Source # |
Instance details Defined in Agda.Termination.Order Methods compare :: Order -> Order -> Ordering Source # (<) :: Order -> Order -> Bool Source # (<=) :: Order -> Order -> Bool Source # (>) :: Order -> Order -> Bool Source # (>=) :: Order -> Order -> Bool Source # max :: Order -> Order -> Order Source # min :: Order -> Order -> Order Source #
Diagonal (CallMatrixAug cinfo) Order Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods diagonal :: CallMatrixAug cinfo -> [Order] Source #

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

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

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

increase :: Int -> Order -> Order Source #

Raw increase which does not cut off.

decrease :: Int -> Order -> Order Source #

Raw decrease which does not cut off.

setUsability :: Bool -> Order -> Order Source #

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

Multiplication of `Order`s. (Corresponds to sequential composition.)

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

The supremum of a (possibly empty) list of `Order`s. 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 `Order`s. Gets the worst information. `Unknown` is the least element, thus, dominant.

orderSemiring :: (?cutoff :: CutOff) => Semiring Order Source #

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

le :: Order Source #

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

lt :: Order Source #

Usable decrease.

unknown :: Order Source #

orderMat :: Matrix Int Order -> Order Source #

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

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

nonIncreasing :: Order -> Bool Source #

decreasing :: Order -> Bool Source #

Decreasing and usable?

isDecr :: Order -> Bool 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.

Methods

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

#### Instances

Instances details

NotWorse CallMatrix Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods notWorse :: CallMatrix -> CallMatrix -> Bool Source #
NotWorse Order Source # | It does not get worse then ``increase'`. If we are still decreasing, it can get worse: less decreasing.
Instance details Defined in Agda.Termination.Order Methods notWorse :: Order -> Order -> Bool Source #
NotWorse (CallMatrixAug cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods notWorse :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool Source #
(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) Source # | We assume the matrices have the same dimension.
Instance details Defined in Agda.Termination.Order Methods notWorse :: Matrix i o -> Matrix i o -> Bool Source #

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