Bedrock構成可能宇宙における ω 再帰
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ構成可能集合上の定義可能な操作と始点から、ホスト側の自然数に関する再帰によって有限反復の列が定まります。本章では各反復を L の内部で表します。有限な正しい表によって内部の数項における値の存在と一意性を示し、置換によって値と添字付きグラフを集め、和集合によって有限段階で得られるすべての要素を含む集合を作ります。
{-# OPTIONS --cubical --safe --guardedness #-}
基礎ライブラリを開き、本書の常の形式に従って、排中律を明示的な仮定として受け取ります。
open import Base.Prelude open import Base.Classical using ( LEM )
モジュールは宇宙レベルを固定し、古典的な仮定に名前を与えます。以下の各定理は、どのレベルの排中律の実例を消費するかを正確に記録します。
module L.GCH.OmegaRecursion {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
反復の記述は対象言語で書かれます。論理式は等号・連言・含意、そして非有界の存在と全称の量化子から作られ、論理式の改名と絶対性が、同じ論理式を異なる環境のもとで読むことを支えます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_ ) 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; #-inj ) open import V.Model {ℓ} using ( pair-spec; union-spec; self∈sucV ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono ) open import L.Ordinal {ℓ} using ( #∈ω; ∈#-elim; boundingOrd )
ホスト側の列を L の集合として表すには、構成可能性に上界を与える段階、近似表を収める有限集合、符号化された順序対と和集合、そして内部自然数集合 ωʟ が必要です。これらにより、各ホスト添字に対する有限表から、モデル内部で添字付けられた一つの値域とグラフへ移ることができます。
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem ) open import L.Axioms.Basic {ℓ} using ( finSet; finSet-in; finSet-out; module FinOf ) open import L.Axioms.Numerals {ℓ} using ( pairʟ; pairʟ-fst; unionʟ; unionʟ-fst ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
再帰のインターフェースは、内部の定義域上で内部的に定義でき、値が一意である関係をまとめます。そのグラフ構成と、適用・順序対・集合論的後続を表す符号化論理式によって、後で有限表の意味論的な議論を L 上の一階の関係へ、さらに L の実際の集合へ移します。
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct ) open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to RecursionGraph ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; prʟ; prʟ-fst ) open import L.Coding.Expressions {ℓ} using ( sucAtL; sucAtL-adequate; numL )
自然数の順序、有界の索引、そして有界の索引と数項の間の変換が、この章の有限の簿記を支えます。
open import Cubical.Data.Nat.Order using ( _≤_; ≤-refl; ≤-trans; <-weaken; pred-≤-pred; suc-≤-suc ) open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
以下のいくつかの同一視は依存対の中で行われます。台となる集合には、その構成可能性を示す命題が伴います。累積階層の h-集合構造により台集合の間の等式は命題となり、直和と二変数の輸送が、符号化された対を読み解く際の分岐と同時代入を扱います。
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop ) open import Cubical.Data.Sum using ( _⊎_ ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Foundations.HLevels using ( isSetΣSndProp ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
階層の後続の演算と切り詰めの仕組みが、構成を完成させます。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet {ℓ} using ( sucV; #_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
構成可能な台がその所属とともに開かれます。それぞれの反復は L の要素だからです。
open hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
絶対性の読みは二つの名前で導入され、L の内部で環境のもとで論理式を読むために使われます。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
改名の意味論は、定数のアルファベットをそのままにして具体化されます。これにより、名前を替えた論理式を、枠を並べ替えた環境のもとで読めます。
module Ren = Sat 𝒮ʟ id
台は h-集合です。階層が h-集合であり、構成可能性が命題だからです。したがって構成可能な集合の間の等式は命題になります。
isSetS : isSet S isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
底の集合が等しければ構成可能な集合も等しくなります。構成可能性の証明が命題だからです。等式がまず底の集合の水準で得られたとき、いつでもこの変換を使います。
S≡ : {x y : S} → fst x ≡ fst y → x ≡ y S≡ = Σ≡Prop (λ v → snd (isL v))
符号化されたグラフは入力を先、値を後に記録します。Holds F x y は、台集合の水準で順序対 (x,y) が F に属することを意味します。論理式の環境ではリストの順序が逆になるため、入力 x、出力 y のステップ関係は (y ∷ x ∷ []) のもとで読みます。
Holds : S → S → S → Type (ℓ-suc ℓ) Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩
自然数 k の構成可能な数項は、周囲の数項にその構成可能性を対にしたものです。数項こそ、反復が記録される位置です。
nn : ℕ → S nn k = # k , numL k
ある要素の台集合が a または b の台集合と等しければ、その要素は内部の非順序対 pairʟ a b に属します。証明では、pairʟ a b の台集合を周囲の非順序対と同一視する等式に沿って、この二つの場合を輸送します。
pairʟ-in : (a b y : S) → (fst y ≡ fst a) ⊎ (fst y ≡ fst b) → ⟨ y ∈ˢ pairʟ a b ⟩ pairʟ-in a b y k = subst (λ w → ⟨ fst y ∈ w ⟩) (sym (pairʟ-fst a b)) (subst ⟨_⟩ (sym (pair-spec (fst a) (fst b) (fst y))) ∣ k ∣₁)
y を A の内部和集合に入れるには、B ∈ A かつ y ∈ B を満たす具体的な構成可能集合 B を示せば十分です。この二つの所属が和集合への所属の通常の証人となり、unionʟ A の台集合に関する等式に沿って輸送されます。
unionʟ-in : (A y B : S) → ⟨ fst B ∈ fst A ⟩ → ⟨ fst y ∈ fst B ⟩ → ⟨ y ∈ˢ unionʟ A ⟩ unionʟ-in A y B hB hy = subst (λ w → ⟨ fst y ∈ w ⟩) (sym (unionʟ-fst A)) (subst ⟨_⟩ (sym (union-spec (fst A) (fst y))) ∣ fst B , (hB , hy) ∣₁)
和の中の所属からは、その要素を含む中間の集合が単に得られます。中間の集合は周囲の要素であり、それ自身の構成可能性の証明は持ちません。
unionʟ-out : (A y : S) → ⟨ y ∈ˢ unionʟ A ⟩ → ∥ Σ[ B ∈ V ℓ ] (⟨ B ∈ fst A ⟩ × ⟨ fst y ∈ B ⟩) ∥₁ unionʟ-out A y h = subst ⟨_⟩ (union-spec (fst A) (fst y)) (subst (λ w → ⟨ fst y ∈ w ⟩) (unionʟ-fst A) h)
定義可能な操作の有限反復
反復のモジュールは、この章の五つの材料を受け取ります。始点、出力が先で入力が後という順のステップの論理式、実際のステップ関数、その論理式がすべての点で関数を定義することの証明、そしてその値だけが充足することの証明です。台全体での全域性がデータの一部です。
module Iterate (a : S) (stepFo : Formula S 2) (step : S → S) (defines : (x : S) → ⟨ (step x ∷ x ∷ []) ⊨ stepFo ⟩) (only : (x y : S) → ⟨ (y ∷ x ∷ []) ⊨ stepFo ⟩ → y ≡ step x) where
反復列は、自然数の上のホスト側の再帰です。a から始まり、前の値にステップ関数を適用します。この段階ではまだ Agda の列にすぎず、その内部での表現がこの章の仕事です。
it : ℕ → S it zero = a it (suc n) = step (it n)
ゼロの節は、数項ゼロのもとで記録されたすべての値の底の集合が、始点の底の集合と同じであることを言います。そこに値が記録されるとは言っていません。
Zero : S → Type (ℓ-suc ℓ) Zero F = (v : S) → Holds F (nn 0) v → fst v ≡ fst a
後続の節は、表が (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' → fst x' ≡ sucV (fst x) → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
下向きの節は、記録された項目の下では、記録された値が単に存在することを言います。これは定義域を完成させる条項であり、証人が選ばれないため、結論は切り詰められています。
Down : S → Type (ℓ-suc ℓ) Down F = (x' v' x : S) → Holds F x' v' → ⟨ fst x ∈ fst x' ⟩ → ∥ Σ[ 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 0)) ⇒̇ ∀̇ ( appAt (suc (suc f)) (suc zero) zero ⇒̇ (var zero ≐ con a) ) )
ゼロの節の読みは、数項ゼロのもとでそれを適用し、適用のアトムを妥当性に沿って運んで、Zero の底の集合の等式を産み出します。
zero-out : ∀ {n} (f : Fin n) (γ : S ^ n) → ⟨ γ ⊨ zeroAt f ⟩ → Zero (lookup f γ) zero-out f γ h v hv = h (nn 0) refl v (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ nn 0 ∷ γ))) hv)
逆に、ホスト側のゼロの節から対象言語の論理式を満たせます。量化された集合 z を前提 z = nn 0 に沿って書き換え、ゼロにおけるグラフへの所属を適用のアトムへ輸送してから、その値を a と同一視します。
zero-in : ∀ {n} (f : Fin n) (γ : S ^ n) → Zero (lookup f γ) → ⟨ γ ⊨ zeroAt f ⟩ zero-in f γ h z ez v hv = h v (subst (λ t → ⟨ pr t (fst v) ∈ fst (lookup f γ) ⟩) ez (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ z ∷ γ)) hv))
ステップの論理式の改名は、二つの枠を使います。最初の変数は位置ゼロにとどまり、二つ目は位置二へ動き、こうして四つの量化された枠が、名前を替えた本体を囲みます。
private ρ : ∀ {n} → Fin 2 → Fin (suc (suc (suc (suc n)))) ρ zero = zero ρ (suc zero) = suc (suc zero)
改名の一致は、二つの環境が、名前を替えられた枠のもとで一致することを確かめます。改名された論理式が読むのは、この位置だけです。
ag : ∀ {n} (γ : 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} (γ : 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) (γ : 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) (γ : 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) (γ : S ^ n) → ⟨ γ ⊨ downAt f ⟩ → Down (lookup f γ) down-out f γ h x' v' x p m = PT.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) (γ : S ^ n) → Down (lookup f γ) → ⟨ γ ⊨ downAt f ⟩ down-in f γ h x' v' x p m = PT.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) (γ : 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) (γ : 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 2 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 = PT.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 → fst v ≡ fst (it k) corr-val F (z , (s , d)) zero v h = z v h corr-val F (z , (s , d)) (suc k) v h = PT.rec (setIsSet (fst v) (fst (it (suc k)))) 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 → fst v ≡ fst (it (suc k)) read (u , hu) = cong 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 ⟩ → fst v ≡ fst (it k) itFo-val k v h = PT.rec (setIsSet (fst v) (fst (it k))) (λ { (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 (fst (e (lower k))) (e (lower k) .snd)) (λ k → stage-ord (fst (e (lower k))) (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 : ℕ) → ⟨ fst (e k) ∈ Lset entryBound ⟩ entry-in-bound k = Lset-mono (entryStages .snd .snd (lift k)) (stage-mem (fst (e k)) (e k .snd))
n を固定すると、表 Fn n は添字 0 から n までの項目の対からなる有限集合である。共通の上界により、それらの対がすべて一つの構成可能階層に属することが分かるので、有限集合の構成によって表全体を L の要素としてまとめられる。
Fn : ℕ → S Fn n = finSet (suc n) (λ i → fst (e (toℕ i))) , FinOf.finSetL entryBound entryBound-ord (suc n) (λ i → fst (e (toℕ i))) (λ 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 ∈ fst (Fn n) ⟩) (prʟ-fst (nn k) (it k)) (finSet-in (suc n) (λ i → fst (e (toℕ i))) (fst (e k)) ∣ fromℕ' (suc n) k (suc-≤-suc p) , cong (λ j → fst (e j)) (toFromId' (suc n) k (suc-≤-suc p)) ∣₁)
外向きの読み出しは、すべての要素を、有界な添字とその反復の値へ分解します。どちらも切り詰めの下で復元されます。
Fn-out : (n : ℕ) (y : S) → ⟨ y ∈ˢ Fn n ⟩ → ∥ Σ[ k ∈ ℕ ] ((k ≤ n) × (fst y ≡ pr (# k) (fst (it k)))) ∥₁ Fn-out n y h = PT.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 → fst (e (toℕ i))) (fst y) h)
対の読み出しは、Kuratowski の対の単射性を使って、有限の表のどの項目も、有界な添字とその反復の値へ分解します。
Fn-pair : (n : ℕ) (x v : S) → Holds (Fn n) x v → ∥ Σ[ k ∈ ℕ ] ((k ≤ n) × ((fst x ≡ # k) × (fst v ≡ fst (it k)))) ∥₁ Fn-pair n x v h = PT.map (λ { (k , (p , q)) → k , (p , pr-inj (sym (prʟ-fst x v) ∙ q)) }) (Fn-out n (prʟ x v) (subst (λ w → ⟨ w ∈ fst (Fn n) ⟩) (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 = PT.rec (setIsSet (fst v) (fst a))
零点の条項では、nn 0 にある項目を読むと、数項が # 0 に等しい添字 k が得られる。数項の符号化の単射性から k = 0 となり、同時に得られた値の等式によって、記録された値は it 0 = a と同一視される。
(λ { (k , (_ , (ex , ev))) → ev ∙ cong (λ j → fst (it j)) (sym (#-inj 0 k ex)) }) (Fn-pair n (nn 0) v h)
ステップの節では、二つの表項目を命題的切り詰めの内側で読み出す。stepFo の充足は命題なので、二つの切り詰めをこの目標へ消去できる。残るのは、二つの添字が連続していることと、それぞれの値が対応する反復であることを示す作業である。
stepC : Step (Fn n) stepC x v x' v' hxv hx'v' s = PT.rec (snd ((v' ∷ v ∷ []) ⊨ stepFo)) outer (Fn-pair n x v hxv) where outer : Σ[ k ∈ ℕ ] ((k ≤ n) × ((fst x ≡ # k) × (fst v ≡ fst (it k)))) → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
最初の読み出しで k が現れた後、二つ目の読み出しから隣接する行の添字 k' が得られる。二つの証人を、命題である充足判断への消去の内側に保つことで、切り詰めの境界を守りながら、添字と値の等式を同時に利用できる。
outer (k , (_ , (ex , ev))) = PT.rec (snd ((v' ∷ v ∷ []) ⊨ stepFo)) inner (Fn-pair n x' v' hx'v') where inner : Σ[ k' ∈ ℕ ] ((k' ≤ n) × ((fst x' ≡ # k') × (fst v' ≡ fst (it k')))) → ⟨ (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 → fst (it j)) 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 = PT.rec squash₁ outer (Fn-pair n x' v' h) where outer : Σ[ k' ∈ ℕ ] ((k' ≤ n) × ((fst x' ≡ # k') × (fst v' ≡ fst (it k')))) → ∥ Σ[ v ∈ S ] Holds (Fn n) x v ∥₁
より小さい添字の項目は、有限の表の内向きの読み出しによって作られ、数項の等式に沿って運ばれます。
outer (k' , (p' , (ex' , _))) = PT.map (λ { (j , (j< , ej)) → it j , subst (λ t → ⟨ pr t (fst (it j)) ∈ fst (Fn n) ⟩) (sym ej) (Fn-in n j (≤-trans (<-weaken j<) p')) }) (∈#-elim k' (fst x) (subst (λ w → ⟨ fst x ∈ 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 = PT.map (λ { (i , p) → lower i , S≡ p })
ここまでで itFo を、内部集合 ωʟ 上の全域かつ一価な関係とみなせる。レコード valR はこの定義域とグラフを、残る関数性の証明とともにまとめる。このレコードに置換を適用することで、それらの値を L の中に集められる。
private valR : Recursion valR = record { dom = ωʟ ; graph = itFo
関数性は、単に存在するだけの数項の表示から組み立てられます。復号が反復の値を産出し、一意性は、復号された数項で証明されます。
; funct = λ q q∈ → mereFunct itFo q (PT.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 : ℕ) → ⟨ fst (it n) ∈ fst values ⟩ values-in n = VR.table-in (nn n) (it n) (#∈ω n) (it-graph n)
値の領域のすべての要素は、単に、なんらかの反復の値です。外向きの読み出しが数項の表示と反復の論理式の充足を復元し、一意性の補題が値を同定します。
values-out : (y : S) → ⟨ y ∈ˢ values ⟩ → ∥ Σ[ n ∈ ℕ ] (fst y ≡ fst (it n)) ∥₁ values-out y hy = PT.rec squash₁ (λ { (q , (q∈ , h)) → PT.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) → ⟨ fst z ∈ fst (it n) ⟩ → ⟨ z ∈ˢ iterUnion ⟩ iterUnion-in n z hz = unionʟ-in values z (it n) (values-in n) hz
合併のすべての要素は、単に、ある有限の反復の中にあります。証明は、合併の所属を消去して中間の集合を見つけ、それを構成可能として包み、値の領域の外向きの読み出しで読みます。
iterUnion-out : (z : S) → ⟨ z ∈ˢ iterUnion ⟩ → ∥ Σ[ n ∈ ℕ ] ⟨ fst z ∈ fst (it n) ⟩ ∥₁ iterUnion-out z h = PT.rec squash₁ (λ { (B , (hB , hz)) → PT.map (λ { (n , eB) → n , subst (λ w → ⟨ fst z ∈ w ⟩) eB hz }) (values-out (B , isL-trans {x = fst values} {y = B} hB (snd values)) 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) (fst (it n)) ∈ fst iter ⟩ iter-in n = subst (λ v → ⟨ pr (# n) (fst v) ∈ fst iter ⟩) (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 ∈ ℕ ] (fst y ≡ pr (# n) (fst (it n))) ∥₁ iter-out y hy = PT.rec squash₁ (λ { (q , q∈ , e) → PT.map (λ { (k , eq) → k , e ∙ cong₂ pr (cong fst (sym eq)) (cong fst (VR.val-uniq q q∈ (it k) (itFo-at (it k) eq (it-graph k)))) }) (ω-num q q∈) })
一般の関数グラフの外向き所属規則から、まず始域の要素 q ∈ ωʟ と、その一意な値を含む符号化された対が得られる。q を数項として復号し、値の一意性を使えば、主張された標準的な対になる。自然数の添字は最後まで命題的切り詰めの内側に保たれる。
(TR.F-out (fst y) hy)
成長のモジュールは、「すべての集合が自分自身のステップの中に含まれる」という仮定によってパラメータづけられます。
module Closure (grows : (x z : S) → ⟨ fst z ∈ fst x ⟩ → ⟨ fst z ∈ fst (step x) ⟩) where
成長の仮定から、隣り合う反復の間の一方向の包含が得られる。すなわち it n の各要素は it (suc n) にも属する。この主張から逆向きの包含、不動点性、あるいは iterUnion の step による閉性は導かれない。
it-mono : (n : ℕ) (z : S) → ⟨ fst z ∈ fst (it n) ⟩ → ⟨ fst z ∈ fst (it (suc n)) ⟩ it-mono n z = grows (it n) z
隣接する段階の包含を k 回繰り返すと、it n ⊆ it (k + n) が得られる。帰納するのは追加するステップ数なので、この結果は明示された有限個のステップだけ離れた二つの段階を比較する。step が任意の包含に関して単調であることも、それらの和集合が何らかの閉性をもつことも主張していない。
it-up : (n k : ℕ) (z : S) → ⟨ fst z ∈ fst (it n) ⟩ → ⟨ fst z ∈ fst (it (k + n)) ⟩ it-up n zero z h = h it-up n (suc k) z h = it-mono (k + n) z (it-up n k z h)