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

Safe Haskell | None

Agda.Termination.CallGraph

Contents

- Structural orderings
- Call matrices
- Calls
- Call graphs
- Tests

Description

Call graphs and related concepts, more or less as defined in "A Predicative Analysis of Structural Recursion" by Andreas Abel and Thorsten Altenkirch.

Synopsis

- data Order = Mat (Matrix Integer Order)
- decr :: [cutoff :: Int] => Int -> Order
- increase :: Int -> Order -> Order
- decrease :: Int -> Order -> Order
- (.*.) :: [cutoff :: Int] => Order -> Order -> Order
- supremum :: [cutoff :: Int] => [Order] -> Order
- infimum :: [cutoff :: Int] => [Order] -> Order
- decreasing :: Order -> Bool
- le :: Order
- lt :: Order
- unknown :: Order
- orderMat :: Matrix Integer Order -> Order
- type Index = Integer
- newtype CallMatrix = CallMatrix {
  - mat :: Matrix Index Order
  }
- (>*<) :: [cutoff :: Int] => Call -> Call -> Call
- callMatrixInvariant :: CallMatrix -> Bool
- data Call = Call {
  - source :: Index
  - target :: Index
  - cm :: CallMatrix
  }
- callInvariant :: Call -> Bool
- data CallGraph meta
- callGraphInvariant :: CallGraph meta -> Bool
- fromList :: Monoid meta => [(Call, meta)] -> CallGraph meta
- toList :: CallGraph meta -> [(Call, meta)]
- empty :: CallGraph meta
- union :: Monoid meta => CallGraph meta -> CallGraph meta -> CallGraph meta
- insert :: Monoid meta => Call -> meta -> CallGraph meta -> CallGraph meta
- complete :: [cutoff :: Int] => Monoid meta => CallGraph meta -> CallGraph meta
- prettyBehaviour :: Show meta => CallGraph meta -> Doc
- tests :: IO Bool

# Structural orderings

data Order

In the paper referred to above, there is an order R with ``Unknown` `<=` `Le` `<=` `Lt``.

This is generalized to ``Unknown` `<=` 'Decr k'` where `Decr 1` replaces `Lt` and `Decr 0` replaces `Le`. A negative decrease means an increase. The generalization allows the termination checker to record an increase by 1 which can be compensated by a following decrease by 2 which results in an overall decrease.

However, the termination checker of the paper itself terminates because there are only finitely many different call-matrices. To maintain termination of the terminator we set a `cutoff` point which determines how high the termination checker can count. This value should be set by a global or file-wise option.

See `Call` for more information.

TODO: document orders which are call-matrices themselves.

Constructors

Mat (Matrix Integer Order) |

Instances

Eq Order |
Ord Order |
Show Order |
Arbitrary Order |
CoArbitrary Order |
HasZero Order |
Pretty Order |

decr :: [cutoff :: Int] => Int -> Order

Smart constructor for `Decr k :: Order` which cuts off too big values.

Possible values for `k`: `- ?cutoff `<=` k `<=` ?cutoff + 1`.

increase :: Int -> Order -> Order

Raw increase which does not cut off.

decrease :: Int -> Order -> Order

Raw decrease which does not cut off.

(.*.) :: [cutoff :: Int] => Order -> Order -> Order

Multiplication of `Order`s. (Corresponds to sequential composition.)

supremum :: [cutoff :: Int] => [Order] -> Order

The supremum of a (possibly empty) list of `Order`s. More information (i.e., more decrease) is bigger. `Unknown` is no information, thus, smallest.

infimum :: [cutoff :: Int] => [Order] -> Order

The infimum of a (non empty) list of `Order`s. `Unknown` is the least element, thus, dominant.

decreasing :: Order -> Bool

le :: Order

`le`, `lt`, `decreasing`, `unknown`: for backwards compatibility, and for external use.

lt :: Order

unknown :: Order

orderMat :: Matrix Integer Order -> Order

Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.

# Call matrices

type Index = Integer

Call matrix indices.

newtype CallMatrix

Call matrices. Note the call matrix invariant (`callMatrixInvariant`).

Constructors

CallMatrix |

Fields

mat :: Matrix Index Order

Instances

Eq CallMatrix |
Ord CallMatrix |
Show CallMatrix |
Arbitrary CallMatrix |
CoArbitrary CallMatrix |

(>*<) :: [cutoff :: Int] => Call -> Call -> Call

`Call` combination.

Precondition: see `<*>`; furthermore the `source` of the first argument should be equal to the `target` of the second one.

callMatrixInvariant :: CallMatrix -> Bool

In a call matrix at most one element per row may be different from `Unknown`.

# Calls

data Call

This datatype encodes information about a single recursive function application. The columns of the call matrix stand for `source` function arguments (patterns); the first argument has index 0, the second 1, and so on. The rows of the matrix stand for `target` function arguments. Element `(i, j)` in the matrix should be computed as follows:

- `Lt` (less than) if the `j`-th argument to the `target` function is structurally strictly smaller than the `i`-th pattern.
- `Le` (less than or equal) if the `j`-th argument to the `target` function is structurally smaller than the `i`-th pattern.
- `Unknown` otherwise.

The structural ordering used is defined in the paper referred to above.

Constructors

Call |

Fields

source :: Index

  The function making the call.

target :: Index

  The function being called.

cm :: CallMatrix

  The call matrix describing the call.

Instances

Eq Call |
Ord Call |
Show Call |
Arbitrary Call |
CoArbitrary Call |

callInvariant :: Call -> Bool

`Call` invariant.

# Call graphs

data CallGraph meta

A call graph is a set of calls. Every call also has some associated meta information, which should be `Monoid`al so that the meta information for different calls can be combined when the calls are combined.

Instances

Eq meta => Eq (CallGraph meta) |
Show meta => Show (CallGraph meta) |
Monoid meta => Monoid (CallGraph meta) | `CallGraph` is a monoid under `union`.
Show meta => Pretty (CallGraph meta) | Displays the recursion behaviour corresponding to a call graph.

callGraphInvariant :: CallGraph meta -> Bool

`CallGraph` invariant.

fromList :: Monoid meta => [(Call, meta)] -> CallGraph meta

Converts a list of calls with associated meta information to a call graph.

toList :: CallGraph meta -> [(Call, meta)]

Converts a call graph to a list of calls with associated meta information.

empty :: CallGraph meta

Creates an empty call graph.

union :: Monoid meta => CallGraph meta -> CallGraph meta -> CallGraph meta

Takes the union of two call graphs.

insert :: Monoid meta => Call -> meta -> CallGraph meta -> CallGraph meta

Inserts a call into a call graph.

complete :: [cutoff :: Int] => Monoid meta => CallGraph meta -> CallGraph meta

``complete` cs` completes the call graph `cs`. A call graph is complete if it contains all indirect calls; if `f -> g` and `g -> h` are present in the graph, then `f -> h` should also be present.

prettyBehaviour :: Show meta => CallGraph meta -> Doc

Displays the recursion behaviour corresponding to a call graph.

# Tests

tests :: IO Bool