この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

宇宙レベルとこの一つの古典的パラメータを固定する。これから定める関係が論理式キー x と集合 y について成り立つのは、台上の局所的な条件を満たす候補の充足関係表が x で y を記録するとき、かつそのときに限る。この段階で主張するのは、そのような局所データの存在だけである。正準な表を選ぶことも、すべてのキーで値が一意であることを証明することもない。

module L.Coding.SatisfactionGraph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

再帰的構成 Sat は各論理式に、それを満たす環境の集合を割り当てる。しかし、このメタ理論上の割当てを L 上の一階定義の内部でそのまま名指すことはできない。本章の課題は、後でそのような問い合わせの関係として使える対象言語の二項論理式を与えることである。論理式の証人は、問い合わせるキーの周囲で再帰方程式を満たすのに十分な局所データを記述するが、正準な表や一価な表がすでに得られているとは仮定しない。

以下で用いる環境の塔のインターフェースが、必要な宇宙レベルでの排中律を仮定するため、本章もその仮定を受け取る。ただし、ここで組み立てる論理式が命題を排中律で場合分けするわけではない。量化子と結合子の意味は、すでに構成された一階意味論から得られる。

論理式の言語には、変数、定数、等号、連言、存在量化がある。定数を使えば、タグに用いる標準の数項のような固定された構成可能集合を論理式に直接入れられる。また、pr はグラフ要素となる順序対を符号化する。これらの論理式を読む意味論は周囲の階層から得られる。

候補データは三つの記述によって組織される。appAt は符号化された対をグラフ要素として読み、domAt T C は表 T のキー領域がちょうど C であることを述べ、closedAt C は C 内の複合論理式キーが必要とする直下の部分式キーも C に属することを要求する。domAt が述べるのは表のキー領域であり、後に表の値として現れる環境集合とは異なる。

残る記述は、局所的な再帰方程式を準備する。towerAt は符号化環境の候補となる各行を与え、Tags は十個の構成子タグのスロットを校正する。tableAt は、候補キー集合上の命題的に切り詰められた全域性、表項目のキーをその集合に限る条件、十個の局所的な外延方程式をまとめる。これらの材料が記述するのは、まだ候補関係だけである。PinnedRecursion は真正な論理式キーで必要となる条件付き一意性を証明し、SatisfactionBridge は独立に、外部の値 Sat への所属を制限構造での充足として解釈する。その後、UniformSatisfaction が AllCodes B 上で存在と固定された一意性を組み合わせ、一様な表を得る。

自由な位置を n 個もつ論理式の解釈環境は、n 個の台の要素からなるベクトルである。lookup はある位置に割り当てられた要素を読み、cons は環境の最も内側に新しい要素を加える。この規約により、任意の外側の環境の前に十四個の補助的な証人を置いても、元の問い合わせ位置を保てる。

対象言語の存在は命題的切り詰めによって解釈される。そのため、存在論理式の証明は証人が存在するという事実だけを残し、どの証人を用いたかを忘れる。これは充足関係グラフにとって本質的である。公開される読みは、適切なタグ、塔、キー集合、表が存在することを示せるが、利用者が候補の表を大域的に一つ選べるようなデータは公開しない。

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )

以下では、S を構成可能構造の台とする。その要素は階層の集合と、それが構成可能であることの証拠からなる。この構造の関係は命題値をとり、山括弧は証明が要素となる基礎の命題を取り出す。したがって、基礎となる階層集合の等しさや所属と、等号や所属を主張する対象言語の論理式とは区別しなければならない。

open hPropView 𝒮ʟ

判定 γ ⊨ φ は、対象言語の論理式 φ が構成可能な環境 γ のもとで成り立つことを意味する。これは意味論的な値の有限ベクトルを論理式の構文に結びつける。特に、キーとその候補値を問い合わせる外側の環境はメタ理論上の割当てであり、環境の塔に並ぶ符号化環境集合の一つではない。

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 → Vec S n → Vec 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) (γ : Vec 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) (γ : Vec 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) (γ : Vec 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 → Vec S n → Type (ℓ-suc ℓ)
  GraphWitOn W x y γ =
    Σ[ ν ∶ (Fin 10 → S) ] (Σ[ E ∶ S ] (Σ[ C ∶ S ] (Σ[ T ∶ S ] (Σ[ b ∶ S ] ((b .fst ≡ W .fst) × (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 ((lookup x γ) .fst) ((lookup y γ) .fst) ∈ T .fst ⟩ × ⟨ (ev ν E C T b γ) ⊨ tableAt Ti Bi Ci Ei NN ⟩))))))))))

satGraphOn の充足と平坦な記録を比較するため、pin、その参照 W、二つの問い合わせ位置、外側の環境を固定する。台の等式を除けば、記録の各欄はすでに枠組みの連言項の中に定まった解釈をもっている。したがって、追加で必要な仮定は pin の読み rd だけである。内向きの含意では等式 b .fst ≡ W .fst を pin の充足へ移し、外向きの含意では pin の充足をその等式として読み戻す。

module _ {n : ℕ} (pin : Formula S (14 + n)) (W : S)
         (x y : Fin n) (γ : Vec S n) where

内向きの読みは、切り詰められた証人の記録を、枠組み全体の充足へ変える。その仮定 rd は、pin をどう読むべきかを言う。十個のタグの値、塔、索引集合、表、台のどんな選択に対しても、台が参照と一致するなら、組み立てられた環境のもとで pin が充足される、というものである。入力は切り詰めであり、出力は充足、それ自体が切り詰めである。したがって証明全体は切り詰めの内部の一つの写しになる。平坦な記録を部品ごとに照らし合わせて、論理式が要求する十四重の証人へ送るのである。どこでも証人は選ばれない。切り詰めの間の写しは、証人が存在するという事実だけを運ぶ。

graphOn-in : ((ν : Fin 10 → S) (E C T b : S) → b .fst ≡ W .fst
               → ⟨ ev ν E C T b γ ⊨ pin ⟩)
           → ∥ GraphWitOn W x y γ ∥₁ → ⟨ γ ⊨ satGraphOn pin x y ⟩
graphOn-in rd = 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

節の族の証明書を最後の連言項に置いた後は、入れ子になった切り詰めを戻せば十分である。map₁ の呼び出しが最も外側の切り詰めを与える。その写像が、最も外側の存在量化に必要な証人の対を返すからである。その対の内側にある十三回の明示的な挿入が、台に至るまでの残りの存在量化を順に与える。したがって、切り詰められた平坦な記録から十四重の存在量化の充足が得られるが、選ばれたデータが命題的切り詰めの外へ出ることはない。

        , h12 ))))))
      ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })

外向きの読みはこの旅を逆向きにたどる。仮定 rd は、今度は pin を逆方向に回する。組み立てられた環境のもとでの pin の充足から、台の等式を回復するのである。入力は枠組み全体の充足であり、その十四重の存在量化はどれも切り詰められている。出力は切り詰められた証人の記録である。証明は存在量化を一段ずつ除去し、そのどれもが、記録の切り詰めという命題を目指す。したがってそれぞれが正当である。この補題は記録そのものを産み出すとは決して主張せず、一つが存在するという事実だけを主張する。

graphOn-out : ((ν : Fin 10 → S) (E C T b : S)
                → ⟨ ev ν E C T b γ ⊨ pin ⟩ → b .fst ≡ W .fst)
            → ⟨ γ ⊨ satGraphOn pin x y ⟩ → ∥ GraphWitOn W x y γ ∥₁
graphOn-out rd h = rec₁ squash₁ (λ { (n9 , h9) →
  rec₁ squash₁ (λ { (n8 , h8) →

rec₁ を一回適用するたびに、切り詰められたタグの証人を一つ除去し、命題である同じ目標 ∥ GraphWitOn W x y γ ∥₁ を保つ。こうしてスロット九から三までの値を次の継続へ渡せるが、切り詰められていないデータとして外へ出すことはできない。この正当な除去を繰り返すことで、対象言語の入れ子の存在量化を一つの平坦な切り詰められた記録に対応させられる。

  rec₁ squash₁ (λ { (n7 , h7) →
  rec₁ squash₁ (λ { (n6 , h6) →
  rec₁ squash₁ (λ { (n5 , h5) →
  rec₁ squash₁ (λ { (n4 , h4) →
  rec₁ squash₁ (λ { (n3 , h3) →

十個すべてのタグの値を復元すると、同じ命題への除去によって候補の塔 E とキー集合 C に到達する。hE' と hC' は、表、台、各証明をまだ含んでいる切り詰められた残りを表す名前であり、塔や閉性の条件の証明ではない。それらの証明は最後の連言の中に残り、T と b も切り詰めの内部で現れた後に初めて記録へ入る。

  rec₁ squash₁ (λ { (n2 , h2) →
  rec₁ squash₁ (λ { (n1 , h1) →
  rec₁ squash₁ (λ { (n0 , h0) →
  rec₁ squash₁ (λ { (E , hE') →
  rec₁ squash₁ (λ { (C , hC') →

最も内側の段で、証明はそれ以上除去するのではなく、写しを行う。残っているのは、台の記録を内容とする切り詰めであり、一つの写しがそれを部品ごとに、切り詰められた平坦な証人へ送る。タグの関数は、名前のついた十の位置から、読みの下で定義された小さな関数によって組み立て直される。そして rd を、組み立て直した関数、三つの構造的な証人、台、pin の充足に施せば、記録の冒頭に立つ台の等式が届く。ここでのどの操作も切り詰めの内部にとどまる。写しは、記録が存在するという事実を運び、向こう側で対応する事実を組み立てるのである。

  rec₁ squash₁ (λ { (T , hT') →
  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 → Vec 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) (γ : Vec 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) (γ : Vec 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)