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



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.