Chapter 82Core route

Well-Founded Recursion

The recursive call in $\gcd (a, b) = {\begin{cases} a & b = 0, \\ \gcd (b, a rem b) & b > 0 \end{cases}$ does not receive a constructor field of either argument. It nevertheless decreases: the remainder is strictly smaller than the positive divisor. Structural recursion from chapter 28 sees syntax; this argument uses a relation. The missing object is a finite certificate that all smaller calls can themselves be evaluated.

Definition 82.1 — Structural-call invariant ¶

Consider a constructor branch of the inductive schema of chapter 28 whose scrutinee has the form $c_{i} (\vec{u}, f_{1}, \dots, f_{r_{i}}) .$ A structural recursor may call itself only at $\begin{matrix} (S t r u c t u r a l - c a l l) & f_{j} (\vec{z}), 1 \leq j \leq r_{i}, \vec{z} : Θ_{i j} . \end{matrix}$ Thus every recursive argument is obtained by applying one recursive constructor field to arguments from its arity telescope. For recursion on the second input of $\gcd$ , the positive branch has input $b \equiv suc (b_{0})$ , but its recursive input $a rem b$ is neither the field $b_{0}$ nor an application of a recursive constructor field. Recursing on the first input fails the same test because the recursive input is $b$ , which need not be a constructor field of $a$ . Hence neither choice makes the Euclidean call an instance of (Structural-call).

Referenced from 3 locations

Well-Founded Recursion

Accessibility records the recursive calls

Let $A : U_{i}$ and let $R : A \to A \to U_{j}$ be a proof-relevant binary relation. We write $b R a$ when a recursive call at $a$ may call the function at $b$ . The order of the arguments is part of this convention. The optional signature $T_{rec}$ is $T_{0}$ extended by the indexed accessibility schema and the labeled constructor, eliminator, and computation rules displayed in this section; accessibility is not a new judgmental principle of $T_{0}$ .

Definition 82.2 — Accessibility and well-foundedness ¶

An element $a : A$ is accessible for $R$ when every $R$ -predecessor of $a$ is accessible. The indexed family ${Acc}_{R} : A \to U_{i ⊔ j}$ is governed first by formation and introduction:

Γ ⊢ A : U_{i}

Γ ⊢ R : A \to A \to U_{j}

Γ ⊢ a : A

Γ ⊢ {Acc}_{R} (a) : U_{i ⊔ j}

Acc-form

Γ ⊢ a : A

Γ ⊢ h : \prod_{b : A} b R a \to {Acc}_{R} (b)

Γ ⊢ {acc}_{a} (h) : {Acc}_{R} (a)

Acc-intro

Thus its constructor has the type ${acc}_{a} : (\prod_{b : A} b R a \to {Acc}_{R} (b)) \to {Acc}_{R} (a) .$ The relation $R$ is well founded when $WellFounded (R) : = \prod_{a : A} {Acc}_{R} (a)$ is inhabited. This definition asserts accessibility of every element; it does not assert that a program can decide $b R a$ .

Referenced from 4 locations

The constructor stores precisely the recursive calls permitted below $a$ . For $p \equiv {acc}_{a} (h)$ and $r : b R a$ , the proof $h b r$ is the smaller certificate used by the recursive call.

Remark 82.3 — Cycles are excluded ¶

If $a_{0} R a_{1} R \dots R a_{n} = a_{0}$ , then no term of ${Acc}_{R} (a_{0})$ exists in a normalizing theory. Repeatedly inspecting the outer $acc$ constructor follows the cycle and produces an infinite sequence of proper subterms. Thus well-foundedness excludes every finite cycle. The converse fails for arbitrary relations: an acyclic relation may still contain an infinite descending chain. For example, on $N$ put $b R a : = {Id}_{N} (b, suc (a)) .$ This relation has no cycle, while $1 R 0$ , $2 R 1$ , $3 R 2$ , and so on give the infinite sequence of successive predecessors $0, 1, 2, 3, \dots$ .

Referenced from 2 locations

Well-Founded Recursion

Definition 82.4 — Accessibility elimination ¶

Let $P : \prod_{a : A} {Acc}_{R} (a) \to U_{k} .$ Put $\begin{aligned} H (a) & : = \prod_{b : A} b R a \to {Acc}_{R} (b), \\ K (a, h) & : = \prod_{b : A} \prod_{r : b R a} P (b, h b r), \\ {Step}_{P} & : = \prod_{a : A} \prod_{h : H (a)} K (a, h) \to P (a, {acc}_{a} (h)) . \end{aligned}$ The proof-dependent accessibility eliminator has the compact rule

Γ ⊢ P : \prod_{a : A} {Acc}_{R} (a) \to U_{k}

Γ ⊢ a : A

Γ ⊢ s : {Step}_{P}

Γ ⊢ p : {Acc}_{R} (a)

Γ ⊢ {accind}_{P} (s, a, p) : P (a, p)

Acc-elim

and its computation rule is ${accStep}_{P} (s, a, h) : = s (a, h, λ b . λ r . {accind}_{P} (s, b, h b r)) .$

Γ ⊢ P : \prod_{a : A} {Acc}_{R} (a) \to U_{k}

Γ ⊢ a : A

Γ ⊢ s : {Step}_{P}

Γ ⊢ h : H (a)

{accind}_{P} (s, a, {acc}_{a} (h)) \equiv {accStep}_{P} (s, a, h) : P (a, {acc}_{a} (h))

Acc-β

Equivalently, $\begin{array}{r} (A c c - β) & {accind}_{P} (s, a, {acc}_{a} (h)) \equiv s (a, h, λ b . λ r . {accind}_{P} (s, b, h b r)) . \end{array}$ The argument $h$ exposes the immediate accessibility subproofs. The final argument gives the induction result at each such subproof. Taking $P (a, p) : = Q (a)$ derives the non-proof-dependent eliminator used for ordinary well-founded recursion.

Referenced from 4 locations

Theorem 82.5 — Accessibility induction ¶

Let $P : A \to U_{k}$ . Suppose $s : \prod_{a : A} (\prod_{b : A} b R a \to P (b)) \to P (a) .$ Define $P^{'} (a, p) : = P (a)$ and $s^{'} (a, h, k) : = s (a, k)$ . Then ${accind}_{P^{'}} (s^{'}) : \prod_{a : A} {Acc}_{R} (a) \to P (a) .$ If $w : WellFounded (R)$ , then $λ a . {accind}_{P^{'}} (s^{'}, a, w a) : \prod_{a : A} P (a)$ .

Referenced from 3 locations

Well-Founded Recursion

Proof of Theorem 82.5 — Accessibility induction

Proof. Fix $a : A$ and $p : {Acc}_{R} (a)$ . Apply Acc-elim to $p$ . For the constant-in-the-certificate motive $P^{'}$ , the displayed definition of $s^{'}$ has type ${Step}_{P^{'}}$ : its recursive-results argument $k$ has type $\prod_{b : A} b R a \to P (b)$ , exactly the second argument required by $s (a)$ . The eliminator has one constructor case. Write $p \equiv {acc}_{a} (h)$ , where $h : \prod_{b : A} b R a \to {Acc}_{R} (b)$ . For each $b : A$ and $r : b R a$ , the induction hypothesis gives ${accind}_{P^{'}} (s^{'}, b, h b r) : P (b) .$ Abstracting $b$ and $r$ produces the recursive-results argument required by $s$ ; applying $s$ gives $P (a)$ . This is exactly the specialization of (Acc-β). If $w$ proves well-foundedness, instantiate the first conclusion with $p : = w a$ at every $a$ . ◻

Exercise 82.1 ¶

★☆☆ Assume $q : a R a$ . Induct directly on the accessibility certificate to construct ${Acc}_{R} (a) \to 0$ . Write the structurally smaller certificate used by the recursive call explicitly. Explain why the nondependent eliminator of definition 82.4 with constant motive $0$ would not by itself establish this fixed-point argument.

Referenced from 3 locations

The recursor and its exact equation

Accessibility induction becomes recursion when the motive describes the result type. Keeping the accessibility certificate visible prevents a hidden proof-irrelevance assumption.

Definition 82.6 — Proof-indexed well-founded recursion ¶

For $P : A \to U_{k}$ and $s : \prod_{a : A} (\prod_{b : A} b R a \to P (b)) \to P (a),$ define the well-founded recursor ${wfrec}_{R, P} (s, a, p) : = {accind}_{λ a . λ p . P (a)} (λ a . λ h . λ k . s (a, k), a, p) .$ Its result and recursive-call types are therefore ${wfrec}_{R, P} (s, a, p) : P (a), k : \prod_{b : A} b R a \to P (b) .$ For a constructor certificate it has the judgmental equation $\begin{array}{r} (W F - β) & {wfrec}_{R, P} (s, a, {acc}_{a} (h)) \equiv s (a, λ b . λ r . {wfrec}_{R, P} (s, b, h b r)) . \end{array}$ Given $w : WellFounded (R)$ , its total specialization is ${wfrec}_{R, P}^{w} (s, a) : = {wfrec}_{R, P} (s, a, w a) .$

Referenced from 6 locations

Equation (WF-β) computes on the accessibility constructor. An equation obtained by replacing ${acc}_{a} (h)$ with an arbitrary $w a$ is not judgmental unless $w a$ unfolds to that constructor. This distinction matters in intensional type theory: different accessibility certificates need not be judgmentally equal.

Here is one complete instance. Let $R_{\emptyset}$ be the empty relation on $1$ , let $h_{⋆} : \prod_{b : 1} b R_{\emptyset} ⋆ \to {Acc}_{R_{\emptyset}} (b)$ eliminate its empty relation proof, and put $s_{0} (x, k) : = 0$ for $x : 1$ . Abbreviate $W (x, p) : = {wfrec}_{R_{\emptyset}, λ x . N} (s_{0}, x, p)$ . Then $\begin{aligned} W (⋆, {acc}_{⋆} (h_{⋆})) & \overset{(W F - β)}{\equiv} s_{0} (⋆, λ b . λ r . W (b, h_{⋆} b r)) \\ \overset{d e f i n i t i o n o f s_{0}}{\equiv} 0 . \end{aligned}$ By contrast, for a variable $z : {Acc}_{R_{\emptyset}} (⋆)$ , the term $W (⋆, z)$ is neutral: its certificate has no outer $acc$ constructor, so (WF-β) has no matching redex.

Proposition 82.7 — Extensional independence of certificates ¶

Assume that $s$ is pointwise extensional: for every $a : A$ and recursive-result functions $k, k^{'}$ , $(\prod_{b : A} \prod_{r : b R a} {Id}_{P (b)} (k b r, k^{'} b r)) \to {Id}_{P (a)} (s (a, k), s (a, k^{'})) .$ Then for $p, q : {Acc}_{R} (a)$ there is an identification ${Id}_{P (a)} ({wfrec}_{R, P} (s, a, p), {wfrec}_{R, P} (s, a, q)) .$

Referenced from 5 locations

Well-Founded Recursion

Proof of Proposition 82.7 — Extensional independence of certificates

Proof. Use accessibility induction on $p$ with the strengthened motive $M (a, p) : = \prod_{q : {Acc}_{R} (a)} {Id}_{P (a)} ({wfrec}_{R, P} (s, a, p), {wfrec}_{R, P} (s, a, q)) .$ In the sole constructor case, let $p \equiv {acc}_{a} (h)$ and fix $q : {Acc}_{R} (a)$ . The second elimination uses the motive $\begin{aligned} W_{x} (q) & : = {wfrec}_{R, P} (s, x, q), \\ I (x, h_{0}) & : = \prod_{b : A} \prod_{r : b R x} M (b, h_{0} b r), \\ N (x, q) & : = \prod_{h_{0} : H (x)} I (x, h_{0}) \to {Id}_{P (x)} (W_{x} ({acc}_{x} (h_{0})), W_{x} (q)) . \end{aligned}$ This motive re-abstracts both $h$ and the outer induction hypothesis, so Acc-elim applies to $q$ without assuming a judgmental inversion at the fixed index. Its constructor case has $q \equiv {acc}_{a} (h^{'})$ . Instantiate the branch at $h$ and at the outer induction hypothesis. For $b : A$ and $r : b R a$ , that hypothesis has type $M (b, h b r)$ . Instantiating its quantified certificate with $h^{'} b r$ gives ${wfrec}_{R, P} (s, b, h b r) =_{P (b)} {wfrec}_{R, P} (s, b, h^{'} b r) .$ Abstracting $b$ and $r$ gives the premise of pointwise extensionality of $s$ . Its conclusion identifies the two applications of $s$ ; conversion by the two instances of (WF-β) closes $N (a, {acc}_{a} (h^{'}))$ at $h$ and the outer hypothesis. The recursive hypotheses generated by this inner Acc-elim are not needed. Hence the outer goal $M (a, {acc}_{a} (h))$ follows. No proof-irrelevance or judgmental equality of $p$ and $q$ is used. ◻

Remark 82.8 — Boundary of certificate independence ¶

Function extensionality implies the pointwise-extensionality hypothesis for every step $s$ : pointwise equal recursive-result functions are then equal, and congruence for $k \mapsto s (a, k)$ gives the required identification. In pure intensional type theory, function extensionality is unavailable and the hypothesis cannot in general be deleted; proposition 82.7 therefore states the exact local extensionality used by its proof.

Referenced from 2 locations

Well-Founded Recursion

Remark 82.9 — Mathematics versus recognition ¶

The recursor consumes $p : {Acc}_{R} (a)$ . It does not search source code for a decreasing argument. A termination checker is an algorithm that constructs such evidence for a selected source language. Soundness of that algorithm is a separate theorem; neither a timeout nor rejection refutes mathematical well-foundedness.

Referenced from 2 locations

Well-Founded Recursion

Measures and lexicographic descent

The usual order on natural numbers is written $m < n$ . Its proof-relevant presentation has constructors witnessing that zero is below every successor and that successor preserves order.

Γ ⊢ n : N

Γ ⊢ ltZero (n) : 0 < suc (n)

Lt-zero

Γ ⊢ p : m < n

Γ ⊢ ltSuc (p) : suc (m) < suc (n)

Lt-suc

These constructor names are used when the proofs below invert a strict inequality.

Definition 82.10 — Weak natural-number order ¶

For $m, n : N$ , write $m \leq n : = {Id}_{N} (m, n) + (m < n) .$ Thus a weak inequality records either equality or a strict inequality; the symbol $\leq$ in this chapter always denotes this sum type.

Referenced from 2 locations

Well-Founded Recursion

Lemma 82.11 — Natural-order inversion and mixed transitivity ¶

For $ℓ, m, n : N$ :

$m \leq 0 \to {Id}_{N} (m, 0)$ ;
$ℓ < suc (n) \to ℓ \leq n$ ;
$ℓ < m \leq n$ implies $ℓ < n$ .

Referenced from 5 locations

Well-Founded Recursion

Proof of Lemma 82.11 — Natural-order inversion and mixed transitivity

Proof. For (1), eliminate the sum defining $m \leq 0$ . Its identity branch is the required term, while its strict branch has type $m < 0$ and is empty by inversion on Lt-zero and Lt-suc. For (2), induct on $n$ . If $n \equiv 0$ , inversion of $ℓ < suc (0)$ gives $ℓ \equiv 0$ , hence the identity injection into $ℓ \leq 0$ . If $n \equiv suc (n^{'})$ , inversion gives either $ℓ \equiv 0$ , when $0 < suc (n^{'})$ , or $ℓ \equiv suc (ℓ^{'})$ with $ℓ^{'} < suc (n^{'})$ . In the latter case, apply the induction hypothesis and map its identity and strict branches through $suc$ . These are precisely the two injections into $ℓ \leq suc (n^{'})$ . For (3), eliminate $m \leq n$ . Transport along its identity branch turns $ℓ < m$ into $ℓ < n$ . In the strict branch, strict transitivity follows by induction on the second $<$ -derivation, applying Lt-suc in its successor case. ◻

Lemma 82.12 — Natural-number accessibility ¶

Every $n : N$ is accessible for $<$ . Hence $<$ is well founded.

Referenced from 3 locations

Well-Founded Recursion

Proof of Lemma 82.12 — Natural-number accessibility

Proof. Prove by induction on $n$ the strengthened statement $Q (n) : = \prod_{m : N} m \leq n \to {Acc}_{<} (m) .$ For $n \equiv 0$ , fix an input $m \leq 0$ . By lemma 82.11(1), obtain $e : {Id}_{N} (m, 0)$ . Construct $p_{0} : = {acc}_{0} (h_{0})$ , where $h_{0}$ eliminates its impossible premise $ℓ < 0$ . Then ${tr}_{e^{- 1}}^{x . {Acc}_{<} (x)} (p_{0}) : {Acc}_{<} (m)$ .

For $n \equiv suc (n^{'})$ , fix $m \leq suc (n^{'})$ . Construct ${acc}_{m} (h)$ . Given $ℓ < m$ , transitivity gives $ℓ < suc (n^{'})$ by lemma 82.11(3), and then lemma 82.11(2) gives $ℓ \leq n^{'}$ . The induction hypothesis at $ℓ \leq n^{'}$ gives ${Acc}_{<} (ℓ)$ , which defines $h$ . Taking $m : = n$ and the left injection of reflexivity into $n \leq n$ concludes the lemma. ◻

Definition 82.13 — Relation induced by a measure ¶

For a function $μ : A \to N$ , define $b <_{μ} a if and only if μ (b) < μ (a) .$ The relation $<_{μ}$ is the measure relation induced by $μ$ .

Referenced from 2 locations

Well-Founded Recursion

Theorem 82.14 — Measure recursion ¶

For every $μ : A \to N$ , the relation $<_{μ}$ is well founded. Consequently a step of type $\prod_{a : A} (\prod_{b : A} μ (b) < μ (a) \to P (b)) \to P (a)$ defines a proof-indexed total result at every $a : A$ .

Referenced from 6 locations

Proof of Theorem 82.14 — Measure recursion

Proof. For $n : N$ and $p : {Acc}_{<} (n)$ , use accessibility induction with the strengthened motive $M (n, p) : = \prod_{a : A} {Id}_{N} (μ (a), n) \to {Acc}_{<_{μ}} (a) .$ In the constructor case $p \equiv {acc}_{n} (h)$ , fix $a : A$ and $e : {Id}_{N} (μ (a), n)$ . For $b : A$ and $r : μ (b) < μ (a)$ , put $r_{e} : = {tr}_{e}^{v . μ (b) < v} (r) : μ (b) < n, p_{b, r} : = h μ (b) r_{e} .$ The induction hypothesis belonging to $p_{b, r}$ proves $M (μ (b), p_{b, r})$ . Its instance at $b$ and reflexivity has type ${Acc}_{<_{μ}} (b)$ ; call that term $I_{b, r}$ . Hence ${acc}_{a} (λ b . λ r . I_{b, r}) : {Acc}_{<_{μ}} (a) .$ Finally apply this construction to $n : = μ (a)$ , the accessibility proof of lemma 82.12, and reflexivity. Accessibility induction then gives the stated recursor. ◻

Definition 82.15 — Lexicographic relation ¶

For relations $R : A \to A \to U_{i}$ and $S : B \to B \to U_{j}$ , their lexicographic relation on $A \times B$ is the proof-relevant relation $((a^{'}, b^{'}) Lex (R, S) (a, b)) : = (a^{'} R a) + ({Id}_{A} (a, a^{'}) \times (b^{'} S b)) .$ The left injection decreases the first coordinate and leaves the second coordinate unrestricted. The right injection keeps the first coordinate identified with $a$ and decreases the second.

Referenced from 3 locations

Well-Founded Recursion

Theorem 82.16 — Lexicographic well-foundedness ¶

If $R$ and $S$ are well founded, then $Lex (R, S)$ is well founded.

Referenced from 4 locations

Proof of Theorem 82.16 — Lexicographic well-foundedness

Proof. Let $w_{R} : WellFounded (R)$ and $w_{S} : WellFounded (S)$ . Apply accessibility induction to $w_{R} a$ with the outer motive $L (a, p) : = \prod_{b : B} {Acc}_{Lex (R, S)} (a, b) .$ In its constructor case $p \equiv {acc}_{a} (h_{R})$ , the outer induction hypothesis is $I_{R} : \prod_{a^{'} : A} a^{'} R a \to \prod_{b^{'} : B} {Acc}_{Lex (R, S)} (a^{'}, b^{'}) .$ Fix $b : B$ and apply accessibility induction to $w_{S} b$ with the inner motive $J (b, q) : = {Acc}_{Lex (R, S)} (a, b) .$ In the case $q \equiv {acc}_{b} (h_{S})$ , the inner induction hypothesis is $I_{S} : \prod_{b^{'} : B} b^{'} S b \to {Acc}_{Lex (R, S)} (a, b^{'}) .$ Construct ${acc}_{(a, b)} (k)$ . For a predecessor $(a^{'}, b^{'})$ , eliminate its witness in the sum of definition 82.15. A left witness $r : a^{'} R a$ is sent to $I_{R} a^{'} r b^{'}$ . A right witness $(e, s) : {Id}_{A} (a, a^{'}) \times (b^{'} S b)$ is sent to ${tr}_{e}^{x . {Acc}_{Lex (R, S)} (x, b^{'})} (I_{S} b^{'} s) : {Acc}_{Lex (R, S)} (a^{'}, b^{'}) .$ These clauses define $k$ . The inner and outer inductions therefore prove accessibility of every pair. ◻

Exercise 82.2 ¶

★★☆ Let $R$ and $S$ be relations on $A$ and $B$ with measures $μ : A \to N$ and $ν : B \to N$ . Prove that the relation which decreases both coordinates strictly is well founded using the measure $(a, b) \mapsto μ (a) + ν (b)$ . Explain why this relation is smaller than the lexicographic relation of theorem 82.16.

Referenced from 3 locations

Euclid’s algorithm as a well-founded program

Write $a rem b$ for natural-number remainder. We use the following division result, whose proof uses the recursor of definition 82.6.

Lemma 82.17 — Natural arithmetic interface ¶

Define truncated subtraction by $\begin{aligned} a \dot{-} 0 & \equiv a, & 0 \dot{-} suc (b) & \equiv 0, & suc (a) \dot{-} suc (b) & \equiv a \dot{-} b . \end{aligned}$ For all $a, b, q, c, r : N$ :

the alternative $a < b$ or $b \leq a$ is decidable;
if $b \leq a$ , then $a = b + (a \dot{-} b)$ , and if also $b > 0$ , then $a \dot{-} b < a$ ;
writing $c ∣ n$ for $\sum_{k : N} {Id}_{N} (n, k c)$ , the implications $\begin{aligned} c ∣ b \land c ∣ r & ⟹ c ∣ (q b + r), \\ c ∣ a \land c ∣ b \land a = q b + r & ⟹ c ∣ r \end{aligned}$ hold.

Referenced from 4 locations

Well-Founded Recursion

Proof of Lemma 82.17 — Natural arithmetic interface

Proof. For decidability, recurse simultaneously on $a$ and $b$ . At $(0, 0)$ choose $b \leq a$ ; at $(0, suc (b^{'}))$ choose $a < b$ ; and at $(suc (a^{'}), 0)$ choose $b \leq a$ . At $(suc (a^{'}), suc (b^{'}))$ , recurse on $(a^{'}, b^{'})$ and apply the successor constructor to the selected order proof. These four clauses return a tagged decision in every case.

For the monus identity, induct on the proof of $b \leq a$ , exposing $a$ and $b$ together. The zero case reduces to $a = 0 + a$ . The successor case reduces $suc (a^{'}) = suc (b^{'}) + (suc (a^{'}) \dot{-} suc (b^{'}))$ to the induction hypothesis $a^{'} = b^{'} + (a^{'} \dot{-} b^{'})$ . If $b > 0$ , write $b = suc (b^{'})$ . The identity has the form $a = suc (b^{'}) + r$ with $r = a \dot{-} b$ ; induction on $b^{'}$ constructs $r < suc (b^{'}) + r = a$ . This proves the strict decrease without appealing to the earlier monus exercise.

For divisibility, first establish by natural-number induction the equations $\begin{aligned} x + y & = y + x, & x y & = y x, & x (y z) & = (x y) z, \\ q (k c) & = (q k) c, \\ (x c) + (y c) & = (x + y) c, \\ (x + y) \dot{-} x & = y, \\ (x c) \dot{-} (y c) & = (x \dot{-} y) c . \end{aligned}$ The addition and multiplication laws use the zero and successor equations in the corresponding induction. For the fourth law, induct on $x$ ; the successor case first rewrites $suc (x) + y = suc (x + y)$ and then applies the successor–successor monus clause. For the last equation, use multiplication commutativity, proved by the same successor induction, to put $c$ first and induct on the pair $(x, y)$ . The successor–successor case cancels one common summand $c$ using $(u + c) \dot{-} (v + c) = u \dot{-} v$ , whose proof is induction on $c$ ; the two zero cases are the defining monus equations. Thus these calculations cover all constructor pairs.

If $b = k c$ and $r = l c$ , associativity and the first two equations give $q b + r = q (k c) + l c = (q k + l) c,$ so $q k + l$ is a divisibility witness. Conversely, suppose $a = k c$ , $b = l c$ , and $a = q b + r$ . Substitution into the fourth displayed law gives $a \dot{-} q b = r$ . Therefore $r = (k c) \dot{-} ((q l) c) = (k \dot{-} q l) c,$ so $k \dot{-} q l$ is the required witness. ◻

Lemma 82.18 — Natural-number division ¶

There are functions $div, rem : N \to N \to N$ such that, for every $a, b : N$ and $u : b > 0$ , $\begin{matrix} (D i v) & a = div (a, b) b + rem (a, b), rem (a, b) < b, \end{matrix}$ and both functions are computed, for fixed positive $b$ , by well-founded recursion on $a$ . Equivalently, the construction gives the two leading components of $\begin{aligned} DivSpec (d, r) & : = \prod_{a, b : N} b > 0 \to \\ ({Id}_{N} (a, d (a, b) b + r (a, b)) \times (r (a, b) < b)) . \end{aligned}$ The resulting package inhabits $\sum_{d : N \to N \to N} \sum_{r : N \to N \to N} DivSpec (d, r) .$

Referenced from 5 locations

Well-Founded Recursion

Proof of Lemma 82.18 — Natural-number division

Proof. For $b \equiv 0$ , define $div (a, b) : = 0$ and $rem (a, b) : = a$ ; the specification has no inhabitant $u : b > 0$ to check. For $b \equiv suc (b_{0})$ , use its constructor proof of $b > 0$ and recurse on the measure $a$ . If $a < b$ , return $q : = 0$ and $r : = a$ . Otherwise $b \leq a$ ; by lemma 82.17, $a = b + (a \dot{-} b)$ , and positivity of $b$ gives $a \dot{-} b < a$ . The recursive result at $a \dot{-} b$ has the form $a \dot{-} b = q^{'} b + r, r < b .$ Return $q : = suc (q^{'})$ and the same $r$ . Then $\begin{aligned} a & \overset{l e m m a 82.17}{=} b + (a \dot{-} b) \\ \overset{r e c u r s i v e e q u a t i o n}{=} b + (q^{'} b + r) \\ \overset{s u c c e s s o r m u l t i p l i c a t i o n a n d a s s o c i a t i v i t y}{=} suc (q^{'}) b + r, \end{aligned}$ while $r < b$ is unchanged. The recursive call is admitted by theorem 82.14 because its displayed measure is strictly smaller. Define $div (a, b) : = q$ and $rem (a, b) : = r$ from the two components returned by this recursion. The decidable cases cover all naturals, completing both functions and their specification. ◻

From this point onward, $a rem b : = rem (a, b)$ and $a div b : = div (a, b)$ denote the two functions constructed by lemma 82.18.

The strict inequality in (Div), rather than the equation itself, is the termination certificate.

Definition 82.19 — Euclidean step ¶

Put $X : = N \times N$ and $(a^{'}, b^{'}) R_{E} (a, b) ⟺ b^{'} < b .$ This is the measure relation for $μ (a, b) : = b$ , so it is well founded by theorem 82.14. For $k : \prod_{x^{'} : X} x^{'} R_{E} x \to N$ define $E ((a, b), k) : = {\begin{cases} a, & b = 0, \\ k ((b, a rem b), r_{a, b, u}), & u : b > 0, \end{cases}$ where $r_{a, b, u} : a rem b < b$ is the second component of lemma 82.18 at $a, b, u$ . For any accessibility certificate $p$ put $\gcd_{p} (a, b) : = {wfrec}_{R_{E}, λ x . N} (E, (a, b), p) .$ Fix the well-foundedness witness $w_{E}$ obtained from theorem 82.14 and define $\gcd (a, b) : = \gcd_{w_{E} (a, b)} (a, b) .$ Certificate independence from proposition 82.7 identifies this choice propositionally with every $\gcd_{p} (a, b)$ .

Referenced from 3 locations

Well-Founded Recursion

The distinction between proof-indexed computation and the fixed total function is visible before any arithmetic unfolds. If $z : {Acc}_{R_{E}} (a, b)$ is a variable, then ${wfrec}_{R_{E}, λ x . N} (E, (a, b), z)$ is stuck: the certificate position is neutral, so the left side of (WF-β) does not match. In particular, the same term with $z : = w_{E} (a, b)$ need not reduce when the chosen well-foundedness proof is opaque.

Every recursive argument and its evidence are visible in the second branch: $(b, a rem b) R_{E} (a, b) because a rem b < b .$ Neither component needs to be a constructor field of $(a, b)$ .

Theorem 82.20 — Euclid equations and termination ¶

For all $a, b : N$ , Euclid’s program is total and satisfies $\gcd (a, 0) = a, b > 0 ⟹ \gcd (a, b) = \gcd (b, a rem b) .$ The equalities are identifications independent of the chosen accessibility certificates. At the proof-indexed function $\gcd_{p}$ , the zero equation is judgmental when $p$ is a constructor certificate and the zero test reduces. The positive equation is judgmental when, in addition, $b \equiv suc (b_{0})$ is a numeral successor, so that its branch test reduces. The equations for the fixed $\gcd$ remain identifications when $w_{E} (a, b)$ is opaque.

Referenced from 3 locations

Well-Founded Recursion

Proof of Theorem 82.20 — Euclid equations and termination

Proof. By well-foundedness of $R_{E}$ , every pair is accessible, so definition 82.6 gives a result in $N$ . Inspect the decidable test $b = 0$ . In the zero branch, (WF-β) and definition 82.19 return $a$ . In the positive branch, lemma 82.18 gives $r_{a, b, u}$ , so the recursive-results function may be applied at $(b, a rem b)$ . Equation (WF-β) then gives the second equation. Changing the outer or recursive accessibility certificate preserves the result by proposition 82.7; the Euclidean step is pointwise extensional because each branch either ignores $k$ or applies it once at the same pair and order proof. ◻

Example 82.21 — A complete Euclidean calculation ¶

The positive divisors in this calculation provide the displayed decrease at each recursive call: $\begin{aligned} \gcd (48, 18) & \overset{48 rem 18 = 12 < 18}{=} \gcd (18, 12) \\ \overset{18 rem 12 = 6 < 12}{=} \gcd (12, 6) \\ \overset{12 rem 6 = 0 < 6}{=} \gcd (6, 0) \\ \overset{t h e o r e m 82.20}{=} 6. \end{aligned}$ The measure sequence is $18 > 12 > 6 > 0$ . The calculation ends because this is a descending sequence of natural numbers, not because either original input is peeled one constructor at a time.

Referenced from 5 locations

Theorem 82.22 — Common-divisor specification ¶

For all $a, b : N$ , the result $d : = \gcd (a, b)$ divides both $a$ and $b$ . Every $c : N$ dividing both $a$ and $b$ also divides $d$ .

Referenced from 2 locations

Well-Founded Recursion

Proof of Theorem 82.22 — Common-divisor specification

Proof. Use accessibility induction on $(a, b)$ for $R_{E}$ . If $b = 0$ , then $d = a$ : it divides $a$ , it divides $0$ , and every common divisor divides $a = d$ .

Suppose $b > 0$ and write $a = q b + r$ with $r = a rem b < b$ . The induction hypothesis at $(b, r)$ says $d : = \gcd (b, r)$ is greatest among common divisors of $b$ and $r$ . If $d$ divides $b$ and $r$ , the first divisibility implication of lemma 82.17 gives $d ∣ (q b + r) = a$ . Conversely, if $c$ divides $a$ and $b$ , the second implication gives $c ∣ r$ from $a = q b + r$ . Thus the common divisors of $(a, b)$ are exactly the common divisors of $(b, r)$ . The second equation of theorem 82.20 identifies their computed greatest common divisors. ◻

Exercise 82.3 ¶

★☆☆ Calculate $\gcd (1071, 462)$ to a numeral. Put the remainder and strict decrease on every equality sign, and list the complete second-coordinate measure sequence.

Referenced from 3 locations

Exercise 82.4 ¶

★★☆ Let $partition (p, x s)$ return lists $l, r$ such that every element of $l$ is at most $p$ , every element of $r$ is greater than $p$ , and $| l | + | r | = | x s |$ . Give the two strict inequalities needed to define quicksort by the measure $| x s |$ on the input $p :: x s$ . State why the partition equation alone does not prove either strict inequality if the pivot is not removed.

Referenced from 3 locations

A special-purpose domain predicate

The generic accessibility predicate mentions every predecessor admitted by a relation. A particular recursive specification often needs fewer calls. The Bove–Capretta construction records exactly those calls in an inductive domain predicate and then recurses structurally on its proof.

Fix a positive divisor $d : N$ with $u : d > 0$ . Consider the equations $\begin{matrix} (Q u o t) & q_{d} (n) = {\begin{cases} 0 & n < d, \\ suc (q_{d} (n - d)) & d \leq n . \end{cases} \end{matrix}$ The recursive input $n - d$ is not a constructor field of $n$ . Instead of choosing a general relation, read the call graph directly from this equation.

Definition 82.23 — Division domain ¶

The family ${Dom}_{d} : N \to U_{i}$ has the two constructors $\begin{aligned} below & : \prod_{n : N} n < d \to {Dom}_{d} (n), \\ subtract & : \prod_{n : N} d \leq n \to {Dom}_{d} (n - d) \to {Dom}_{d} (n) . \end{aligned}$ The second constructor stores exactly the domain proof required by the sole recursive call in (Quot).

Referenced from 2 locations

Well-Founded Recursion

Definition 82.24 — Structural quotient on a domain proof ¶

Define $q_{d}^{♯} (n, p) : N$ by structural recursion on $p : {Dom}_{d} (n)$ : $\begin{aligned} q_{d}^{♯} (n, below (v)) & : = 0, \\ q_{d}^{♯} (n, subtract (v, p^{'})) & : = suc (q_{d}^{♯} (n - d, p^{'})) . \end{aligned}$ The recursive proof $p^{'}$ is a constructor field, so this definition satisfies the structural-call invariant of definition 82.1.

Referenced from 2 locations

Well-Founded Recursion

The remaining obligation is to show that every intended input inhabits the domain. Positivity of $d$ gives the decrease needed for that proof.

Theorem 82.25 — The division domain is total ¶

For every $n : N$ , the type ${Dom}_{d} (n)$ is inhabited.

Referenced from 3 locations

Well-Founded Recursion

Proof of Theorem 82.25 — The division domain is total

Proof. Use measure induction on $n$ . Decide $n < d$ . In the positive case, $below (n, v)$ has the required type. Otherwise obtain $w : d \leq n$ . Since $u : d > 0$ , natural arithmetic gives $n - d < n$ . The induction hypothesis at that strict decrease gives $p^{'} : {Dom}_{d} (n - d)$ . Hence $subtract (n, w, p^{'}) : {Dom}_{d} (n)$ . ◻

Choose the proof $p_{n}$ supplied by theorem 82.25 and put $q_{d} (n) : = q_{d}^{♯} (n, p_{n})$ . Certificate independence is proved by induction on the first domain proof: the branch decision at $n$ determines which constructor can inhabit the second proof, and the induction hypothesis identifies the recursive results. Consequently $q_{d}$ satisfies (Quot) propositionally even when $p_{n}$ is opaque.

This construction is special-purpose accessibility. The domain proof is the accessibility tree for the recursive calls generated by one equation; it does not replace the generic relation-indexed recursor. Bove and Capretta develop the same separation between a recursive equation, its domain predicate, structural recursion on domain evidence, and totality of that domain [BC05].

Suggested first pass.

None of these problems is a prerequisite. Begin with exercise 82.5, then complete exercise 82.7.

Exercise 82.5 ¶

★★☆ Reconstruct theorem 82.5 from the sole constructor of ${Acc}_{R}$ . Instantiate it with the motive $P (a) : = N$ and derive (WF-β) with the types of $h$ , $k$ , and every recursive call visible.

Referenced from 4 locations

Exercise 82.6 ¶

★★★ Define a three-coordinate lexicographic relation on $A \times B \times C$ . Assuming well-founded relations on the three factors, prove its well-foundedness by three nested accessibility inductions. In each predecessor case state which induction hypothesis decreases and which coordinates remain unrestricted.

Referenced from 3 locations

A proof-carrying call checker.

Exercise 82.7 ¶

★★★ Practical project.well-founded-call-checker Implement in Kappa a checker for annotations of the form “recursive call $x^{'}$ has natural measure smaller than $x$ ”. Maintain the invariant that every accepted call carries a checked proof of $μ (x^{'}) < μ (x)$ ; do not accept a Boolean comparison without its proof. Run it on the calls of example 82.21, which must produce the measure trace $18, 12, 6, 0$ , and on the mutation $\gcd (a, b) \mapsto \gcd (b, a)$ , which must be rejected at the first call from $(48, 18)$ . The acceptance test passes exactly when all three Euclidean calls are accepted with those measures and the mutation is rejected at $(48, 18)$ with the nondecrease $48 ≮ 18$ .

Referenced from 5 locations

Sources. The accessibility presentation and its recursion principle follow Paulson’s construction [Pau86]; the HoTT Book, §10.3, gives the same constructor and derives well-founded recursion [Uni13]. Abel and Pientka treat a stronger sized calculus [AP16]; none of its normalization theorem is used for $T_{rec}$ here.