Chapter 83Optional

Size-Change Termination

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Consider the two functions $\begin{aligned} f (x, y) & : = {\begin{cases} g (x, y - 1) & y > 0, \\ 0 & y = 0, \end{cases} \\ g (x, y) & : = {\begin{cases} f (x - 1, x) & x > 0, \\ 0 & x = 0. \end{cases} \end{aligned}$ The arguments range over $N$ , and subtraction is truncated at zero. The call from $f$ decreases its second argument; the call from $g$ decreases its first. No single argument decreases on every call. A componentwise checker therefore rejects the program even though every alternating pair of calls decreases the first argument of $f$ . We need to compose information across calls before choosing the descending argument.

Matrices record usable decreases

Let $≺$ be a well-founded relation on a value type $V$ . Write $a ⪯ b$ for its reflexive closure. The two relations have different roles: $≺$ contributes strict descent, while $⪯$ only transports a candidate thread through a call.

Definition 83.1 — Size-change label ¶

A size-change label is one of $?, ⇓^{=}, ⇓^{<} .$ The unknown label $?$ asserts nothing. The weak label $⇓^{=}$ asserts $v^{'} ⪯ v$ . The strict label $⇓^{<}$ asserts $v^{'} ≺ v$ . Their information order is $? <_{info} ⇓^{=} <_{info} ⇓^{<} .$

Referenced from 3 locations

Size-Change Termination

The decorations prevent the weak label from being confused with the object-language order $⪯$ . A label is information about one edge; it is not itself a comparison between values.

Definition 83.2 — Size-change matrix ¶

Suppose a caller $f$ has parameters $x_{1}, \dots, x_{m}$ and a callee $g$ has parameters $y_{1}, \dots, y_{n}$ . A size-change matrix $M : f \to g$ is an $n$ -by- $m$ matrix of labels. Its entry $M_{i j}$ describes the relation of callee value $y_{i}$ to caller value $x_{j}$ . The matrix is truthful for a call when every weak entry denotes a true $y_{i} ⪯ x_{j}$ and every strict entry denotes a true $y_{i} ≺ x_{j}$ .

Referenced from 2 locations

Size-Change Termination

Rows belong to the callee and columns to the caller. Reversing that convention transposes composition and can manufacture a false diagonal. For the displayed program, use parameter order $(x, y)$ at both functions. The two call matrices are $M_{f g} = (\begin{matrix} ⇓^{=} & ? \\ ? & ⇓^{<} \end{matrix}), M_{g f} = (\begin{matrix} ⇓^{<} & ? \\ ⇓^{=} & ? \end{matrix}) .$ The guard $y > 0$ makes $y - 1 < y$ , so the lower-right entry of $M_{f g}$ is strict. Without that guard, truncated subtraction at $y = 0$ would justify only a weak entry.

Definition 83.3 — Label product and join ¶

Define path composition $a \otimes b$ by $a \otimes b : = {\begin{cases} ? & a = ? or b = ?, \\ ⇓^{<} & a \neq ? and b \neq ? and (a = ⇓^{<} or b = ⇓^{<}), \\ ⇓^{=} & a = b = ⇓^{=} . \end{cases}$ Define $a \oplus b$ as the greater label in the information order of definition 83.1. Thus competing paths retain the strongest comparison proved by either path.

Referenced from 2 locations

Size-Change Termination

Definition 83.4 — Matrix composition ¶

For $M : f \to g$ and $N : g \to h$ , define $N; M : f \to h$ by $(N; M)_{i j} : = ⨁_{k} N_{i k} \otimes M_{k j} .$ The middle index $k$ ranges over parameters of $g$ .

Referenced from 3 locations

Size-Change Termination

The product of two true weak comparisons is weak. A true strict comparison followed or preceded by a weak comparison is strict, by mixed transitivity of $≺$ and $⪯$ . Therefore composition preserves truthfulness.

Lemma 83.5 — Truthful composition ¶

Let $M : f \to g$ be truthful for a call $\vec{v} \mapsto \vec{w}$ , and let $N : g \to h$ be truthful for a call $\vec{w} \mapsto \vec{z}$ . Then $N; M$ is truthful for the two-call path $\vec{v} \mapsto \vec{z}$ .

Referenced from 2 locations

Size-Change Termination

Proof of Lemma 83.5 — Truthful composition

Proof. Fix an entry $(i, j)$ . If $(N; M)_{i j} = ?$ , there is no claim to prove. A weak entry is obtained from some middle parameter $k$ with two weak entries. Their truth gives $z_{i} ⪯ w_{k} ⪯ v_{j}$ , hence $z_{i} ⪯ v_{j}$ . A strict entry is obtained from a middle parameter $k$ for which one constituent entry is strict and the other is weak or strict. Mixed transitivity gives $z_{i} ≺ v_{j}$ . The join retains only a claim proved by at least one such $k$ . ◻

For the two-call path $f \to g \to f$ , $M_{g f}; M_{f g} = (\begin{matrix} ⇓^{<} & ? \\ ⇓^{=} & ? \end{matrix}) .$ The strict first diagonal is the decrease missed by a one-call componentwise check. Squaring this self-matrix yields $(\begin{matrix} ⇓^{<} & ? \\ ⇓^{<} & ? \end{matrix}),$ which is stable under another square.

Exercise 83.1 ¶

★☆☆ Calculate $M_{f g}; M_{g f} : g \to g$ . Identify every intermediate parameter that witnesses a known entry. Check its square and state which diagonal is strict.

Referenced from 3 locations

Multipaths and descending threads

A finite matrix calculation must rule out an infinite call sequence. The bridge is a thread: a sequence of parameter positions connected by known matrix entries.

Definition 83.6 — Multipath and thread ¶

A multipath is a finite or infinite composable sequence $f_{0} \overset{M_{0}}{\to} f_{1} \overset{M_{1}}{\to} f_{2} \overset{M_{2}}{\to} \dots .$ A thread chooses a parameter index $i_{k}$ of $f_{k}$ at each selected stage so that $(M_{k})_{i_{k + 1}, i_{k}}$ is known. It is infinitely descending when the selected labels are strict for infinitely many $k$ .

Referenced from 2 locations

Size-Change Termination

Truthfulness turns an infinitely descending thread into an infinite $≺$ -descent. Weak edges transport values between strict edges; deleting the finite weak segments gives $v_{k_{1}} ≺ v_{k_{0}}, v_{k_{2}} ≺ v_{k_{1}}, \dots,$ contradicting well-foundedness.

Definition 83.7 — Safe call graph ¶

A finite call graph $G$ is size-change safe when every infinite call path permitted by its control-flow graph has a multipath containing an infinitely descending thread.

Referenced from 2 locations

Size-Change Termination

Theorem 83.8 — Size-change descent ¶

Let $G$ be a finite first-order call graph over a well-founded value order. If every concrete call is covered by a truthful edge matrix and $G$ is size-change safe, then the program has no infinite call sequence.

Referenced from 6 locations

Proof of Theorem 83.8 — Size-change descent

Proof. Assume an infinite call sequence. Choose for each call a truthful covering matrix. Safety gives an infinitely descending thread through their multipath. Truthfulness and the preceding weak-segment contraction produce an infinite strict descent in the value order, contradicting well-foundedness. ◻

The proof uses every hypothesis. With a false strict label, the matrix thread need not describe the execution. With a non-well-founded order, a truthful infinite descent is possible. Without safety, the infinite path may contain no descending thread.

Finite closure detects every bad cycle

Safety quantifies over infinite paths. A checker needs an equivalent finite condition. There are finitely many function names, arities, and matrices, so composition reaches a fixed point after finitely many insertions.

Definition 83.9 — Composition closure and idempotent test ¶

The composition closure $C (G)$ contains every edge matrix of a finite call graph $G$ and every well-typed finite composition of its members. A square matrix $M : f \to f$ is idempotent when $M; M = M$ . The idempotent-cycle test accepts $G$ when every idempotent $M : f \to f$ in $C (G)$ has $M_{i i} = ⇓^{<}$ for some parameter $i$ of $f$ .

Referenced from 4 locations

Size-Change Termination

Exercise 83.2 ¶

★★☆ Take the nonterminating call $h (x) = h (x)$ on naturals. Label its self-edge strict and show that the idempotent-cycle test of definition 83.9 accepts it. Identify the exact hypothesis of theorem 83.8 that fails, then replace the label by the strongest truthful one.

Referenced from 3 locations

Closure is finite. A matrix between fixed arities has three choices per entry, and the graph has finitely many function pairs. Repeatedly inserting all composable products must therefore stop. Termination of this saturation algorithm is separate from termination of the analyzed program.

Lemma 83.10 — A strict diagonal repeats ¶

Let $M : f \to f$ be idempotent and suppose $M_{i i} = ⇓^{<}$ . Then the infinite repetition $M, M, M, \dots$ contains an infinitely descending thread at parameter $i$ .

Referenced from 3 locations

Size-Change Termination

Proof of Lemma 83.10 — A strict diagonal repeats

Proof. Choose index $i$ at every stage. Each selected entry is the strict diagonal $M_{i i}$ . Hence every edge of the thread is strict. ◻

Theorem 83.11 — Finite idempotent criterion ¶

Let $G$ be a finite first-order call graph. Every infinite multipath in $G$ has an infinitely descending thread if and only if every idempotent self-matrix in $C (G)$ has a strict diagonal.

Referenced from 5 locations

Size-Change Termination

Proof of Theorem 83.11 — Finite idempotent criterion

Proof. The theorem is the graph criterion of Lee, Jones, and Ben-Amram at their finite size-change-graph signature [LJBA01].

For the reverse implication, suppose an infinite multipath has no infinitely descending thread. Some function $f$ occurs infinitely often. For two occurrences of $f$ , color the pair by the composite matrix along the segment between them. There are finitely many colors. Infinite Ramsey’s theorem for pairs gives an infinite subsequence on which every segment has the same composite $M : f \to f$ . Three occurrences give $M; M = M$ . If $M$ had a strict diagonal, lemma 83.10 would give an infinitely descending thread through those segments. Hence $M$ is a bad idempotent in the closure.

For the forward implication, let $M : f \to f$ be an idempotent without a strict diagonal. Repeat a path whose composite is $M$ . The source graph lemma says that a thread through a finite segment exists exactly when the corresponding composite entry is known, and it is strict exactly when that entry is strict. Suppose a thread through the repeated path had infinitely many strict edges. Record its parameter index at every segment boundary. Some index $i$ occurs at two boundaries with a strict edge between them, by the pigeonhole principle. The corresponding entry of $M^{k}$ is strict for some $k > 0$ ; idempotence gives $M^{k} = M$ , so $M_{i i}$ is strict, a contradiction. The repeated multipath therefore has no infinitely descending thread. This is the contrapositive of the required direction. The graph lemma is proved by induction on segment length from definition 83.4; the two-step case is exactly the choice of the middle index $k$ . ◻

Combining theorem 83.8, theorem 83.11 gives a sound termination certificate.

Corollary 83.12 — Sound finite checker ¶

Let $G$ be finite, let its labels be truthful for all concrete calls, and let the value order be well founded. If the idempotent-cycle test accepts $G$ , then the represented program has no infinite call sequence.

Referenced from 2 locations

Size-Change Termination

Proof of Corollary 83.12 — Sound finite checker

Proof. By theorem 83.11, acceptance makes $G$ size-change safe. Apply theorem 83.8. ◻

The criterion is complete for safety of the finite graph abstraction. It is not complete for termination of programs: graph extraction may omit semantic facts, and a terminating program may have no safe abstraction in the selected three-label language.

Exercise 83.3 ¶

★★☆ Let $p (m, n, r) = {\begin{cases} p (m, r - 1, n) & r > 0, \\ p (r, n - 1, m) & r = 0 and n > 0, \\ m & r = n = 0. \end{cases}$ Build one matrix for each recursive branch. Compute enough closure matrices to exhibit the idempotent self-cycles and locate a strict diagonal in each.

Referenced from 3 locations

Exercise 83.4 ¶

★★☆ Give three separate counterexamples to the soundness conclusion, dropping in turn truthfulness, well-foundedness of the value order, and the strict-diagonal condition. Keep the other two hypotheses valid in each example.

Referenced from 3 locations

Bibliographic note

The size-change graphs, multipaths, descent theorem, composition, and finite idempotent criterion are reconstructed from Lee, Jones, and Ben-Amram [LJBA01]. Their criterion concerns a finite first-order abstraction with truthful edges. It is not by itself a verified termination checker for a dependent language.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 83.5, exercise 83.8.

Exercise 83.5 ¶

★★★ For the mutually recursive $f / g$ program at the chapter opening, build the two matrices, close them under path composition, and list every idempotent self-matrix. Prove that each has a strict diagonal. Then erase both positivity guards from the abstraction, replace the lower-right strict entry of $M_{f g}$ and the upper-left strict entry of $M_{g f}$ by weak entries, and calculate the first idempotent matrix with no strict diagonal.

Referenced from 4 locations

Exercise 83.6 ¶

★★★ Reconstruct the reverse implication of theorem 83.11. State the finite coloring, use three members of the homogeneous set to derive idempotence, and show how a strict diagonal would produce the forbidden thread. Label the exact use of graph finiteness.

Referenced from 3 locations

Exercise 83.7 ¶

★★☆ Design a truthful extraction for calls over pairs of natural numbers using only syntactic predecessor, projection, and variable permutation. Give one semantic decrease that the extraction misses and explain why that loss harms completeness but not soundness.

Referenced from 3 locations

Exercise 83.8 ¶

★★★ Practical project.size-change-checker Implement in Kappa the three labels, matrix composition, finite closure, and the idempotent-cycle test of definition 83.9. Maintain the invariant that every stored edge has compatible source and target arities and that Closed is returned only at a genuine fixed point. For the chapter’s $f / g$ graph, print the saturated self-cycle and accept it with a strict first diagonal. Replace that diagonal by a weak comparison; the mutated idempotent self-cycle must be rejected with the exact witness no-strict-diagonal. The acceptance test passes exactly when the first graph is accepted, the mutation is rejected with that witness, and audit returns [].

Referenced from 5 locations