構成可能宇宙における ω 再帰

反復列は、自然数の上のホスト側の再帰である。a から始まり、前の値にステップ関数を適用する。この段階ではまだ Agda の列にすぎず、その内部での表現がこの章の仕事である。

it : ℕ → S
it     = a
it (suc n) = step (it n)

ゼロの節は、数項ゼロのもとで記録されたすべての値の底の集合が、始点の底の集合と同じであることを言う。そこに値が記録されるとは言っていない。

Zero : S → Type (ℓ-suc ℓ)
Zero F = (v : S) → Holds F (nn ) v → v .fst ≡ a .fst

後続の節は、表が (x, v) と (x', v') の両方を記録し、x' の底の集合が x のそれの後続であるなら、二つの値の間にステップの関係が成り立つ、と言う。

Step : S → Type (ℓ-suc ℓ)
Step F = (x v x' v' : S) → Holds F x v → Holds F x' v'
       → x' .fst ≡ sucV (x .fst) → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩

下向きの節は、記録された項目の下では、記録された値が単に存在することを言う。これは定義域を完成させる条項であり、証人が選ばれないため、結論は切り詰められている。

Down : S → Type (ℓ-suc ℓ)
Down F = (x' v' x : S) → Holds F x' v' → ⟨ x .fst ∈ x' .fst ⟩
       → ∥ Σ[ v ∶ S ] Holds F x v ∥₁

正しい近似とは、三つの節の連言である。それは関数のグラフとしての正しさよりも意図的に弱く、正確な定義域も一意性も定めない。

Correct : S → Type (ℓ-suc ℓ)
Correct F = Zero F × (Step F × Down F)

ゼロの節は、対象言語で書かれる。数項ゼロと等しいすべての z と、そこに記録されたすべての値について、その値は始点と等しい、と言うのである。

opaque
  zeroAt : ∀ {n} → Fin n → Formula S n
  zeroAt f = ∀̇ ( (var zero ≐ con (nn ))
               ⇒̇ ∀̇ ( appAt (suc (suc f)) (suc zero) zero ⇒̇ (var zero ≐ con a) ) )

ゼロの節の読みは、数項ゼロのもとでそれを適用し、適用のアトムを妥当性に沿って運んで、Zero の底の集合の等式を産み出す。

  zero-out : ∀ {n} (f : Fin n) (γ : Vec S n) → ⟨ γ ⊨ zeroAt f ⟩ → Zero (lookup f γ)
  zero-out f γ h v hv = h (nn ) refl v
    (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ nn  ∷ γ))) hv)

逆に、ホスト側のゼロの節から対象言語の論理式を満たせる。量化された集合 z を前提 z = nn 0 に沿って書き換え、ゼロにおけるグラフへの所属を適用のアトムへ輸送してから、その値を a と同一視する。

  zero-in : ∀ {n} (f : Fin n) (γ : Vec S n) → Zero (lookup f γ) → ⟨ γ ⊨ zeroAt f ⟩
  zero-in f γ h z ez v hv = h v
    (subst (λ t → ⟨ pr t (v .fst) ∈ (lookup f γ) .fst ⟩) ez
      (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ z ∷ γ)) hv))

ステップの論理式の改名は、二つの枠を使う。最初の変数は位置ゼロにとどまり、二つ目は位置二へ動き、こうして四つの量化された枠が、名前を替えた本体を囲む。

private
  ρ : ∀ {n} → Fin  → Fin (suc (suc (suc (suc n))))
  ρ zero       = zero
  ρ (suc zero) = suc (suc zero)

改名の一致は、二つの環境が、名前を替えられた枠のもとで一致することを確かめる。改名された論理式が読むのは、この位置だけである。

  ag : ∀ {n} (γ : Vec S n) (x v x' v' : S)
     → Ren.Agrees ρ (v' ∷ x' ∷ v ∷ x ∷ γ) (v' ∷ v ∷ [])
  ag γ x v x' v' zero       = refl
  ag γ x v x' v' (suc zero) = refl

後続の節は、表の二つの項目 (x,v) と (x',v') を全称量化する。入れ子になった含意は、まず両方の項目が表に現れることを仮定し、次に添字 x' の台集合が x の集合論的後続であることを仮定する。

opaque
  stepAt : ∀ {n} → Fin n → Formula S n
  stepAt f = ∀̇ (∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc (suc f)))) (suc (suc (suc zero))) (suc (suc zero))
    ⇒̇ ( appAt (suc (suc (suc (suc f)))) (suc zero) zero

この三つの前提のもとで、結論は v' と v を関係づける改名済みのステップ論理式である。改名は四つの量化変数から出力と入力の位置を選び、有限表の隣り合う行を、元の二変数による step の定義へ結ぶ。

    ⇒̇ ( sucAtL (suc (suc (suc zero))) (suc zero)
    ⇒̇ renameFo ρ stepFo ) ) ))))

改名のパスは、改名の意味論で証明される。名前を替えた論理式の長い環境での充足は、もとの論理式の短い環境での充足と等しくなる。二つの環境が、替えられた枠のもとで一致しているからである。

  private
    gr : ∀ {n} (γ : Vec S n) (x v x' v' : S)
       → ⟨ (v' ∷ x' ∷ v ∷ x ∷ γ) ⊨ renameFo ρ stepFo ⟩ ≡ ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
    gr γ x v x' v' = cong ⟨_⟩
      (Ren.⊨-rename ρ stepFo (v' ∷ x' ∷ v ∷ x ∷ γ) (v' ∷ v ∷ []) (ag γ x v x' v'))

後続の節の読みは、二つの適用のアトムを妥当性に逆らって運び、四つの全称量化子を適用し、改名のパスを使う。

  step-out : ∀ {n} (f : Fin n) (γ : Vec S n) → ⟨ γ ⊨ stepAt f ⟩ → Step (lookup f γ)
  step-out f γ h x v x' v' p q s = transport (gr γ x v x' v')
    (h x v x' v'
      (subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc (suc f)))) (suc (suc (suc zero))) (suc (suc zero)) (v' ∷ x' ∷ v ∷ x ∷ γ))) p)
      (subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v' ∷ x' ∷ v ∷ x ∷ γ))) q)

最後の前提は、x' が x の集合論的な後者であることを表す。二つの表所属と合わせると、これは隣接する行を比較するためにちょうど必要な仮定となり、意味論的な読みから二つの値の間のステップ関係が得られる。

      (subst ⟨_⟩ (sym (sucAtL-adequate (suc (suc (suc zero))) (suc zero) (v' ∷ x' ∷ v ∷ x ∷ γ))) s))

後続の節の埋めは、ホスト側のステップの実例から出発して、同じ輸送を逆向きに実行する。

  step-in : ∀ {n} (f : Fin n) (γ : Vec S n) → Step (lookup f γ) → ⟨ γ ⊨ stepAt f ⟩
  step-in f γ h x v x' v' p q s = transport (sym (gr γ x v x' v'))
    (h x v x' v'
      (subst ⟨_⟩ (appAt-adequate (suc (suc (suc (suc f)))) (suc (suc (suc zero))) (suc (suc zero)) (v' ∷ x' ∷ v ∷ x ∷ γ)) p)
      (subst ⟨_⟩ (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v' ∷ x' ∷ v ∷ x ∷ γ)) q)

逆に、隣接する行についてのホスト側の証明から対象言語の節を満たせる。妥当性の等式によって三つの前提は二つの符号化された項目と後者関係に対応し、改名の意味論によって元の二変数のステップ論理式が復元される。

      (subst ⟨_⟩ (sucAtL-adequate (suc (suc (suc zero))) (suc zero) (v' ∷ x' ∷ v ∷ x ∷ γ)) s))

下向きの節は三つの全称量化子と一つの存在量化子をもつ。表が (x',v') を含み、x が x' の台集合の要素なら、x に何らかの値が記録されていると主張する。存在量化子の意味論が保持するのは、そのような値が存在するという命題だけである。

opaque
  downAt : ∀ {n} → Fin n → Formula S n
  downAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero)
    ⇒̇ ( (var zero ∈̇ var (suc (suc zero)))

その存在の結論は、記録された値の切り詰められた存在そのものである。

    ⇒̇ ∃̇ (appAt (suc (suc (suc (suc f)))) (suc zero) zero) ) )))

下向きの論理式を読むとき、存在量化子は命題的切り詰めのまま保たれる。切り詰めの内部にある各証人の値と適用のアトムを、対応するホスト側のグラフ所属へ写し、切り詰めの外で証人を選ぶことはしない。

  down-out : ∀ {n} (f : Fin n) (γ : Vec S n) → ⟨ γ ⊨ downAt f ⟩ → Down (lookup f γ)
  down-out f γ h x' v' x p m = map₁
    (λ { (v , q) → v , subst ⟨_⟩ (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v ∷ x ∷ v' ∷ x' ∷ γ)) q })
    (h x' v' x (subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero) (x ∷ v' ∷ x' ∷ γ))) p) m)

埋めは、この輸送を逆向きに実行する。ホスト側の切り詰められた項目から、存在の充足へである。

  down-in : ∀ {n} (f : Fin n) (γ : Vec S n) → Down (lookup f γ) → ⟨ γ ⊨ downAt f ⟩
  down-in f γ h x' v' x p m = map₁
    (λ { (v , q) → v , subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v ∷ x ∷ v' ∷ x' ∷ γ))) q })
    (h x' v' x (subst ⟨_⟩ (appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero) (x ∷ v' ∷ x' ∷ γ)) p) m)

対象言語での正しさは、三つの節の連言である。

opaque
  corrAt : ∀ {n} → Fin n → Formula S n
  corrAt f = zeroAt f ∧̇ (stepAt f ∧̇ downAt f)

三つの連言成分から、先に分けて定めた Zero、Step、Down の意味論的条件がそのまま復元される。特に、論理式を数学的な主張へ読み戻しても、定義域の等式や一価性の仮定が新たに加わることはない。

  corr-out : ∀ {n} (f : Fin n) (γ : Vec S n) → ⟨ γ ⊨ corrAt f ⟩ → Correct (lookup f γ)
  corr-out f γ (z , (s , d)) = zero-out f γ z , (step-out f γ s , down-out f γ d)

逆方向は、この三つの意味論的条件だけで連言を満たすことを示す。したがって corrAt は、意図的に弱く定めた Correct を一階の論理式として正確に表しており、近似がすでに全域関数のグラフであるという強い主張にはなっていない。

  corr-in : ∀ {n} (f : Fin n) (γ : Vec S n) → Correct (lookup f γ) → ⟨ γ ⊨ corrAt f ⟩
  corr-in f γ (z , (s , d)) = zero-in f γ z , (step-in f γ s , down-in f γ d)

論理式 itFo は、ある正しい近似が添字 q に値 y を記録することを表す。グラフ内部の符号では項目は順序対 (q,y) であり、論理式の環境は (y ∷ q ∷ []) である。したがって itFo は再帰方程式を述べるものではなく、有限な正しい近似によって証される関係を内部化する。

opaque
  itFo : Formula S 
  itFo = ∃̇ ( corrAt zero ∧̇ appAt zero (suc (suc zero)) (suc zero) )

itFo の充足から復元できるのは、証人となる表 F の命題的切り詰めと、その内側にある Correct F および項目 (q,y) だけである。したがってこの論理式は、適切な有限近似の存在を保証する一方、どの近似を用いたかは意図的に忘れている。

  itFo-out : (y q : S) → ⟨ (y ∷ q ∷ []) ⊨ itFo ⟩
           → ∥ Σ[ F ∶ S ] (Correct F × Holds F q y) ∥₁
  itFo-out y q = map₁ (λ { (F , (hc , ha)) → F
    , ( corr-out zero (F ∷ y ∷ q ∷ []) hc
      , subst ⟨_⟩ (appAt-adequate zero (suc (suc zero)) (suc zero) (F ∷ y ∷ q ∷ [])) ha ) })

逆方向では、(q,y) を含む具体的な正しい近似がどれでも itFo(y,q) の証人になる。その近似がどれであるかは直ちに命題的切り詰めの内側へ置かれるため、後の議論では存在と一意性を利用できるが、特定の表を選び出すことはできない。

  itFo-in : (y q F : S) → Correct F → Holds F q y → ⟨ (y ∷ q ∷ []) ⊨ itFo ⟩
  itFo-in y q F hc hq = ∣ F
    , ( corr-in zero (F ∷ y ∷ q ∷ []) hc
      , subst ⟨_⟩ (sym (appAt-adequate zero (suc (suc zero)) (suc zero) (F ∷ y ∷ q ∷ []))) hq ) ∣₁

itFo の充足は、数項の枠の等式に沿って運ばれる。値の枠は固定されたままである。

itFo-at : (v : S) {x y : S} → x ≡ y
        → ⟨ (v ∷ x ∷ []) ⊨ itFo ⟩ → ⟨ (v ∷ y ∷ []) ⊨ itFo ⟩
itFo-at v e = subst (λ t → ⟨ (v ∷ t ∷ []) ⊨ itFo ⟩) e

一意性の補題は、反復の索引による場合分けで始まる。ゼロでは、ゼロの節が直接等式を与える。後続では、下向きの切り詰められた証人をまず消去しなければならない。目標が h-集合の中の等式であるため、この消去は正当である。

corr-val : (F : S) → Correct F → (k : ℕ) (v : S)
         → Holds F (nn k) v → v .fst ≡ (it k) .fst
corr-val F (z , (s , d))     v h = z v h
corr-val F (z , (s , d)) (suc k) v h =
  rec₁ (setIsSet (v .fst) ((it (suc k)) .fst)) read

後者の添字では、Down により、前の数項に記録された値が命題的切り詰めの内側で得られる。帰納法の仮定がこの値を it k と同一視し、続いて Step が現在の値と前の値による stepFo の充足を与え、only が現在の値を一意に定める。

    (d (nn (suc k)) v (nn k) h (self∈sucV (# k)))
  where
  read : Σ[ u ∶ S ] Holds F (nn k) u → v .fst ≡ (it (suc k)) .fst
  read (u , hu) = cong (λ p → p .fst) (only (it k) v
    (subst (λ t → ⟨ (v ∷ t ∷ []) ⊨ stepFo ⟩)

帰納法の仮定から、u と it k の基礎となる集合が等しいことが分かる。構成可能性は命題なので、S≡ はこの等しさを S における等式へ持ち上げる。そこで stepFo の入力を it k に置き換えられ、最後に only が v を step (it k) = it (suc k) と同一視する。

      (S≡ (corr-val F (z , (s , d)) k u hu))
      (s (nn k) u (nn (suc k)) v hu h refl)))

正準な数項での値は一意である。反復の論理式が nn k で成立するなら、記録された値の基礎の集合は it k の基礎の集合と等しくなる。証明は、切り詰められた正しい表を消去して、その表の中で一意性の補題を適用する。

itFo-val : (k : ℕ) (v : S) → ⟨ (v ∷ nn k ∷ []) ⊨ itFo ⟩ → v .fst ≡ (it k) .fst
itFo-val k v h = rec₁ (setIsSet (v .fst) ((it k) .fst))
  (λ { (F , (hc , hv)) → corr-val F hc k v hv }) (itFo-out v (nn k) h)

それぞれの反復は、モデルの要素として提示される。その数項と反復自身の順序対で、どちらも構成可能である。

private
  e : ℕ → S
  e k = prʟ (nn k) (it k)

すべての項目の段階の添字に対する上界の順序数は、項目の対の段階の添字の族に、上界の補題を適用して得られる。

private
  entryStages = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ)
    (λ k → stage ((e (lower k)) .fst) (e (lower k) .snd))
    (λ k → stage-ord ((e (lower k)) .fst) (e (lower k) .snd))

この共通の順序数上界を entryBound と書く。後で有限表の長さが n とともに変わっても、すべての表を同じ段階 Lset entryBound の中で構成できることが、この上界を取り出す目的である。

  entryBound : V ℓ
  entryBound = entryStages .fst

この上界自身は順序数なので、構成可能階層の段階を添字付けられる。最小性は必要ない。すべての項目の段階の添字より上にある順序数なら、有限集合を構成するには十分である。

  entryBound-ord : IsOrd entryBound
  entryBound-ord = entryStages .snd .fst

各項目は、共通の上界を添字とする構成可能階層に属する。実際、項目はまずそれ自身の段階に属し、Lset の単調性によって、boundingOrd が与える順序数の比較に沿って共通の段階へ移される。

  entry-in-bound : (k : ℕ) → ⟨ (e k) .fst ∈ Lset entryBound ⟩
  entry-in-bound k = Lset-mono (entryStages .snd .snd (lift k))
    (stage-mem ((e k) .fst) (e k .snd))

n を固定すると、表 Fn n は添字 0 から n までの項目の対からなる有限集合である。共通の上界により、それらの対がすべて一つの構成可能階層に属することが分かるので、有限集合の構成によって表全体を L の要素としてまとめられる。

Fn : ℕ → S
Fn n = finSet (suc n) (λ i → (e (toℕ i)) .fst) ,
  FinOf.finSetL entryBound entryBound-ord
    (suc n) (λ i → (e (toℕ i)) .fst) (λ i → entry-in-bound (toℕ i))

k ≤ n なら、標準的な項目 (nn k, it k) は Fn n に現れる。したがってこの表は、末尾の添字 n で反復の論理式を証言するために必要な初切片をすべて含む。

Fn-in : (n k : ℕ) → k ≤ n → Holds (Fn n) (nn k) (it k)
Fn-in n k p = subst (λ w → ⟨ w ∈ (Fn n) .fst ⟩) (prʟ-fst (nn k) (it k))
  (finSet-in (suc n) (λ i → (e (toℕ i)) .fst) ((e k) .fst)
    ∣ fromℕ' (suc n) k (suc-≤-suc p)
    , cong (λ j → (e j) .fst) (toFromId' (suc n) k (suc-≤-suc p)) ∣₁)

外向きの読み出しは、すべての要素を、有界な添字とその反復の値へ分解する。どちらも切り詰めの下で復元される。

Fn-out : (n : ℕ) (y : S) → ⟨ y ∈ˢ Fn n ⟩
       → ∥ Σ[ k ∶ ℕ ] ((k ≤ n) × (y .fst ≡ pr (# k) ((it k) .fst))) ∥₁
Fn-out n y h = map₁ (λ { (i , q) → toℕ i
  , (pred-≤-pred (toℕ<n i) , sym q ∙ prʟ-fst (nn (toℕ i)) (it (toℕ i))) })
  (finSet-out (suc n) (λ i → (e (toℕ i)) .fst) (y .fst) h)

対の読み出しは、Kuratowski の対の単射性を使って、有限の表のどの項目も、有界な添字とその反復の値へ分解する。

Fn-pair : (n : ℕ) (x v : S) → Holds (Fn n) x v
        → ∥ Σ[ k ∶ ℕ ] ((k ≤ n) × ((x .fst ≡ # k) × (v .fst ≡ (it k) .fst))) ∥₁
Fn-pair n x v h = map₁ (λ { (k , (p , q)) → k , (p , pr-inj (sym (prʟ-fst x v) ∙ q)) })
  (Fn-out n (prʟ x v) (subst (λ w → ⟨ w ∈ (Fn n) .fst ⟩) (sym (prʟ-fst x v)) h))

有限の表は正しい。三つの条項は、表の項目の対の読み出しから組み立てられる。

Fn-correct : (n : ℕ) → Correct (Fn n)
Fn-correct n = zeroC , (stepC , downC)
  where
  zeroC : Zero (Fn n)
  zeroC v h = rec₁ (setIsSet (v .fst) (a .fst))

零点の条項では、nn 0 にある項目を読むと、数項が # 0 に等しい添字 k が得られる。数項の符号化の単射性から k = 0 となり、同時に得られた値の等式によって、記録された値は it 0 = a と同一視される。

    (λ { (k , (_ , (ex , ev))) → ev ∙ cong (λ j → (it j) .fst) (sym (#-inj  k ex)) })
    (Fn-pair n (nn ) v h)

ステップの節では、二つの表項目を命題的切り詰めの内側で読み出す。stepFo の充足は命題なので、二つの切り詰めをこの目標へ消去できる。残るのは、二つの添字が連続していることと、それぞれの値が対応する反復であることを示す作業である。

  stepC : Step (Fn n)
  stepC x v x' v' hxv hx'v' s = rec₁ (((v' ∷ v ∷ []) ⊨ stepFo) .snd) outer (Fn-pair n x v hxv)
    where
    outer : Σ[ k ∶ ℕ ] ((k ≤ n) × ((x .fst ≡ # k) × (v .fst ≡ (it k) .fst)))
          → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩

最初の読み出しで k が現れた後、二つ目の読み出しから隣接する行の添字 k' が得られる。二つの証人を、命題である充足判断への消去の内側に保つことで、切り詰めの境界を守りながら、添字と値の等式を同時に利用できる。

    outer (k , (_ , (ex , ev))) = rec₁ (((v' ∷ v ∷ []) ⊨ stepFo) .snd) inner (Fn-pair n x' v' hx'v')
      where
      inner : Σ[ k' ∶ ℕ ] ((k' ≤ n) × ((x' .fst ≡ # k') × (v' .fst ≡ (it k') .fst)))
            → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
      inner (k' , (_ , (ex' , ev'))) =

二つの表の読み出しにより、v は it k と、v' は it k' とそれぞれ同一視される。二つの位置を結ぶ後者の等式から k' = suc k が従うので、これらを置き換えた後に必要な充足はちょうど defines (it k) である。モデルの台における等式には、構成可能性の証明成分が命題であることを用いて S≡ を適用する。

        subst2 (λ p q → ⟨ (p ∷ q ∷ []) ⊨ stepFo ⟩)
          (S≡ (sym (ev' ∙ cong (λ j → (it j) .fst) k'≡)))
          (S≡ (sym ev))
          (defines (it k))
        where

k' = suc k を得るには、第二の位置が第一の位置の後者であるという等式を、それぞれの位置を # k' と # k に同一視する等式と合成する。すると数項の符号化の単射性により、符号化された有限順序数の等しさが自然数の添字の等しさへ変わる。

        k'≡ : k' ≡ suc k
        k'≡ = #-inj k' (suc k) (sym ex' ∙ s ∙ cong sucV ex)

下向きの条項は、切り詰められた対の読み出しを消去して、すでに正準な項目のあるより小さい添字を見つけることで証明される。

  downC : Down (Fn n)
  downC x' v' x h m = rec₁ squash₁ outer (Fn-pair n x' v' h)
    where
    outer : Σ[ k' ∶ ℕ ] ((k' ≤ n) × ((x' .fst ≡ # k') × (v' .fst ≡ (it k') .fst)))
          → ∥ Σ[ v ∶ S ] Holds (Fn n) x v ∥₁

より小さい添字の項目は、有限の表の内向きの読み出しによって作られ、数項の等式に沿って運ばれる。

    outer (k' , (p' , (ex' , _))) = map₁
      (λ { (j , (j< , ej)) → it j
         , subst (λ t → ⟨ pr t ((it j) .fst) ∈ (Fn n) .fst ⟩) (sym ej)
             (Fn-in n j (≤-trans (<-weaken j<) p')) })
      (∈#-elim k' (x .fst) (subst (λ w → ⟨ x .fst ∈ w ⟩) ex' m))

それぞれの正準な対が反復の論理式を満たす。自分自身の有限の表を証人として使う。すべての目標の数項が、それぞれ自分の表をもつ。一つの表がすべての位置に仕えるとは主張していない。

it-graph : (k : ℕ) → ⟨ (it k ∷ nn k ∷ []) ⊨ itFo ⟩
it-graph k = itFo-in (it k) (nn k) (Fn k) (Fn-correct k) (Fn-in k k ≤-refl)

数項の表示とは、自然数と、それを台の要素と同一視する等式の、明示的な対である。

Num : S → Type (ℓ-suc ℓ)
Num q = Σ[ k ∶ ℕ ] (nn k ≡ q)

モデル内部の自然数集合 ωʟ に属することから得られる数項表示は、命題的切り詰めの内側にとどまる。後で結論が命題となる一意性の議論にはこれで十分だが、任意の計算に使える自然数が取り出されるわけではない。

ω-num : (q : S) → ⟨ q ∈ˢ ωʟ ⟩ → ∥ Num q ∥₁
ω-num q = map₁ (λ { (i , p) → lower i , S≡ p })

ここまでで itFo を、内部集合 ωʟ 上の全域かつ一価な関係とみなせる。レコード valR はこの定義域とグラフを、残る関数性の証明とともにまとめる。このレコードに置換を適用することで、それらの値を L の中に集められる。

private
  valR : Recursion
  valR = record
    { dom   = ωʟ
    ; graph = itFo

関数性は、単に存在するだけの数項の表示から組み立てられる。復号が反復の値を産出し、一意性は、復号された数項で証明される。

    ; funct = λ q q∈ → mereFunct itFo q (map₁ (wit q) (ω-num q q∈)) }
    where
    wit : (q : S) → Num q
        → Σ[ y ∶ S ] (⟨ (y ∷ q ∷ []) ⊨ itFo ⟩
                     × ((y' : S) → ⟨ (y' ∷ q ∷ []) ⊨ itFo ⟩ → y' ≡ y))

具体的な表示 nn k ≡ q が与えられたら、it k をファイバーの中心とする。グラフの証明は q へ順向きに移し、競合する値の証明は nn k へ戻して itFo-val により同一視する。外側の mereFunct は、このような一意な中心の切り詰められた存在を、ファイバーの可縮性へ変える。

    wit q (k , eq) = it k
      , ( itFo-at (it k) eq (it-graph k)
        , λ y' h → S≡ (itFo-val k y' (itFo-at y' (sym eq) h)) )

valR に付随する一般の置換構成から、その値を集めた集合と、正確な所属規則が得られる。これらの規則によって、内部で集めた集合と、ホスト側で定義した列 it とが結び付く。

  module VR = Of valR

集合 values は、関係 itFo による ωʟ の置換像である。有限反復の値を含み、重複する値は集合として自動的に一つにまとまる。これは値の集合であって、後で構成する添字付きの関数グラフではない。

values : S
values = VR.table

ホスト側で定義した各反復は、この値の集合に属する。内部の数項 nn n について、nn n ∈ ωʟ と有限表による証明 it-graph n を合わせることで、この所属が得られる。

values-in : (n : ℕ) → ⟨ (it n) .fst ∈ values .fst ⟩
values-in n = VR.table-in (nn n) (it n) (#∈ω n) (it-graph n)

値の領域のすべての要素は、単に、なんらかの反復の値である。外向きの読み出しが数項の表示と反復の論理式の充足を復元し、一意性の補題が値を同定する。

values-out : (y : S) → ⟨ y ∈ˢ values ⟩ → ∥ Σ[ n ∶ ℕ ] (y .fst ≡ (it n) .fst) ∥₁
values-out y hy = rec₁ squash₁
  (λ { (q , (q∈ , h)) → map₁
    (λ { (k , eq) → k , itFo-val k y (itFo-at y (sym eq) h) }) (ω-num q q∈) })
  (VR.table-out y hy)

値の領域の合併は、モデルの合併の操作によって作られ、L の集合である。

iterUnion : S
iterUnion = unionʟ values

各有限反復のすべての要素は iterUnion に属する。まず values-in により反復そのものが values に入り、次に和集合の所属規則により、その各要素が和集合に入る。ここで示されるのは it n ⊆ iterUnion であり、it n 自身が iterUnion の要素だということではない。

iterUnion-in : (n : ℕ) (z : S) → ⟨ z .fst ∈ (it n) .fst ⟩ → ⟨ z ∈ˢ iterUnion ⟩
iterUnion-in n z hz = unionʟ-in values z (it n) (values-in n) hz

合併のすべての要素は、単に、ある有限の反復の中にある。証明は、合併の所属を消去して中間の集合を見つけ、それを構成可能として包み、値の領域の外向きの読み出しで読む。

iterUnion-out : (z : S) → ⟨ z ∈ˢ iterUnion ⟩ → ∥ Σ[ n ∶ ℕ ] ⟨ z .fst ∈ (it n) .fst ⟩ ∥₁
iterUnion-out z h = rec₁ squash₁
  (λ { (B , (hB , hz)) → map₁
    (λ { (n , eB) → n , subst (λ w → ⟨ z .fst ∈ w ⟩) eB hz })
    (values-out (B , isL-trans {x = values .fst} {y = B} hB (values .snd)) hB) })

和集合の外向きの規則から、B ∈ values かつ z ∈ B を満たす中間集合 B が、命題的切り詰めの内側で得られる。L の推移性により B を S の要素とみなすための構成可能性の証人が補われ、続いて values-out が B をある it n と同一視する。この添字も切り詰めの外へ選び出されることはない。

  (unionʟ-out values z h)

添字付きグラフと有限段階の成長

値の集合とその和集合に加えて、同じ再帰レコードから内部の関数グラフも定まる。その要素は入力の数項と対応する反復値の両方を保持するので、後の議論で値全体の集合だけでなく特定の有限段階を参照する必要があるときに利用できる。

private module TR = RecursionGraph valR using ( F; F-in; F-out )

関数のグラフは、数項と反復の値の順序対を集める。

iter : S
iter = TR.F

それぞれの正準な対は、グラフの要素である。置換の値の一意性に沿って運ばれる。

iter-in : (n : ℕ) → ⟨ pr (# n) ((it n) .fst) ∈ iter .fst ⟩
iter-in n = subst (λ v → ⟨ pr (# n) (v .fst) ∈ iter .fst ⟩)
  (VR.val-uniq (nn n) (#∈ω n) (it n) (it-graph n)) (TR.F-in (nn n) (#∈ω n))

逆に、グラフの各要素は、ある自然数 n に対する標準的な対 (# n, it n) に単に等しい。一般のグラフ規則から得られる始域の要素とその数項表示は、どちらも命題的切り詰めの内側に保たれる。値の一意性により第二成分を同一視できるが、n が切り詰めの外へ取り出されることはない。

iter-out : (y : S) → ⟨ y ∈ˢ iter ⟩ → ∥ Σ[ n ∶ ℕ ] (y .fst ≡ pr (# n) ((it n) .fst)) ∥₁
iter-out y hy = rec₁ squash₁
  (λ { (q , q∈ , e) → map₁ (λ { (k , eq) → k
    , e ∙ cong₂ pr (cong (λ p → p .fst) (sym eq))
      (cong (λ p → p .fst) (VR.val-uniq q q∈ (it k) (itFo-at (it k) eq (it-graph k)))) }) (ω-num q q∈) })

一般の関数グラフの外向き所属規則から、まず始域の要素 q ∈ ωʟ と、その一意な値を含む符号化された対が得られる。q を数項として復号し、値の一意性を使えば、主張された標準的な対になる。自然数の添字は最後まで命題的切り詰めの内側に保たれる。

  (TR.F-out (y .fst) hy)

成長のモジュールは、「すべての集合が自分自身のステップの中に含まれる」という仮定によってパラメータづけられる。

module Closure (grows : (x z : S) → ⟨ z .fst ∈ x .fst ⟩ → ⟨ z .fst ∈ (step x) .fst ⟩) where

it-mono : (n : ℕ) (z : S) → ⟨ z .fst ∈ (it n) .fst ⟩ → ⟨ z .fst ∈ (it (suc n)) .fst ⟩
it-mono n z = grows (it n) z

it-up : (n k : ℕ) (z : S) → ⟨ z .fst ∈ (it n) .fst ⟩ → ⟨ z .fst ∈ (it (k + n)) .fst ⟩
it-up n     z h = h
it-up n (suc k) z h = it-mono (k + n) z (it-up n k z h)