Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Termination.Lexicographic
Description
Lexicographic order search, more or less as defined in "A Predicative Analysis of Structural Recursion" by Andreas Abel and Thorsten Altenkirch.
Synopsis
type LexOrder arg = [arg]
data RecBehaviour arg call = RB {
columns :: Map arg (Column call)
calls :: Set call
size :: Size Integer
}
type Column call = Map call Order
recBehaviourInvariant :: Eq call => RecBehaviour arg call -> Bool
fromDiagonals :: (Ord call, Ix arg) => [(call, Array arg Order)] -> RecBehaviour arg (Integer, call)
lexOrder :: (Ord arg, Ord call) => RecBehaviour arg call -> Either (Set arg, Set call) (LexOrder arg)
tests :: IO Bool
Documentation
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.
Constructors
RB
columns :: Map arg (Column call)
calls :: Set callThe indices to the columns.
size :: Size Integer
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.
tests :: IO BoolSource
Produced by Haddock version 2.6.0