---
title: "充足関係表を記述する"
module: L.Coding.SatisfactionClauses
lang: ja
site: "Bedrock"
description: "充足関係表を記述する"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 63
canonical: https://bedrock.institute/ja/L.Coding.SatisfactionClauses.html
html: L.Coding.SatisfactionClauses.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionClauses.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, L.Constructible, L.Coding.Model, L.Coding.Expressions, L.Coding.Quantification]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.SatisfactionClauses.md, https://bedrock.institute/zh/L.Coding.SatisfactionClauses.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```
# 充足関係表を記述する
```agda
open import Base.Prelude
```
この記述には二つの水準がある。Agda は構成を検査するメタ理論を与え、以下で組み立てる論理式は構成可能な構造の一階対象言語に属する。本章は排中律を仮定しない。直観主義的に妥当な演算から論理式を組み立て、構文上の有界性を示すだけだからである。
```agda
module L.Coding.SatisfactionClauses {ℓ : Level} where
```
```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax using
( Formula; Term; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
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 )
```
対象言語から、メタ言語にある論理式上の再帰を直接呼び出すことはできない。そこで、その再帰が作るべきグラフを有界な仕方で記述する必要がある。本章では `T` を、論理式の鍵と環境集合からなる候補関係とみなし、一致する各要素が従うべき局所方程式を調べる。その答えは十個の構成子の節と、`T` の第一射影に関する二条件である。意味論的な正しさ、一意性、符号領域の閉性、正準なデータの存在には、さらに後の議論が必要である。
`j` 個の自由な枠をもつ論理式は、それらの枠に構成可能な台の元を入れてから解釈される。所属、等号、命題結合子、有界量化子だけで、以下のすべての節を述べられる。最後の Δ₀ の証人が扱うのは、この対象言語の構文である。それだけで節を解釈したり、節に現れる証人を与えたりするものではない。
候補関係は符号化された順序対によって表される。本章を組織する形は三つある。環境の塔の要素はアリティ `ar` と環境集合 `F` を対にし、論理式の鍵は同じアリティとタグ付きペイロードを対にし、`T` の要素はその鍵と候補値集合をさらに対にする。有界な対の読みがこれらの成分を取り出し、後続と cons の述語がそれぞれアリティの増加と符号化環境の拡張を記述する。
論理式の構成子にはちょうど十個の位置があり、`Fin 10` で添字付けられる。その添字を自然数へ移すことで、一つの族から対応する節を選べる。ただし、ここでタグの枠に入る値はまだ任意のパラメータである。各枠を意図された標準数項と同定するのは、後の `Tags` 仮定である。
対象言語の変数はすべて、構成可能な構造の台 `S` 上を動く。`T`、`C`、`w` のような枠は付値内の位置を名指すだけで、評価された後に初めて構成可能集合を表す。この区別により、構文上の節を、メタ理論における充足関係表や符号集合の構成と取り違えずに済む。
```agda
open hPropView 𝒮ʟ using ( S )
```
## 表の枠組みと十個の節
最初の再利用可能な考えは、正確な外延条件である。候補集合 `y`、基準集合 `F`、性質 `φ` に対し、`extB` の前半は `y` の各要素が `F` に属して `φ` を満たすと述べ、一方の包含を与える。後半は、`F` のうち `φ` を満たすすべての要素が `y` に属すと述べ、逆の包含を与える。したがって `extB` は `y` を、`F` の中で `φ` が切り出す部分集合として外延的に特徴づけるが、その集合を構成せず、存在も主張しない。
```agda
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` は対の符号化に使われる容器を有界かつ全称的にたどる。対の述語が第一成分の候補を同定するたびに、その成分を付値へ加えたところで本体が成り立たなければならない。二段の有界全称は順序対の集合論的表現のためにあり、数学的には、可能なすべての分解に対して第一成分を一度だけ条件付きで読む操作である。
```agda
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` を要求する。これは一致する要素すべてに対する全称的な含意なので、要素を選ばず、値の一意性も示さない。その鍵に要素がなければ条件は空虚に成り立ちえる。後で要素を得るには、全域性に加え、子の鍵が符号領域に属するという別の証明が必要である。
```agda
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` に現れることも保証しない。
```agda
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` では、同じ変数符号が複数の候補値を検証しえる。
```agda
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` は、最初の二つのタグ枠を、新たに束縛された変数の先まで移すだけである。この添字の調整は参照先を保つが、枠を標準数項と同定する等式は加えない。
```agda
module Rel {m : ℕ} (T w : Fin m) (N : Fin 10 → Fin m) where
```
```agda
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` を連言、選言、含意でそれぞれ具体化することで、三つを同じ条件へ押し込めず、対応する極性を保てる。
```agda
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'` が本体の値集合に命題的に切り詰められて存在することだけを求める。大域的に選ばれた拡張関数は得られない。
```agda
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`、拡張が命題的に切り詰められて存在すれば十分である。符号化環境の関係が多値なら、この極性の違いは実質的である。この節は関係を修復せず、項の値の一意性も示さない。
```agda
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` の要素からではなく、定数または変数の符号形から直接得られる。
```agda
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` を空集合として特徴づけるが、空の値や表要素を構成しない。
```agda
botRel : Formula S (12 + m)
botRel = extB i0 i8 ⊥̇
```
二項結合子では、ペイロードを二つの論理式符号 `a` と `b` に分解する。続く二回の同アリティ読み取りは、子の鍵 `(ar,a)` と `(ar,b)` に一致する `T` のすべての値をたどる。得られる子の値の組合せごとに、`extB` が二項の本体によって `yc` を特徴づける。したがって候補関係が多値なら、すべての組合せに方程式が課される。この関係構成子は、どちらの子の値についても存在や一意性を仮定しない。
```agda
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` の上を動く。このため記述は有界に保たれる。
```agda
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` と連言を使う。
```agda
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` から子の鍵を読むことはない。この区別は構文木を反映している。論理式は直下の部分論理式を再帰的にたどるが、この小さな項言語は二つの符号形から直接解釈される。
```agda
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` を、それぞれ連言と選言で結ぶ。校正より前には、これらは対応するタグの枠によって選ばれる節にすぎず、その枠に標準の数項がすでに入っているとはいえない。
```agda
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` が前件となり、本体の値集合に符号化拡張が命題的に切り詰められて存在することを要求する。
```agda
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 までの間にあるからである。
```agda
relN 9 = bqRel ∃̇∈ _∧̇_
relN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) = ⊤̇
```
これで構成子関係を共通の枠へ置ける。結び付けるデータは、環境の塔の対、同じアリティとタグ付きペイロードをもつ論理式符号、そしてその符号における `T` の候補要素である。同じ局所関係モジュールを再利用することで、どのタグも同じ `T`、`w`、二つの項符号タグの解釈の下で判定される。
```agda
module Clause {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) where
```
```agda
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` に対応する数項とは同定しない。
```agda
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` が単値になることもない。
```agda
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` であり、一つのケースが欠けているわけではない。通常の連言もこの有限連言も、個々の節の内部にすでにある命題的切り詰めに加えて、新たな切り詰めを導入しない。
```agda
ten : Formula S m
ten = bigAnd 9 clause
```
論理式 `tableAt` は三つの要求を連言する。`C` 上の命題的に切り詰められた全域性、各表要素の鍵が `C` に属するという制限、そして十個すべての構成子の節である。これは候補関係に対する局所的で有界な仕様である。`C` が子の符号について閉じていること、`E` が意図された環境の塔であること、タグが標準的であること、値が一意であること、候補が正準な充足関係表であることは証明しない。後の章が、環境の塔と符号領域の記述、タグの校正、意味論的な橋渡し、固定の議論をそれぞれ与え、適切な候補を正準なデータへ結び付ける。
```agda
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`、対の容器、または候補値集合のいずれかで制限されるため、記述する論理式に非有界量化子は入らない。この結論は構文を分類するだけである。適切な表の存在も、候補が各節を満たすことも示さず、意味論的な正しさ、絶対性、完全性のいずれも確立しない。
```agda
Δ₀-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` に必要な双方向の意味論的な読み、固定、および完全性を確立しなければならない。それらの結果も、充足関係表や大域的に選ばれた値も、この章では構成されない。