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

Safe Haskell | None

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