Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered



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



type LexOrder arg = [arg]Source

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 Source

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.




columns :: Map arg (Column call)
calls :: Set call

The indices to the columns.

size :: Size Integer


(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 OrderSource

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 -> BoolSource

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)Source

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)Source

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.