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.