Agda.Termination.Lexicographic

Lexicographic order search, more or less as defined in "A Predicative Analysis of Structural Recursion" by Andreas Abel and Thorsten Altenkirch.

Documentation

type LexOrder arg = [arg]

A lexicographic ordering for the recursion behaviour of a given function is a permutation of the argument indices which can be used to show that the function terminates. See the paper referred to above for more details.

data RecBehaviour arg call

A recursion behaviour expresses how a certain function calls itself (transitively). For every argument position there is a value (Column) describing how the function calls itself for that particular argument. See also recBehaviourInvariant.

Constructors

RB

Fields

columns :: Map arg (Column call)

calls :: Set call

The indices to the columns.

size :: Size Integer

Instances

(Show arg, Show call) => Show (RecBehaviour arg call)

(Arbitrary call, Arbitrary arg, Ord arg, Ord call) => Arbitrary (RecBehaviour call arg)

(CoArbitrary call, CoArbitrary arg) => CoArbitrary (RecBehaviour call arg)

type Column call = Map call Order

A column expresses how the size of a certain argument changes in the various recursive calls a function makes to itself (transitively).

recBehaviourInvariant :: Eq call => RecBehaviour arg call -> Bool

RecBehaviour invariant: the size must match the real size of the recursion behaviour, and all columns must have the same indices.

fromDiagonals :: (Ord call, Ix arg) => [(call, Array arg Order)] -> RecBehaviour arg (Integer, call)

Constructs a recursion behaviour from a list of matrix diagonals ("rows"). Note that the call indices do not need to be distinct, since they are paired up with unique Integers.

Precondition: all arrays should have the same bounds.

lexOrder :: (Ord arg, Ord call) => RecBehaviour arg call -> Either (Set arg, Set call) (LexOrder arg)

Tries to compute a lexicographic ordering for the given recursion behaviour. This algorithm should be complete.

If no lexicographic ordering can be found, then two sets are returned:

• A set of argument positions which are not properly decreasing, and
• the calls where these problems show up.

tests :: IO Bool