ch:size-change-termination: ch:size-change-termination

Problem and result. Implement the finite two-parameter size-change test. The finished program prints the saturated self-cycle of the chapter’s $f/g$ graph, accepts its strict first diagonal, and rejects the weak mutation with no-strict-diagonal.

Representation. Use three constructors Unknown, Weak, and Strict, and store a two-by-two matrix as four entries. This fixed representation makes the selected graph executable and its four compositions visible. A general list-of-lists representation would support arbitrary arities but would add bounds checks unrelated to this exercise.

First complete version. Implement composition of two comparison labels, then join the two paths through an intermediate parameter. Apply the operation to all four entries of a matrix product. Repeatedly insert every well-typed composition until no new edge appears. The direct self-composite is $[[\mathtt{Strict},?],[\mathtt{Weak},?]]$; its square is the saturated matrix $[[\mathtt{Strict},?],[\mathtt{Strict},?]]$. If an implementation uses fuel, return a distinct Exhausted result and never accept it as a closure.

Remaining cases. Test idempotence by comparing the matrix with its square. Inspect both diagonal entries and accept only when one is Strict. For the mutation, replace the saturated matrix’s first diagonal by Weak, obtaining $[[\mathtt{Weak},?],[\mathtt{Strict},?]]$.

A failing version. Accept an idempotent matrix merely because it has a known weak diagonal. The prescribed weakened saturated matrix then passes, contradicting the required no-strict-diagonal verdict.

Acceptance test. Require the exact accepted closure witness, the exact rejected mutation, the final two-case summary, and an empty audit.

Mathematical boundary. The program decides the finite matrices supplied to it. It does not prove the imported theorem that an accepted safe call graph has no infinite call path.