Agda.Termination.CallMatrix

Call matrix indices = function argument indices.

Machine integer Int is sufficient, since we cannot index more arguments than we have addresses on our machine.

Call matrices.

A call matrix for a call f --> g has dimensions ar(g) × ar(f).

Each column corresponds to one formal argument of caller f. Each row corresponds to one argument in the call to g.

In the presence of dot patterns, a call argument can be related to several different formal arguments of f.

See e.g. testsucceedDotPatternTermination.agda:

    data D : Nat -> Set where
      cz : D zero
      c1 : forall n -> D n -> D (suc n)
      c2 : forall n -> D n -> D n

    f : forall n -> D n -> Nat
    f .zero    cz        = zero
    f .(suc n) (c1  n d) = f n (c2 n d)
    f n        (c2 .n d) = f n d
  

Call matrices (without guardedness) are

          -1 -1   n < suc n  and       n <  c1 n d
           ?  =                   c2 n d <= c1 n d

           = -1   n <= n     and  n < c2 n d
           ? -1                   d < c2 n d
  

Here is a part of the original documentation for call matrices (kept for historical reasons):

This datatype encodes information about a single recursive function application. The columns of the call matrix stand for source function arguments (patterns). 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.

Call matrix multiplication and call combination.

Call matrix augmented with path information.

Non-augmented call matrix.

Sets of incomparable call matrices augmented with path information. Use overloaded null, empty, singleton, mappend.

Insert into a call matrix set.

Union two call matrix sets.

Convert into a list of augmented call matrices.