---
title: "Graphs of recursive definitions"
module: L.Recursion.Graph
lang: en
site: "Bedrock"
description: "Graphs of recursive definitions"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 59
canonical: https://bedrock.institute/en/L.Recursion.Graph.html
html: L.Recursion.Graph.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Recursion/Graph.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.Renaming, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Recursion, L.Coding.Model]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Recursion.Graph.md, https://bedrock.institute/ja/L.Recursion.Graph.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Graphs of recursive definitions

A recursion in `L` gives a unique value at every point of an internal domain. A set-theoretic function is represented by its graph, the set of ordered pairs `pr(x , y)` with input first and output second. This chapter turns the value relation of a recursion into such a set `F`, then proves that `F` is functional and has exactly the original domain.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
```

The graph must itself be described in the object language. The available syntax forms conjunctions and existential statements, while renaming places an existing two-variable value relation beneath a new quantifier. The ambient operation `pr` supplies ordered-pair codes, and its injectivity later recovers both coordinates from an equality of codes.

```agda
open import FOL.Syntax using ( Formula; _∧̇_; ∃̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj )
```

The constructible pairing operation produces an element of `L` whose underlying set is the ambient ordered-pair code. The general recursion theorem can then apply replacement to a formula describing those pairs. Equality of constructible elements is reduced to equality of their underlying sets because constructibility proofs are propositions.

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion; module Of )
open import L.Coding.Model {ℓ}
  using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; domAt; domAt-intro )

open import Cubical.Data.Sigma using ( Σ≡Prop )
```

Several propositions below are obtained from truncated existence statements. They may be eliminated only into propositional goals. Membership and equality in the cumulative hierarchy have precisely this property, which allows witnesses to be used without making a global choice.

```agda
open import Cubical.Foundations.HLevels using ( isPropΣ )
open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
```

The formulas are interpreted in the constructible structure. The local satisfaction notation and its renaming theorem connect syntactic substitutions with changes of environment; all later claims about the graph are statements in this semantics.

```agda
open hPropStructure 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
module PairFo (φ : Formula S 2) where
```

## A formula for ordered pairs

Fix a two-variable formula `φ`, read as a relation between a value and an index. The module `PairFo` constructs another two-variable formula: at a candidate pair `e` and an index `p`, it asserts that some value `z` satisfies `φ(z,p)` and that `e` is the ordered pair `pr(p,z)`.

```agda
  ρ : Fin 2 → Fin 3
  ρ zero       = zero
  ρ (suc zero) = suc (suc zero)
```

The renaming map records how the two free variables of `φ` occur below the existential quantifier. The value variable remains in slot zero and is bound by that quantifier; the index variable moves to slot two. The formula `pairFo` is opaque, so subsequent reasoning uses its proved semantic characterization rather than unfolding it.

```agda
  opaque
    pairFo : Formula S 2
```

The formula conjoins two assertions under the existential quantifier. The first says that `e` codes the ordered pair of `p` and the quantified value; the second is the renamed copy of `φ`. Thus the syntax directly mirrors the mathematical description of a member of a function graph.

```agda
    pairFo = ∃̇ (prAtL (suc zero) (suc (suc zero)) zero ∧̇ renameFo ρ φ)
```

The agreement proof verifies that renaming preserves the intended environment. In the longer environment `(z ∷ e ∷ p ∷ [])`, the renamed value slot reads `z` and the renamed index slot reads `p`, exactly as the original formula does in `(z ∷ p ∷ [])`.

```agda
    private
      ag : (z e p : S) → Ren.Agrees ρ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ [])
      ag z e p zero       = refl
      ag z e p (suc zero) = refl
```

Two semantic equalities prepare the outward direction. Correctness of the ordered-pair formula identifies its satisfaction with the ambient equality `fst e ≡ pr (fst p) (fst z)`. The renaming theorem identifies satisfaction of the renamed formula with satisfaction of the original `φ` at value `z` and index `p`.

```agda
      at : (z e p : S)
         → ⟨ (z ∷ e ∷ p ∷ []) ⊨ prAtL (suc zero) (suc (suc zero)) zero ⟩
         ≡ (fst e ≡ pr (fst p) (fst z))
      at z e p = cong ⟨_⟩ (prAtL-adequate (suc zero) (suc (suc zero)) zero (z ∷ e ∷ p ∷ []))

      gr : (z e p : S)
```

Reading `pairFo` outward yields a propositionally truncated value `z`, together with the ordered-pair equation and a proof of `φ(z,p)`. Reading it inward reverses these transports: such a value, equation, and graph proof construct a satisfaction witness for `pairFo`. These are the two semantic directions used below.

```agda
         → ⟨ (z ∷ e ∷ p ∷ []) ⊨ renameFo ρ φ ⟩ ≡ ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
      gr z e p = cong ⟨_⟩ (Ren.⊨-rename ρ φ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ []) (ag z e p))

    pair-out : (e p : S) → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
             → ∥ Σ[ z ∈ S ] ((fst e ≡ pr (fst p) (fst z)) × ⟨ (z ∷ p ∷ []) ⊨ φ ⟩) ∥₁
    pair-out e p = PT.map (λ { (z , (q , h)) →
```

The inward lemma completes the semantic equivalence and the construction now turns to a fixed recursion. Its original domain and value relation are retained; only the values sent to replacement will change from bare outputs to ordered pairs of inputs and outputs.

```agda
      z , (transport (at z e p) q , transport (gr z e p) h) })

    pair-in : (e p z : S) → fst e ≡ pr (fst p) (fst z) → ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
            → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
    pair-in e p z q h = ∣ z , (transport (sym (at z e p)) q , transport (sym (gr z e p)) h) ∣₁
module Graph (R₀ : Recursion) where
```

## Domain and values

The recursion supplies a domain, its original graph formula, and contractibility of the graph-value fiber at each domain member. Its derived value is written `fn`. The local predicate `Mem x` is the underlying membership assertion that `fn` requires.

```agda
  open Of R₀ public using ( dom; graph; funct ) renaming ( val to fn )
  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst dom ⟩

  isPropMem : (x : S) → isProp (Mem x)
  isPropMem x = snd (fst x ∈ fst dom)
```

Membership in a set is proposition-valued, so `Mem x` is a proposition. Consequently, any two proofs that `x` belongs to the domain are equal. This proof irrelevance ensures that the value `fn x m` does not depend on the chosen membership certificate.

```agda
  private
    defines : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    defines x m = funct x m .fst .snd

    only : (x : S) (m : Mem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m
    only x m y h = sym (cong fst (funct x m .snd (y , h)))
```

Contractibility provides two facts about the original value relation. The selected centre proves that the formula `graph` is satisfied in the environment `(fn x m ∷ x ∷ [])`. Its contraction proves that any other `y` satisfying the formula at `x` equals `fn x m`.

```agda
    module Fo = PairFo graph renaming ( pairFo to fo; pair-out to out; pair-in to into )

    fn-irr : (x : S) (m m' : Mem x) → fn x m ≡ fn x m'
    fn-irr x m m' = cong (fn x) (isPropMem x m m')
    pairOf : (x : S) → Mem x → S
    pairOf x m = prʟ x (fn x m)
```

The ordered-pair formula is now specialized to the original value relation. Proof irrelevance for `Mem x` gives `fn-irr`, while `pairOf x m` is the constructible ordered pair of `x` and its value. Its underlying set is `pr (fst x) (fst (fn x m))`.

```agda
    uniq : (x : S) (m : Mem x) (p : S) → ⟨ (p ∷ x ∷ []) ⊨ Fo.fo ⟩ → p ≡ pairOf x m
    uniq x m p h = PT.rec (isSetS p (pairOf x m))
      (λ { (z , (e , g)) → Σ≡Prop (λ v → snd (isL v))
        (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z g) ∙ sym (prʟ-fst x (fn x m))) })
      (Fo.out p x h)
```

Suppose a candidate `p` satisfies the specialized pair formula at `x`. The outward lemma merely supplies a value `z`, an equality between the underlying set of `p` and `pr(x,z)`, and a proof that `z` satisfies the original graph. Original-value uniqueness identifies `z` with `fn x m`; composing the resulting equalities proves `p ≡ pairOf x m`.

```agda
    R : Recursion
    R = record
      { dom   = dom
      ; graph = Fo.fo
      ; funct = λ x m →
```

## Collecting the graph

A new recursion uses the same domain and the ordered-pair formula as its value relation. At `x`, its centre is `pairOf x m`; the inward semantic lemma proves that this pair satisfies the formula, and `uniq` proves that every other satisfying candidate is equal to it.

```agda
          ( pairOf x m
          , Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m) )
        , λ { (p , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ Fo.fo)) (sym (uniq x m p h)) } }

    module T = Of R using ( table; table-in; table-out )

  F : S
```

The dependent-pair contraction compares a candidate value together with its satisfaction proof against the chosen centre. Equality of their first components is `uniq`; the satisfaction components are propositions, so this equality determines the whole dependent-pair path. The result is a valid `Recursion` for ordered pairs.

```agda
  F = T.table

  F-in : (x : S) (m : Mem x) → ⟨ pr (fst x) (fst (fn x m)) ∈ fst F ⟩
  F-in x m = subst (λ w → ⟨ w ∈ fst F ⟩) (prʟ-fst x (fn x m))
    (T.table-in x (pairOf x m) m
      (Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m)))
```

Replacement applied to this recursion forms the value range of its ordered-pair values. That range is the desired graph `F`. Thus `F` is an element of `L`, and every element placed in it is an ordered pair of a domain element with its recursively determined value.

```agda
  F-out : (p : V ℓ) → ⟨ p ∈ fst F ⟩
        → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁
  F-out p h = PT.rec squash₁ step (T.table-out pS h)
    where
    pS : S
```

The inward membership direction is immediate from the replacement specification. For a domain witness `m`, the constructible ordered pair `pairOf x m` satisfies the pair formula, hence belongs to the replacement range. Transport along `prʟ-fst` restates this as membership of the ambient code `pr (fst x) (fst (fn x m))` in the underlying set of `F`.

```agda
    pS = p , isL-trans {x = fst F} {y = p} h (snd F)

    step : Σ[ x ∈ S ] (Mem x × ⟨ (pS ∷ x ∷ []) ⊨ Fo.fo ⟩)
         → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁
    step (x , (m , g)) = PT.map
      (λ { (z , (e , gz)) →
```

For the outward direction, begin with an ambient set `p ∈ fst F`. Downward closure of constructibility packages `p` as an element `pS` of `L`. The replacement specification first yields, merely, an index `x`, a domain proof `m`, and satisfaction of the ordered-pair formula by `pS`.

```agda
        x , m , (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z gz)) })
      (Fo.out pS x g)
  Fib : S → S → Type (ℓ-suc ℓ)
  Fib x y = Σ[ m ∈ Mem x ] (fst y ≡ fst (fn x m))

  isPropFib : (x y : S) → isProp (Fib x y)
```

The semantic outward lemma then opens a second truncation and supplies a value `z`, an ordered-pair equality, and a proof of the original graph relation. Original-value uniqueness replaces `z` by `fn x m`. The result states merely that `p` is the code `pr(x,fn x m)` for some domain element `x`.

```agda
  isPropFib x y = isPropΣ (isPropMem x) (λ m → setIsSet (fst y) (fst (fn x m)))

  pair-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → Fib x y
  pair-out x y h = PT.rec (isPropFib x y) step (F-out (pr (fst x) (fst y)) h)
    where
    step : Σ[ x' ∈ S ] Σ[ m' ∈ Mem x' ] (pr (fst x) (fst y) ≡ pr (fst x') (fst (fn x' m')))
```

## Recovering the coordinates

For fixed `x` and `y`, the fiber `Fib x y` consists of a domain proof `m : Mem x` and an equality between the underlying set of `y` and that of `fn x m`. Both components are propositions: domain membership is proposition-valued and equality in `V` is a proposition. Hence the whole fiber is a proposition.

```agda
         → Fib x y
    step (x' , m' , e) = subst (λ z → Fib z y)
      (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj e .fst))) (m' , pr-inj e .snd)

  γ : S ^ 2
  γ = F ∷ dom ∷ []
```

If the ordered-pair code `pr(fst x,fst y)` belongs to `F`, the outward description gives `x'`, `m'`, and an equality with `pr(fst x',fst(fn x' m'))`. Injectivity of `pr` yields equalities of both coordinates. The input equality transports `m'` to a proof that `x` lies in the domain; the output equality gives the second component of `Fib x y`.

```agda
  sv : ⟨ γ ⊨ svAt zero ⟩
  sv = svAt-in zero γ (λ x y y' p q →
    let (m , e)   = pair-out x y p
        (m' , e') = pair-out x y' q
    in e ∙ cong fst (fn-irr x m m') ∙ sym e')
```

The environment `γ = F ∷ dom ∷ []` assigns the two free variables used by the formulas for single-valuedness and domain. To prove single-valuedness, take two pairs in `F` with the same first coordinate `x`. Their fibers provide membership proofs `m` and `m'` and output equalities to `fn x m` and `fn x m'`. Proof irrelevance identifies the two function values, so the outputs are equal.

```agda
  dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
  dm = domAt-intro zero (suc zero) γ (λ x → fwd x , bwd x)
    where
    fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩ → Mem x
    fwd x = PT.rec (isPropMem x) (λ { (y , p) → fst (pair-out x y p) })
```

Finally, the domain formula is proved in both directions. If `x` occurs as the first coordinate of some ordered pair in `F`, `pair-out` returns a fiber and hence a proof `Mem x`. Conversely, from `m : Mem x`, the pair `pr(x,fn x m)` belongs to `F` by `F-in`, so `x` occurs as a first coordinate. Therefore the domain of the collected graph is exactly `dom`.

```agda
    bwd : (x : S) → Mem x → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩
    bwd x m = ∣ fn x m , F-in x m ∣₁
```