Recursive definitions are internalizable

A definition by recursion produces a table: an index, and for each index a value. The table is a family in the meta-language, and the question this chapter answers is when it is a set of L. Everything later that speaks about a recursively-defined notion inside the object language needs an answer, because a formula can only name a set.

The answer is short, and the reason it is short is worth stating first. The hard version of this question asks for a table to be definable inside a stage, where what a formula means is not what it means outside, so the certificate has to be absolute, so every clause of it has to be Δ₀ and every constant of it has to be bounded by the stage. That is a heavy discipline and it is the shape the question usually takes.

It is not the shape it takes here, because the previous chapters paid for the general case once. Replacement in L holds for formulas of any complexity, and its formulas are read at the class model, where a formula means what it means. So a recursion whose graph is expressible at all, at any complexity, has its table in L: the table is the replacement image, and there is nothing else to prove.

What is left is exactly what should be left. The graph must be expressible, and the recursion must be single-valued. Neither is generic; both are the mathematics of whatever is being defined.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Truth
open import Base.Classical using ( LEM )

module L.Recursion {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; ∃̇_ )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset-mono )
open import L.Ordinal {ℓ} using ( boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.Prelude using ( isPropIsContr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

What a recursion has to supply

Three things, and the record names them so that an instance is a filled form rather than a re-run of an argument.

The domain is the index set, and it is an element of the model, so the indices are sets of L and the whole index is one set. The graph is a formula in two variables, the value first and the index second, in the order the model's replacement field states. Its constants may be any elements of L, so a recursion that reads an already-internalized table names it here, and there is no further condition on it: no complexity bound, no bound on where its constants live.

Single-valuedness is what turns a relation into a definition. It is stated as contractibility rather than as existence plus uniqueness, which is the same thing and is what the field consumes. Stated this way it also is the value function: the centre is the value, and the rest of the chapter reads it off.

record Recursion : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom   : S
    graph : Formula S 
    funct : (x : S) → ⟨ x ∈ˢ dom ⟩
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)

What a graph may not do

One line, stated because it decides a design question that otherwise gets decided by wasted work. Satisfaction is read at the model, so an existential quantifier of the object language ranges over the model: to satisfy one is to produce an element of L, not merely a set.

The consequence is a rule about what may appear in a graph. A graph may say "there is a y such that ..." only when the y it needs is already known to be an element of L. In particular a graph may not describe an object by asserting the existence of the very object being described: that describes nothing, because discharging the assertion is exactly the problem it was meant to solve. A table of values may therefore not be reached by writing "there is a table satisfying the recursion equations"; it has to be reached by naming something smaller that is already in hand, and letting this chapter collect the pieces.

witnessInModel : ∀ {n} (γ : S ^ n) (φ : Formula S (suc n))
               → ⟨ γ ⊨ (∃̇ φ) ⟩ → ∥ (Σ[ x ∈ S ] ⟨ (x ∷ γ) ⊨ φ ⟩) ∥₁
witnessInModel γ φ h = h

Of the three, the domain is the one that looks like it might be hard, and it is not. An index set is usually given as a family in the meta-language, indexed by some type of the ambient size: the closed formulas, the pairs of them, whatever the recursion is over. Such a family does not have to be collected into a set at all. It only has to be contained in one, and any small family of elements of L is contained in a single stage, by the bounding lemma applied to their earliest stages. A stage is a set of L, so it serves as the domain.

The recursion is then defined on more than its intended indices, and that costs nothing: the graph is made total by giving the uninteresting elements a default value, and the intended table is recovered by separation, which is now available for arbitrary formulas. So the obligation "the index set is a set of L", which an instance would otherwise discharge by internalizing its own syntax, is discharged here once for every instance at once.

smallDom : (X : Type ℓ) (f : X → S) → Σ[ d ∈ S ] ((x : X) → ⟨ f x ∈ˢ d ⟩)
smallDom X f = LsetS β oβ , mem
  where
  b = boundingOrd X (λ x → stage (fst (f x)) (f x .snd))
        (λ x → stage-ord (fst (f x)) (f x .snd))
  β = b .fst
  oβ : IsOrd β
  oβ = b .snd .fst
  mem : (x : X) → ⟨ f x ∈ˢ LsetS β oβ ⟩
  mem x = Lset-mono {α = β} {β = stage (fst (f x)) (f x .snd)} (b .snd .snd x)
            (stage-mem (fst (f x)) (f x .snd))

The table

The table is the replacement image, so it is an element of L by construction rather than by a theorem, and its membership specification is the field's own output. The two directions of that specification are what instances use: a value at an index is in the table, and a member of the table is a value at some index.

The value function comes off the single-valuedness, together with the two facts an instance wants about it: it satisfies the graph, and it is the only thing that does. Uniqueness is what lets an instance identify the value it computed by hand with the one the table records.

module Of (R : Recursion) where
  open Recursion R public

  private
    Image : S → Ω
    Image y = ⋁ S (λ x → (x ∈ˢ dom) ⊓ ((y ∷ x ∷ []) ⊨ graph))

    r : SetOf Image
    r = hasReplacementL dom graph funct .fst

  table : S
  table = r .fst

  table-mem : (y : S) → (y ∈ˢ table) ≡ Image y
  table-mem = r .snd

  table-in : (x y : S) → ⟨ x ∈ˢ dom ⟩ → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
           → ⟨ y ∈ˢ table ⟩
  table-in x y x∈ h = subst ⟨_⟩ (sym (table-mem y)) ∣ x , (x∈ , h) ∣₁

  table-out : (y : S) → ⟨ y ∈ˢ table ⟩ → ⟨ Image y ⟩
  table-out y h = subst ⟨_⟩ (table-mem y) h

  val : (x : S) → ⟨ x ∈ˢ dom ⟩ → S
  val x x∈ = funct x x∈ .fst .fst

  val-graph : (x : S) (x∈ : ⟨ x ∈ˢ dom ⟩)
            → ⟨ (val x x∈ ∷ x ∷ []) ⊨ graph ⟩
  val-graph x x∈ = funct x x∈ .fst .snd

  val-uniq : (x : S) (x∈ : ⟨ x ∈ˢ dom ⟩) (y : S)
           → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → val x x∈ ≡ y
  val-uniq x x∈ y h = cong fst (funct x x∈ .snd (y , h))

  val∈table : (x : S) (x∈ : ⟨ x ∈ˢ dom ⟩) → ⟨ val x x∈ ∈ˢ table ⟩
  val∈table x x∈ = table-in x (val x x∈) x∈ (val-graph x x∈)

When the value function cannot be written down

The form below asks an instance for a function on the whole model. That is the right thing to ask when the instance has one, and the wrong thing when its indices are encoded: a recursion over coded syntax knows what to do at a code, and to say what it does at an arbitrary element of the model it would first have to decide whether that element is a code and, if so, recover the syntax it encodes. Nothing in the recursion needs that, and paying for it would be paying for a decoding the instance never uses.

Single-valuedness does not need it either, and the reason is worth naming. Contractibility is a proposition. So an instance may decide by cases, and may take apart a truncated witness, on the way to proving it: what has to be produced is a value, and it only has to be produced merely. The lemma below is that observation, and it is what a recursion over an encoded index uses in place of the form below.

mereFunct : (graph : Formula S ) (x : S)
          → ∥ (Σ[ y ∈ S ] (⟨ (y ∷ x ∷ []) ⊨ graph ⟩
                          × ((y' : S) → ⟨ (y' ∷ x ∷ []) ⊨ graph ⟩ → y' ≡ y))) ∥₁
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)
mereFunct graph x = PT.rec isPropIsContr
  (λ { (y , (hy , uniq)) → (y , hy)
     , (λ { (y' , hy') → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph))
                           (sym (uniq y' hy')) }) })

Defining a function, rather than a relation

Asking an instance for single-valuedness is asking the wrong thing, because an instance never has a relation to start with. It has a function, written in the meta-language by ordinary recursion, and what it wants is that function's table. The recursion itself is Agda's business, not the object language's: the step, the well-founded descent, the pattern match on the constructors, all of that happens outside and none of it needs internalizing. Only the graph does.

So the form to fill is a function together with a formula that defines it, and defining it is two implications. One says the formula holds of the function's own value, the other that nothing else satisfies it. Single-valuedness then comes for free, because a type of things equal to a given one is contractible, and that is the whole derivation.

This is where the chapter's title is earned. A recursive definition is internalizable when its graph is expressible, and nothing about the recursion's shape, its depth, its order of descent, or the complexity of its clauses appears in the condition.

record Definition : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom     : S
    fn      : S → S
    graph   : Formula S 
    defines : (x : S) → ⟨ x ∈ˢ dom ⟩ → ⟨ (fn x ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) → ⟨ x ∈ˢ dom ⟩ → (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x

asRecursion : Definition → Recursion
asRecursion D = record
  { dom   = D.dom
  ; graph = D.graph
  ; funct = λ x x∈ → (D.fn x , D.defines x x∈)
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ D.graph))
                            (sym (D.only x x∈ y h)) } }
  where module D = Definition D

And the theorem in the form an instance consumes: the image of a definable function on a set of L is a set of L, with its two membership directions. The backward one is truncated, because a member of the image is the value at some index and the index is not recoverable; every consumer so far only needs it truncated.

module Image (D : Definition) where
  open Definition D public
  private
    module R = Of (asRecursion D)

  table : S
  table = R.table

  fn∈table : (x : S) → ⟨ x ∈ˢ dom ⟩ → ⟨ fn x ∈ˢ table ⟩
  fn∈table x x∈ = R.table-in x (fn x) x∈ (defines x x∈)

  table→fn : (y : S) → ⟨ y ∈ˢ table ⟩
           → ∥ (Σ[ x ∈ S ] (⟨ x ∈ˢ dom ⟩ × (y ≡ fn x))) ∥₁
  table→fn y h = PT.map (λ { (x , (x∈ , sat)) → x , (x∈ , only x x∈ y sat) })
    (R.table-out y h)

What this does and does not say

It says: a function on a set of L whose graph is expressible has its table in L. Every recursion whose values are determined by a formula is covered, whatever the formula's complexity and wherever its constants live, and the recursion itself stays in the meta-language where it was written.

It does not say that any particular recursion has such a formula. Writing the graph of a recursion in the object language is the work, and it is the same work whether or not this chapter exists; what this chapter removes is the second job that usually rides along with it, of making that formula bounded and its constants stage-local so that a stage can read it. That job is gone, and it was the larger of the two.

It also does not leave the domain as an obligation. smallDom discharges it for every instance at once: a small family of elements of L is contained in a stage, and a stage is a set of L. What an instance supplies is that its indices are elements of L, one at a time, which for coded syntax is pairing and the numerals.

Recap

Definition is the form an instance fills when it has a function on the whole model to offer: a domain in L, that function, and a formula that defines its graph, in the two directions. An instance whose indices are encoded has no such function without a decoder it does not otherwise need, and fills

Recursion directly through mereFunct instead, which is sound because contractibility is a proposition. smallDom fills the domain for any small family of elements of L, and single-valuedness is derived, so the defining formula and its adequacy are the entire obligation. Image reads off the table and its two membership directions.

The chapter is a wrapper around hasReplacementL, and that is the point. The general-formula comprehension fields were the expensive thing; once they are paid, internalizing a recursion is not a theorem but a corollary, and the per-clause absoluteness discipline that the bounded setting forces never has to be entered.