Motivation

A proof assistant based on type theory has to reject non-terminating definitions: a function that loops can inhabit any type, including the empty one, and so proves everything. Agda therefore checks every recursive definition for termination before accepting it. Purely syntactic checks, which require some argument to become structurally smaller at each recursive call, reject many terminating programs, for example recursion through a higher-order function such as map, or corecursive definitions by copattern matching whose productivity depends on sizes rather than syntax.

Two lines of work address this. Size-change termination (Lee, Jones and Ben-Amram, 2001) abstracts each call into a graph recording which arguments decrease, and accepts a program when every infinite call sequence would force an infinite descent. Sized types record an upper bound on the depth of data in its type, so that termination follows from typing. Kanstantsin Nisht's 2024 master's thesis, supervised by Andreas Abel, combines the two in a type-based termination checker for Agda-style programs. Sizes are inferred automatically, and termination is checked by size-change analysis over the inferred sizes. The thesis proves that every program the checker accepts is well-typed and strongly normalizing. This mission formalizes that soundness proof in Lean.

Setting

System $F_\omega^{\mathrm{cop,SCT}}$ is a higher-order polymorphic lambda calculus with copattern matching. Its kinds carry polarities $\pi \in \{\circ, +, -, \top\}$ that record how a type operator uses its argument. Size expressions are $\infty + n$ or minima $(i_1 + n_1) \wedge \dots \wedge (i_k + n_k)$ of size variables, and size contexts $\Psi$ bound each size variable from above. Sized inductive and coinductive types $\mu^a S$ and $\nu^a R$ are indexed by a size $a$. Programs are sequences of mutual blocks $\Xi$ of functions defined by copattern clauses, checked against a global signature $\Sigma$ of previously accepted functions.

Termination is certified by an invocation-graph family $\mathcal{G}$, which assigns to each pair of functions a set of bipartite graphs relating the caller's size arguments to the callee's by $<$ or $\le$. The size-change criterion $\vdash \mathcal{G}$ (SCTValid) requires a strict self-decrease in every idempotent graph of the closure. Semantically, types denote Girard–Tait reducibility candidates of strongly normalizing terms. Sizes denote ordinals, and $\Sigma \models \Xi$ (SemMutualBlockValid) says that every function in $\Xi$ belongs to the interpretation of its type.

Algorithm 2 takes a block written without sizes, in System $F_\omega^c$. It encodes each declared type with fresh size variables, elaborates patterns and clause bodies while emitting size constraints, solves the constraints with Algorithm 1, builds the invocation-graph family of the calls, and accepts the block if the size-change criterion holds. The result is a size-annotated block $\Xi_{\mathrm{annot}}$.

Formalization targets

Goal: soundness of the termination checker (Theorem 15, corrected)

$$\mathsf{scopeBlockExtension}\ \Sigma\ \Xi_{\mathrm{annot}} \;\wedge\; \mathsf{SemSigValidIn}\ \Sigma\ \Xi_{\mathrm{annot}} \;\wedge\; \mathsf{PostcheckedAlgorithm2Accepts}\ \Sigma\ \Xi\ \Xi_{\mathrm{annot}} \;\Longrightarrow\; \Sigma \vdash \Xi_{\mathrm{annot}} \;\wedge\; \Sigma \models \Xi_{\mathrm{annot}}$$

If a new block extends a valid, closed signature without forward references, and Algorithm 2 accepts it, then the annotated block is well-typed and every function in it is strongly normalizing. Lean name: NishtAbel2024V2.theorem_15.

Milestones, in the thesis's order

• Lemma 1 and Theorem 1: graph composition preserves conformance, and $\vdash \mathcal{G}$ makes the size-change call relation well-founded.
• Theorems 2–3 (corrected): soundness of size judgments and of expression and clause typing.
• Theorems 4–6 and Lemma 2 (corrected): strong normalization of mutual blocks, signatures and programs, and the embedding of lexicographic termination ($F_\omega^{\mathrm{cop}}$) into $F_\omega^{\mathrm{cop,SCT}}$.
• Theorems 7–9 and Lemmas 3–5 (corrected): well-kindedness of the signature encoding, pattern and spine elaboration, and polarities of rigid size variables.
• Theorems 10–12 (corrected): polarity of generated constraints, and absence of constraints from flexible to rigid size variables.
• Theorems 13–14 and Corollary (corrected): typing of size-instantiated clauses, and coherence of the substitution computed by Algorithm 1.

Significance

The result. Theorem 15 is the soundness guarantee a proof assistant needs before it can adopt the checker: accepted definitions cannot be used to derive a contradiction through non-termination. Theorem 6 shows that the type system subsumes lexicographic termination: every block typable in $F_\omega^{\mathrm{cop}}$ with a lexicographic size measure is typable in $F_\omega^{\mathrm{cop,SCT}}$ once the measure is erased. The semantic results, Theorems 1–5, apply to any front end that produces derivations in $F_\omega^{\mathrm{cop,SCT}}$, not only to Algorithm 2.

Formalizing it. The thesis's proofs are on paper. Formalizing them showed that the first Lean statements of Theorems 2–3, 4–6, 7–9 with Lemmas 3–5, 10–12, 13–14 and 15 were all false. Each has a machine-checked counterexample, and each refuted statement records the reason on its own page. Theorems 2–6 and 15 were stated without the thesis's scope discipline: an existing function could share a name with, or refer to, a function of the new block, forming a loop through the existing signature that the size-change check of the new block does not see. Theorem 11 checked one occurrence of a rigid size variable where the thesis requires all occurrences to lie in least fixpoints. Theorems 13–14 omitted well-formedness of the global signature. The Lemma 5 statement allowed inputs that the thesis's encoding never produces. The counterexamples show where the paper argument depends on assumptions it states informally. They do not refute the thesis's theorems under those assumptions.

As of November 2026, Lemma 1 and Theorem 1 are proved over the original definitions, with no statement over the corrected definitions yet. The corrected Theorems 7–14 are proved, and the corrected Theorems 2–6 and 15 are open. The milestone list shows the current state.

Difficulty

The central step is Theorem 4: a mutual block is strongly normalizing once its calls satisfy the size-change criterion. Induction on a single size argument does not suffice, because mutually recursive calls may decrease different arguments along different call paths. Strong normalization of one function therefore depends on the whole call structure of the block, and the semantic typing of Theorem 3 has to hold uniformly while the existing signature stays fixed.

On the inference side, constraint solving is sound only if no constraint forces a flexible size variable below a rigid one. Establishing this (Theorems 10–12) requires tracking the polarity of every size occurrence through higher-kinded type operators, including operators that ignore an argument. The first formal attempts show that a statement of these invariants close to the prose is false, so finding a provable statement is itself part of the work.

Formalization scope

Lean names with the suffix V2 (namespace NishtAbel2024V2) are the corrected statements, built on three definition modules: NishtAbel2024V2_Syntax, NishtAbel2024V2_Semantics and NishtAbel2024V2_Inference. The namespace NishtAbel2024 holds the first formalization, whose refuted statements remain on the platform with their disproofs. The corrected statements commit to the following conventions.

• Scope. A new block extends a closed, duplicate-free signature and refers only to itself and earlier functions (scopeBlockExtension; scopeOrderedBlocks for programs).
• Ambient validity. The existing signature is assumed semantically valid in the world that includes the new block (SemSigValidIn).
• Postchecked Algorithm 2. Acceptance includes a final check that each size-instantiated clause body type-checks (PostcheckedAlgorithm2Accepts). Corrected Theorem 13 and the typing half of Theorem 15 therefore rest on this check. The thesis's stronger claim, that inference always produces well-typed output from a well-formed signature, is not part of the targets.
• Checked solver. Corrected Theorem 14 concerns CheckedConstraintSolver.checkedSolve, which returns Algorithm 1's substitution only when a finite coherence certificate succeeds.
• Guarded inference. Corrected Theorems 10–12 concern the instrumented variants GuardedCompareTypes, SafeInferTerm and SafeCheckTerm; the last two erase to the original inference judgments.
• Occurrences. Corrected Lemmas 4–5 bound the polarity of kinding-aware size occurrences (CheckUse) instead of stating the thesis's four-way classification.
• Measures. Theorem 6 requires a non-empty lexicographic measure.

The main goal does not assume that the new block terminates. It assumes validity of the existing signature only, so the strong normalization conclusion is not built into the hypotheses.

Several proved milestones (scope stability, Theorem 2 size soundness, a guarded Theorem 10, Theorems 7–9, Lemma 3, and the lexicographic graph construction of Theorem 6) are stated over the original NishtAbel2024 definitions. They are correct results about that model but do not transfer to the corrected definitions. Contributions are welcome for:

• a statement and proof of Lemma 1 and Theorem 1 over the corrected definitions;
• proofs of corrected Theorems 2–3, 4–6 and 15;
• a proof that the postcheck always succeeds for well-formed signatures, which would recover the thesis's form of Theorem 13;
• a source-level review of Lemma 4.

Selected references

• K. Nisht, Type-Based Termination Checking in Agda, MSc thesis, Chalmers University of Technology and University of Gothenburg, 2024; supervisor A. Abel. Extended abstract at TYPES 2024, Copenhagen. https://knisht.github.io/agda/msc.pdf
• C. S. Lee, N. D. Jones, A. M. Ben-Amram, The size-change principle for program termination, POPL 2001. https://doi.org/10.1145/360204.360210
• A. Abel, B. Pientka, Well-founded recursion with copatterns and sized types, Journal of Functional Programming 26, 2016. https://doi.org/10.1017/S0956796816000022