Bedrock段階順序の記述の妥当性
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップメタ理論には、すでにすべての構成可能な段階で狭義の整列順序がありますが、L の対象言語は論理式を通してしか語れません。この章は、その順序を論理式へ翻訳します。各集合の誕生段階・台とともに動くコードの集合・段階順序の比較の規則を記述し、それらがメタ言語の意味に忠実であることを証明します。ただ一つ、意図的に引数のまま残したものがあります。固定された誕生段階の内部での比較です。
{-# OPTIONS --cubical --safe --guardedness #-}
古典的推論は、明示された一つの仮定 lem を通してだけ入ります。順序数段階を比較するときにこれを用いますが、この章で構成する論理式は対象言語の通常の論理式のままです。したがって、意味論的な議論で排中律を使っても、解釈される言語に新しい公理を加えることにはなりません。
open import Base.Prelude open import Base.Classical using ( LEM )
初めから二つの言語水準を区別しておきます。すでに構成された orderAt は、メタ言語における狭義の整列順序です。ここでの目標は、その基礎にある比較を充足によって表す論理式を作ることです。この章の論理式が SWO 構造を作り直したり、その整礎性を証明し直したりするわけではありません。
module L.Choice.StageOrderAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
この翻訳で使うのは、対象言語の通常の原子式と結合子だけです。所属の原子式は候補となる証人が段階やコード集合に属することを述べ、等号の原子式は表現された二つの対象を同一視し、存在量化は記述に必要な補助集合を隠します。後の証明では、これらの論理式を構成可能な構造で解釈し、得られた命題を対応するメタ言語の命題と比較します。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; Term; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Model {ℓ} using ( ∈sucV-elim )
ここで必要な階層の姿は単純です。順序数は各段階を線形に並べ、順序数の添字どうしの所属は塔を単調にし、ある順序数の後続はその段階と次の定義可能冪の段階を分けます。これらの事実により、候補となる誕生順序数の後続を、集合が初めて現れる段階と比較して、その候補を同定できます。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; IsOrd; isPropIsOrd; Lset-mono; Lset→isL; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( suc-ord; mem-ord ) open import L.Ordinal.Linear {ℓ} lem using ( ord-tri ) open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
構成可能集合 x を含む最初の段階は後続段階であり、birth x はその直前の順序数です。したがって x は Lset (birth x) には属さず、前者の定義可能冪である Lset (sucV (birth x)) には属します。論理式 BirthAt が表すのはこの二つの所属事実であり、最小性そのものはメタ言語の定理から得られます。
open import L.Axioms.Basic {ℓ} using ( Lset-suc; LsetS; 𝒟ₒS; extensionalL ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem; stage-earliest ) open import L.Choice.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj ) open import L.Choice.StageOrders {ℓ} lem using ( birth; birth-ord; birth-suc; birth-mem; birth-stage; birth-proof
既存の段階順序は、二つの要素を誕生段階によって辞書式に比較します。誕生が早ければ比較はそこで決まり、誕生が等しければ、その段階の新しい要素上の局所順序に委ねられます。後で作る論理式は、この一回の展開方程式だけを正確に写します。したがって、その妥当性が対象とするのは orderAt がすでに備える関係であり、順序の構成ではありません。
; Mem; New; relOf; carry; Under; stepAt ; orderAt; orderAt-step; module Family ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate ) open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both )
同じ段階の内部での比較には、共通の誕生順序数とともに変わる台上の論理式が必要です。そのため、使う構文を一つの段階にあらかじめ固定することはできません。以下のコード述語は、変数スロットに置かれた台に相対して、すべての有限アリティを扱い、台とその論理式コードを一緒に動かせるようにします。
open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt ) open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-stage ) open import L.Coding.CodeSet {ℓ} lem using ( arityNumAtL; arityNumAtL-in; arityNumAtL-out; hasWitnessAt ; witnessAt-in; witnessAt-out; keyS; codeS
最終的な目標は、L の中で関係を順序対の集合として表すことです。周囲の段階より下の表が局所関係の値を与え、論理式は符号化された各順序対についてメタ言語の比較と一致しなければなりません。この一致には表の値の正しさと存在の両方が必要であり、局所ステップの論理式について与えられる二方向の妥当性を前提とします。
; AllCodes; AllCodes-in; AllCodes-out; IsKeyOverAny ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Choice.OrderTable {ℓ} lem using ( Ordering; strict; Related; IsRel; Values; Entries ; related-in; module Described )
表現された関係の要素は、コード pr u v として読まれます。したがって妥当性には二つの向きがあります。このような対のコードから比較される要素 u と v を何らかの形で取り出し、その段階順序による比較を示す向きと、既知の比較から対応する対のコードを表現集合に入れる向きです。ここでの存在は命題的切り詰めを受けているため、標準的な分解を選びません。
open import V.Coding {ℓ} using ( pr )
証明では、等しい段階添字や等しい対のコードに沿って関係を何度か輸送します。順序数性と構成可能性の証拠は命題なので、それらの証拠を取り替えても、表現される数学的対象は変わりません。この証明無関係性により、証明書を余分な選択へ変えることなく輸送できます。
import FOL.Absoluteness open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Data.Sigma using ( Σ≡Prop )
存在量化の充足は一貫して命題的切り詰めを受けています。段階の値、定義可能冪の値、復号された論理式、表の項を証明で使えるのは、行き先も命題である場合だけです。したがって、以下の除去から標準的な証人、選ばれた復号器、局所関係の値を割り当てる選択関数が得られることはありません。
import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
ここには役割の異なる二つの後続構成があります。sucV は順序数段階を一つ進め、数項は階層の内部で有限アリティを符号化します。両者を区別することで、集合が誕生段階の後続で現れるという事実と、論理式コードのアリティ成分とを混同せずに済みます。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( sucV; #_ )
論理式は構成可能な構造 𝒮ʟ で解釈されるため、その意味は命題値です。充足は、記述された所属・等号・存在が L の内部で成り立つかを記録し、それらの意味を比較する証明は、周囲の Cubical Agda のメタ理論に属します。
open hPropStructure 𝒮ʟ
環境における論理式の充足を γ ⊨ φ、項の値を ⟦ t ⟧ γ と書きます。この記法が、すべての妥当性の主張を結ぶ橋です。左辺は対象言語の構文を読み、右辺はメタ理論における対応する集合・順序数・関係を同定します。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ; ⟦_⟧ᵐ to ⟦_⟧ )
最初のずらしは、変数を二つ外の枠に名前づけし、四つの対象を束縛する論理式のための準備をします。
sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i)
二つ目のずらしは、変数を三つ外の枠へ動かします。
sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i))
非公開のずらしは、変数を四つ外の枠へ動かします。次の節で、四つの対象を束縛する論理式のために取っておかれたものです。
private sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n)))) sh4 i = suc (suc (suc (suc i)))
項のずらしは、一つの項を、新しく加わった四つの束縛の向こう側へ運びます。定数はその値を保ち、変数はどれも同じずらしで名前を変えます。
tm4 : ∀ {n} → Term S n → Term S (suc (suc (suc (suc n)))) tm4 (con k) = con k tm4 (var i) = var (sh4 i)
ずらされた項の評価は、新しく加わった四つの束縛の影響を受けません。この定義的な一致は一度記録され、その後は静かに再利用されます。
tm4-val : ∀ {n} (t : Term S n) (a b c d : S) (γ : S ^ n) → ⟦ tm4 t ⟧ (d ∷ c ∷ b ∷ a ∷ γ) ≡ ⟦ t ⟧ γ tm4-val (con k) a b c d γ = refl tm4-val (var i) a b c d γ = refl
Lset β を論理式の環境に置くため、その段階を構成可能性の証明と組にして S の要素にします。順序数性の仮定がこの証明を与えます。数学的に重要なのは、次に示す第一射影の等式です。この包装が表す集合はちょうど Lset β なので、BirthAt を内向きに読む際の段階の証人として使えます。
opaque towerS : (β : V ℓ) → IsOrd β → S towerS β ob = LsetS β ob
まとめられた段階の底の集合は、定義により、その段階そのものです。
towerS-fst : (β : V ℓ) (ob : IsOrd β) → fst (towerS β ob) ≡ Lset β towerS-fst β ob = refl
BirthAt が必要とする第二の証人は、その段階の定義可能冪です。𝒟ₒ (Lset β) も同じように包装します。その構成可能性は順序数 β における段階の事実から従い、第一射影が論理式の要求する集合になります。
powS : (β : V ℓ) → IsOrd β → S powS β ob = 𝒟ₒS β ob
その底の集合は、定義により、その順序数の段階の定義可能冪です。
powS-fst : (β : V ℓ) (ob : IsOrd β) → fst (powS β ob) ≡ 𝒟ₒ (Lset β) powS-fst β ob = refl
誕生段階を内部で述べる
BirthAt b x は二つの補助集合を束縛します。第一の集合は候補スロット b で記述される塔の段階 Lset β であり、x はそこに属しません。第二の集合は第一の集合の定義可能冪であり、x はそこに属します。したがって、この論理式は連続する二段階の境界を表します。β が順序数であるとは主張せず、対象言語内の最小性条件も含みません。
BirthAt : ∀ {n} → Fin n → Fin n → Formula S n BirthAt b x = ∃̇ ( LsetGraphAt zero (suc b) ∧̇ ( ¬̇ (var (suc x) ∈̇ var zero) ∧̇ ∃̇ ( DefAt zero (suc zero) ∧̇ (var (sh2 x) ∈̇ var zero) ) ) )
環境 γ を固定します。候補となる順序数はスロット b の要素の底の集合であり、誕生を調べる集合はスロット x の要素です。以下の議論はすべてこの二つの解釈に相対的なので、定理は特別に選んだ定数ではなく、任意の変数割り当てについて成り立ちます。
module _ {n : ℕ} (b x : Fin n) (γ : S ^ n) where private β : V ℓ β = fst (lookup b γ)
要素 z は、その底の集合と、それが L に属するという証拠をともに持ちます。メタ言語の関数 birth はその証拠を用いて順序数を作りますが、証明無関係性により、得られる順序数が構成可能性の証明の選択を符号化することはありません。
z : S z = lookup x γ
内側の記録は、候補の段階 c の上の定義可能冪の値 d と、冪の記述の充足、そして引数が d に属することを集めます。
Inner : S → Type (ℓ-suc ℓ) Inner c = Σ[ d ∈ S ] ( ⟨ (d ∷ c ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ⟨ fst z ∈ fst d ⟩ )
外側の記録はさらに、上げられた添字のもとでの段階のグラフの充足、引数が候補の段階に属さないことの反証、そして内側の記録の切り詰めを加えます。三つ合わせて、これこそ誕生の論理式が主張することです。
Outer : S → Type (ℓ-suc ℓ) Outer c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ × ( (⟨ fst z ∈ fst c ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥) × ∥ Inner c ∥₁ )
中心となる意味論的補題は、β が順序数であり、x が 𝒟ₒ (Lset β) に属する一方で Lset β には属さないと仮定します。まさにこの境界の事実から β ≡ birth x を示します。順序数性はこの読みへの入力であり、BirthAt の充足から取り出されるものではありません。
decideBirth : IsOrd β → ⟨ fst z ∈ 𝒟ₒ (Lset β) ⟩ → (⟨ fst z ∈ Lset β ⟩ → Empty.⊥) → β ≡ birth (fst z) (snd z) decideBirth ob hin hout = go (ord-tri (sucV β) (suc-ord ob) (stage (fst z) (snd z))
Lset-suc により、𝒟ₒ (Lset β) への所属は Lset (sucV β) への所属に変わります。これは x を含む最初の段階が β の後続より後ではないことを意味しますが、さらに早い可能性をすべて排除する必要があります。
(stage-ord (fst z) (snd z))) where mem : ⟨ fst z ∈ Lset (sucV β) ⟩ mem = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (Lset-suc β)) hin
x の最初の段階が sucV β に属すると仮定します。後続順序数への所属は、その段階が β に属する場合と β に等しい場合に分かれます。前者では単調性により、後者では直接の輸送により、どちらも x が Lset β に属することになり、仮定した非所属に反します。
early : ⟨ stage (fst z) (snd z) ∈ sucV β ⟩ → Empty.⊥ early h = Empty.rec* (∈sucV-elim {A = β} {x = stage (fst z) (snd z)} Empty.isProp⊥* h below same) where below : ⟨ stage (fst z) (snd z) ∈ β ⟩ → Empty.⊥*
stage x ∈ β なら、段階の単調性により、既知の x ∈ Lset (stage x) から x ∈ Lset β が従います。stage x ≡ β なら、その等式に沿う輸送によって同じ結論が直接得られます。どちらも境界の仮定 x ∉ Lset β に反します。
below k = Empty.rec (hout (Lset-mono {α = β} {β = stage (fst z) (snd z)} k {x = fst z} (stage-mem (fst z) (snd z)))) same : stage (fst z) (snd z) ≡ β → Empty.⊥* same e = Empty.rec (hout (subst (λ u → ⟨ fst z ∈ Lset u ⟩) e
等しい場合には、stage x ≡ β に沿って既知の所属 x ∈ Lset (stage x) を x ∈ Lset β へ輸送します。これが、最初の段階が β 以下にはありえないことを示すための第二の矛盾です。
(stage-mem (fst z) (snd z))))
ここで順序数の三岐性により sucV β と stage x を比較します。前者が真に早ければ、x ∈ Lset (sucV β) が stage x の定義上の最小性に反します。stage x が早ければ、直前の議論が x ∉ Lset β に反します。したがって、等しい場合だけが残ります。
go : ⟨ sucV β ∈ stage (fst z) (snd z) ⟩ ⊎ ((sucV β ≡ stage (fst z) (snd z)) ⊎ ⟨ stage (fst z) (snd z) ∈ sucV β ⟩) → β ≡ birth (fst z) (snd z) go (inl h) = Empty.rec (stage-earliest (fst z) (snd z) (sucV β) (suc-ord ob) mem h)
sucV β ≡ stage x と stage x ≡ sucV (birth x) から、順序数の後続の単射性によって β ≡ birth x が得られます。結論は二つの狭義の場合を排除したことで強制されるのであり、論理式から誕生の証人を選んでいるのではありません。
go (inr (inl e)) = ord-suc-inj β (birth (fst z) (snd z)) ob (e ∙ sym (birth-suc (fst z) (snd z))) go (inr (inr h)) = Empty.rec (early h)
読みの補題は、その枠の順序数性の仮定を運びます。論理式だけでは、その枠が順序数であることを証明しません。証明は、切り詰められた存在量化を解いて、外側の記録に到達します。
BirthAt-out : ⟨ γ ⊨ BirthAt b x ⟩ → IsOrd β → β ≡ birth (fst z) (snd z) BirthAt-out h ob = PT.rec (setIsSet β (birth (fst z) (snd z))) atCarrier h where atInner : (c : S) → ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
候補の段階ごとに、内側の記録は、引数を含む定義可能冪の値と、引数が候補の段階に属さないことの反証を供給します。判定の補題が、この三つのデータに適用されます。
→ (⟨ fst z ∈ fst c ⟩ → Empty.⊥) → Inner c → β ≡ birth (fst z) (snd z) atInner c hg hn (d , (hd , hm)) = decideBirth ob (subst (λ u → ⟨ fst z ∈ u ⟩) qd hm) (λ k → hn (subst (λ u → ⟨ fst z ∈ u ⟩) (sym qc) k))
上げられた添字のもとでの段階のグラフは、階層の記述の一意性によって、候補の順序数の段階と同一視されます。そして冪の値は、記述の段階の等式によって、その段階の定義可能冪と同一視されます。
where qc : fst c ≡ Lset β qc = Lset-only zero (suc b) (c ∷ γ) hg ob qd : fst d ≡ 𝒟ₒ (Lset β) qd = subst ⟨_⟩ (DefAt-stage β ob zero (suc zero) (d ∷ c ∷ γ) qc) hd
外側の記録は内側の読みへ消去され、内側の読みが判定の補題に渡されます。証明全体は、切り詰めを、順序数の等式という命題の中へ消去します。
atCarrier : Σ[ c ∈ S ] Outer c → β ≡ birth (fst z) (snd z)
atCarrier (c , (hg , (hn , hi))) =
PT.rec (setIsSet β (birth (fst z) (snd z)))
(atInner c hg (λ k → lower (hn k))) hi
逆向きでは、スロット b の順序数が x のメタ言語での誕生に等しいと仮定します。二つの存在証人には、包装された段階 Lset β と、その包装された定義可能冪を用います。存在量化の充足が要求する通り、これらは命題的切り詰めの中に置かれるので、この構成は論理式の証人が一意に定まるとは主張しません。
BirthAt-in : IsOrd β → β ≡ birth (fst z) (snd z) → ⟨ γ ⊨ BirthAt b x ⟩ BirthAt-in ob e = ∣ towerS β ob , (hg , (hn , ∣ powS β ob , (hd , hm) ∣₁)) ∣₁ where hg : ⟨ (towerS β ob ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
上げられた添字のもとでの段階のグラフが成立するのは、まとめられた段階が、提示の定義の等式によって、その添字の段階だからです。
hg = Lset-defines zero (suc b) (towerS β ob ∷ γ) ob (towerS-fst β ob)
もし x が Lset β に属するなら、β を birth x で置き換えることで、x は stage x = sucV (birth x) より真に低い段階ですでに現れることになります。これは stage-earliest に反し、BirthAt が要求する非所属を与えます。
hn : ⟨ fst z ∈ fst (towerS β ob) ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥ hn k = lift (stage-earliest (fst z) (snd z) β ob (subst (λ u → ⟨ fst z ∈ u ⟩) (towerS-fst β ob) k) (subst (λ u → ⟨ u ∈ stage (fst z) (snd z) ⟩) (sym e) (birth-stage (fst z) (snd z))))
DefAt の段階における等式は、その充足命題を 𝒟ₒ (Lset β) との等しさに同一視します。powS β ob の射影の等式がまさにこの等しさを与えるので、包装された定義可能冪は必要な条項を満たします。
hd : ⟨ (powS β ob ∷ towerS β ob ∷ γ) ⊨ DefAt zero (suc zero) ⟩
hd = subst ⟨_⟩
(sym (DefAt-stage β ob zero (suc zero)
(powS β ob ∷ towerS β ob ∷ γ) (towerS-fst β ob)))
(powS-fst β ob)
最後に、birth-mem は x を Lset (sucV (birth x)) に入れます。候補順序数を誕生順序数で置き換え、Lset-suc を使い、さらに包装された定義可能冪の射影方程式を使うことで、この所属を第二の証人へ輸送します。外向きの読みと合わせると、候補スロットが順序数であると仮定した場合に BirthAt が誕生順序数を正確に記述することが分かります。内部で順序数性を加えることも、標準的な存在証人を与えることもありません。
hm : ⟨ fst z ∈ fst (powS β ob) ⟩
hm = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (powS-fst β ob))
(subst (λ u → ⟨ fst z ∈ u ⟩) (Lset-suc β)
(subst (λ u → ⟨ fst z ∈ Lset (sucV u) ⟩) (sym e)
(birth-mem (fst z) (snd z))))
スロットにある台上の任意アリティの符号
符号ごとの認識式は、二つの条項を合わせます。最初の条項が符号からアリティの数項を読み、二つ目の条項が、その符号が作業のアルファベットの上の論理式の証人であることを確認します。合わせて、その符号がなんらかのアリティでの本物の論理式の符号であると言います。
isCodeAnyAt : ∀ {n} → Fin n → Fin n → Formula S n isCodeAnyAt c w = arityNumAtL c ∧̇ hasWitnessAt w c
内向きの読み出しは、作業集合 A、二つの枠、A と揃った環境、アリティ k の論理式、そして符号の枠をその論理式のキーと同一視する等式に対して述べられ、二つの連言項を満たします。
module _ (A : S) where codeAnyAt-in : ∀ {n k} (c w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A → (ψ : Formula ⟪ fst A ⟫ k) → fst (lookup c γ) ≡ fst (keyS A ψ) → ⟨ γ ⊨ isCodeAnyAt c w ⟩
二つの連言項は、それぞれの内向きの読み出しで満たされます。アリティの読み出しが自然数と符号を名指し、証人の読み出しが、論理式が揃えられたアルファベットの上にあることを確認します。
codeAnyAt-in {k = k} c w γ qw ψ qc = arityNumAtL-in c γ k (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc
外向きの読み出しが、切り詰められた符号の証人を復元します。あるアリティとある論理式がこのキーを作ります。切り詰められたデータは、命題の切り詰めの中にとどまります。
codeAnyAt-out : ∀ {n} (c w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A → ⟨ γ ⊨ isCodeAnyAt c w ⟩ → ⟨ IsKeyOverAny A (lookup c γ) ⟩ codeAnyAt-out c w γ qw (hk , hw) =
証明は、アリティの読み出しを、自然数と符号の対の中へ消去し、証人の読み出しを、符号のレベルの切り詰められた存在の中へ写像します。
PT.rec squash₁ step (arityNumAtL-out c γ hk) where step : Σ[ m ∈ ℕ ] Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# m) (fst z)) → ⟨ IsKeyOverAny A (lookup c γ) ⟩ step (m , (z , qz)) = PT.map (λ { (ψ , q) → m , (ψ , q) })
証人の読み出しの消去が、正しいアリティで論理式と符号の等式を復元し、切り詰められた存在を完成させます。
(witnessAt-out A w c γ qw hw m z qz)
符号集合を一度の外延性で得る
CodesAt c w は符号集合を構成するのではありません。extAt を通して、すでにスロット c にある集合を記述します。その集合に属する要素は、スロット w の台上の、ある有限アリティの論理式のキーであり、またそのときに限ります。これによりスロットの値は外延的に AllCodes A と定まりますが、所属の読みで用いる論理式の証人はすべて命題的に切り詰められたままです。
CodesAt : ∀ {n} → Fin n → Fin n → Formula S n CodesAt c w = extAt c (isCodeAnyAt zero (suc w))
符号の集合の外向きの読み出しは、その枠が作業のアルファベットの符号の集合をちょうど保持すると言います。証明は、二方向で外延性によって進みます。
module _ (A : S) {n : ℕ} (c w : Fin n) (γ : S ^ n) (qw : fst (lookup w γ) ≡ fst A) where CodesAt-out : ⟨ γ ⊨ CodesAt c w ⟩ → lookup c γ ≡ AllCodes A CodesAt-out h = extensionalL step where
第一の包含では、codeAnyAt-out が、記述されたスロットへの所属を「その要素はある論理式のキーである」という命題的切り詰めへ読み替えます。AllCodes-in はまさにこの主張を、固定されたメタ言語の集合 AllCodes A への所属へ変えます。特定の復号が選ばれることはありません。
step : (x : S) → (x ∈ˢ lookup c γ) ≡ (x ∈ˢ AllCodes A) step x = ⇔toPath (λ hx → AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw (extAt-out c (isCodeAnyAt zero (suc w)) γ h x hx)))
逆向きの包含では、AllCodes A への所属から得られるのは、与えられた要素をキーにもつアリティと論理式の命題的切り詰めだけです。符号ごとの論理式の充足は命題なので、そこで切り詰めを除去して codeAnyAt-in を適用できます。ただし、特定の復号が取り出されるわけではありません。
(λ hx → extAt-in c (isCodeAnyAt zero (suc w)) γ h x (PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w))) (λ { (k , (ψ , q)) → codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ q }) (AllCodes-out A x hx)))
逆に、スロット c の値が AllCodes A に等しいとします。CodesAt を示すには、外延を述べる論理式が要求する二つの所属の含意を示せば十分です。すなわち、スロットの要素は符号ごとの述語を満たし、その述語を満たすものはスロットに属します。
CodesAt-in : lookup c γ ≡ AllCodes A → ⟨ γ ⊨ CodesAt c w ⟩ CodesAt-in q = extAt-in-both c (isCodeAnyAt zero (suc w)) γ into back where into : (x : S) → ⟨ fst x ∈ fst (lookup c γ) ⟩ → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩
第一の含意では、集合の等式によってスロットへの所属を AllCodes A への所属へ移します。そこから論理式の証人が得られるのは命題的切り詰めのもとだけですが、目標は isCodeAnyAt の充足という命題なので、その目標へ切り詰めを除去できます。
into x hx = PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w))) (λ { (k , (ψ , qk)) → codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ qk }) (AllCodes-out A x (subst (λ u → ⟨ fst x ∈ fst u ⟩) q hx))
逆向きの含意では、codeAnyAt-out が充足を「候補はある論理式のキーである」という命題的切り詰めへ読み替えます。AllCodes-in はまさにこの切り詰められた主張から AllCodes A への所属を示し、集合の等式がその結論をスロット c へ戻します。
back : (x : S) → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩ → ⟨ fst x ∈ fst (lookup c γ) ⟩ back x hx = subst (λ u → ⟨ fst x ∈ fst u ⟩) (sym q) (AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw hx))
段階の順序を一度だけ展開する
順序数 δ では、前章ですでに構成された orderAt δ が Lset δ の要素を比較します。その順序を名前の構成が要求する小さい台へ移すことで、stepAt δ は New δ、すなわち Lset (sucV δ) の要素上に局所的な狭義整列順序 stepOrder δ を作ります。
stepOrder : (δ : V ℓ) → IsOrd δ → SWO (New δ) stepOrder δ oδ = stepAt δ (carry (Lset δ) (orderAt δ oδ))
δ ≡ δ' なら、δ での Under の比較を δ' での比較へ輸送できます。依存対のパスは、台が順序数であることの二つの証明も同時に一致させます。これは IsOrd が命題だから可能です。したがって、輸送された比較は、選んだ順序数性の証明に依存しません。
stepMoved : (δ δ' : V ℓ) (e : δ ≡ δ') (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ) → Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y stepMoved δ δ' e o o' x y = subst (λ p → Under (fst p) (stepOrder (fst p) (snd p)) x y) (Σ≡Prop isPropIsOrd {u = δ , o} {v = δ' , o'} e)
構成可能集合 x の誕生順序数が順序数 α に属するとします。その誕生順序数の後続は、α に属するか α に等しいかのどちらかです。x はその後続を添字とする段階に属するので、どちらの場合も x を Lset α に置けます。
bornIn : (α : V ℓ) → IsOrd α → (x : V ℓ) (p : ⟨ isL x ⟩) → ⟨ birth x p ∈ α ⟩ → ⟨ x ∈ Lset α ⟩ bornIn α oα x p h = reach (suc∈or≡ (birth x p) α (birth-ord x p) oα h) where reach : ⟨ sucV (birth x p) ∈ α ⟩ ⊎ (sucV (birth x p) ≡ α) → ⟨ x ∈ Lset α ⟩
suc∈or≡ が与える二つの場合で議論は完了します。誕生順序数の後続が α に属するなら、単調性によって birth-mem を Lset α まで運べます。その後続が α に等しいなら、等式に沿う輸送によって同じ所属が直接得られます。
reach (inl k) = Lset-mono {α = α} {β = sucV (birth x p)} k {x = x} (birth-mem x p) reach (inr e) = subst (λ w → ⟨ x ∈ Lset w ⟩) e (birth-mem x p)
周囲の順序数 α を固定します。Lset α の各要素は α より下の誕生順序数をもつので、orderAt α の再帰方程式が必要とする前段階の順序は、ちょうど必要な添字で利用できます。これにより、その方程式を二つの要素の誕生段階の比較として直接述べられます。
module _ (α : V ℓ) (oα : IsOrd α) where private module Fam = Family α (λ δ _ → orderAt δ) oα
層のすべての要素は構成可能です。層の構成可能性と、所属に沿う推移性によるものです。
memberL : (a : Mem (Lset α)) → ⟨ isL (fst a) ⟩ memberL a = Lset→isL α oα (fst a) (snd a)
Lset α の各要素 a は構成可能なので、誕生順序数をもちます。この順序数を bornOf a と書きます。これは α での順序を展開するときの第一の比較キーになります。
bornOf : (a : Mem (Lset α)) → V ℓ bornOf a = birth (fst a) (memberL a)
bornOf a ∈ α という事実には二つの役割があります。まず、orderAt α の展開で誕生順序数を前段階の添字として使えることを保証します。さらに後では、対象言語による誕生の記述から、bornIn によって a の周囲の段階への所属を回復できます。
bornMem : (a : Mem (Lset α)) → ⟨ bornOf a ∈ α ⟩ bornMem a = Fam.bornAt a .snd
展開の等式が、本章の接続点です。α での順序が a と b の間で成立するのは、a の誕生の順序数が b のそれより厳密に下にあるか、あるいは、同じ誕生の順序数を共有していて、その誕生の順序数での局所のステップの順序が a を b の下に置くときで、そのときに限ります。
order-unfold : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b ≡ ( ⟨ bornOf a ∈ bornOf b ⟩ ⊎ ( (bornOf b ≡ bornOf a) × Under (bornOf a) (stepOrder (bornOf a)
証明は orderAt-step で所属再帰を一段だけ開き、その基礎にある関係へ合同性を適用します。したがって、この二場合の等式は前章で構成済みの順序から導かれます。ここでその狭義整列順序を構成し直したり、証明し直したりはしません。
(mem-ord {A = α} oα (bornOf a) (bornMem a))) (fst a) (fst b) ) ) order-unfold a b = cong (λ z → relOf (z oα) a b) (orderAt-step α)
要素から台への包みが、層のそれぞれの要素を台の要素としてまとめ、論理式の環境がそれを収められるようにします。
opaque memS : (α : V ℓ) (oα : IsOrd α) → Mem (Lset α) → S memS α oα a = fst a , memberL α oα a
第一射影の等式が、まとめが基礎の集合を保つことを確認します。
memS-fst : (α : V ℓ) (oα : IsOrd α) (a : Mem (Lset α)) → fst (memS α oα a) ≡ fst a memS-fst α oα a = refl
誕生の提示は、誕生の順序数と、包む順序数 α から運ばれた構成可能性を対にします。
bornS : (α : V ℓ) (oα : IsOrd α) → ⟨ isL α ⟩ → Mem (Lset α) → S bornS α oα pα a = bornOf α oα a , isL-trans {x = α} {y = bornOf α oα a} (bornMem α oα a) pα
第一射影の等式が、まとめが誕生の順序数を保つことを確認します。
bornS-fst : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α)) → fst (bornS α oα pα a) ≡ bornOf α oα a bornS-fst α oα pα a = refl
誕生の等式が、まとめられた誕生が、まとめられた要素の計算された誕生と一致することを確認します。
bornS-birth : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α)) → fst (bornS α oα pα a) ≡ birth (fst (memS α oα a)) (snd (memS α oα a)) bornS-birth α oα pα a = refl
ステップをパラメータとして順序を記述する
ステップの論理式の型は、台の枠・表の枠・そして比較のための二つの枠をパラメータとする、四つの枠の論理式の族です。
StpFo : Type (ℓ-suc ℓ) StpFo = ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
ステップ論理式の外向きの妥当性は、順序数の台 d、表 f、比較される二つの対象に相対して述べられます。表についての仮定は、d で記録された各値 r が段階の関係 IsRel d r を実現するというものです。Stp の充足から得られるのは、対応する Under の比較の命題的切り詰めだけです。
StpOut StpIn : StpFo → Type (ℓ-suc ℓ) StpOut Stp = ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) → ((r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst (lookup d γ)) r) → ⟨ γ ⊨ Stp d f u v ⟩
外向きは意図的に ∥ Under ... ∥₁ を返すので、局所的な比較の存在だけを与え、標準的な証人を選びません。内向きの入力は異なります。呼び出し側が一つの特定の値 r と、それが表の d で記録されている証拠、さらに r がそこでの関係を実現する証明を与えます。
→ ∥ Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od) (fst (lookup u γ)) (fst (lookup v γ)) ∥₁ StpIn Stp = ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) → (r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst (lookup d γ)) r
内向きの読み出しが、特定の表の項目と Under の比較から、論理式の充足を作ります。
→ Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od) (fst (lookup u γ)) (fst (lookup v γ)) → ⟨ γ ⊨ Stp d f u v ⟩
モジュール Ordered は、抽象的なステップ論理式と、この二つの読みを仮定します。したがって以下で得られるのは、誕生段階優先の規則の条件つき翻訳です。同じ誕生段階での比較の妥当性から段階全体の比較の妥当性を導きますが、具体的なステップ論理式がこのインターフェースを満たすことは、この章では主張しません。
module Ordered (Stp : StpFo) (stp-out : StpOut Stp) (stp-in : StpIn Stp) where
新たに束縛される四つの対象は、比較される集合 u,v と、その誕生順序数の候補 du,dv です。最初の二つの条項は BirthAt du u と BirthAt dv v を主張します。これらが候補を実際の誕生段階と同一視するのは、後の読みが du と dv の順序数性を与えたときです。
OrdBody : ∀ {n} → Term S n → Fin n → Formula S (suc (suc (suc (suc n)))) OrdBody tb f = BirthAt (suc zero) (sh3 zero) ∧̇ ( BirthAt zero (sh2 zero) ∧̇ ( (var (suc zero) ∈̇ tm4 tb)
次の二つの条項は、誕生段階の二つの候補がともに項 tb の表す段階に属することを要求します。最後の選言は誕生段階優先の規則を再現します。すなわち、du ∈ dv であるか、または dv ≡ du であり、与えられたステップ論理式がその共通の台で u と v を比較します。ここでは u と v の間の集合所属を主張していません。
∧̇ ( (var zero ∈̇ tm4 tb) ∧̇ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ) ) )
CondCore はまず、比較される二つの対象 u と v を存在量化します。対を表す論理式は、スロット z の引数がそれらの順序対であることを要求します。さらに二つの存在量化が誕生段階の候補を束縛し、その後で OrdBody が誕生段階優先の比較を調べます。四つの証人はいずれも存在論理式の充足意味論のもとにあるため、命題的に切り詰められています。
opaque CondCore : ∀ {n} → Fin n → Term S n → Fin n → Formula S n CondCore z tb f = ∃̇ ( ∃̇ ( prAtL (sh2 z) (suc zero) zero ∧̇ ∃̇ (∃̇ (OrdBody tb f)) ) )
記述の意味を双方向に読む
CondCore を読むため、tb が表す順序数段階と、その段階上の表を固定します。Values は記録された各値が対応する局所関係を実現することを保証し、Entries は段階より下の各台で何らかの値が記録されていることだけを述べます。これらが、後の二方向で使う仮定です。
module _ {n : ℕ} (z : Fin n) (tb : Term S n) (f : Fin n) (γ : S ^ n) (oα : IsOrd (fst (⟦ tb ⟧ γ))) (vals : Values (lookup f γ) (fst (⟦ tb ⟧ γ))) (ents : Entries (lookup f γ) (fst (⟦ tb ⟧ γ))) where private
段階の順序数が、直接参照のために名づけられます。
α : V ℓ α = fst (⟦ tb ⟧ γ)
ずらしの補題が、四つの枠の改名が段階の項の表示を保つことを確認します。
shift : (u v du dv : S) → ⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ) ≡ ⟦ tb ⟧ γ shift u v du dv = tm4-val tb u v du dv γ
α より下の台 d に対し、Entries が与える表の値は命題的に切り詰められています。この補助補題は、その切り詰めを任意の命題 P へ除去できます。得られた各 r について Values が IsRel d r を証明し、継続関数が記録された順序対とその証明を使って P を導きます。
value : (d : S) → ⟨ fst d ∈ α ⟩ → (P : hProp (ℓ-suc ℓ)) → ((r : S) → ⟨ pr (fst d) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst d) r → ⟨ P ⟩) → ⟨ P ⟩ value d hd P k = PT.rec (snd P)
具体的には、ents d hd は値 r とその表項目からなる命題的切り詰めを与えます。ここで切り詰めを除去できるのは P が hProp だからであり、その後 vals が継続関数に必要な関係の実現証明を与えます。この構成は、その命題の外で表の値を選びません。
(λ { (r , hr) → k r hr (vals d r hd hr) }) (ents d hd)
深い充足の型が、比較の二つの対象と、それらの誕生の順序数から作られた四つの枠の環境で、順序づけられた本体を読みます。
Deep : (u v du : S) → S → Type (ℓ-suc ℓ) Deep u v du dv = ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ OrdBody tb f ⟩
二つの読みは、CondCore の同じ定義方程式を逆向きに使います。外向きには、四つの存在束縛を一対の要素と二つの誕生段階の候補として読みます。内向きには、すでにある Related の比較からそれらの束縛を与えます。Stp について仮定した読みを使うのは、誕生段階が等しい枝だけです。
opaque unfolding CondCore
外向きの読みは、入れ子になった四つの存在証人を順に開きます。まず比較される対象 u,v、次に誕生段階の候補 du,dv です。各証人は命題的切り詰めを通してのみ得られ、どの除去も命題 Related α ... を目標とします。最も内側のデータは、その後で数学的な比較の議論へ渡されます。
CondCore-out : ⟨ γ ⊨ CondCore z tb f ⟩ → ⟨ Related α (fst (lookup z γ)) ⟩ CondCore-out = PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (u , hv) → PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (v , (hp , hdu)) → PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (du , hdv) → PT.rec (snd (Related α (fst (lookup z γ))))
局所名 Goal は、スロット z の引数がメタ言語の述語 Related α を満たすという命題を表します。復元された四つの証人から、順序対の等式と OrdBody の充足が得られ、この二つが atDeep に渡されます。残りの証明は、それらをこの関係づけの命題へ変換します。
(λ { (dv , hd) → atDeep u v du dv hp hd }) hdv }) hdu }) hv }) where Goal : Type (ℓ-suc ℓ) Goal = ⟨ Related α (fst (lookup z γ)) ⟩
四つの存在証人を命題 Related へ除去すると、外向きの証明には二種類の情報が残ります。hp は引数が u と v の符号化された順序対であることを述べ、深い記録は du,dv が周囲の段階より下にある誕生段階の候補で、誕生段階優先の比較を満たすことを述べます。これらの証人は命題である目標の中だけで使われ、標準的な対や誕生データが選ばれるわけではありません。
atDeep : (u v du dv : S) → ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ → Deep u v du dv → Goal atDeep u v du dv hp (hbu , (hbv , (hmu₀ , (hmv₀ , hcmp)))) = subst (λ w → ⟨ Related α w ⟩) (sym qz)
対を表す論理式の妥当性により、スロット z の集合は pr (fst u) (fst v) と同一視されます。これは u と v の等式ではありません。この等式によって目標を、表された対についての Related α に書き換え、そこで誕生段階の比較を分析できます。
(PT.rec (snd (Related α (pr (fst u) (fst v)))) atCase hcmp) where qz : fst (lookup z γ) ≡ pr (fst u) (fst v) qz = subst ⟨_⟩ (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)) hp
第一の誕生段階の順序数への所属は、環境のずらしに沿って運ばれます。誕生段階のずらした読みとずらさない読みは、底の集合について一致するのです。
hmu : ⟨ fst du ∈ α ⟩ hmu = subst (λ w → ⟨ fst du ∈ fst w ⟩) (shift u v du dv) hmu₀
第二の誕生段階も同じずらしで運ばれ、こうして二つの誕生段階とも順序数の中にあることが分かります。
hmv : ⟨ fst dv ∈ α ⟩ hmv = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (shift u v du dv) hmv₀
第一の誕生段階は順序数です。順序数の中にあり、順序数の要素は順序数だからです。
odu : IsOrd (fst du) odu = mem-ord {A = α} oα (fst du) hmu
第二の誕生段階も同じ議論で順序数になります。
odv : IsOrd (fst dv) odv = mem-ord {A = α} oα (fst dv) hmv
誕生の論理式の読みの補題が、第一の誕生段階に適用されます。その順序数性のもとで、誕生の論理式の充足が、記録された段階を、最初の対象の本当の誕生順序数と同一視するのです。
qu : fst du ≡ birth (fst u) (snd u) qu = BirthAt-out (suc zero) (sh3 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbu odu
同じ読みが、第二の誕生段階と第二の対象に適用されます。
qv : fst dv ≡ birth (fst v) (snd v) qv = BirthAt-out zero (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbv odv
これで最初の対象を Lset α の要素とみなせます。構成可能性の証拠はすでに u が持っており、新たに得るのは周囲の段階への所属です。これは、同定された誕生順序数が α に属することから bornIn によって従います。
a : Mem (Lset α) a = fst u , bornIn α oα (fst u) (snd u) (subst (λ w → ⟨ w ∈ α ⟩) qu hmu)
第二の対象も同じようにまとめられます。
c : Mem (Lset α) c = fst v , bornIn α oα (fst v) (snd v) (subst (λ w → ⟨ w ∈ α ⟩) qv hmv)
まとめられた要素 a と u の底の集合は同じですが、a の構成可能性の証明は段階への所属から得られています。birth-proof はこの証拠についての証明無関係性を表し、a から計算した誕生と u から計算した誕生が一致することを示します。さらに qu と合成すると、記録された段階 du と同一視できます。
qa : bornOf α oα a ≡ fst du qa = birth-proof (fst u) (memberL α oα a) (snd u) ∙ sym qu
まとめられた第二の対象の誕生順序数は、記録された第二の誕生段階と一致します。
qc : bornOf α oα c ≡ fst dv qc = birth-proof (fst v) (memberL α oα c) (snd v) ∙ sym qv
残る目標は、メタ言語での比較 relOf (orderAt α oα) a c を示すことです。順序表のインターフェースは、その比較を、二つの底の集合の符号化された順序対が Related α に属するという命題へ移します。この段階で対象言語の関係集合を選んでいるわけではありません。
fill : relOf (orderAt α oα) a c → ⟨ Related α (pr (fst u) (fst v)) ⟩ fill = related-in α oα a c
OrdBody が符号化する比較には、orderAt を一段開いたときと同じ二つの枝があります。du ∈ dv の場合、qa と qc によって、これは a と c の「誕生がより早い」枝へ書き換えられます。さらに order-unfold に沿って輸送すると、両者の段階順序での比較が得られます。
atCase : ⟨ fst du ∈ fst dv ⟩ ⊎ ( (fst dv ≡ fst du) × ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ⟩ ) → ⟨ Related α (pr (fst u) (fst v)) ⟩ atCase (inl h) = fill (transport (sym (order-unfold α oα a c))
誕生段階が等しい枝では、OrdBody から抽象的な論理式 Stp の充足が得られます。共通の誕生段階の順序数性と Values の仮定を stp-out に渡すと、命題的に切り詰められた Under の比較だけが得られます。Related は命題なので、この切り詰めをそこへ除去できます。この議論は、Stp が表の値をどのように得たかを調べず、その値を取り出すこともありません。
(inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym qa) (sym qc) h))) atCase (inr (e , hs)) = PT.rec (snd (Related α (pr (fst u) (fst v)))) atUnder (stp-out (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) odu (λ r hr → vals du r hmu hr) hs)
記録された共通の誕生段階での Under の比較が与えられたら、それを、まとめられた要素 a に付随する誕生段階とそろえる必要があります。そろえた比較は order-unfold の同じ誕生の枝を与え、得られた orderAt の比較が Related によって表されます。
where atUnder : Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v) → ⟨ Related α (pr (fst u) (fst v)) ⟩ atUnder und = fill (transport (sym (order-unfold α oα a c)) (inr (qc ∙ e ∙ sym qa
この整合には、二つの台となる順序数の等式 qa を使います。stepMoved はこの等式に沿って局所比較を輸送し、証明無関係性によって二つの順序数性の証明を一致させます。共通の順序数の推移性を使ったり、新しい局所順序を作ったりはしません。
, stepMoved (fst du) (bornOf α oα a) (sym qa) odu (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) (fst u) (fst v) und)))
内向きでは、Related α z は順序数性の証明と、命題的切り詰めのもとに置かれた次のデータを含みます。Lset α の二つの要素 a,c、z がそれらの符号化された順序対であるという等式、そして両者の Ordering による比較です。Pairs はこのペイロードに名前を付け、構成中の充足命題への除去だけを行えるようにします。
private Pairs : IsOrd α → Type (ℓ-suc ℓ) Pairs o = Σ[ a ∈ Mem (Lset α) ] ∥ (Σ[ c ∈ Mem (Lset α) ] ( (fst (lookup z γ) ≡ pr (fst a) (fst c)) × ⟨ Ordering α o a c ⟩ )) ∥₁
内向きの読みは、Related の切り詰められた内容を CondCore の充足へ除去します。順序数性の証明と表された要素の対が局所的に得られると、atRel が四つの存在証人と誕生段階優先の比較を組み立てます。表す要素の対を大域的に選ぶものではありません。
CondCore-in : ⟨ Related α (fst (lookup z γ)) ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩ CondCore-in = PT.rec (snd (γ ⊨ CondCore z tb f)) atOrd where atRel : (o : IsOrd α) (a c : Mem (Lset α)) → fst (lookup z γ) ≡ pr (fst a) (fst c)
周囲の順序数性 oα は、読み全体の仮定としてすでに与えられています。ここで局所的に取り出すのは、段階を表す項の値がもつ構成可能性の成分 pα です。その後、最初の要素の誕生段階における値を表に求めます。目標は充足という命題なので、表の値の単なる存在をそこへ除去できます。
→ ⟨ Ordering α o a c ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩ atRel o a c q hord = value (bornS α oα pα a) hmu (γ ⊨ CondCore z tb f) atValue where pα : ⟨ isL α ⟩
各項は構造 𝒮ʟ で解釈され、その要素は底の集合と、その構成可能性の証拠との組です。したがって ⟦ tb ⟧ γ の第二射影が isL α を与えます。これは項の意味値の一部であり、別の充足仮定ではありません。
pα = snd (⟦ tb ⟧ γ)
ここで CondCore の証人を局所的に与えます。u,v は二つの段階要素を 𝒮ʟ の要素としてまとめ、du,dv はそれぞれの実際の誕生順序数をまとめます。これらはこの命題の証明に使う証人であり、Related から取り出される標準的な選択ではありません。
u v du dv : S u = memS α oα a v = memS α oα c du = bornS α oα pα a dv = bornS α oα pα c
Lset α の各要素について、その真の誕生順序数は α より下にあります。bornS の第一射影はその順序数なので、同じ所属の主張がスロット du に置かれた値についても成り立ちます。対象言語の条項が調べるのはこの形です。
hmu : ⟨ fst du ∈ α ⟩
hmu = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα a))
(bornMem α oα a)
第二の要素の誕生段階も、同じ輸送によって順序数の中にあります。
hmv : ⟨ fst dv ∈ α ⟩ hmv = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα c)) (bornMem α oα c)
第一の誕生段階は順序数です。順序数の中にあるからです。
odu : IsOrd (fst du) odu = mem-ord {A = α} oα (fst du) hmu
第二の誕生段階も、同じ読みによって順序数です。
odv : IsOrd (fst dv) odv = mem-ord {A = α} oα (fst dv) hmv
構成済みの段階順序を開くと、二つの枝からなる辞書式の規則が得られます。a が c より真に早く生まれたか、または両者の誕生が一致し、その共通の誕生段階での局所的な stepOrder が a の底の集合を c の底の集合より前に置くかです。
cmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩ ⊎ ( (bornOf α oα c ≡ bornOf α oα a) × Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) )
比較は、二つの順序数性の証明の同一視に沿って、狭義の読みを運ぶことで得られます。順序数性は命題であり、二つの証明は同じ順序数を記述するからです。
cmp = transport (order-unfold α oα a c) (strict α oα a c (subst (λ o' → ⟨ Ordering α o' a c ⟩) (isPropIsOrd α o oα) hord))
Related に含まれる等式は、引数を a と c の底の集合からなる順序対と同一視します。memS の第一射影の等式によって、その二つの端点をスロット u と v に置かれた値へ書き換えると、CondCore が要求する対の条項がちょうど得られます。
hp : ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ hp = subst ⟨_⟩ (sym (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ))) (q ∙ cong₂ pr (sym (memS-fst α oα a)) (sym (memS-fst α oα c)))
最初の BirthAt の条項を満たすため、内向きの読みは妥当性補題が必要とする二つの事実を与えます。du が順序数であることと、その底の集合がちょうど u の誕生順序数であることです。論理式それ自体が順序数性を主張したり、最小の段階を選んだりするわけではありません。
hbu : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt (suc zero) (sh3 zero) ⟩ hbu = BirthAt-in (suc zero) (sh3 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu (bornS-birth α oα pα a)
第二の誕生段階の誕生の論理式も、同じ深い環境のもとで埋められます。
hbv : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt zero (sh2 zero) ⟩ hbv = BirthAt-in zero (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odv (bornS-birth α oα pα c)
誕生が等しい枝では、cmp から、a の実際の誕生段階を台とし、a,c の底の集合を端点とする Under の比較が得られます。一方、ステップ論理式はまとめられた値 du,u,v で読まれるため、台と二つの端点をそれらの表現へ輸送する必要があります。
moved : Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) → Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v) moved und = subst2 (λ p r → Under (fst du) (stepOrder (fst du) odu) p r)
二つの端点の輸送には、memS の底の集合について公開された等式を使います。台の輸送には bornS-fst と stepMoved を使い、その依存パスは IsOrd が命題であることから二つの順序数性の証明も同一視します。ここで推移性は使いません。
(sym (memS-fst α oα a)) (sym (memS-fst α oα c)) (stepMoved (bornOf α oα a) (fst du) (sym (bornS-fst α oα pα a)) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) odu (fst a) (fst c) und)
Entries は最初の誕生段階における表の値 r の単なる存在を与え、Values はそのように記録されたどの値も IsRel を実現すると示します。各局所ペイロードについて、atValue は二つの要素と二つの誕生段階を挿入し、CondCore の充足を構成します。同じ誕生の枝では、この表の値をその場で stp-in に渡しますが、大域的に選ばれた値にはしません。
atValue : (r : S) → ⟨ pr (fst du) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst du) r → ⟨ γ ⊨ CondCore z tb f ⟩ atValue r hr hrel = ∣ u , ∣ v , (hp , ∣ du , ∣ dv , (hbu , (hbv , (hmu₀ , (hmv₀ , side)))) ∣₁ ∣₁) ∣₁ ∣₁ where
OrdBody の内部では、もとの環境の前に四つの束縛が加わるため、段階を表す項は tm4 tb となります。シフトの等式により、この持ち上げられた項も α を表すことが分かり、第一の誕生段階について既知の所属を対象言語の条項が要求する形へ輸送できます。
hmu₀ : ⟨ fst du ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩ hmu₀ = subst (λ w → ⟨ fst du ∈ fst w ⟩) (sym (shift u v du dv)) hmu
第二の誕生段階も、同じずらしの等式で運ばれます。
hmv₀ : ⟨ fst dv ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩ hmv₀ = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (sym (shift u v du dv)) hmv
残る条項は、order-unfold から得た二つの枝をそのまま再現しなければなりません。すなわち、誕生がより早い場合と、誕生が等しく、その後に局所的なステップ比較を行う場合です。補助関数はこの場合分けを充足命題の内部に保つので、証人や切り詰められた表の項目は、許される命題の目標の中だけで使われます。
atCmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩ ⊎ ( (bornOf α oα c ≡ bornOf α oα a) × Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) )
誕生がより早い枝では、bornS について公開された等式により、実際の誕生どうしのメタ言語での所属を du と dv の所属へ書き換えます。その証明を対象言語の選言の左側へ入れます。この選言の充足は命題的に切り詰められています。
→ ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩ atCmp (inl h) = ∣ inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym (bornS-fst α oα pα a)) (sym (bornS-fst α oα pα c)) h) ∣₁
誕生が等しい枝では、誕生の等式を dv と du の等式へ書き換えます。次に、内向きの妥当性の仮定 stp-in が、特定の記録値 r、その表への所属、IsRel の証明、輸送された Under の比較を使って局所ステップ論理式を満たします。具体的な局所表の値が手元にあるのは、まさにこの向きです。
atCmp (inr (e , und)) = ∣ inr ( bornS-fst α oα pα c ∙ e ∙ sym (bornS-fst α oα pα a) , stp-in (suc zero) (sh4 f) (sh3 zero) (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu r hr hrel (moved und) ) ∣₁
この二つの枝の翻訳を cmp に適用すると、OrdBody の比較の条項が完成します。二つの誕生の記述と、α より下にあるという二つの境界条件と合わせて、CondCore が要求する深い記録が得られます。新たな選択や順序論的主張が加わるわけではありません。
side : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩ side = atCmp cmp
対の水準の組み立ては、第二の要素の切り詰められた存在を消去します。a と関係づけられるそれぞれの候補 c に対して、局所の組み立てが核心の節の充足を産み出します。
atPairs : (o : IsOrd α) → Pairs o → ⟨ γ ⊨ CondCore z tb f ⟩ atPairs o (a , h) = PT.rec (snd (γ ⊨ CondCore z tb f)) (λ { (c , (q , hord)) → atRel o a c q hord }) h
Related の外側のペイロードは順序数性の証明 o と、Pairs o の命題的切り詰めだけを与えます。CondCore の充足は命題なので、atOrd はこの切り詰めを除去し、表された各対を atPairs に渡せます。特定の順序数性の証明に依存しないことは、これより前に isPropIsOrd によって o と周囲の証明 oα を同一視するときに使われています。
atOrd : Σ[ o ∈ IsOrd α ] ∥ Pairs o ∥₁ → ⟨ γ ⊨ CondCore z tb f ⟩ atOrd (o , h) = PT.rec (snd (γ ⊨ CondCore z tb f)) (atPairs o) h
仕様は、核心の節の充足と、符号化された対の関係とを、両方向の命題のパスとして同一視します。
CondCore-spec : (γ ⊨ CondCore z tb f) ≡ Related α (fst (lookup z γ)) CondCore-spec = ⇔toPath CondCore-out CondCore-in
フレームの二つの仮定を解消する
段階と表がすでに周囲の環境の変数スロットにあるときは、Cond の形を使います。新しい第零スロットは検査する符号化された順序対のために確保され、もとの段階と表の添字はその先へ持ち上げられます。したがって Cond は段階の証人を導入せず、周囲の文脈がすでに与えた段階を参照します。
Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n) Cond b f = CondCore zero (var (suc b)) (suc f)
Cond₀ B F は、分出に必要な定数段階の形です。唯一の存在束縛が表の値を与え、等式の条項がその値を固定した定数 F に一致させます。段階はすでに定数項 B です。残る自由スロットには、検査される符号化された順序対が入ります。後の仕様は、この形と Cond が同じ Related の比較を記述することを示しますが、それは依然として与えられた StpOut と StpIn に相対的です。どちらの形も段階順序そのものを構成しません。
Cond₀ : S → S → Formula S 1 Cond₀ B F = ∃̇ ( (var zero ≐ con F) ∧̇ CondCore (suc zero) (con B) zero )
変数形式は、段階と順序表を周囲の環境に残したまま、有序対の候補 z を調べます。段階が順序数であり、順序表が所定の値と項目の読みをもつと仮定すると、その妥当性の等式は Cond の充足をホスト側のクラス Related と同一視します。したがって、この論理式はすでに構成された段階順序の比較を記述するのであって、新たな順序を構成するのではありません。
cond-spec : ∀ {n} (b f : Fin n) (γ : S ^ n) → IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ)) → (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z) cond-spec b f γ ob vals ents z =
z を環境の先頭に加えると、もとの各スロットは一つ後ろへ移ります。そこで核心はスロット零で z を読み、var (suc b) を通して段階を、suc f を通して順序表を読みます。このずらしを施せば、CondCore の一般的な等式から、必要な変数形式の等式が直接得られます。
CondCore-spec zero (var (suc b)) (suc f) (z ∷ γ) ob vals ents
分出を行うとき、周囲の環境には候補 z しかないため、定数形式は参照する順序表を束縛しなければなりません。束縛された要素 c の基礎集合が固定された順序表 F の基礎集合と等しく、c を順序表のスロットに置いた核心の比較が成り立つなら、c は適切な証人です。補助命題 Held c はこの二つの事実をまとめます。c は順序表の代表であり、論理式の符号ではありません。
module _ (B F : S) (oB : IsOrd (fst B)) (vals : Values F (fst B)) (ents : Entries F (fst B)) (z : S) where private Held : S → Type (ℓ-suc ℓ) Held c = (fst c ≡ fst F)
二スロットの環境 c ∷ z ∷ [] では、スロット零が束縛された順序表の代表、スロット一が有序対の候補であり、段階は定数項 con B で与えられます。この配置により、同じ核心で定数の場合も表せます。外向きに読むときは、F についての順序表の読みを、それと外延的に等しい代表 c へ移さなければなりません。
× ⟨ (c ∷ z ∷ []) ⊨ CondCore (suc zero) (con B) zero ⟩
外向きの証明は、束縛された順序表について、命題的切り詰めを施した存在証人から始まります。Related 自体が命題なので、その切り詰めをこの目標へ除去できます。補助定義 atHeld は、一時的な代表 c と二つの Held の事実のもとだけで推論します。代表はこの証明の外へ出ないため、この議論から標準的な証人や選択関数は得られません。
cond₀-out : ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ → ⟨ Related (fst B) (fst z) ⟩ cond₀-out = PT.rec (snd (Related (fst B) (fst z))) atHeld where atHeld : Σ[ c ∈ S ] Held c → ⟨ Related (fst B) (fst z) ⟩ atHeld (c , (qc , hc)) =
等式 qc によって、二つの順序表の読みを、束縛された代表と F の間で互いに逆向きに移せます。c にあると仮定した項目は、まず F へ運ばれ、その値が段階の関係を実現することを vals が示します。逆に、ents は F にある項目を命題的切り詰めのもとで与え、その内側で写像することにより、項目を c へ戻します。
CondCore-out (suc zero) (con B) zero (c ∷ z ∷ []) oB (λ x r hx hp → vals x r hx (subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) qc hp)) (λ x hx → PT.map (λ { (r , hr) → r , subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) (sym qc) hr })
こうして移された読みは、核心の比較を外向きに読むために必要な仮定そのものです。それらを hc に適用すると、z についての Related の事実が得られます。この過程を通じて項目の証人は命題的に切り詰められたままですが、核心の充足も得られる関係の主張も命題なので、それで十分です。
(ents x hx)) hc
内向きには、指定された順序表 F がすでにあるので、それ自身を存在証人にでき、定数で指定された順序表との等式は反射性で与えられます。続いて核心の内向きの読みが、与えられた Related の事実を、F を順序表のスロットに置いた充足へ変えます。ここでは命題的切り詰めの内側に証人を構成しているのであり、切り詰められた情報から証人を取り出したり、順序表の代表が一意に選ばれると主張したりしてはいません。
cond₀-in : ⟨ Related (fst B) (fst z) ⟩ → ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ cond₀-in h = ∣ F , (refl , CondCore-in (suc zero) (con B) zero (F ∷ z ∷ []) oB vals ents h) ∣₁
二つの含意から、Cond₀ B F の充足命題と Related (fst B) (fst z) の間の道が得られます。したがって、同じ順序数性、値、項目についての仮定のもとで、定数形式は変数形式とまったく同じ数学的な読みをもちます。この等式は命題値の意味に関するものであり、二つの論理式を構文的に同一視したり、順序表の特別な提示を選んだりするものではありません。
cond₀-spec : (B F : S) → IsOrd (fst B) → Values F (fst B) → Entries F (fst B) → (z : S) → ((z ∷ []) ⊨ Cond₀ B F) ≡ Related (fst B) (fst z) cond₀-spec B F oB vals ents z = ⇔toPath (cond₀-out B F oB vals ents z) (cond₀-in B F oB vals ents z)
これで一般的な順序表の構成は、段階と順序表が変数スロットを占める場合には Cond を、固定された定数である場合には Cond₀ を使えます。そこから得られる関係の対象は、先に構成済みの狭義整列順序 orderAt の基礎となる比較を表現します。ここで整列順序を作り直してはいません。すべての結果は、抽象的なステップ論理式に対する StpOut と StpIn に相対的です。後に InternalWellOrder が具体的なステップについてこの二つの読みを与え、残るパラメータを除きます。
open Described Cond Cond₀ cond-spec cond₀-spec public
まとめ
この章では、先に構成された段階順序の基礎となる関係を対象言語で記述しました。BirthAt が誕生順序数を同定するのは外から順序数性を仮定した場合だけであり、CodesAt が台とともに動く符号集合を定めるのは外延的な意味においてだけです。また、CondCore が誕生段階優先の比較と一致するのは、StpOut、StpIn、Values、Entries に相対してだけです。存在、復号、表の値、Under の証人は、すべて命題的切り詰めの内側にとどまります。次の章で、具体的なステップ論理式とその二つの読みを与えます。