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

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]

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

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 |

Fields

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

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

`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)

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)

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