Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ構成は任意の宇宙レベルで行い、表示された後続レベルでの排中律だけを仮定する。後で得られる関係集合が引き継ぐのは、ちょうどこの仮定である。
module L.Choice.InternalWellOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
各構成可能段階では、orderAt がその要素上のホスト側の狭義整列順序をすでに与えている。この章の課題は、その基礎となる比較を L で解釈される論理式からも使えるようにすることである。各順序数段階について、順序対の所属が relOf (orderAt α oα) と対ごとに両方向で対応する関係集合を得る。ここで新しい整列順序を構成することも、この関係が整列順序であると述べる対象言語の論理式を証明することもない。
この章では二つの水準を一貫して区別する。整列順序はホスト理論の数学的構造であるが、L の内部でそれを表すものは、一階言語から指すことのできる集合でなければならない。
一回の比較ステップを内部で記述するには、変数と定数を、所属・等号・連言・存在量化で結べば十分である。以下の六つの存在束縛は、同じ論理構成子を繰り返し用いたものである。
この関係は順序数段階を添字とする。そのため、証人は構成可能集合として同定され、後続段階への所属は直前の段階上での定義可能性と結び付けられなければならない。
意味論的な目標には二つの水準がある。orderAt δ od は、Lset δ の要素上のホスト側の狭義整列順序である。その再帰的記述で用いる同じ誕生段階のステップについて、Under δ (stepOrder δ od) u v は、u と v が Lset (sucV δ) に属することと、そこから得られる二要素が stepOrder δ od で関係づけられることを記録する。Lset δ 上の最小名が、このホスト側のステップを以下で構成する論理式へ結び付ける。
再帰的な順序表には、妥当なステップ記述から関係集合を作る仕組みがすでにある。残る仕事は、具体的な論理式を一つ与えてその意味論的な二方向を証明し、抽象的なステップ引数への順序表の依存を取り除くことである。
この論理式は、段階の塔、その定義可能部分集合、段階における表の値、塔上のコードという四つの変動する対象を同定しなければならない。これらの同定条件により、任意の充足する割り当てを意図した数学的データへ戻せる。
さらに二つの証人は固定された定数である。コード上の比較関係と、空のアルファベットに対するコード集合である。これらは順序表から得る変動する関係値とともに、最小名を比較するための補助関係と領域を与える。
充足関係は構成可能集合の命題的構造で解釈される。したがって、各存在節は命題的に切り詰められた依存対を生む。証人は証明を支えるが、命題の外で選択済みのデータとして取り出すことはできない。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
比較は後続段階の要素の間で行われる。段階を小さい型で表示することで、ホスト側の整列順序をその要素に作用させられる。sucV は、比較される二対象を位置付ける後続順序数を記録する。
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
using ( module InfinitySet )
open InfinitySet using ( sucV )
ここから先、論理式は L が備える一階構造で解釈される。したがって、スロットに置く要素は、その基礎集合と、その集合が構成可能であるという命題の両方を含む。
open hPropView 𝒮ʟ
以下では、この解釈を γ ⊨ φ と書く。絶対性によって、同定論理式を基礎集合についての具体的事実として読めるため、後で証人を読み解くことができる。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
記述が束縛する要素
六つの枠のずらしは、すべての変数を、ステップの論理式の六つの証人の向こう側へ運ぶ。
private
sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
sh6 i = suc (suc (suc (suc (suc (suc i)))))
六つの証人をすべて束縛した後、StepAt はそのうち五つを直接参照する。塔 tw、表の関係 rl、コード集合 cs、コード順序 ro、空のアルファベットのコード集合 c0 である。定義可能冪集合の証人 pw は周囲の所属条件で使われ、StepAt には渡されない。
iTow iRel iCod iOrd iNil
: ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n))))))
iTow = suc (suc (suc (suc (suc zero))))
iRel = suc (suc (suc zero))
iCod = suc (suc zero)
最も内側の二つの添字は ro と c0 を選ぶ。新たな束縛を導入するのではなく、すでに束縛された二つの証人が、完全に拡張された環境のどこにあるかを記録するだけである。
iOrd = suc zero
iNil = zero
ステップの論理式
Stp d f u v の六つの証人は、依存関係に従う順序で導入される。最初は d が指す段階の塔であり、次はその定義可能冪集合である。後者への所属条件が、u と v の指す対象を後続段階で比較できることを保証する。
opaque
Stp : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
Stp d f u v =
∃̇ ( LsetGraphAt zero (suc d)
∧̇ ∃̇ ( DefAt zero (suc zero)
第三の証人は、その段階で順序表に記録された値 rl であり、第四の証人は塔上のコード集合である。最後の二証人は対象言語の等号で制約される変数で、それぞれ正準なコード順序と空のアルファベットに対するコード集合に固定される。
∧̇ ( (var (sh2 u) ∈̇ var zero)
∧̇ ( (var (sh2 v) ∈̇ var zero)
∧̇ ∃̇ ( appAt (sh3 f) (sh3 d) zero
∧̇ ∃̇ ( CodesAt zero (sh3 zero)
∧̇ ∃̇ ( (var zero ≐ con codeOrder)
最内部では、StepAt は七つの意味論的スロットを見る。上で選んだ五つの補助証人と、六つの束縛を越えてずらされた二つの元の対象である。そこで述べるのは両者の最小名の比較であり、表現された関係が L の内部で整列順序の論理式を満たすという主張ではない。
∧̇ ∃̇ ( (var zero ≐ con (AllCodes ∅ʟ))
∧̇ StepAt iOrd iRel iTow iCod iNil
(sh6 u) (sh6 v) ) ) ) ) ) ) ) )
六つの束縛を層ごとに扱う
読みのモジュールは、四つの枠・環境・そして解読された段階の順序数性を固定する。ホストの順序がその順序数性を必要とするからである。
module Reading {n : ℕ} (d f u v : Fin n) (γ : Vec S n)
(od : IsOrd ((lookup d γ) .fst)) where
private
δ : V ℓ
δ = (lookup d γ) .fst
ホストの順序は、段階の提示の上に運ばれる。要素の狭義の順序が、小さな索引型の上で使えるのである。
ordW : SWO ⟪ Lset δ ⟫
ordW = carry (Lset δ) (orderAt δ od)
Lset (sucV δ) にある集合の名前は Lset δ 上で作られ、その直前の段階に移された順序 ordW に関してのみ最小名として区別される。述語 IsLeastName は、その名前が与えられた集合を表すことと、それより小さい別の名前がないことの両方を記録する。これが、後続段階の集合と StepAt が用いる名前比較との正確な橋渡しである。
module NM = Naming (Lset δ) ordW
意味論的な目標は、命題的に切り詰められた Under の主張である。そこには二つの後続段階への所属とステップ比較が含まれるが、存在論理式を読むことで分かるのは、そのような証拠が存在することだけである。名前や六つの束縛対象をデータとして選ぶことはない。
Goal : Type (ℓ-suc ℓ)
Goal = ∥ Under δ (stepOrder δ od) ((lookup u γ) .fst) ((lookup v γ) .fst) ∥₁
六つの証人で環境をすべて拡張した後、StepHolds tw pw rl cs ro c0 は、最内部の StepAt 論理式が充足されることそのものである。これは六つの存在の層の内側にある最後の意味論的条件である。各層の証人を命題的切り詰めの下に置くのは周囲の束縛子であり、StepHolds 自体ではない。
opaque
StepHolds : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ)
StepHolds tw pw rl cs ro c0 =
⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ)
⊨ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ⟩
最内部のペイロードは、c0 を固定する等式とステップの充足そのものを含む。これらはペイロード内では通常の連言の証拠であり、命題的切り詰めは外側の存在層によって導入される。
Six : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ)
Six tw pw rl cs ro c0 =
⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con (AllCodes ∅ʟ)) ⟩
× StepHolds tw pw rl cs ro c0
一層外では、ro が正準なコード順序に固定され、適切な c0 の存在は命題的に切り詰められる。等式は意図した基礎集合を定めるが、証明が選択済みの存在証人を公開することはない。
Five : (tw pw rl cs ro : S) → Type (ℓ-suc ℓ)
Five tw pw rl cs ro =
⟨ (ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con codeOrder) ⟩
× ∥ (Σ[ c0 ∶ S ] Six tw pw rl cs ro c0) ∥₁
コード集合の条件は、束縛された塔上の cs を特徴付ける。論理式を読むとき、その妥当性と先に得た塔の同定から cs の基礎集合が定まる。残る内側の証人は、なお命題的切り詰めの下にある。
Four : (tw pw rl cs : S) → Type (ℓ-suc ℓ)
Four tw pw rl cs =
⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩
× ∥ (Σ[ ro ∶ S ] Five tw pw rl cs ro) ∥₁
順序表の適用条件は、rl が復号された段階で記録された何らかの値であることを述べる。読み出す向きでは、rl はそこで記録された任意の値であり得るため、後の関係仮定はそのすべての値を全称的に扱う必要がある。埋める向きでは、与えられた特定の rl を使う。
Three : (tw pw rl : S) → Type (ℓ-suc ℓ)
Three tw pw rl =
⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩
× ∥ (Σ[ cs ∶ S ] Four tw pw rl cs) ∥₁
定義可能冪集合の条件が pw を同定し、続く二つの連言が比較対象をともにそこへ置く。tw と pw が同定されれば、これらの所属は Lset (sucV δ) への所属となり、Under が必要とする二つの領域成分を与える。
Two : (tw pw : S) → Type (ℓ-suc ℓ)
Two tw pw =
⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩
× ( ⟨ (lookup u γ) .fst ∈ pw .fst ⟩
× ( ⟨ (lookup v γ) .fst ∈ pw .fst ⟩
二つの所属の後、残るペイロードは表の値 rl の切り詰められた存在から始まる。最終目標 Goal 自体が命題なので、再利用できる証人の選択を取り出すことなく、各切り詰めをこの目標へ消去できる。
× ∥ (Σ[ rl ∶ S ] Three tw pw rl) ∥₁ ) )
最外部のペイロードは、段階グラフを満たす証人 tw から始まる。順序数性により、この記述は基礎集合の水準で一意なので、任意の充足する tw を Lset δ と同定できる。後続するすべての証人の入れ子の存在は、命題的に切り詰められたままである。
One : (tw : S) → Type (ℓ-suc ℓ)
One tw = ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩
× ∥ (Σ[ pw ∶ S ] Two tw pw) ∥₁
段階におけるステップの妥当性
六つの束縛要素のうち StepAt に入るのは五つだけであり、pw はその外側にある二つの所属条件で使われる。そこで Slots は、塔と符号集合を意図した対象と同一視し、rl が対ごとの表現性 IsRel δ rl をもつと仮定し、ro と c0 を必要な二つの定数に固定する。これらは、先に証明した名前比較の妥当性定理が必要とする条件そのものである。
module Slots (tw pw rl cs ro c0 : S)
(qtw : tw .fst ≡ Lset δ)
(hrel : IsRel δ rl)
(qcs : cs .fst ≡ (AllCodes (LsetS δ od)) .fst)
(qro : ro .fst ≡ codeOrder .fst)
(qc0 : c0 .fst ≡ (AllCodes ∅ʟ) .fst) where
整合の内部では、名前づけの妥当性が段階のもとで具体化され、その局所の一歩の比較が、コードの順序と関係の値のもとで開かれる。関係の表現の両方向が供給される。
private module A6 = At (Lset δ) ((LsetS δ od) .snd) ordW
private module L6 = A6.Least codeOrder rl codeOrder-rep codeOrder-fill
(ixRel-rep δ od rl hrel) (ixRel-fill δ od rl hrel)
これらの保証により、名前比較の定理を完全に拡張された環境で具体化できる。その七つの意味論的スロットは、比較される二対象と、iTow、iRel、iCod、iOrd、iNil が選ぶ五つの補助証人からなる。
private module St = L6.Step iOrd iRel iTow iCod iNil (sh6 u) (sh6 v)
(c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ)
qro refl (Σ≡Prop (λ x → (isL x) .snd) qtw) qcs qc0
第一の対象について、LeastFst t は「t がその最小名である」という主張の局所的な形である。そこに含まれる表示の等式は、IsLeastName の対応する等式とは逆向きである。以下の変換補題は、その等式を反転しながら同じ最小性の主張を保つ。
LeastFst : NM.Name → Type (ℓ-suc ℓ)
LeastFst = St.LeastOf (sh6 u)
LeastSnd は第二の対象について同じ橋渡しを与える。StepAt は最小名の存在だけを述べるのではなく、一方の最小名を他方と比較するので、二つの述語を並行に保つことが必要である。
LeastSnd : NM.Name → Type (ℓ-suc ℓ)
LeastSnd = St.LeastOf (sh6 v)
公開された述語 IsLeastName と妥当性定理は、解釈の等式を互いに逆向きに述べる。パスの対称性で第一の対象の等式を変換し、極小性条件も各競合名の等式を同様に反転して移す。
leastFst-in : (t : NM.Name)
→ IsLeastName δ ordW t ((lookup u γ) .fst) → LeastFst t
leastFst-in t (q , mn) = sym q , λ t' q' → mn t' (sym q')
第二の対象の変換も同じ形である。変わるのは等式の向きだけであり、最小性の数学的内容は保たれる。
leastSnd-in : (t : NM.Name)
→ IsLeastName δ ordW t ((lookup v γ) .fst) → LeastSnd t
leastSnd-in t (q , mn) = sym q , λ t' q' → mn t' (sym q')
読み出す向きでは、同じ対称性によって第一の対象の IsLeastName を回復する。パスを二度反転すれば元の向きに戻るので、この変換で情報は失われない。
leastFst-out : (t : NM.Name)
→ LeastFst t → IsLeastName δ ordW t ((lookup u γ) .fst)
leastFst-out t (q , mn) = sym q , λ t' q' → mn t' (sym q')
第二の最小名述語も同じ方法で読み戻され、ホスト側のステップ補題に渡せる二つの通常の最小名の事実が得られる。
leastSnd-out : (t : NM.Name)
→ LeastSnd t → IsLeastName δ ordW t ((lookup v γ) .fst)
leastSnd-out t (q , mn) = sym q , λ t' q' → mn t' (sym q')
最内部の論理式に対する二つの意味論的な向きは、意図的に非対称である。二つの具体的な最小名とその比較が与えられると、holds-in は StepHolds を証明する。逆に holds-out が StepHolds から返すのは、適切な二つの最小名とその比較が存在することの命題的切り詰めだけであり、選ばれた名前の組が論理式の外へ出ることはない。
opaque
unfolding StepHolds
内向きでは、t₁ と t₂ についての局所的な最小名の事実と t₁ ≺ₙ t₂ を合わせると、最内部の論理式に必要な意味論的内容がすべて揃う。名前比較の妥当性定理は、まさにこの三つの事実を StepHolds へ移す。
holds-in : (t₁ t₂ : NM.Name) → LeastFst t₁ → LeastSnd t₂ → t₁ NM.≺ₙ t₂
→ StepHolds tw pw rl cs ro c0
holds-in = St.StepAt-fill
逆に、最内部の充足を読むと、命題的切り詰めの下で二つの最小名とその名前比較が得られる。この切り詰めは本質的である。結果は適切な名前の存在を述べるが、選択済みの一対を公開しない。
holds-out : StepHolds tw pw rl cs ro c0
→ ∥ Σ[ t₁ ∶ NM.Name ] Σ[ t₂ ∶ NM.Name ]
(LeastFst t₁ × (LeastSnd t₂ × (t₁ NM.≺ₙ t₂))) ∥₁
holds-out = St.StepAt-read
束縛を読み解く
全体の読み出しは、充足する割り当てが与えるどの六証人に対しても働かなければならない。最初の仮定は、tw が復号された段階のグラフ記述を満たし、pw がその上の定義可能冪集合の記述を満たし、第一の比較対象が pw に属することを述べる。後で一意性と妥当性を使い、これらを具体的な段階についての事実へ変換する。
private
atAll : (tw pw rl cs ro c0 : S)
→ ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩
→ ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩
→ ⟨ (lookup u γ) .fst ∈ pw .fst ⟩
続く仮定は、第二の所属、順序表の適用、コード集合の記述を与える。特に、関係についての前提は、順序表が δ で記録するすべての r に及ぶ。読み出す向きでは、存在論理式がそのどの rl を束縛していてもよいからである。ここで最後に現れる等式は、ro を正準なコード順序に固定する。
→ ⟨ (lookup v γ) .fst ∈ pw .fst ⟩
→ ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩
→ ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩
→ ((r : S) → ⟨ pr δ (r .fst) ∈ (lookup f γ) .fst ⟩ → IsRel δ r)
→ ro .fst ≡ codeOrder .fst
外向きの議論は、ここで最内側の条件に到達する。六つの存在証人を同定すると、atAll は StepAt の充足から、二つの最小の名前とその名前比較が単に存在することを読み出す。次の議論をこの命題的切り詰めの上で写すことで、切り詰めの外へ名前を選び出すことなく、名前比較を必要なホスト側の Under 比較へ変換する。
→ c0 .fst ≡ (AllCodes ∅ʟ) .fst
→ StepHolds tw pw rl cs ro c0 → Goal
atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep =
map₁ atNames (K.holds-out hstep)
where
塔の同定の等式が、論理式で束縛された塔が、入力の順序数での構成可能な段階に等しいことを、層の妥当性の補題で読み出す。
qtw : tw .fst ≡ Lset δ
qtw = Lset-only zero (suc d) (tw ∷ γ) hg od
定義可能な部分集合の同定が、束縛された集合がその段階の定義可能冪集合であることを、塔の等式に沿って述べる。
qpw : pw .fst ≡ 𝒟ₒ (Lset δ)
qpw = subst ⟨_⟩ (DefAt-stage δ od zero (suc zero) (pw ∷ tw ∷ γ) qtw) hdef
後続の段階への所属は、二度の輸送によって復元される。最初の輸送が、構成可能な層の後続の恒等式を使って、定義可能冪集合と後続の段階を同一視する。二つ目の輸送が、束縛された集合がその定義可能冪集合と等しいという等式に沿って書き換える。二つ合わせて、比較される対象を後続の段階 Lset (sucV δ) の中に置く。
inSuc : (x : V ℓ) → ⟨ x ∈ pw .fst ⟩ → ⟨ x ∈ Lset (sucV δ) ⟩
inSuc x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (Lset-suc δ))
(subst (λ z → ⟨ x ∈ z ⟩) qpw h)
最初の比較の候補は、枠 u の基礎の集合であり、復元の補題によって後続の段階の要素として提示される。
a : New δ
a = (lookup u γ) .fst , inSuc ((lookup u γ) .fst) hu
二つ目の比較の候補は、枠 v の基礎の集合で、同様に提示される。
b : New δ
b = (lookup v γ) .fst , inSuc ((lookup v γ) .fst) hv
適用論理式の充足は、rl が表の δ に記録された値であることを述べる。外向きの仮定 vals は、そのように記録されたすべての値を意図的に対象とするため、Stp の内部で選ばれたこの証人についても IsRel δ rl を与える。これは可能な表の証人すべてに対する健全性の条件であり、表の値の一意性を主張するものではない。
hrel : IsRel δ rl
hrel = vals rl
(subst ⟨_⟩ (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ pw ∷ tw ∷ γ)) happ)
符号集合の記述を外向きに読むと、cs は AllCodes (LsetS δ od)、すなわち現在の段階 Lset δ 上の符号集合と同一視される。比較される対象は後続段階に属するが、その名前は直前の段階に関して作られるので、ここでの符号集合は sucV δ ではなく δ で添字づけられる。
qcs : cs .fst ≡ (AllCodes (LsetS δ od)) .fst
qcs = cong (λ p → p .fst) (CodesAt-out (LsetS δ od) zero (sh3 zero)
(cs ∷ rl ∷ pw ∷ tw ∷ γ) qtw hcs)
塔、段階関係、符号集合、二つの固定された符号対象がすべて同定されたので、Slots は六つの証人を、すでに証明された名前比較の妥当性定理へ接続する。この共通の具体化により、残りの議論では最内側の論理式と対応する最小名のデータを相互に読み替えられる。
module K = Slots tw pw rl cs ro c0 qtw hrel qcs qro qc0
名前の妥当性定理が返す命題的切り詰めの内部で、t₁ と t₂ を比較される二つの集合の最小名とし、t₁ ≺ₙ t₂ とする。目標の Under は最後の比較だけでなく、二つの集合がともに Lset (sucV δ) に属することも記録する。この二つの所属成分は、すでに a と b によって得られている。
atNames : Σ[ t₁ ∶ NM.Name ] Σ[ t₂ ∶ NM.Name ]
( K.LeastFst t₁ × ( K.LeastSnd t₂ × (t₁ NM.≺ₙ t₂) ) )
→ Under δ (stepOrder δ od) ((lookup u γ) .fst) ((lookup v γ) .fst)
atNames (t₁ , (t₂ , (l₁ , (l₂ , lt)))) =
a .snd
二つの最小名についての外向きの読みは、局所的な述語を IsLeastName へ戻す。続いて stepAt-fill は、これらの最小名の比較から、それらが表す新しい要素の間の stepOrder δ od 関係が従うことを示す。直前に得た二つの所属と合わせて、Under が完成する。
, ( b .snd
, stepAt-fill δ ordW a b t₁ t₂
(K.leastFst-out t₁ l₁) (K.leastSnd-out t₂ l₂) lt )
束縛を組み立てる
逆向きの議論では、実際の表の値 rl と、それが表の δ に記録され、必要な段階関係を表すことの証拠を固定する。さらに、Under 比較が含む二つの後続段階への所属も固定する。外向きの場合と異なり、この構成では具体的な局所表の値が手元にあるため、それを Stp の三番目の存在証人として使える。
module Pack (rl : S) (hpr : ⟨ pr δ (rl .fst) ∈ (lookup f γ) .fst ⟩)
(hrel : IsRel δ rl)
(hx : ⟨ (lookup u γ) .fst ∈ Lset (sucV δ) ⟩)
(hy : ⟨ (lookup v γ) .fst ∈ Lset (sucV δ) ⟩)
where
組み立てる議論では、Stp が定める順序で六つの証人を使う。すなわち towerS δ od、powS δ od、与えられた表の値 rl、AllCodes (LsetS δ od)、codeOrder、AllCodes ∅ʟ である。特に第四の証人は現在の段階 Lset δ 上の符号集合であり、その後続段階に属するのは比較される二つの対象である。
private module K = Slots (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od))
codeOrder (AllCodes ∅ʟ) (towerS-fst δ od) hrel refl refl refl
最初の比較の候補は、後続の段階での所属によって提示される。
private
a : New δ
a = (lookup u γ) .fst , hx
二つ目の比較の候補も同じように提示される。
b : New δ
b = (lookup v γ) .fst , hy
固定されたホスト側の整列順序 ordW に関して、各新要素には最小名があるので、最初の候補から名前とその IsLeastName の証明の組が得られる。これは論理式を満たすための明示的で局所的な証人であり、Stp が名前を一意に定めると主張するものではない。
n₁ : Σ[ t ∶ NM.Name ] IsLeastName δ ordW t ((lookup u γ) .fst)
n₁ = leastNameOf δ ordW a
同じ定理から、二つ目の候補についても最小名が得られる。局所的に選んだ二つの名前を比較し、StepAt の内向きの妥当性定理へ渡す。その論理式の存在の意味論と、それを囲む Stp の六つの存在束縛子によって、名前は再び隠される。この構成が選ばれた名前の組を外へ出すことはない。
n₂ : Σ[ t ∶ NM.Name ] IsLeastName δ ordW t ((lookup v γ) .fst)
n₂ = leastNameOf δ ordW b
最初の証人には towerS δ od を取る。その定義定理は、これが拡張された環境で LsetGraphAt を満たし、したがって第一の束縛子が要求する Lset δ を基礎集合にもつことを示す。
hg : ⟨ (towerS δ od ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩
hg = Lset-defines zero (suc d) (towerS δ od ∷ γ) od (towerS-fst δ od)
二つ目の証人は powS δ od であり、その基礎集合は定義可能部分集合の集合 𝒟ₒ (Lset δ) である。DefAt-stage が与える等式は DefAt の充足を特徴づける。この特徴づけに沿って powS-fst を輸送すると、必要な充足の主張が得られる。ここで使うのはこの段階の定義可能部分集合の集合であり、完全な冪集合ではない。
hdef : ⟨ (powS δ od ∷ towerS δ od ∷ γ) ⊨ DefAt zero (suc zero) ⟩
hdef = subst ⟨_⟩
(sym (DefAt-stage δ od zero (suc zero)
(powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od)))
(powS-fst δ od)
Stp の二つの所属の連言を満たすため、ここで必要なのは後続段階から選ばれた定義可能部分集合の対象へ向かう向きである。等式 Lset-suc δ により、Lset (sucV δ) への所属を 𝒟ₒ (Lset δ) への所属へ書き換え、さらに powS-fst により、それを powS δ od の基礎となる集合への所属へ書き換える。
inPow : (x : V ℓ) → ⟨ x ∈ Lset (sucV δ) ⟩ → ⟨ x ∈ (powS δ od) .fst ⟩
inPow x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (powS-fst δ od))
(subst (λ z → ⟨ x ∈ z ⟩) (Lset-suc δ) h)
適用の充足は、表の項目の証明から、適用の符号化の妥当性に沿って運ばれる。
happ : ⟨ (rl ∷ powS δ od ∷ towerS δ od ∷ γ)
⊨ appAt (sh3 f) (sh3 d) zero ⟩
happ = subst ⟨_⟩
(sym (appAt-adequate (sh3 f) (sh3 d) zero
(rl ∷ powS δ od ∷ towerS δ od ∷ γ))) hpr
第四の証人について、CodesAt の内向きの読みは、AllCodes (LsetS δ od) が塔 Lset δ 上の符号集合の記述を満たすことを示す。後続段階上の符号集合は必要ない。
hcs : ⟨ (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ)
⊨ CodesAt zero (sh3 zero) ⟩
hcs = CodesAt-in (LsetS δ od) zero (sh3 zero)
(AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ)
(towerS-fst δ od) refl
ホスト側の stepOrder 比較を仮定する。すでに選んだ二つの最小名は、内向きの等式の向きを調整すると、局所的な最小名述語を満たす。残るのは、ホスト側の比較を最内側の StepAt 論理式が要求する名前比較へ変換することだけである。
hstep : relOf (stepOrder δ od) a b
→ StepHolds (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od))
codeOrder (AllCodes ∅ʟ)
hstep cmp = K.holds-in (n₁ .fst) (n₂ .fst)
(K.leastFst-in (n₁ .fst) (n₁ .snd)) (K.leastSnd-in (n₂ .fst) (n₂ .snd))
定理 stepAt-read は、n₁ と n₂ の最小性の証明を使って、ちょうどこの変換を行う。得られた名前比較を holds-in に渡すと、最内側の充足が証明される。この議論は既存のホスト側の stepOrder を用いるのであり、新しい整列順序を構成するものではない。
(stepAt-read δ ordW a b (n₁ .fst) (n₂ .fst) (n₁ .snd) (n₂ .snd) cmp)
対象言語の六つの存在量化は、依存対の命題的切り詰めが六重に入れ子になったものとして解釈される。packAll は towerS δ od とその LsetGraphAt の証明から、この入れ子を組み始める。証明の内部では具体的な証人を構成するが、最も外側の存在の境界では、その命題的切り詰めだけが直ちに残る。
packAll : relOf (stepOrder δ od) a b → ∥ (Σ[ tw ∶ S ] One tw) ∥₁
packAll cmp =
∣ towerS δ od
, ( hg
, ∣ powS δ od
第二の証人は powS δ od であり、DefAt の充足と、後続段階から輸送した二つの所属が付随する。第三の証人は与えられた表の値 rl であり、その順序対の所属証明から必要な appAt の充足が得られる。したがって、埋める向きでは、表から値を選ぶのではなく、呼び出し側がすでに与えた特定の関係値を使う。
, ( hdef
, ( inPow ((lookup u γ) .fst) hx
, ( inPow ((lookup v γ) .fst) hy
, ∣ rl
, ( happ
符号の集合の充足のあとに、符号の順序の要素とその同定の等式が続き、さらに空のアルファベットの符号の集合が続く。
, ∣ AllCodes (LsetS δ od)
, ( hcs
, ∣ codeOrder
, ( refl
, ∣ AllCodes ∅ʟ
最後の包み込みでは、空のアルファベットの符号集合、それを同定する等式、最内側のステップ論理式の充足を挿入する。六つの切り詰めをすべて閉じることで Stp が証明されるが、選んだ塔、関係、符号、名前の証人は後の利用者へ公開されない。
, ( refl , hstep cmp ) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁ ) ) ) ∣₁ ) ∣₁
二つの読み
二つの読みは、再帰的な表が必要とする正確なインターフェースを与え、その型が本質的な非対称性を記録する。外向きは、その段階で記録されたすべての関係値を扱わなければならず、返すのは ∥ Under ... ∥₁ だけである。内向きは、指定された一つの記録済みの値とその IsRel の証明、さらに切り詰められていない Under の比較を受け取り、そこから Stp の充足を構成する。
opaque
unfolding Stp StepHolds
外向きの読みでは、表の δ に記録されたすべての値が必要な段階関係を表すと仮定する。Stp の充足が与える存在証人は命題的に切り詰められているため、read は六つの切り詰めを一つずつ、同じく命題的に切り詰められた Goal へ除去する。
read : ((r : S) → ⟨ pr δ (r .fst) ∈ (lookup f γ) .fst ⟩ → IsRel δ r)
→ ⟨ γ ⊨ Stp d f u v ⟩ → Goal
read vals = rec₁ squash₁
(λ { (tw , (hg , hpw)) → rec₁ squash₁
(λ { (pw , (hdef , (hu , (hv , hrl)))) → rec₁ squash₁
除去は束縛子の順、すなわち塔、定義可能部分集合の集合、表の値、符号集合、符号順序、空のアルファベットの符号集合の順に進む。各段階の証人は次の切り詰めを扱う継続の内部でだけ利用でき、選択された六つ組が返されることはない。
(λ { (rl , (happ , hcs)) → rec₁ squash₁
(λ { (cs , (hcs , hro)) → rec₁ squash₁
(λ { (ro , (qro , hc0)) → rec₁ squash₁
(λ { (c0 , (qc0 , hstep)) →
atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep })
六つの証人とその条件が局所的にすべて揃うと、atAll は命題的に切り詰められた Under 比較を返す。その後、入れ子の除去子が構文とは逆の順で閉じられ、対象言語の存在量化が要求する切り詰めの境界が保たれる。
hc0 }) hro }) hcs }) hrl }) hpw })
内向きの読み出しは、特定の表の値と、その所属と関係の証明と、二つの所属の証明とホスト側の比較を消費して、すべてを六重の存在量化の中にまとめる。
fill : (r : S) → ⟨ pr δ (r .fst) ∈ (lookup f γ) .fst ⟩ → IsRel δ r
→ Under δ (stepOrder δ od) ((lookup u γ) .fst) ((lookup v γ) .fst)
→ ⟨ γ ⊨ Stp d f u v ⟩
fill r hpr hrel (hx , (hy , cmp)) = Pack.packAll r hpr hrel hx hy cmp
ステップの論理式の外向きの読み出しが、最初の妥当性の方向として書き出される。充足が、切り詰められたステップの比較を含意する、というものである。
stp-out : StpOut Stp
stp-out = Reading.read
フレームを具体化する
ステップの論理式の内向きの読み出しが、二つ目の妥当性の方向として書き出される。正しい関係をもつ特定の表の値とホスト側の比較が合わせて、論理式の充足を含意する、というものである。
stp-in : StpIn Stp
stp-in = Reading.fill
Stp とこの二つの読みを抽象的な構成へ与えることで、段階順序の表が完全に具体化される。とくに各順序数段階について内部集合 relL と relL-fill、relL-rep が得られ、orderAt のホスト側の関係と、対応する順序対が relL に属することを要素ごとに相互変換できる。ここで得られるのは関係グラフの表現であり、relL が整列順序の論理式を満たすという対象言語の主張は証明されていない。
open Ordered Stp stp-out stp-in public
上界順序数における順序
構成可能集合 a に対し、stageBound は ω と a が最初に現れる段階の両方より上にある順序数を選ぶ。したがって Lset boundOrd は、a の要素と、さらにそれらの要素を含むのに十分高く、後の横断集合の議論に必要な局所的な論域となる。選ばれた上界はこの目的には十分であるが、a に対する最小の上界または一意に定まる上界だとは主張しない。
module Bound (a : V ℓ) (p : ⟨ isL a ⟩) where
boundOrd : V ℓ
boundOrd = stageBound a p .fst
同じ上界の結果は、boundOrd が順序数であることも証明する。この証明により、すでに構成されているホスト側の族 orderAt を段階 Lset boundOrd に特殊化できる。
boundOrd-ord : IsOrd boundOrd
boundOrd-ord = stageBound a p .snd .fst
この添字で内部の関係対象を得るには、表の構成は添字自身が構成可能であることも必要とする。順序数は自分自身の後続段階に属するので、boundOrd ∈ Lset (sucV boundOrd) が、Lset→isL によって isL boundOrd を示すための証人になる。
boundOrd-isL : ⟨ isL boundOrd ⟩
boundOrd-isL = Lset→isL (sucV boundOrd) (suc-ord boundOrd-ord) boundOrd
(ord∈Lset-suc boundOrd boundOrd-ord)
表現する関係は、すでに存在するホスト側の狭義整列順序 orderAt boundOrd boundOrd-ord であり、その台は Mem (Lset boundOrd) である。整列順序の構造はこの SWO 値が持っており、以下の行はその二項関係を L の内部の集合として実現するだけである。
boundOrder : SWO (Mem (Lset boundOrd))
boundOrder = orderAt boundOrd boundOrd-ord
表は、選ばれた順序数におけるこの内部集合を relL として与える。したがって orderL はモデルの要素であり、その要素は関係グラフの順序対を表す。これは新しい整列順序の構成ではなく、整列順序の公理を対象理論の内部で満たすという証明も、ここでは付与されない。
orderL : S
orderL = relL boundOrd boundOrd-isL boundOrd-ord
順方向の表現補題は、ホスト側の比較 relOf boundOrder x y から、符号化された順序対 pr (x .fst) (y .fst) を orderL に入れる。これにより、既存の SWO の関係とその内部グラフとの要素ごとの対応の一方向が得られる。
orderL-fill : (x y : Mem (Lset boundOrd)) → relOf boundOrder x y
→ ⟨ pr (x .fst) (y .fst) ∈ orderL .fst ⟩
orderL-fill = relL-fill boundOrd boundOrd-isL boundOrd-ord
逆に、符号化された順序対が orderL に属することから、ホスト側の比較を復元できる。orderL-fill と orderL-rep を合わせると、どの順序対が内部の関係グラフに現れるかが要素ごとに正確に特徴づけられる。これらは、そのグラフを表す集合の一意性を主張せず、それが整列順序であることを対象言語の内部で証明するものでもない。
orderL-rep : (x y : Mem (Lset boundOrd))
→ ⟨ pr (x .fst) (y .fst) ∈ orderL .fst ⟩ → relOf boundOrder x y
orderL-rep = relL-rep boundOrd boundOrd-isL boundOrd-ord
まとめ
狭義整列順序そのものは、Mem (Lset α) 上のホスト側の構造 orderAt α oα である。集合 relL α hα oα は、その二項関係を関係グラフとして表す L の要素であり、relL-fill と relL-rep は、各要素対についてその表現の二方向を証明する。六つの束縛子をもつ論理式とその妥当性の読みは、この関係グラフを後の対象言語の論理式から利用できるようにするが、新しい整列順序も、対象言語における整列順序の主張も証明しない。