充足関係表の Δ₀ 記述

module SatSound {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (tg : Tags γ N)
  (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) (hC : ⟨ γ ⊨ codesAt C w E N ⟩)
  (hT : ⟨ γ ⊨ tableAt T w C E N ⟩) where

open Alphabet W

候補の表、コード領域、環境の塔が表す底の集合を、それぞれ Tv、Cv、Ev と書く。節の意味論は、これらの集合についての有界論理式を、構造的な議論に必要な周囲の所属と等しさへ結ぶ橋を与える。

open Bridge W
private
  Tv = (lookup T γ) .fst
  Cv = (lookup C γ) .fst
  Ev = (lookup E γ) .fst

Ev の項目が、すでに n と F の符号化された対として表されているとする。塔を読むと、命題的切り詰めのもとでアリティ k と等式 n = # k が得られる。同時に得られる F = envSet W k を忘れると、候補の論理式の鍵を解析するためにちょうど必要なアリティの事実になる。逆向きの塔の読みは各々の実際のアリティの項目を Ev に入れるので、実際の鍵を Cv に入れることもできる。

  module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
  arity : (n F : S) → ⟨ pr (n .fst) (F .fst) ∈ Ev ⟩ → ∥ Σ[ k ∶ ℕ ] (n .fst ≡ # k) ∥₁
  arity n F q∈ = map₁ (λ { (k , (qk , _)) → k , qk }) (TR.entry-out n F q∈)
  module CS = CodesSound C w E N γ W qw tg arity (hC .fst)
  module CC = CodesComplete C w E N γ W qw tg TR.entry-in (hC .snd)

仮定 hT は、全域性、領域条件、十個の構成子の節からなり、Frame はそれらの意味論的な読みを与える。SatSoundC の固定の議論は、全域性と十個の節を、環境の塔に関する事実および候補の符号領域の閉性に組み合わせる。固定すべき表の要素は、すでに実際の論理式の鍵における対として与えられているため、この段階で領域条件は必要ない。その条件は、後で任意の提示された表の対を読むときに使われる。

  module Fr = Frame T w C E N γ tg
  module SC = SatSoundC T w C E N γ W qw tg hE CS.closed hT

二つの領域条件は互いを補う形をしている。全域性は、Cv の各 c に対し、pr c y が Tv に属するような y が存在することを、命題的切り詰めのもとで与える。領域条件は Tv の任意の要素 e から始め、再び命題的切り詰めのもとで、e を pr c y と分解し、c が Cv に属することを与える。どちらも値や対の成分を大域的に選ばず、またどちら一方だけで表が一価の関係になるわけでもない。

  hTot = hT .fst
  hOn = hT .snd .fst

コード領域の完全性によって論理式 a の実際の鍵を Cv に入れ、その鍵に全域性を適用する。結論は、ある値とその鍵との対が Tv に属することを単に述べ、証人は命題的切り詰めのもとに残る。選ばれた値も復号関数も得られず、後では命題への消去にだけ使われる。

  sub : ∀ {n} (a : Formula Ab n) → ∥ Σ[ ya ∶ S ] ⟨ pr ((keyS W a) .fst) (ya .fst) ∈ Tv ⟩ ∥₁
  sub a = Fr.total-out hTot (keyS W a) (CC.key-in a)

固定の述語は次を言う。値 y と ψ のキーの対が候補の表に属するならば、y の底の集合は ψ の再帰的な充足集合の底の集合と等しくなる。固定されるのは底の集合だけである。y の構成可能性の証明も、論理式そのものも、これでは固定されない。

Pinned : ∀ {n} (ψ : Formula Ab n) → Type (ℓ-suc ℓ)
Pinned ψ = (y : S) → ⟨ pr ((keyS W ψ) .fst) (y .fst) ∈ Tv ⟩ → y .fst ≡ (SatW ψ) .fst

証明は ψ の構造再帰によって進む。Cv の閉性が直接の部分論理式の鍵を与え、全域性がその鍵での表の値を命題的切り詰めのもとでのみ与える。再帰的な仮定はそれらの子の値を固定し、対応する構成子の節は意味論的再帰と同じ外延条件を与える。そのため、外延性によって親の値が固定される。CC.key-in ψ は、ψ の鍵でこの議論を始めるために必要な、候補の符号領域への所属を与える。

pinned : ∀ {n} (ψ : Formula Ab n) → Pinned ψ
pinned ψ = SC.pinned ψ (CC.key-in ψ)

候補のコード領域の各要素は正準なコード集合に属する。候補の鍵の読みからアリティ、論理式、鍵の等式が得られるのは、命題的切り詰めのもとだけである。目標である正準集合への所属は命題なので、そこへ証人を消去し、その等式に沿って所属を運べる。この議論は論理式を選ばない。

C-out : (c : S) → ⟨ c .fst ∈ Cv ⟩ → ⟨ c .fst ∈ (AllCodes W) .fst ⟩
C-out c c∈ = rec₁ ((c .fst ∈ (AllCodes W) .fst) .snd)
  (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ (AllCodes W) .fst ⟩) (sym e) (key∈AllCodes W ψ) })
  (CS.key-out c c∈)

逆に、正準なコード集合の各要素は Cv に属する。正準集合への所属は、命題的切り詰めのもとで論理式の鍵としての表示を与え、コード領域の完全性がその鍵を候補領域に入れる。ここでも証人は所属を証明するためだけに使われ、復号器の定義には使われない。

C-in : (c : S) → ⟨ c .fst ∈ (AllCodes W) .fst ⟩ → ⟨ c .fst ∈ Cv ⟩
C-in c c∈ = rec₁ ((c .fst ∈ Cv) .snd)
  (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ Cv ⟩) (sym e) (CC.key-in ψ) })
  (AllCodes-out W c c∈)

塔の外向きの読みが扱うのは、すでに pr n F として表された項目である。命題的切り詰めのもとで自然数 k が得られ、n = # k かつ F = envSet W k となる。k を大域的に選ぶことも、この補題だけで Ev の任意の要素に符号化された対としての表示を与えることもない。

E-out : (n F : S) → ⟨ pr (n .fst) (F .fst) ∈ Ev ⟩
      → ∥ Σ[ k ∶ ℕ ] ((n .fst ≡ # k) × (F .fst ≡ (envSet W k) .fst)) ∥₁
E-out = TR.entry-out

塔の内向きの読みは、命題的切り詰めを伴わずに補完的な事実を与える。与えられた各自然数 k について、標準的な項目 pr (# k) (envSet W k) は Ev に属する。前の読みと合わせて標準的な符号化項目を双方向に制御するが、塔の任意の要素ごとにアリティを選ぶとは主張しない。

E-in : (k : ℕ) → ⟨ pr (# k) ((envSet W k) .fst) ∈ Ev ⟩
E-in = TR.entry-in

表の読みは、健全性の方向の中心である。それは、x と y の順序対としてすでに提示された要素に対してだけ述べられる。候補の表の任意の要素は、この補題の範囲ではない。

T-out : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ Tv ⟩
      → Σ[ mx ∶ ⟨ x .fst ∈ (AllCodes W) .fst ⟩ ] (y .fst ≡ (Table.val W W x mx) .fst)
T-out x y h = rec₁ (isPropΣ ((x .fst ∈ (AllCodes W) .fst) .snd) (λ mx → setIsSet _ _))
  (λ { (c , yc , (ee , c∈)) → rec₁ (isPropΣ ((x .fst ∈ (AllCodes W) .fst) .snd) (λ mx → setIsSet _ _))
    (λ { (k , ψ , e) →

対の等式は両辺の第一成分に分解され、コードの等式が、記録されたキーを、復号されたある論理式のキーと同一視する。その論理式のキーが正準なコード集合に属することは、輸送によって従う。

      let q = pr-inj ee
          qx : x .fst ≡ (keyS W ψ) .fst
          qx = q .fst ∙ e
          mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩
          mx = subst (λ u → ⟨ u ∈ (AllCodes W) .fst ⟩) (sym qx) (key∈AllCodes W ψ)

固定によって記録された値を再帰的な充足集合と同一視し、val-at によってその集合を同じ鍵における関数的な表の値と同一視する。結論は、正準なコード集合への所属と底の集合の等しさからなる。結論自体は命題的切り詰められていないが、依存対全体が命題なので、命題的切り詰められた復号から得られる。これは計算的な復号ではない。

      in mx , ( pinned ψ y (subst (λ u → ⟨ u ∈ Tv ⟩) (cong (λ a → pr a (y .fst)) qx) h)
              ∙ sym (cong (λ p → p .fst) (val-at W W ψ x mx qx)) ) })
    (CS.key-out c c∈) })
  (Fr.onC-out hOn (down (lookup T γ) (pr (x .fst) (y .fst)) h) h)

表の逆向きの読みでは、指定された正準コード x から始める。AllCodes W への所属により、命題的切り詰めのもとで、鍵が x である論理式 ψ が得られる。次に全域性から、再び命題的切り詰めのもとで、その論理式の鍵に記録された候補の値が得られる。

T-in : (x : S) (mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩) → ⟨ pr (x .fst) ((Table.val W W x mx) .fst) ∈ Tv ⟩
T-in x mx = rec₁ ((pr (x .fst) ((Table.val W W x mx) .fst) ∈ Tv) .snd)
  (λ { (k , ψ , e) → rec₁ ((pr (x .fst) ((Table.val W W x mx) .fst) ∈ Tv) .snd)
    (λ { (y , my) →
      subst (λ u → ⟨ u ∈ Tv ⟩)

候補の値は、再帰的な充足の集合に固定され、値の補題がそれを関数的な表の値と整列させる。そして所属が、順序対の等式に沿って運ばれる。どちらの消去も、命題である表の所属に着地する。

        (cong₂ pr (sym e) (pinned ψ y my ∙ sym (cong (λ p → p .fst) (val-at W W ψ x mx e))))
        my })
    (sub ψ) })
  (AllCodes-out W x mx)

module SatHolds {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (qT : (lookup T γ) .fst ≡ (SatGraph.pairs W) .fst)
  (qC : (lookup C γ) .fst ≡ (AllCodes W) .fst) (qE : (lookup E γ) .fst ≡ (Tower.tower W) .fst)
  (tg : Tags γ N) where

open Alphabet W

表と符号領域のスロットにある基礎集合を Tv と Cv と書く。同定 qT と qC は、それらの所属事実をそれぞれ実際のグラフと正準な符号集合へ運ぶ。したがって、すでに対の形で提示された表の要素はグラフの読みによって扱えるが、符号の復号は命題的切り詰めのもとでのみ得られる。以下の等式はすべて、引き続き階層の基礎集合を比較する。

open Bridge W
private
  Tv = (lookup T γ) .fst
  Cv = (lookup C γ) .fst

論理式のキーと同一視された符号のもとでの表の値は、その論理式の再帰的な充足の集合と等しくなる。証明は、本物の充足のグラフから対を読み出し、提示されたキーと論理式のキーの同一視に沿って第二成分を運び、値の補題で締めくくる。

  val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → c .fst ≡ (keyS W ψ) .fst
       → ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩ → yc .fst ≡ (SatW ψ) .fst
  val≡ ψ c yc qc h =
    let p = SatGraph.pairs-out W c yc (subst (λ u → ⟨ pr (c .fst) (yc .fst) ∈ u ⟩) qT h)
    in p .snd ∙ cong (λ p → p .fst) (SatGraph.valOf≡ W c (p .fst)) ∙ cong (λ p → p .fst) (val-at W W ψ c (p .fst) qc)

コード領域の要素が pr (# n) z として表されているなら、それを AllCodes W へ運ぶことで、命題的切り詰めのもとで復号できる。すなわち、ペイロードが z である論理式 ψ : Formula Ab n が存在する。論理式は選ばれず、復号の一意性も得られないので、復号関数は定義されない。

  decode : (c : S) → ⟨ c .fst ∈ Cv ⟩ → (n : ℕ) (z : V ℓ) → c .fst ≡ pr (# n) z
         → ∥ Σ[ ψ ∶ Formula Ab n ] (z ≡ cd ψ) ∥₁
  decode c c∈ = Match.decodeAll W c (subst (λ u → ⟨ c .fst ∈ u ⟩) qC c∈)

候補コード c は、正準なコード集合との整合によって、実際のグラフへの正しい入力になる。そのグラフの値から表の項目を得て、Tv と SatGraph.pairs W の整合に沿って運び戻す。得られる存在の主張は、全域性の節が要求する通り、命題的切り詰めのもとに残る。

  tot : (c : S) → ⟨ c .fst ∈ Cv ⟩ → ∥ Σ[ yc ∶ S ] ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩ ∥₁
  tot c c∈ =
    let mx = subst (λ u → ⟨ c .fst ∈ u ⟩) qC c∈
    in ∣ SatGraph.valOf W c mx , subst (λ u → ⟨ pr (c .fst) ((SatGraph.valOf W c mx) .fst) ∈ u ⟩) (sym qT) (SatGraph.pairs-in W c mx) ∣₁

実際のグラフは、任意の表の要素に必要な形も与える。命題的切り詰めのもとで、その各要素は、あるコードとそのグラフの値からなる符号化された対であり、そのコードは Cv に属する。これは存在だけを述べる分解であり、各要素の成分を選ぶものではない。

  onc : (e : S) → ⟨ e .fst ∈ Tv ⟩
      → ∥ Σ[ c ∶ S ] Σ[ yc ∶ S ] ((e .fst ≡ pr (c .fst) (yc .fst)) × ⟨ c .fst ∈ Cv ⟩) ∥₁
  onc e e∈ = map₁
    (λ { (x , mx , ee) → x , SatGraph.valOf W x mx , (ee , subst (λ u → ⟨ x .fst ∈ u ⟩) (sym qC) mx) })
    (SatGraph.pairs-shape W e (subst (λ u → ⟨ e .fst ∈ u ⟩) qT e∈))

SatHoldsC.holds への入力は異なる役割を担う。実際の環境の塔が環境の行を与え、val≡ が実際の論理式の鍵での値を同定し、decode が形の定まった符号から論理式を命題的切り詰めのもとでのみ復号し、tot と onc が二つの領域条件を示す。構造的な議論は、続いて十個の構成子の節をすべて検証する。命題的に切り詰められたアリティ、論理式、分解を使うときは、対応する節が満たされるという命題にのみその証人を消去する。復号器や表の値の選択がその外へ出ることはない。

holds : ⟨ γ ⊨ tableAt T w C E N ⟩
holds = SatHoldsC.holds W T w C E N γ qw tg
  (TowerHolds.holds E w (N f0) γ W qw qE (tg f0)) val≡ decode tot onc

module SatRead {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (tg : Tags γ N) (h : ⟨ γ ⊨ satAt T w C E N ⟩) where

private module SS = SatSound T w C E N γ W qw tg
          (satAt-out T w C E N γ h .fst) (satAt-out T w C E N γ h .snd .fst) (satAt-out T w C E N γ h .snd .snd)

コードについては、二方向の読みが AllCodes W への所属を比較する。塔の項目については、標準的な対 pr (# k) (envSet W k) を読んだり挿入したりする。表の項目については、提示された対を正準コードにおける関数的な表の値と比較する。この三種類の結論を区別しておくことで、根拠のない強い一意性の主張を避けられる。

open SS public using ( C-out; C-in; E-out; E-in; T-out; T-in )