充足関係表を記述する

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

対象言語から、メタ言語にある論理式上の再帰を直接呼び出すことはできません。そこで、その再帰が作るべきグラフを有界な仕方で記述する必要があります。本章では T を、論理式の鍵と環境集合からなる候補関係とみなし、一致する各要素が従うべき局所方程式を調べます。その答えは十個の構成子の節と、T の第一射影に関する二条件です。意味論的な正しさ、一意性、符号領域の閉性、正準なデータの存在には、さらに後の議論が必要です。

{-# OPTIONS --cubical --safe --guardedness #-}

この記述には二つの水準があります。Agda は構成を検査するメタ理論を与え、以下で組み立てる論理式は構成可能な構造の一階対象言語に属します。本章は排中律を仮定しません。直観主義的に妥当な演算から論理式を組み立て、構文上の有界性を示すだけだからです。

open import Base.Prelude
module L.Coding.SatisfactionClauses {ℓ : Level} where

j 個の自由な枠をもつ論理式は、それらの枠に構成可能な台の元を入れてから解釈されます。所属、等号、命題結合子、有界量化子だけで、以下のすべての節を述べられます。最後の Δ₀ の証人が扱うのは、この対象言語の構文です。それだけで節を解釈したり、節に現れる証人を与えたりするものではありません。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ )
open import L.Constructible {ℓ} using ( 𝒮ʟ )

候補関係は符号化された順序対によって表されます。本章を組織する形は三つあります。環境の塔の要素はアリティ ar と環境集合 F を対にし、論理式の鍵は同じアリティとタグ付きペイロードを対にし、T の要素はその鍵と候補値集合をさらに対にします。有界な対の読みがこれらの成分を取り出し、後続と cons の述語がそれぞれアリティの増加と符号化環境の拡張を記述します。

open import L.Coding.Model {ℓ} using ( prAtL )
open import L.Coding.Expressions {ℓ} using ( sucAtL; consAtL )
open import L.Coding.Quantification {ℓ} using
  ( f0; f1; i0; i1; i2; i3; i4; i5; i6; i8; i9; i11; i12; i14; i16; i17; i19; sh
  ; sndEx; sndAll; bothEx; bothAll; bigAnd )

論理式の構成子にはちょうど十個の位置があり、Fin 10 で添字付けられます。その添字を自然数へ移すことで、一つの族から対応する節を選べます。ただし、ここでタグの枠に入る値はまだ任意のパラメータです。各枠を意図された標準数項と同定するのは、後の Tags 仮定です。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.Unit using ( tt )

対象言語の変数はすべて、構成可能な構造の台 S 上を動きます。T、C、w のような枠は付値内の位置を名指すだけで、評価された後に初めて構成可能集合を表します。この区別により、構文上の節を、メタ理論における充足関係表や符号集合の構成と取り違えずに済みます。

open hPropStructure 𝒮ʟ using ( S )

表の枠組みと十個の節

最初の再利用可能な考えは、正確な外延条件です。候補集合 y、基準集合 F、性質 φ に対し、extB の前半は y の各要素が F に属して φ を満たすと述べ、一方の包含を与えます。後半は、F のうち φ を満たすすべての要素が y に属すと述べ、逆の包含を与えます。したがって extB は y を、F の中で φ が切り出す部分集合として外延的に特徴づけますが、その集合を構成せず、存在も主張しません。

extB : ∀ {j} → Fin j → Fin j → Formula S (1 + j) → Formula S j
extB y F φ = ∀̇∈ (var y) ((var i0 ∈̇ var (sh 1 F)) ∧̇ φ)
           ∧̇ ∀̇∈ (var F) (φ ⇒̇ (var i0 ∈̇ var (sh 1 y)))

符号化された対の第二成分 v が既知のとき、fstAll は対の符号化に使われる容器を有界かつ全称的にたどります。対の述語が第一成分の候補を同定するたびに、その成分を付値へ加えたところで本体が成り立たなければなりません。二段の有界全称は順序対の集合論的表現のためにあり、数学的には、可能なすべての分解に対して第一成分を一度だけ条件付きで読む操作です。

fstAll : ∀ {j} → Fin j → Fin j → Formula S (2 + j) → Formula S j
fstAll x v body = ∀̇∈ (var x) (∀̇∈ (var i0) (prAtL (sh 2 x) i0 (sh 2 v) ⇒̇ body))

論理式上の再帰では、まず同じアリティでの読み取りが必要です。subAt T ar a body は、鍵が対 (ar,a) である T のすべての要素について body を要求します。これは一致する要素すべてに対する全称的な含意なので、要素を選ばず、値の一意性も示しません。その鍵に要素がなければ条件は空虚に成り立ちえます。後で要素を得るには、全域性に加え、子の鍵が符号領域に属するという別の証明が必要です。

subAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S (4 + j) → Formula S j
subAt T ar a body = ∀̇∈ (var T) (bothAll i0 (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body))

量化された論理式の本体では利用できる変数が一つ増えるため、再帰的な読み取りはアリティを変えなければなりません。subSucAt T ar a body は、鍵が (ar',a) であるすべての表要素を調べ、さらに ar' = suc ar という条件を課してから body を要求します。同じアリティの読みと同様に、要素もその分解も全称的に量化されています。この論理式は ar' や値を選ばず、持ち上げられた子の鍵が T に現れることも保証しません。

subSucAt : ∀ {j} → Fin j → Fin j → Fin j → Formula S (6 + j) → Formula S j
subSucAt T ar a body =
  ∀̇∈ (var T) (bothAll i0 (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body)))

項の評価には二つの符号形があります。tmIs t z v N0 N1 は、t が v を収めた定数の符号であるか、添字 i を収めた変数の符号であり、グラフ要素 (i,v) が符号化環境 z に属することを述べます。選言と変数添字の証人は、命題的切り詰めの下で解釈されます。また、後の Tags 仮定が N0 と N1 をゼロと一の数項に同定するまでは、これらはタグの枠にすぎません。任意の多値関係 z では、同じ変数符号が複数の候補値を検証しえます。

tmIs : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S j
tmIs t z v N0 N1 =
  prAtL t N0 v ∨̇ sndEx t N1 (∃̇∈ (var (sh 2 z)) (prAtL i0 i1 (sh 3 v)))

以下の五つの構成子関係は、候補関係 T、台を与える境界 w、十個のタグ枠からなる族 N という三つのパラメータを共有します。局所名 N0 と N1 は、最初の二つのタグ枠を、新たに束縛された変数の先まで移すだけです。この添字の調整は参照先を保ちますが、枠を標準数項と同定する等式は加えません。

module Rel {m : ℕ} (T w : Fin m) (N : Fin 10 → Fin m) where
  private
    N0 N1 : ∀ {j} → Fin (j + m)
    N0 {j} = sh j (N f0)
    N1 {j} = sh j (N f1)

二つの子の値 ya と yb を読んだ後、二項の節は、一つの符号化環境 z がそれらとどう関わるかを調べます。二つの命題は単に z ∈ ya と z ∈ yb であり、パラメータ op がそれらを結びます。op を連言、選言、含意でそれぞれ具体化することで、三つを同じ条件へ押し込めず、対応する極性を保てます。

  binBody : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (24 + m)
  binBody op = op (var i0 ∈̇ var i5) (var i0 ∈̇ var i1)

符号化された論理式の非有界量化子を記述するとき、記述側の論理式は w を明示的な境界として使います。q を ∃[]-syntax とすれば、ある x ∈ w が条件を満たすことを命題的切り詰めの下で主張するだけです。∀[]-syntax とすれば、すべての x ∈ w が条件を満たさなければなりません。どちらの場合も内側の条件は、x を z の先頭へ cons して得られる符号化拡張 e' が本体の値集合に命題的に切り詰められて存在することだけを求めます。大域的に選ばれた拡張関数は得られません。

  quBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S (19 + m)
  quBody q = q (var (sh 19 w)) (∃̇∈ (var i4) (consAtL i0 i1 i2))

有界量化子では、境界となる項の値も求めなければなりません。全称の場合は ∀[]-syntax と含意を組み合わせ、tmIs が検証するすべての候補値 v、さらに v に属するすべての x ∈ w について、本体の値集合に符号化拡張が命題的に切り詰められて存在することを要求します。存在の場合は ∃[]-syntax と連言を組み合わせ、そのような v、x、拡張が命題的に切り詰められて存在すれば十分です。符号化環境の関係が多値なら、この極性の違いは実質的です。この節は関係を修復せず、項の値の一意性も示しません。

  bqBody : (∀ {j} → Term S j → Formula S (suc j) → Formula S j)
         → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (22 + m)
  bqBody q c =
    q (var (sh 22 w)) (c (tmIs i9 i1 i0 N0 N1)
      (q (var (sh 23 w)) (c (var i0 ∈̇ var i1) (∃̇∈ (var i5) (consAtL i0 i1 i3)))))

原子論理式は子論理式を再帰的に参照しません。そのペイロードは二つの項の符号からなるので、原子の本体は、tmIs で検証される二つの値 v,x ∈ w が命題的に切り詰められて存在することを求め、その上で指定された原子関係を検査します。所属の場合は v ∈ x を使い、等号の場合は v と x を比較します。項の値は T の要素からではなく、定数または変数の符号形から直接得られます。

  atomBody : Formula S (18 + m) → Formula S (16 + m)
  atomBody rel =
    ∃̇∈ (var (sh 16 w)) (∃̇∈ (var (sh 17 w))
      (tmIs i4 i2 i1 N0 N1 ∧̇ (tmIs i3 i2 i0 N0 N1 ∧̇ rel)))

偽は最も単純な外延方程式を与えます。その性質は成り立ちえないので、順方向の包含は候補値 yc に要素がないことを述べます。逆方向の包含は、F の要素が偽を満たすことはないため直ちに成り立ちます。こうしてこの節は yc を空集合として特徴づけますが、空の値や表要素を構成しません。

  botRel : Formula S (12 + m)
  botRel = extB i0 i8 ⊥̇

二項結合子では、ペイロードを二つの論理式符号 a と b に分解します。続く二回の同アリティ読み取りは、子の鍵 (ar,a) と (ar,b) に一致する T のすべての値をたどります。得られる子の値の組合せごとに、extB が二項の本体によって yc を特徴づけます。したがって候補関係が多値なら、すべての組合せに方程式が課されます。この関係構成子は、どちらの子の値についても存在や一意性を仮定しません。

  binRel : (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (12 + m)
  binRel op =
    bothAll i3 (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (binBody op))))

非有界量化論理式のペイロードは、その本体の符号です。この関係はその符号を後続アリティでだけ読み、extB によって、候補値と量化子本体を満たす環境とを比較します。符号化された量化子は意味論的には意図された台全体を動きますが、記述側の論理式は明示された集合 w の上を動きます。このため記述は有界に保たれます。

  quRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j) → Formula S (12 + m)
  quRel q = subSucAt (sh 12 T) i9 i3 (extB i6 i14 (quBody q))

有界量化子のペイロードは、境界となる項の符号と本体の符号からなる対 (t,a) です。再帰的に読み取られるのは a だけで、ここでも後続アリティが使われます。t は tmIs によって局所的に評価されます。二つのパラメータが後で正確な極性を与えます。有界全称は ∀[]-syntax と含意を使い、有界存在は ∃[]-syntax と連言を使います。

  bqRel : (∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → (∀ {j} → Formula S j → Formula S j → Formula S j) → Formula S (12 + m)
  bqRel q c = bothAll i3 (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (bqBody q c)))

原子のペイロードでは、対の読みが二つの項符号を取り出し、extB が F 内の候補となる各符号化環境に原子の本体を適用します。T から子の鍵を読むことはありません。この区別は構文木を反映しています。論理式は直下の部分論理式を再帰的にたどりますが、この小さな項言語は二つの符号形から直接解釈されます。

  atomRel : Formula S (18 + m) → Formula S (12 + m)
  atomRel rel = bothAll i3 (extB i3 i11 (atomBody rel))

最初の四つのタグは、四つの正確な真理条件を述べます。タグの枠が Tags によって校正されると、タグ 0 は所属原子になります。v と x がそれぞれ第一、第二の項の値なら、必要な条件は v ∈ x です。タグ 1 は等号原子で、v = x を要求します。タグ 2 と 3 は、同じアリティの子に関する二つの主張 z ∈ ya と z ∈ yb を、それぞれ連言と選言で結びます。校正より前には、これらは対応するタグの枠によって選ばれる節にすぎず、その枠に標準の数項がすでに入っているとはいえません。

  relN : ℕ → Formula S (12 + m)
  relN 0 = atomRel (var i1 ∈̇ var i0)
  relN 1 = atomRel (var i1 ≐ var i0)
  relN 2 = binRel _∧̇_
  relN 3 = binRel _∨̇_

タグ 4 は、残る二項の極性を与えます。左の子から右の子へ、z ∈ ya が z ∈ yb を含意します。タグ 5 は、偽の外延を空にします。タグ 6 と 7 は一つの本体を後続アリティで読み、タグ 6 は w 上の ∃[]-syntax、タグ 7 は ∀[]-syntax を使います。タグ 8 は有界全称です。各 v ∈ w について、tmIs は v が境界となる項の値であることを検証する前件です。続いて各 x ∈ w について、所属 x ∈ v が前件となり、本体の値集合に符号化拡張が命題的に切り詰められて存在することを要求します。

  relN 4 = binRel _⇒̇_
  relN 5 = botRel
  relN 6 = quRel ∃̇∈
  relN 7 = quRel ∀̇∈
  relN 8 = bqRel ∀̇∈ _⇒̇_

タグ 9 は存在の極性をもちます。∃[]-syntax と連言を使い、tmIs で検証されるある v ∈ w、x ∈ v を満たすある x ∈ w、および本体の値集合にある符号化拡張が、命題的に切り詰められて存在することだけを要求します。これで 0 から 9 までの十個の場合がそろいます。10 以上の自然数に対して relN は真を返しますが、この最後の方程式が表の仕様に場合を加えることはありません。k : Fin 10 ならば、toℕ k は必ず 0 から 9 までの間にあるからです。

  relN 9 = bqRel ∃̇∈ _∧̇_
  relN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) = ⊤̇

これで構成子関係を共通の枠へ置けます。結び付けるデータは、環境の塔の対、同じアリティとタグ付きペイロードをもつ論理式符号、そしてその符号における T の候補要素です。同じ局所関係モジュールを再利用することで、どのタグも同じ T、w、二つの項符号タグの解釈の下で判定されます。

module Clause {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) where
  private
    module R = Rel T w N

k を固定すると、節は正確な連鎖をたどります。すべての q ∈ E と各分解 q=(ar,F)、c=(ar,p) を満たすすべての c ∈ C、各分解 p=(N k,r)、さらに e=(c,yc) を満たすすべての e ∈ T を考えます。完全に一致する各枠において、yc は relN (toℕ k) を満たさなければなりません。各分解は全称的な含意で条件付けられているため、この節はこれらの枠のデータが存在するとは主張しません。また、F と N k を与えられた値として扱うだけで、真の環境集合や k に対応する数項とは同定しません。

  clause : Fin 10 → Formula S m
  clause k =
    ∀̇∈ (var E) (bothAll i0 (∀̇∈ (var (sh 4 C)) (sndAll i0 i2 (sndAll i0 (sh 7 (N k))
      (∀̇∈ (var (sh 9 T)) (sndAll i0 i5 (R.relN (toℕ k))))))))

二つの領域条件は、全称的な局所節だけでは得られない存在を補います。total は、各 c ∈ C について、(c,yc) ∈ T となる yc が命題的に切り詰められて存在すると述べます。表要素もその対分解も切り詰めの内部に残ります。逆に onC は、すべての e ∈ T が、c ∈ C である (c,yc) として命題的に切り詰められて分解されると述べます。二条件を合わせると T の第一射影の領域は C になりますが、選択関数は得られず、T が単値になることもありません。

  total onC : Formula S m
  total = ∀̇∈ (var C) (∃̇∈ (var (sh 1 T)) (sndEx i0 i1 ⊤̇))
  onC = ∀̇∈ (var T) (bothEx i0 (var i1 ∈̇ var (sh 4 C)))

十個の局所節は、一つの有限連言にまとめられます。引数 9 が意味する添字型は Fin (suc 9)、すなわち Fin 10 であり、一つのケースが欠けているわけではありません。通常の連言もこの有限連言も、個々の節の内部にすでにある命題的切り詰めに加えて、新たな切り詰めを導入しません。

  ten : Formula S m
  ten = bigAnd 9 clause

論理式 tableAt は三つの要求を連言します。C 上の命題的に切り詰められた全域性、各表要素の鍵が C に属するという制限、そして十個すべての構成子の節です。これは候補関係に対する局所的で有界な仕様です。C が子の符号について閉じていること、E が意図された環境の塔であること、タグが標準的であること、値が一意であること、候補が正準な充足関係表であることは証明しません。後の章が、環境の塔と符号領域の記述、タグの校正、意味論的な橋渡し、固定の議論をそれぞれ与え、適切な候補を正準なデータへ結び付けます。

tableAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
tableAt T w C E N = Clause.total T w C E N ∧̇ (Clause.onC T w C E N ∧̇ Clause.ten T w C E N)

最後に、構造検査は tableAt が Δ₀ であることの証人を与えます。探索に見える量化はすべて、T、C、E、w、対の容器、または候補値集合のいずれかで制限されるため、記述する論理式に非有界量化子は入りません。この結論は構文を分類するだけです。適切な表の存在も、候補が各節を満たすことも示さず、意味論的な正しさ、絶対性、完全性のいずれも確立しません。

Δ₀-tableAt : ∀ {m} (T w C E : Fin m) (N : Fin 10 → Fin m) → Δ₀ (tableAt T w C E N)
Δ₀-tableAt T w C E N = checkΔ₀ (tableAt T w C E N) tt

まとめ

論理式 tableAt は、total、onC、および ten が集める十個の局所的な構成子の節の連言です。ここで total が与えるのは、C の各符号に対する表の値の命題的に切り詰められた存在だけです。onC は第一射影の領域を C に制限し、十個の節は全称的な局所外延方程式を課します。定理 Δ₀-tableAt が保証するのは、この記述が構文上有界であることだけです。

さらに後の議論で、E を意図された環境の塔と同定し、C が必要な子の符号を含むことを証明し、Tags によってタグの枠を校正し、正準なグラフと全体の述語 satAt に必要な双方向の意味論的な読み、固定、および完全性を確立しなければなりません。それらの結果も、充足関係表や大域的に選ばれた値も、この章では構成されません。