| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

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

`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 `Integer`s. 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 Bool | Source

Produced by Haddock version 2.4.2