Partiality and General Recursion in Dependent Type Theory

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

Suppose every type admitted $${\mathsf{fix}}_A:(A\to A)\to A,{\mathsf{fix}}_A(f)\equiv f({\mathsf{fix}}_A(f)).$$ At $A=\mathrm{\perp }$, choose $f=\lambda x.x$. Then ${\mathsf{fix}}_{\mathrm{\perp }}(f):\mathrm{\perp }$. An unrestricted proof-level fixpoint makes the empty type inhabited before any program is run. General recursion must therefore return a computation that may fail to produce an $A$, rather than an inhabitant of $A$ itself.

Partial elements record time without promising a result

The type $A^{\nu }$ is not $A+\mathbf{1}$. Case analysis on $A+\mathbf{1}$ decides whether a value is present. Constructively, an arbitrary partial element need not satisfy $$(\mathrm{\exists }a.x\Downarrow a)\vee x\Uparrow .$$ Every finite observation of $\mathsf{never}$ returns $\mathsf{later}$, but no finite observation proves that all later observations do so.

Proof of Lemma 105.3 — Delay laws

Proof. First prove determinacy of convergence: if $x\Downarrow a$ and $x\Downarrow b$, induction on the first derivation and inversion of the second give $a=b$. The return case inverts both derivations; the step case removes one Conv-Step from each and applies the induction hypothesis.

For the first formula, inversion of Conv-Step gives $▹x\Downarrow a\Rightarrow x\Downarrow a$, and Conv-Step gives the converse. For the second, inversion of Conv-Return shows that $⟨a⟩\Downarrow b$ exactly when $a=b$. If $x\Downarrow a$, determinacy gives $x\Downarrow b⟺a=b$; substitute both facts in definition 105.2. The reverse implication specializes equality at $a$ and uses Conv-Return. The third formula applies the first inversion in both directions. Reflexivity, symmetry, and transitivity hold pointwise because logical equivalence has those three properties. ◻

Sequencing partial computations

The input step is retained. A tempting definition $f^{\ast }(▹x)=f^{\ast }(x)$ is unguarded: computing its first constructor may require inspecting infinitely many input steps. Guarding the recursive call is forced by productivity.

Proof of Lemma 105.5 — Bind convergence

Proof. For the forward implication, induct on the convergence derivation. If $x=⟨a⟩$, choose $a$; Conv-Return proves the first conjunct and the premise proves the second. If $x=▹x^{\prime }$, inversion of the bind equation changes the final Conv-Step premise to $(x^{\prime }\gg =f)\Downarrow b$. The induction hypothesis supplies $a$, and Conv-Step gives $x\Downarrow a$.

For the reverse implication, induct on the derivation of $x\Downarrow a$. The return case reduces bind to $f(a)$. In the step case, the induction hypothesis gives $(x^{\prime }\gg =f)\Downarrow b$; one use of Conv-Step and the second bind equation gives $(▹x^{\prime }\gg =f)\Downarrow b$. ◻

Proof of Lemma 105.7 — Extensional return and bind

Proof. Reflexivity, symmetry, and transitivity of ${\mathrm{Eq}}_{TA}$ hold pointwise because logical equivalence has those properties. Moreover, $$\begin{array}{}\text{(}R\text{)}& {\mathrm{Conv}}_A(⟨a⟩,c)⟺{\mathrm{Eq}}_A(a,c).\end{array}$$ If ${\mathrm{Eq}}_A(a,a^{\prime })$, transitivity and symmetry of ${\mathrm{Eq}}_A$ make the right side of (R) equivalent with ${\mathrm{Eq}}_A(a^{\prime },c)$. Thus ${\eta }_A$ preserves the setoid relations, proving clause 1.

For the forward implication of (K), choose $b_0:|B|$ with $$f^{\ast }(x)\Downarrow b_0,{\mathrm{Eq}}_B(b_0,b).$$ By lemma 105.5, choose $a_0:|A|$ such that $x\Downarrow a_0$ and $f(a_0)\Downarrow b_0$. Reflexivity gives ${\mathrm{Conv}}_A(x,a_0)$, while the second displayed relation gives ${\mathrm{Conv}}_B(f(a_0),b)$.

Conversely, choose $a:|A|$ from the right side of (K), then choose $a_0:|A|$ such that $$x\Downarrow a_0,{\mathrm{Eq}}_A(a_0,a).$$ Because $f$ is a Kleisli arrow, ${\mathrm{Eq}}_{TB}(f(a_0),f(a))$. Hence ${\mathrm{Conv}}_B(f(a),b)$ gives ${\mathrm{Conv}}_B(f(a_0),b)$. Choose $b_0:|B|$ with $f(a_0)\Downarrow b_0$ and ${\mathrm{Eq}}_B(b_0,b)$. Bind convergence gives $f^{\ast }(x)\Downarrow b_0$, which proves the left side of (K).

If ${\mathrm{Eq}}_{TA}(x,y)$, formula (K) has equivalent right sides for $x$ and $y$. Thus $f^{\ast }$ preserves the lifted relation. If also $f(a)$ and $g(a)$ are related for every $a$, replace both the first conjunct by the equivalence between $x$ and $y$ and the second by the equivalence between $f(a)$ and $g(a)$ in (K). The resulting equivalence for every $b:|B|$ is clause 3. ◻

Proof of Theorem 105.8 — Partiality Kleisli triple

Proof. All displayed maps are setoid maps by lemma 105.7. For the first law, formula (K) and (R) give, for every $a:|A|$, The reverse direction of the second step chooses $b=a$; the forward direction uses the witness for ${\mathrm{Conv}}_A(x,b)$ and transitivity of ${\mathrm{Eq}}_A$. Hence ${\eta }_A^{\ast }$ and ${\mathsf{id}}_{TA}$ are pointwise related.

The return equation in definition 105.4 gives $f^{\ast }({\eta }_A(a))=f(a)$, so reflexivity of ${\mathrm{Eq}}_{TB}$ proves the second law. For the third, fix $x:|A{|}^{\nu }$ and $c:|C|$. Repeated use of (K) gives the annotated calculation This is pointwise ${\mathrm{Eq}}_{TC}$, as required. ◻

The construction acts on setoids, not only on their carrier types. The extensionality lemma and the three calculations above supply the setoid action and all three Kleisli laws. Equality of maps is pointwise setoid equality, so the proof uses neither functional extensionality nor quotient choice.

A partial recursive program

Fix a decidable predicate $P:\mathsf{Nat}\to \mathsf{Bool}$. Unbounded search from $n$ is defined guardedly by Each recursive call lies below $▹$, so it defines a partial element even when no witness exists.

Proof of Theorem 105.9 — Search adequacy

Proof. For the forward implication, induct on the convergence derivation while unfolding the defining equation at the starting index. If $P(n)$ is true, the computation is $⟨n⟩$; inversion gives $m=n$, and the bounded universal has no instance. If $P(n)$ is false, inversion of Conv-Step gives ${\mathsf{search}}_P(n+1)\Downarrow m$. The induction hypothesis gives $n+1\le m$, $P(m)=\mathsf{true}$, and falsity on $[n+1,m)$; add $P(n)=\mathsf{false}$.

For the reverse implication, induct on $m-n$. At zero, $m=n$ and $P(n)=\mathsf{true}$, so Conv-Return applies. At a successor difference, the bounded premise gives $P(n)=\mathsf{false}$. The induction hypothesis yields convergence from $n+1$, and Conv-Step yields convergence from $n$. ◻

This theorem is partial correctness plus an exact convergence criterion. A total-correctness theorem additionally needs $\mathrm{\exists }m\ge n.P(m)=\mathsf{true}$. Without that premise, $P(k)=\mathsf{false}$ for all $k$ makes every finite observation return $\mathsf{later}$.

The construction scales to partial recursive functions. A partial-recursive presentation of arity $k$ is generated by zero, successor, projections, composition, primitive recursion, and minimization. Recursion on such a presentation $f:{\mathsf{Nat}}^k\rightharpoonup \mathsf{Nat}$ defines a term $f^{\nu }:{\mathsf{Nat}}^k\to {\mathsf{Nat}}^{\nu }$: total base functions are followed by $\eta$, composition uses the strict tuple followed by Kleisli extension, primitive recursion first recurses on the returned natural number and then extends over its partial argument, and minimization tests successive values by a guarded search.

Proof of Theorem 105.10 — Representability of partial-recursive presentations

Proof. Induct on the partial-recursive presentation. The induction hypothesis for each immediate subpresentation is the displayed equivalence at every input and output.

For zero and successor, $f^{\nu }(\overrightarrow{n})$ is respectively $\eta (0)$ and $\eta (n+1)$. Inversion of Conv-Return proves both directions. For the $i$-th projection, the strict tuple forces all inputs; each input is already a returned natural number, so its only convergence is to $n_i$.

Suppose $f=h\circ ⟨g_1,\dots ,g_j⟩$. Repeated use of the Kleisli convergence law (K) gives $$f^{\nu }(\overrightarrow{n})\Downarrow m⟺\mathrm{\exists }{a}_1,\dots ,a_j.\underset{i=1}{\overset{j}{\bigwedge }}{g}_i^{\nu }(\overrightarrow{n})\Downarrow a_i\wedge h^{\nu }(\overrightarrow{a})\Downarrow m.$$ Apply the induction hypotheses for the $g_i$ and $h$. The result is exactly the relational clause for composition.

For primitive recursion, write $$f(\overrightarrow{n},0)=g(\overrightarrow{n}),f(\overrightarrow{n},r+1)=h(\overrightarrow{n},r,f(\overrightarrow{n},r)).$$ The translation defines an auxiliary $f^{\prime \nu }$ by recursion on the returned counter and defines $f^{\nu }$ by Kleisli-extending $f^{\prime \nu }$ over that counter. A subsidiary induction on $r$ proves $$f^{\prime \nu }(\overrightarrow{n},r)\Downarrow m⟺f(\overrightarrow{n},r)=m.$$ The zero case is the induction hypothesis for $g$. The successor case uses (K) once; its witness $a$ is characterized by the subsidiary induction hypothesis, and the remaining convergence is characterized by the induction hypothesis for $h$. A final use of (K) accounts for a partial counter and yields the required equivalence.

For minimization, suppose $f(\overrightarrow{n})=\mu r.g(\overrightarrow{n},r)=0$. Define the guarded search ${\mathsf{least}}_g^{\nu }(\overrightarrow{n},r)$ by first evaluating $g^{\nu }(\overrightarrow{n},r)$; a returned zero yields $\eta (r)$, and a returned successor takes one $▹$-step before searching from $r+1$. The search lemma is proved by the two inductions used for theorem 105.9: forward, invert the finite convergence derivation; backward, induct on $m-r$. At every test, the induction hypothesis for $g$ converts evaluation of $g^{\nu }$ into the graph equation for $g$. Taking $r=0$ gives the defining least-witness clause for minimization. These six constructor cases exhaust the presentation grammar and complete the outer induction. ◻

The theorem supplies representability of every partial recursive function, not a decision procedure for convergence.

Fixed points and exact assumptions

For functions $f,g:A\to B^{\nu }$, write $f⊑g$ when every convergence of $f(a)$ is a convergence of $g(a)$. An operator $F:(A\to B^{\nu })\to (A\to B^{\nu })$ is finitary when, for every $f:A\to B^{\nu }$, $a:A$, and $b:B$, a derivation $F(f)(a)\Downarrow b$ supplies a finite list $(a_1,b_1),\dots ,(a_n,b_n)$ such that $f(a_i)\Downarrow b_i$ for every $i$, and every $g:A\to B^{\nu }$ satisfying all $g(a_i)\Downarrow b_i$ also satisfies $F(g)(a)\Downarrow b$.

The fixed point is built by racing the approximants against one another, and the race has to be written down: it is the only construction in the chapter that a reader could not guess, and the choice-freedom claim below depends on its exact shape.

Each recursive call sits under a $▹$, so both definitions are productive. At step $n$ the accumulated element has been raced against $h(0),\dots ,h(n-1)$, so every member of the sequence is eventually entered; that is the exact sense of “fair”. Two consequences of the definition are used below: ${\mathsf{race}}^{\mathrm{\infty }}(h)\Downarrow b$ implies $h(n)\Downarrow b$ for some $n$, because a convergence derivation is finite and its length bounds the index reached; and if $h$ is increasing for $⊑$, the converse holds.

Proof of Theorem 105.12 — Finitary least fixed point

Proof. Let $k_0(a)=\mathsf{never}$ and $k_{n+1}=F(k_n)$, and define $$Y(F)(a):={\mathsf{race}}^{\mathrm{\infty }}(\lambda n.k_n(a)).$$ First, $F$ is monotone: if $f⊑g$ and $F(f)(a)\Downarrow b$, finitarity supplies pairs $(a_i,b_i)$ with $f(a_i)\Downarrow b_i$; each is then a convergence of $g(a_i)$, so its closure clause gives $F(g)(a)\Downarrow b$. Since $k_0⊑k_1$ holds because $\mathsf{never}$ converges to nothing, induction gives $k_n⊑k_{n+1}$, so the sequence is increasing and definition 105.11 gives $$Y(F)(a)\Downarrow b⟺\mathrm{\exists }n.k_n(a)\Downarrow b.$$

If $F(Y(F))(a)\Downarrow b$, finitarity selects finitely many convergences of $Y(F)$. Each appears at some approximant; their maximum index $N$ places them all in $k_N$. Therefore $k_{N+1}(a)=F(k_N)(a)\Downarrow b$, so $Y(F)(a)\Downarrow b$. Conversely, induction on $n$ shows $k_n⊑F(Y(F))$, using monotonicity and $k_n⊑Y(F)$. Thus $F(Y(F)){=}_{\nu }Y(F)$.

If $F(f)⊑f$, induction gives $k_n⊑f$ for every $n$; the displayed convergence characterization yields $Y(F)⊑f$. Finitarity supplies the finite maximum index, while monotonicity moves the approximation chain through $F$.

No countable choice is used, and the reason is now visible. Choice would be needed to turn the family of statements “$k_n(a)$ converges for some $n$” into a function selecting such an $n$. Nothing here does that: ${\mathsf{race}}^{\mathrm{\infty }}$ is a guarded corecursive program that takes the whole sequence as one argument, and the index is not chosen but read off the length of a finite convergence derivation. ◻

Dropping finitarity invalidates the maximum-index step: an output could depend on infinitely many approximants at once. Extensional equality is also substantive; the parallel search need not have the same constructor timing as $F(Y(F))$.

Two programs, five techniques

Two programs are enough to separate the techniques, provided both are written out. Let It is total, but neither recursive call is on an immediate constructor subterm of either argument, so a structural checker rejects it. ${\mathsf{search}}_P$ of section 105.3 is genuinely partial. Take each program through the two definitional techniques in turn, and write down what is actually accepted.

Accessibility, for the total program.

Well-foundedness is expressed positively by the accessibility predicate with $\mathsf{wf}A(\prec ):=\mathrm{\forall }a:A.\mathsf{Acc}A(\prec )a$. Its eliminator is the principle of well-founded recursion computing by $\mathsf{wfr}Pa(\mathsf{acc}ah)e=ea(\mathsf{acc}ah)(\lambda y.\lambda q.\mathsf{wfr}Py(hyq)e)$. To accept ${\mathsf{gcd}}_{\mathsf{sub}}$, instantiate $A:=\mathsf{Nat}\times \mathsf{Nat}$, take and supply two things: a proof $\mathsf{allacc}:\mathsf{wf}(\mathsf{Nat}\times \mathsf{Nat})(\prec )$, which follows from well-foundedness of on $\mathsf{Nat}$ by transporting along $m+n$; and one obligation per recursive call, both of which reduce to and respectively. The result is a total function $\mathsf{Nat}\to \mathsf{Nat}\to \mathsf{Nat}$, and it is a genuine value: ${\mathsf{gcd}}_{\mathsf{sub}}(6,4)$ evaluates to $2$ with no residual proof obligation.

The same definition is accepted in the measure form $$\mathsf{Program}\mathsf{Fixpoint}\mathsf{gcd}(m,n:\mathsf{Nat})\{\mathsf{measure}(m+n)\},$$ which generates the same two obligations and discharges the accessibility proof internally. The boundary is worth recording: the measure form supplies the definition and nothing else. It provides no induction principle for reasoning about the function afterwards, because the elaborated term is not the one the user wrote; the explicit $\mathsf{wfr}$ form keeps $\mathsf{Acc}$ visible and so supports well-founded induction over the same relation.

Accessibility, for the partial program.

The same route fails, and it fails for a stated reason rather than by awkwardness. A well-founded relation for ${\mathsf{search}}_P$ would have to make $n+1\prec n$ whenever $P(n)=\mathsf{false}$. If $P$ is false everywhere, that relation has the infinite descending chain $0\succ 1\succ 2\succ \cdots$, so no inhabitant of $\mathsf{Acc}\mathsf{Nat}(\prec )0$ exists and the first argument of $\mathsf{wfr}$ cannot be supplied. Restricting the domain to inputs below a witness repairs this, but only by assuming $\mathrm{\exists }m\ge n.P(m)=\mathsf{true}$—the very statement the search was meant to decide.

Delay, for both programs.

The delay type accepts both without an obligation, because definition 105.1 makes every recursive call guarded. Define of type $\mathsf{Nat}\to \mathsf{Nat}\to {\mathsf{Nat}}^{\nu }$. Both definitions are accepted, and the difference is in what one can then observe. For the total program the observations converge and the measure argument above turns into a convergence proof: $${\mathsf{observe}}_2({\mathsf{gcd}}^{\nu }(6,4))=\mathsf{later},{\mathsf{observe}}_3({\mathsf{gcd}}^{\nu }(6,4))=\mathsf{done}(2),$$ since the arguments pass through $(6,4)$, $(2,4)$, $(2,2)$, and $(0,2)$, whose sums witness the measure, so ${\mathsf{gcd}}^{\nu }(6,4)={▹}^3⟨2⟩$. For $P(k)$ testing $k^2=2$, by contrast, $${\mathsf{observe}}_k({\mathsf{search}}_P(0))=\mathsf{later}\text{for every }k,$$ and exercise 105.3 shows that no finite $k$ improves on this. The delay type therefore accepts the partial program at the price that its result is a partial element: extracting $\mathsf{Nat}$ from ${\mathsf{Nat}}^{\nu }$ needs a convergence proof, which for ${\mathsf{gcd}}^{\nu }$ is available and for ${\mathsf{search}}_P$ is exactly what does not exist.

Inductive domains, for both programs.

The third technique changes the domain instead of the codomain. Read the recursive equations of a function as the clauses of an inductive predicate that holds exactly where the call tree is finite. For ${\mathsf{gcd}}_{\mathsf{sub}}$ this is and the function is then defined by structural recursion on the extra proof argument, ${\mathsf{gcd}}^{\mathsf{d}}:\mathrm{\forall }mn.\mathsf{Dom}mn\to \mathsf{Nat}$, matching on ${\mathsf{d}}_0$ through ${\mathsf{d}}_3$. For the total program one then proves $\mathrm{\forall }mn.\mathsf{Dom}mn$—by the same measure $m+n$—and recovers the type $\mathsf{Nat}\to \mathsf{Nat}\to \mathsf{Nat}$; evaluation now proceeds by recursion on the domain argument, which costs time the accessibility definition does not. For ${\mathsf{search}}_P$ the same predicate is definable and the same function is definable on it, but $\mathrm{\forall }n.\mathsf{Dom}n$ is not provable, so what one obtains is a partial function one can still compute with and reason about—on exactly the arguments where the predicate is inhabited.

Termination casts and general recursion.

The two remaining techniques do not produce a definition inside the total theory at all. A termination cast asserts the missing obligation rather than discharging it: it accepts ${\mathsf{gcd}}_{\mathsf{sub}}$ at the total type without the measure argument, and it accepts ${\mathsf{search}}_P$ at that type too, which is precisely why the assertion is a trusted input and not a proof. A language with general recursion runs both programs as written: ${\mathsf{gcd}}_{\mathsf{sub}}(6,4)$ prints $2$ and ${\mathsf{search}}_P(0)$ loops. Sjöberg’s calculus makes this respectable by separating the fragment whose terms may appear in types from the fragment that may diverge; the price is that the second fragment’s results are not available as proofs.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 105.4, then complete exercise 105.6.

Exercise 105.4¶

★★☆ Reconstruct lemma 105.5 with every inversion rule named. Use it to prove congruence: if $x{=}_{\nu }y$ and $f(a){=}_{\nu }g(a)$ for every $a$, then $x\gg =f{=}_{\nu }y\gg =g$.

Referenced from 4 locations

• Partiality and General Recursion in Dependent Type Theory
• ch:dependent-partiality: partiality

Exercise 105.5¶

★★★ Define subtraction-based gcd as a delayed computation. Prove that the measure $m+n$ decreases in every recursive branch and derive convergence. Then state the total value extracted from the convergence proof. Compare the accepted definition with one using an accessibility argument.

Referenced from 3 locations

• Partiality and General Recursion in Dependent Type Theory
• ch:dependent-partiality: partiality

Exercise 105.6¶

★★★ Practical project.partiality-fuel-observer Implement in Kappa a finite observer for return, step, bind, subtraction gcd, and unbounded search represented by a step function. Maintain the invariant that one unit of fuel removes at most one $\mathsf{step}$. On gcd-6-4-20, search-even-from-3-4, and search-never-12, print done 2, done 4, and later, respectively. A mutation that removes a step without consuming fuel must fail an exact step-count oracle. The observer witnesses finite convergence; printing later is not a proof of divergence.

Referenced from 5 locations

• Partiality and General Recursion in Dependent Type Theory
• Erasure, dependent protocols, effects, specifications, and partiality: executable records
• ch:dependent-partiality: fuel-bounded observation