|
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 |
|
|
|
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 | |
|
|
|
A column expresses how the size of a certain argument changes in
the various recursive calls a function makes to itself
(transitively).
|
|
|
RecBehaviour invariant: the size must match the real size of
the recursion behaviour, and all columns must have the same
indices.
|
|
|
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.
|
|
|
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.
|
|
|
|
Produced by Haddock version 2.6.0 |