Safe Haskell | Safe-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]
- data RecBehaviour arg call = RB {}
- 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
.
(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 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.