Bedrock充足関係のグラフを表す論理式
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ再帰的構成 Sat は各論理式に、それを満たす環境の集合を割り当てます。しかし、このメタ理論上の割当てを L 上の一階定義の内部でそのまま名指すことはできません。本章の課題は、後でそのような問い合わせの関係として使える対象言語の二項論理式を与えることです。論理式の証人は、問い合わせるキーの周囲で再帰方程式を満たすのに十分な局所データを記述しますが、正準な表や一価な表がすでに得られているとは仮定しません。
{-# OPTIONS --cubical --safe --guardedness #-}
以下で用いる環境の塔のインターフェースが、必要な宇宙レベルでの排中律を仮定するため、本章もその仮定を受け取ります。ただし、ここで組み立てる論理式が命題を排中律で場合分けするわけではありません。量化子と結合子の意味は、すでに構成された一階意味論から得られます。
open import Base.Prelude open import Base.Classical using ( LEM )
宇宙レベルとこの一つの古典的パラメータを固定します。これから定める関係が論理式キー x と集合 y について成り立つのは、台上の局所的な条件を満たす候補の充足関係表が x で y を記録するとき、かつそのときに限ります。この段階で主張するのは、そのような局所データの存在だけです。正準な表を選ぶことも、すべてのキーで値が一意であることを証明することもありません。
module L.Coding.SatisfactionGraph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
論理式の言語には、変数、定数、等号、連言、存在量化があります。定数を使えば、タグに用いる標準の数項のような固定された構成可能集合を論理式に直接入れられます。また、pr はグラフ要素となる順序対を符号化します。これらの論理式を読む意味論は周囲の階層から得られます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr )
候補データは三つの記述によって組織されます。appAt は符号化された対をグラフ要素として読み、domAt T C は表 T のキー領域がちょうど C であることを述べ、closedAt C は C 内の複合論理式キーが必要とする直下の部分式キーも C に属することを要求します。domAt が述べるのは表のキー領域であり、後に表の値として現れる環境集合とは異なります。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( domAt; appAt; appAt-adequate ) open import L.Coding.Closure {ℓ} using ( closedAt ) open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9; i0; i1; i2; i3; i4; i5; i6; i7; i8; i9; i10; i11; i12; i13; sh )
残る記述は、局所的な再帰方程式を準備します。towerAt は符号化環境の候補となる各行を与え、Tags は十個の構成子タグのスロットを校正します。tableAt は、候補キー集合上の命題的に切り詰められた全域性、表項目のキーをその集合に限る条件、十個の局所的な外延方程式をまとめます。これらの材料が記述するのは、まだ候補関係だけです。PinnedRecursion は真正な論理式キーで必要となる条件付き一意性を証明し、SatisfactionBridge は独立に、外部の値 Sat への所属を制限構造での充足として解釈します。その後、UniformSatisfaction が AllCodes B 上で存在と固定された一意性を組み合わせ、一様な表を得ます。
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; towerAt ) open import L.Coding.CodeDomain {ℓ} using ( Tags ) open import L.Coding.SatisfactionClauses {ℓ} using ( tableAt ) open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ )
自由な位置を n 個もつ論理式の解釈環境は、n 個の台の要素からなるベクトルです。lookup はある位置に割り当てられた要素を読み、cons は環境の最も内側に新しい要素を加えます。この規約により、任意の外側の環境の前に十四個の補助的な証人を置いても、元の問い合わせ位置を保てます。
open import Cubical.Data.Vec using ( _∷_; []; lookup )
対象言語の存在は命題的切り詰めによって解釈されます。そのため、存在論理式の証明は証人が存在するという事実だけを残し、どの証人を用いたかを忘れます。これは充足関係グラフにとって本質的です。公開される読みは、適切なタグ、塔、キー集合、表が存在することを示せますが、利用者が候補の表を大域的に一つ選べるようなデータは公開しません。
import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
以下では、S を構成可能構造の台とします。その要素は階層の集合と、それが構成可能であることの証拠からなります。この構造の関係は命題値をとり、山括弧は証明が要素となる基礎の命題を取り出します。したがって、基礎となる階層集合の等しさや所属と、等号や所属を主張する対象言語の論理式とは区別しなければなりません。
open hPropStructure 𝒮ʟ
判定 γ ⊨ φ は、対象言語の論理式 φ が構成可能な環境 γ のもとで成り立つことを意味します。これは意味論的な値の有限ベクトルを論理式の構文に結びつけます。特に、キーとその候補値を問い合わせる外側の環境はメタ理論上の割当てであり、環境の塔に並ぶ符号化環境集合の一つではありません。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
再帰条件を守る枠組み
最初の四つの名前は、十四個の新しい位置の構造的な中心を表します。最も内側から順に、台 b、候補となる充足関係表 T、その候補キー集合 C、候補となる環境の塔 E が入ります。これらの役割を分けると、二つの混同を避けられます。C の要素は論理式キーであり、T の要素はキーと値の対を符号化します。また、E によって表される各行は、符号化環境をアリティごとに組織します。
Bi Ti Ci Ei : ∀ {n} → Fin (14 + n) Bi = i0 Ti = i1 Ci = i2 Ei = i3
続く十個の位置は構成子タグです。NN は共通の位置対応を与え、まず構成子の添字ゼロから三までを i4 から i7 に送ります。校正前の各位置には任意の台の要素が入りうるため、局所的な節はそれらを符号の形を識別するパラメータとして用いるだけです。
NN : ∀ {n} → Fin 10 → Fin (14 + n) NN zero = i4 NN (suc zero) = i5 NN (suc (suc zero)) = i6 NN (suc (suc (suc zero))) = i7
同じ対応は構成子八まで連続して続きます。この一様な添字付けが必要なのは、閉性条件と十個の表方程式が、各論理式構成子をどの数項で示すかについて一致しなければならないからです。校正後は、一つの節の族で原子式、三つの二項結合子、偽、二つの非有界量化子、二つの有界量化子を扱えます。
NN (suc (suc (suc (suc zero)))) = i8 NN (suc (suc (suc (suc (suc zero))))) = i9 NN (suc (suc (suc (suc (suc (suc zero)))))) = i10 NN (suc (suc (suc (suc (suc (suc (suc zero))))))) = i11 NN (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = i12
最後の方程式は構成子九を i13 に置き、最も内側から外へ並ぶ b, T, C, E, N0, ..., N9 という配置を完成させます。環境の塔が占める位置は候補集合 E の一つだけです。アリティで添字付けられた各行は towerAt が記述する符号化要素であり、このベクトル内の別の十個の位置ではありません。
NN (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = i13
問い合わせるキーと候補値は、この十四個の位置の外側にある呼び出し側の環境に残ります。シフト sh14 は元の位置を十四個すべての束縛の先へ移すので、後の appAt Ti (sh14 x) (sh14 y) も、元の対 (x,y) が T に記録されているかを問います。
sh14 : ∀ {n} → Fin n → Fin (14 + n) sh14 i = sh 14 i
関数 ev は、この位置対応を意味論的に実現します。b、T、C、E と、ν が与える十個の値を外側の環境 γ の前に並べます。その結果、Tags、towerAt、closedAt、domAt、tableAt が用いる各スロットは、議論を通して同じ証人を指します。
ev : ∀ {n} → (Fin 10 → S) → S → S → S → S → S ^ n → S ^ (14 + n) ev ν E C T b γ = b ∷ T ∷ C ∷ E ∷ ν f0 ∷ ν f1 ∷ ν f2 ∷ ν f3 ∷ ν f4 ∷ ν f5 ∷ ν f6 ∷ ν f7 ∷ ν f8 ∷ ν f9 ∷ γ
正準なタグの割当てでは、構成子の添字 k をモデルの数項 nn (toℕ k) に送ります。その基礎となる階層集合は k を表す有限順序数であり、第二成分は構成可能性を証明します。数項を S の要素としてまとめることで、対象言語から定数として名指せます。
numν : Fin 10 → S numν k = nn (toℕ k)
Tags γ NN は各構成子の添字 k について、位置 NN k にある要素の基礎集合が k の数項であるかを問います。numν から作った環境では、lookup と第一射影を計算するとその数項になるため、最初の四つの場合は反射律で成り立ちます。この主張が比較するのは基礎集合であり、構成可能性の証明書そのものの定義的な等しさは要求しません。
numTags : ∀ {n} (E C T b : S) (γ : S ^ n) → Tags (ev numν E C T b γ) NN numTags E C T b γ zero = refl numTags E C T b γ (suc zero) = refl numTags E C T b γ (suc (suc zero)) = refl numTags E C T b γ (suc (suc (suc zero))) = refl
添字四から八の場合も反射律で証明できます。長い後続の形が担うのは有限添字の整理だけです。NN k は numν k が入るスロットを選び、その第一射影が必要な数項になります。したがって、この証明は各点での計算のままであり、特定の構成子に固有の意味論的仮定を加えません。
numTags E C T b γ (suc (suc (suc (suc zero)))) = refl numTags E C T b γ (suc (suc (suc (suc (suc zero))))) = refl numTags E C T b γ (suc (suc (suc (suc (suc (suc zero)))))) = refl numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl
添字九で Fin 10 の全要素が尽くされるため、同じ反射律の議論によって、正準な割当てが Tags を満たすことの全域的な証明が完成します。別の割当ても候補の証人にはなれますが、十個の構成子の節を意図したタグで読むには、この各点での一致を自ら証明しなければなりません。
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl
対象言語の論理式 numsAt は、同じ校正を右結合した等式の連言として始めます。最初の八つの等式は、位置 i4 から i11 の値が順に定数 nn 0 から nn 7 であることを述べます。したがって、後の変数で台を与える形は台を定数として名指しませんが、グラフの論理式はこれらの固定された標準の数項を名指します。
numsAt : ∀ {n} → Formula S (14 + n) numsAt = (var i4 ≐ con (nn 0)) ∧̇ ((var i5 ≐ con (nn 1)) ∧̇ ((var i6 ≐ con (nn 2)) ∧̇ ((var i7 ≐ con (nn 3)) ∧̇ ((var i8 ≐ con (nn 4)) ∧̇ ((var i9 ≐ con (nn 5)) ∧̇ ((var i10 ≐ con (nn 6)) ∧̇ ((var i11 ≐ con (nn 7)) ∧̇
i12 と i13 の等式が、数項八と九によって校正を完成させます。したがって、連言全体の充足は Tags が要求する十個の等式をちょうど含み、続く読みの補題が入れ子の連言からそれらを取り出します。この校正が同定するのは構成子タグだけであり、候補キー集合が整形式な論理式符号の完全な集合だという主張は加えません。
((var i12 ≐ con (nn 8)) ∧̇ (var i13 ≐ con (nn 9))))))))))
nums-out は numsAt の充足をホスト層の族 Tags に移します。連言は対として解釈されるので、タグゼロの場合は第一射影を取り、タグ一と二の場合は第二射影をたどってから次の第一射影を取ります。この補題は任意のタグ割当て ν に使えるため、どの候補グラフの証人がもつ校正も読み出せます。
nums-out : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n) → ⟨ ev ν E C T b γ ⊨ numsAt ⟩ → Tags (ev ν E C T b γ) NN nums-out ν E C T b γ h zero = h .fst nums-out ν E C T b γ h (suc zero) = h .snd .fst nums-out ν E C T b γ h (suc (suc zero)) = h .snd .snd .fst
より大きい各添字について、nums-out は右結合した積の第二射影をたどり、対応する等式に到達します。ここで行うのは連言の除去だけであり、タグの値を選ぶことも、その一意性を証明することもありません。後に十四個の存在証人を命題的切り詰めのもとで除去するとき、これらの射影が、論理式の充足にすでに含まれているタグの証明を復元します。
nums-out ν E C T b γ h (suc (suc (suc zero))) = h .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc zero)))) = h .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc zero))))) = h .snd .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc zero)))))) = h .snd .snd .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc zero))))))) = h .snd .snd .snd .snd .snd .snd .snd .fst
右結合した連言の最も深い成分は、タグ八と九に関する二つの等式の対です。その二つの射影によって各点の等式族が完成するため、numsAt の充足から Fin 10 のすべての添字での一致が一度に得られます。この段階で行うのは十個の等式の組み直しだけであり、候補キー集合や候補表に新しい条件を加えることはありません。
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .snd
逆向きの読み nums-in は Tags から出発します。各構成子の添字について、選ばれたタグと対応する標準数項の基底集合が等しいというデータです。これら十個の等式を右結合の連言に並べると、numsAt の充足が得られます。nums-out と nums-in により、以下では対象言語の校正論理式とホスト層の等式族との間を双方向に移れます。
nums-in : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n) → Tags (ev ν E C T b γ) NN → ⟨ ev ν E C T b γ ⊨ numsAt ⟩ nums-in ν E C T b γ tg = tg f0 , (tg f1 , (tg f2 , (tg f3 , (tg f4 , (tg f5 , (tg f6 , (tg f7 , (tg f8 , tg f9))))))))
補助的な論理式の族 satGraphOn が、ここで枠組み全体を組み立てます。パラメータ pin は拡張された環境上の論理式であり、新たに束縛される台と外側の参照との関係だけを指定します。問い合わせ位置 x と y は外側の環境に残ります。十四重の存在量化が十個のタグ、塔、キー集合、表を束縛し、最後に最も内側で台を束縛します。最初の連言項が pin なので、台の固定方法を変えても候補グラフのほかの条件は変わりません。
private satGraphOn : ∀ {n} → Formula S (14 + n) → Fin n → Fin n → Formula S n satGraphOn pin x y = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (( pin
pin に続く連言は、一つの表項目を解釈するための条件を並べます。校正論理式 numsAt は、十個のタグのスロットを標準数項と同一視します。towerAt Ei Bi (NN f0) は、候補の塔が、束縛された台上で再帰の節に必要な行の構造をもつことを要求しますが、その塔が正準であるとは主張しません。closedAt Ci は候補キー集合を、七通りの直接の部分式のキーについて閉じます。domAt Ti Ci は表のキー領域がちょうど C であることを述べ、appAt Ti (sh14 x) (sh14 y) は、x と y を十四の束縛の先へ移した後も、もとの問い合わせの対が表項目であることを述べます。
∧̇ ( numsAt ∧̇ ( towerAt Ei Bi (NN f0) ∧̇ ( closedAt Ci ∧̇ ( domAt Ti Ci ∧̇ ( appAt Ti (sh14 x) (sh14 y)
最後の連言項 tableAt Ti Bi Ci Ei NN は、局所的な再帰の仕様を与えます。第一の領域条件は、C の各キーに対して、命題的切り詰めのもとで何らかの値があることを述べます。第二の条件は、T の各要素が、やはり命題的切り詰めのもとで、C のキーと値との対に分解できることを述べます。残る十個の節は論理式の構成子に一つずつ対応し、該当する表の項目を外延的な等式で特徴づけます。これらは候補関係を局所的に記述するだけで、T を一価にせず、各キーの値を選びもしません。真正な論理式のキーにおける一意性は、後の PinnedRecursion で構造帰納法により示されます。
∧̇ tableAt Ti Bi Ci Ei NN ))))))))))))))))))))
充足関係グラフの証人
ホスト層の型 GraphWitOn は、同じ情報を五つのデータ ν、E、C、T、b と、それに続く七つの証明書へ平らにします。証明書は、b と参照 W の基底集合の等しさ、十個すべてのタグの一致、組み立てた環境での塔、閉性、正確なキー領域の各節の充足、問い合わせの対が表の基底集合に属すること、そして tableAt の充足を述べます。二つの領域に関する証明書は後で異なる役割をもちます。domAt は問い合わせのキーが C に属することを導き、tableAt に含まれる全域性は構造帰納法で部分式のキーに値を供給します。公開される読みは、この具体的な記録を命題的切り詰めを通してのみ示すため、候補の表の存在を確立しても、特定の一つを選びません。
private GraphWitOn : ∀ {n} → S → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ) GraphWitOn W x y γ = Σ[ ν ∈ (Fin 10 → S) ] (Σ[ E ∈ S ] (Σ[ C ∈ S ] (Σ[ T ∈ S ] (Σ[ b ∈ S ] ((fst b ≡ fst W) × (Tags (ev ν E C T b γ) NN × (⟨ (ev ν E C T b γ) ⊨ towerAt Ei Bi (NN f0) ⟩ × (⟨ (ev ν E C T b γ) ⊨ closedAt Ci ⟩ × (⟨ (ev ν E C T b γ) ⊨ domAt Ti Ci ⟩ × (⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst T ⟩ × ⟨ (ev ν E C T b γ) ⊨ tableAt Ti Bi Ci Ei NN ⟩))))))))))
satGraphOn の充足と平坦な記録を比較するため、pin、その参照 W、二つの問い合わせ位置、外側の環境を固定します。台の等式を除けば、記録の各欄はすでに枠組みの連言項の中に定まった解釈をもっています。したがって、追加で必要な仮定は pin の読み rd だけです。内向きの含意では等式 fst b ≡ fst W を pin の充足へ移し、外向きの含意では pin の充足をその等式として読み戻します。
module _ {n : ℕ} (pin : Formula S (14 + n)) (W : S) (x y : Fin n) (γ : S ^ n) where
内向きの読みは、切り詰められた証人の記録を、枠組み全体の充足へ変えます。その仮定 rd は、pin をどう読むべきかを言います。十個のタグの値、塔、索引集合、表、台のどんな選択に対しても、台が参照と一致するなら、組み立てられた環境のもとで pin が充足される、というものです。入力は切り詰めであり、出力は充足、それ自体が切り詰めです。したがって証明全体は切り詰めの内部の一つの写しになります。平坦な記録を部品ごとに照らし合わせて、論理式が要求する十四重の証人へ送るのです。どこでも証人は選ばれません。切り詰めの間の写しは、証人が存在するという事実だけを運びます。
graphOn-in : ((ν : Fin 10 → S) (E C T b : S) → fst b ≡ fst W → ⟨ ev ν E C T b γ ⊨ pin ⟩) → ∥ GraphWitOn W x y γ ∥₁ → ⟨ γ ⊨ satGraphOn pin x y ⟩ graphOn-in rd = PT.map (λ { (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) →
平坦な記録は、配置の逆の順序で再び入れ子にされます。最も外側の存在量化が第九構成子のタグを受け取り、次が第八、という具合に、最も内側の存在量化が台を受け取るまで続きます。これはまさに配置の de Bruijn の順序を、外から内へ読んだものです。pin の充足は rd が供給します。組み立てられた証人と、記録が運ぶ台の等式に適用するのです。校正は nums-in が、ホスト層の一致から十個の等式の充足へと変換し、後のどの連言項も標準数項を使うようにします。
ν f9 , ∣ ν f8 , ∣ ν f7 , ∣ ν f6 , ∣ ν f5 , ∣ ν f4 , ∣ ν f3 , ∣ ν f2 , ∣ ν f1 , ∣ ν f0 , ∣ E , ∣ C , ∣ T , ∣ b , ( rd ν E C T b eb , ( nums-in ν E C T b γ tg
三つの保護条件の証明書は、そのまま通り抜けます。それらは、枠組みが組み立てるその環境のもとで読んだ論理式の充足だからです。問い合わせの項目が、言語を変えねばならない唯一の部品です。ホスト側ではそれはありふれた所属、すなわち二つの問い合わせ値の順序対が表の基礎集合に属することです。適用の原子の妥当性の法則は、原子の充足をまさにこの所属と同一視し、証明はその一本の道に沿って運搬します。これが内向きの方向における唯一の実質的な橋であり、ほかのすべては組み直しにすぎません。
, ( hE , ( hc , ( hd , ( subst ⟨_⟩ (sym (appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ))) ha
節の族の証明書を最後の連言項に置いた後は、入れ子になった切り詰めを戻せば十分です。PT.map の呼び出しが最も外側の切り詰めを与えます。その写像が、最も外側の存在量化に必要な証人の対を返すからです。その対の内側にある十三回の明示的な挿入が、台に至るまでの残りの存在量化を順に与えます。したがって、切り詰められた平坦な記録から十四重の存在量化の充足が得られますが、選ばれたデータが命題的切り詰めの外へ出ることはありません。
, h12 )))))) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
外向きの読みはこの旅を逆向きにたどります。仮定 rd は、今度は pin を逆方向に回します。組み立てられた環境のもとでの pin の充足から、台の等式を回復するのです。入力は枠組み全体の充足であり、その十四重の存在量化はどれも切り詰められています。出力は切り詰められた証人の記録です。証明は存在量化を一段ずつ除去し、そのどれもが、記録の切り詰めという命題を目指します。したがってそれぞれが正当です。この補題は記録そのものを産み出すとは決して主張せず、一つが存在するという事実だけを主張します。
graphOn-out : ((ν : Fin 10 → S) (E C T b : S) → ⟨ ev ν E C T b γ ⊨ pin ⟩ → fst b ≡ fst W) → ⟨ γ ⊨ satGraphOn pin x y ⟩ → ∥ GraphWitOn W x y γ ∥₁ graphOn-out rd h = PT.rec squash₁ (λ { (n9 , h9) → PT.rec squash₁ (λ { (n8 , h8) →
PT.rec を一回適用するたびに、切り詰められたタグの証人を一つ除去し、命題である同じ目標 ∥ GraphWitOn W x y γ ∥₁ を保ちます。こうしてスロット九から三までの値を次の継続へ渡せますが、切り詰められていないデータとして外へ出すことはできません。この正当な除去を繰り返すことで、対象言語の入れ子の存在量化を一つの平坦な切り詰められた記録に対応させられます。
PT.rec squash₁ (λ { (n7 , h7) → PT.rec squash₁ (λ { (n6 , h6) → PT.rec squash₁ (λ { (n5 , h5) → PT.rec squash₁ (λ { (n4 , h4) → PT.rec squash₁ (λ { (n3 , h3) →
十個すべてのタグの値を復元すると、同じ命題への除去によって候補の塔 E とキー集合 C に到達します。hE' と hC' は、表、台、各証明をまだ含んでいる切り詰められた残りを表す名前であり、塔や閉性の条件の証明ではありません。それらの証明は最後の連言の中に残り、T と b も切り詰めの内部で現れた後に初めて記録へ入ります。
PT.rec squash₁ (λ { (n2 , h2) → PT.rec squash₁ (λ { (n1 , h1) → PT.rec squash₁ (λ { (n0 , h0) → PT.rec squash₁ (λ { (E , hE') → PT.rec squash₁ (λ { (C , hC') →
最も内側の段で、証明はそれ以上除去するのではなく、写しを行います。残っているのは、台の記録を内容とする切り詰めであり、一つの写しがそれを部品ごとに、切り詰められた平坦な証人へ送ります。タグの関数は、名前のついた十の位置から、読みの下で定義された小さな関数によって組み立て直されます。そして rd を、組み立て直した関数、三つの構造的な証人、台、pin の充足に施せば、記録の冒頭に立つ台の等式が届きます。ここでのどの操作も切り詰めの内部にとどまります。写しは、記録が存在するという事実を運び、向こう側で対応する事実を組み立てるのです。
PT.rec squash₁ (λ { (T , hT') → PT.map (λ { (b , (hpin , (hnum , (hE , (hc , (hd , (ha , h12))))))) → let ν : Fin 10 → S ν = ν' n0 n1 n2 n3 n4 n5 n6 n7 n8 n9 in ν , (E , (C , (T , (b , (rd ν E C T b hpin
残る欄は、平坦な記録が要求する向きに復元されます。校正の連言項は nums-out によってホスト層の Tags の等式族として読まれます。塔、閉性、正確なキー領域の充足はすでに必要な型をもつので、そのまま保たれます。問い合わせの原子の充足だけは通常の所属へ戻す必要があります。appAt-adequate に沿って移送すると、問い合わせの順序対が T の基礎集合に属することが得られます。
, ( nums-out ν E C T b γ hnum , ( hE , ( hc , ( hd , ( subst ⟨_⟩
tableAt の充足が、記録の最後の証明書を与えます。蓄積した継続を順に適用すると、入れ子の除去がすべて完了し、∥ GraphWitOn W x y γ ∥₁ の要素が得られます。二つの読みにより、枠組みの充足と、条件を満たす平坦な記録の命題的に切り詰められた存在とは、互いを含意します。これは二つの命題の間の一対の含意であって、標準的な表を選ぶ手続きではなく、表の値の一意性も主張しません。
(appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ)) ha , h12 )))))))))) }) hT' }) hC' }) hE' }) h0 }) h1 }) h2 }) h3 }) h4 }) h5 }) h6 }) h7 }) h8 }) h9 }) h where
存在論理式では十個のタグが別々の束縛値として現れますが、GraphWitOn は一つの関数 Fin 10 → S を要求します。局所関数 ν' は構成子の添字について場合分けし、この二つの表示を一致させます。最初の四つの分岐は a0 から a3 を順に返します。ここで意味論的な事実は使わず、構成子の添字と、論理式から取り出したスロットとの固定された対応だけを用います。
ν' : S → S → S → S → S → S → S → S → S → S → Fin 10 → S ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 zero = a0 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc zero) = a1 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc zero)) = a2 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc zero))) = a3
構成子の添字四から八についても、同じ場合分けが対応する値 a4 から a8 を返します。これらの分岐は添字写像 NN に従うため、nums-out が取り出した等式を、表と閉性の節がタグを要求するちょうどそのスロットで、再構成した関数に適用できます。
ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc zero)))) = a4 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc zero))))) = a5 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc zero)))))) = a6 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc zero))))))) = a7 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = a8
添字九の場合で Fin 10 が尽くされ、ν' は全域関数になります。したがって、十四個の別々の対象言語の証人は、ホスト側の記録では、一つの十項目のタグ関数と E、C、T、b によって正確に表されます。これは表示の変更にすぎず、新しいタグを作ることも、存在データを捨てることもありません。
ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = a9
変数で与える台
変数で台を与える証人型は、周囲の環境から参照を選びます。GraphWitAt B x y γ では、内部の台 b の基底集合が lookup B γ の基底集合と等しければよく、証明を伴って包装された要素そのものを同一視する必要はありません。参照を環境から読み取るため、後の論理式がグラフの外側に束縛を加え、それに応じて台のスロットを移しても、同じ証人型を使えます。
GraphWitAt : ∀ {n} → Fin n → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ) GraphWitAt B x y γ = GraphWitOn (lookup B γ) x y γ
論理式 satGraphAt B x y は、pin var Bi ≐ var (sh14 B) によってこの参照を実現します。新しく束縛された台のスロットを、十四の内部束縛の先へ移した元の台のスロットと等置するのです。したがって、この版は台を定数として埋め込みませんが、numsAt にある十個の標準数項の定数は残ります。論理式を不透明にすることで、より大きな記述はこれを一つの関係として利用できます。その充足を組み立て、また読み出すための公開インターフェースは、証人についての二つの読みが与えます。
opaque satGraphAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n satGraphAt B x y = satGraphOn (var Bi ≐ var (sh14 B)) x y
satGraphAt の本体を展開するのは、証人に関する二つの含意を確立する間だけです。この範囲では、大きな論理式と GraphWitAt を欄ごとに比較できます。その外では、後の議論は graphAt-in と graphAt-out の正確な主張だけを使うため、十四個の束縛は同じ関係の内部的な表示にとどまります。
opaque unfolding satGraphAt
内向きの読みでは、pin の読みの仮定は恒等関数です。変項の等式の充足は、GraphWitAt にすでに記録された基底集合の等式そのものだからです。したがって、任意の周囲の環境における命題的に切り詰められた証人の記録から、その環境での satGraphAt の充足が得られます。この柔軟性は、DefAt の中で DefBody が要素のスロットと隣接する二つの存在量化の下にグラフを置く場面と、DenoteBody の中でグラフが新たな五つのスロットの先に同じ台を参照する場面で具体的に使われます。どちらでも、台は呼び出し側の環境に残り、定数としてグラフの論理式へ代入されません。
graphAt-in : ∀ {n} (B x y : Fin n) (γ : S ^ n) → ∥ GraphWitAt B x y γ ∥₁ → ⟨ γ ⊨ satGraphAt B x y ⟩ graphAt-in B x y γ = graphOn-in (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ e → e)
外向きの読みは、変数で与える台のインターフェースを完成させます。satGraphAt B x y の充足証明から、GraphWitAt B x y γ が記録するのと同じ候補データと証明を、命題的切り詰めのもとで取り出します。特に、内部で束縛された台の基礎集合は外側のスロット B の値と一致し、問い合わせるキーと値は引き続き外側のスロット x と y から読み取られます。graphOn-out に渡される恒等関数は、この変数同士を固定する条件をそのまま表しています。後の一意性の議論のように、命題を証明するためなら得られた切り詰めを除去できますが、特定の塔、部分符号について閉じたキー集合、あるいは特定の表を選んで保持することはできません。
graphAt-out : ∀ {n} (B x y : Fin n) (γ : S ^ n) → ⟨ γ ⊨ satGraphAt B x y ⟩ → ∥ GraphWitAt B x y γ ∥₁ graphAt-out B x y γ = graphOn-out (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ h → h)
台を定数に固定する
台が要素 B としてすでに与えられている場合、第二の具体化では外側の台のスロットを参照せず、定数 B を用います。自由な位置はちょうど二つで、suc zero が入力のキー、zero が候補となる出力値です。枠組みの残りは変わらないため、この論理式が述べるのは、局所的な条件を満たす何らかの候補データがこの問い合わせを記録することだけです。具体的には、SatisfactionClauses が候補表の全域性、キー領域の制限、十個の局所方程式を与えますが、それらの節にも、この具体化そのものにも、グラフを一価にする条件はありません。
opaque satGraph : S → Formula S 2 satGraph B = satGraphOn (var Bi ≐ con B) (suc zero) zero
証人型は、この二項関係の向きを明示します。環境 y ∷ x ∷ [] では、最も内側の位置に y、その次に x が入ります。したがって GraphWit B x y は、候補表が x をキー、y を値とする符号化された対を含むことを表します。参照する台は固定された要素 B です。この記録にはさらに、校正されたタグ、候補となる環境の塔、部分符号について閉じた候補キー集合、キー領域がちょうどその集合である表、そして tableAt が要求する証明が入ります。キー集合に仮定されるのは局所的な閉性だけであり、この定義はそれを実際の論理式キーすべてからなる集合と同一視しません。
GraphWit : (B x y : S) → Type (ℓ-suc ℓ) GraphWit B x y = GraphWitOn B (suc zero) zero (y ∷ x ∷ [])
定数による固定条件についても、証人に関する同じ二つの含意が成り立ち、この範囲でだけ satGraph を展開して証明します。これらの含意は、大きな存在論理式を安定した二項関係として扱えるようにします。graph-in は命題的に切り詰められた候補記録から関係を確立し、graph-out は関係からまさにその切り詰めを復元します。UniformSatisfaction はこの形の satGraph B を抽象的再帰のグラフパラメータとして使います。
opaque unfolding satGraph
内向きの読みは、定数による固定条件に一般の変換を適用します。記録の先頭には、内部で束縛された台と B の基礎集合が等しいという証明があります。対象言語の等式 var Bi ≐ con B の充足はまさにこの内容をもつので、固定条件を読む関数は恒等関数です。残りの成分はすでに、タグの校正、塔と閉性の条件、正確なキー領域、問い合わせた表要素、そしてまとめられた表の条件を証明しています。この記録を graphOn-in で写しても命題的切り詰めは保たれます。得られるのは適切なデータが存在するという証明であって、後で使う一組を選ぶことではありません。
graph-in : (B x y : S) → ∥ GraphWit B x y ∥₁ → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ graph-in B x y = graphOn-in (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ e → e)
外向きの読みはこの変換を逆にたどり、本章を締めくくります。二項の論理式の充足から得られるのは、問い合わせた要素を含む候補の記録を命題的に切り詰めたものだけです。これが、この章における充足関係グラフの正確な限界です。続く PinnedRecursion は、実際の論理式について構造的再帰を行い、そのキーが候補キー集合に属し、候補表がそこで値を記録しているならば、その値が外部で定義された値 Sat と同じ基礎集合をもつことを証明します。SatisfactionBridge は別に、その値への所属を制限構造での充足と結びつけ、値に意味論的な内容を与えます。最後に UniformSatisfaction は、実際の領域 AllCodes B 上で satGraph B を用います。その領域での存在と、固定性から得られる一意性を合わせて抽象的再帰定理の仮定を満たし、一つの一様な表を組み立てます。本章の二つの読みは、これらの後続の議論が扱う表現された関係を与えますが、それ自体が表を選んだり、一意性を証明したり、その意味論を説明したりするわけではありません。
graph-out : (B x y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → ∥ GraphWit B x y ∥₁ graph-out B x y = graphOn-out (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ h → h)