---
title: "Internalizing recursive definitions in L"
module: L.Recursion
lang: en
site: "Bedrock"
description: "Internalizing recursive definitions in L"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 58
canonical: https://bedrock.institute/en/L.Recursion.html
html: L.Recursion.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Recursion.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Full]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Recursion.md, https://bedrock.institute/ja/L.Recursion.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Internalizing recursive definitions in L

A recursive definition may first be given in the metatheory, while its values are later needed as a set of `L`. The replacement theorem supplies this passage. Given a domain in `L` and an object-language formula that has exactly one value at every point of the domain, it forms the set of all those values. The graph formula retains the dependence on the index; the set obtained by replacement is the value range, so equal values arising at different indices occur only once.

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

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

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

The relation defining the values is written as an object-language formula with two free variables, read in the order value then index. Its satisfaction is evaluated in the constructible structure. This lets replacement speak about a relation internal to `L` while the proof of uniqueness remains available in the metatheory.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

The construction also uses the stage structure of `L`. Every constructible set appears at some stage, and the stages containing a family indexed by a type in `Type ℓ` can be bounded by one ordinal. This produces a single set containing the whole family when a convenient domain bound is needed.

```agda
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 )
```

Replacement in `L` applies to an arbitrary formula of the required arity. At this point no additional proof that the formula is Δ₀, or that all of its constants lie in a chosen stage, is required from the caller; those issues were handled in the proof of the general replacement theorem. Paths between dependent pairs with propositional second components will express the uniqueness of values.

```agda
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
```

For a predicate on the constructible carrier, `SetOf` is the type of a set together with a membership specification realizing that predicate. This is the form in which replacement returns the value range. Propositional truncation records an originating index without choosing one.

```agda
open PT using ( ∣_∣₁; ∥_∥₁ )

open hPropStructure 𝒮ʟ

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

The satisfaction notation below is the semantics of formulas in `𝒮ʟ`. The general replacement theorem already connects this semantics with the stagewise argument used to prove replacement; this chapter uses the resulting theorem and does not assume that arbitrary formulas are absolute between `L` and the ambient hierarchy.

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

## What a recursion has to supply

Three things. The **domain** is the index set, itself 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, value first and 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 that table here; there is no complexity bound and no bound on where its constants live.

```agda
record Recursion : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom   : S
    graph : Formula S 2
```

**Functionality** here includes both existence and uniqueness. At every index in the domain, the type of a value paired with a proof that it satisfies the graph must be contractible. Its centre supplies a value, while the contraction proves that every other satisfying value agrees with it.

```agda
    funct : (x : S) → ⟨ x ∈ˢ dom ⟩
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)
```

The lemma `smallDom` gives a common containing set for a family `f : X → S` indexed by `X : Type ℓ`. It does not assert that this containing set is the exact image of `f`, nor does it by itself supply the domain of every recursion. When a larger stage is used as a domain, totality and uniqueness must still be proved at all of its members.

```agda
smallDom : (X : Type ℓ) (f : X → S) → Σ[ d ∈ S ] ((x : X) → ⟨ f x ∈ˢ d ⟩)
smallDom X f = LsetS β oβ , mem
  where
```

The bounding principle is applied to the stages of the values: each `f x` is constructible, so it appears at some stage, and the stages of all the `f x` lie below a single ordinal `β`. That ordinal, certified to be an ordinal, names the stage set used as the domain.

```agda
  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
```

Membership then follows in two steps: each value appears at its own stage, and stages are monotone, so a value below `β` in the stage order is a member of the stage at `β`. Every `f x` is thus an element of the domain set.

```agda
  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 value range

For a recursion `R`, let `Image y` mean that some index `x` belongs to the domain and the graph relates `x` to `y`. The existential is propositionally truncated, so it records only that `y` occurs as a value. Replacement realizes this predicate as a set; it does not construct a set of index-value pairs.

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

  private
    Image : S → hProp (ℓ-suc ℓ)
    Image y = ∃[ x ∶ S ] (x ∈ˢ dom) ⊓ ((y ∷ x ∷ []) ⊨ graph)
```

Applying replacement to the domain, graph, and functionality proof yields a set realizing `Image`. The result contains both the value-range set and the exact proposition describing membership in it.

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

The value range is the first component of this result. Its membership specification states that `y` belongs to it exactly when there merely exists an index in the domain at which the graph has value `y`.

```agda
  table : S
  table = r .fst

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

The two directions of the specification are useful separately. A concrete graph witness places its value in the range. Conversely, membership in the range yields only the truncated existence of an originating index and graph witness; it does not choose that index.

```agda
  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
```

Functionality also determines a metatheoretic value at every member of the domain: it is the first component of the contraction centre. Any other `y` satisfying the graph at the same index is equal to this value, by the contraction supplied in the recursion data.

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

  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))
```

## From unique existence to functionality

Some constructions naturally prove only that a unique graph value merely exists. The lemma `mereFunct` converts this propositionally truncated unique-existence statement into the contractibility required by `Recursion`. It makes no decidability assumption and does not choose a value independently of its uniqueness proof.

```agda
mereFunct : (graph : Formula S 2) (x : S)
          → ∥ (Σ[ y ∈ S ] (⟨ (y ∷ x ∷ []) ⊨ graph ⟩
                          × ((y' : S) → ⟨ (y' ∷ x ∷ []) ⊨ graph ⟩ → y' ≡ y))) ∥₁
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)
```

Because contractibility is a proposition, the truncation may be eliminated into this goal. A representative unique value supplies the contraction centre, and its uniqueness clause identifies every other pair with that centre; the propositional graph component then determines the full dependent-pair equality.

```agda
mereFunct graph x = PT.rec isPropIsContr
  (λ { (y , (hy , uniq)) → (y , hy)
     , (λ { (y' , hy') → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph))
                           (sym (uniq y' hy')) }) })
```

## Starting from a metatheoretic function

The `Definition` form is convenient when a total function `fn : S → S` is already available in the metatheory. Besides a domain and a graph formula, it asks for proofs that the formula holds of `fn x` on the domain and that every value admitted by the formula equals `fn x`.

```agda
record Definition : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom     : S
    fn      : S → S
    graph   : Formula S 2
```

Saying that the formula defines the function is two implications. One says the formula holds of the function's own value at each index. The other says nothing else satisfies it: any value the graph admits at an index equals the function's value there. Together they are the two directions of graph adequacy.

```agda
    defines : (x : S) → ⟨ x ∈ˢ dom ⟩ → ⟨ (fn x ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) → ⟨ x ∈ˢ dom ⟩ → (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x
```

These two implications determine a recursion structure. Its domain and graph are inherited unchanged; the remaining task is to prove that the graph-value fiber is contractible at every point of the domain.

```agda
asRecursion : Definition → Recursion
asRecursion D = record
  { dom   = D.dom
  ; graph = D.graph
```

Functionality is derived, not assumed. The centre is the pair of the function's value and the proof that the graph holds of it. Any competing pair is identified with the centre through the second implication, which forces its value to equal the function's; the identification is transported across the pair, whose satisfaction component is a proposition. Thus the graph-value fiber is contractible on the stated domain.

```agda
  ; 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
```

## The image of a definable function

Applying the preceding conversion to a `Definition` produces its value range as a set of `L`. The function remains a metatheoretic description, while the graph formula and replacement certify that all of its values over the stated domain form an internal set.

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

The module exposes this range under the name `table`. No separate membership lemmas are re-exported here; when their full specification is needed, it remains the one proved for the underlying `Recursion`.

```agda
  table : S
  table = R.table
```

## Scope of the construction

The result applies when three obligations are met: the domain is a set of `L`; the relation is expressed by a two-variable formula over the constructible structure; and it has a unique value at every point of that domain. The `Definition` form proves the last condition from a total metatheoretic function and two adequacy implications. The helper `smallDom` can supply a common containing stage for a `Type ℓ`-indexed family, but using that stage as the domain still requires functionality on every additional member.

No complexity bound on the graph formula or stage-locality certificate for its constants is required at this point. This convenience comes from the already proved general replacement theorem; it does not assert that arbitrary formulas are absolute, and each application must still provide the formula and its adequacy proof.

## Recap

Replacement turns a functional formula on an internal domain into its value range in `L`. A `Recursion` states functionality directly as contractibility; `mereFunct` derives it from truncated unique existence; and `Definition` derives it from a total metatheoretic function together with the two directions of graph adequacy. The resulting set records which values occur, while the graph formula continues to record which index produces which value.