Safe Haskell	None
Language	Haskell2010

Mikan.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
decr :: (?cutoff :: CutOff) => Bool -> Int -> Order
increase :: Int -> Order -> Order
decrease :: Int -> Order -> Order
setUsability :: Bool -> Order -> Order
(.*.) :: (?cutoff :: CutOff) => Order -> Order -> Order
supremum :: [Order] -> Order
infimum :: [Order] -> Order
orderSemiring :: (?cutoff :: CutOff) => Semiring Order
le :: Order
lt :: Order
unknown :: 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.

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.

Instances

Instances details

Pretty CallMatrix Source #
Instance details Defined in Mikan.Termination.CallMatrix Methods pretty :: CallMatrix -> Doc Source # prettyPrec :: Int -> CallMatrix -> Doc Source # prettyList :: [CallMatrix] -> Doc Source #
Pretty Order Source #
Instance details Defined in Mikan.Termination.Order Methods pretty :: Order -> Doc Source # prettyPrec :: Int -> Order -> Doc Source # prettyList :: [Order] -> Doc Source #
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 Mikan.Termination.CallMatrix Methods (>*<) :: CallMatrix -> CallMatrix -> CallMatrix Source #
NotWorse CallMatrix Source #
Instance details Defined in Mikan.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 Mikan.Termination.Order Methods notWorse :: Order -> Order -> Bool Source #
HasZero Order Source #
Instance details Defined in Mikan.Termination.Order Methods zeroElement :: Order Source #
PrettyTCM CallMatrix Source #
Instance details Defined in Mikan.Termination.Monad Methods prettyTCM :: MonadPretty m => CallMatrix -> m Doc 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 Mikan.Termination.Order Methods comparable :: Comparable Order Source #
Show Order Source #
Instance details Defined in Mikan.Termination.Order Methods showsPrec :: Int -> Order -> ShowS # show :: Order -> String # showList :: [Order] -> ShowS #
Eq Order Source #
Instance details Defined in Mikan.Termination.Order Methods (==) :: Order -> Order -> Bool # (/=) :: Order -> Order -> Bool #
Ord Order Source #
Instance details Defined in Mikan.Termination.Order Methods compare :: Order -> Order -> Ordering # (<) :: Order -> Order -> Bool # (<=) :: Order -> Order -> Bool # (>) :: Order -> Order -> Bool # (>=) :: Order -> Order -> Bool # max :: Order -> Order -> Order # min :: Order -> Order -> Order #
Diagonal (CallMatrixAug cinfo) Order Source #
Instance details Defined in Mikan.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 Orders. (Corresponds to sequential composition.)

supremum :: [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 :: [Order] -> Order Source #

The infimum of a (non empty) list of Orders. 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 #

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 Mikan.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 Mikan.Termination.Order Methods notWorse :: Order -> Order -> Bool Source #
NotWorse (CallMatrixAug cinfo) Source #
Instance details Defined in Mikan.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 Mikan.Termination.Order Methods notWorse :: Matrix i o -> Matrix i o -> Bool Source #

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