Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ論理式に現れる定数がすべて与えられた述語を満たすとき、その論理式はその述語で有界である。この構造的な証明書は述語の含意に沿って弱められ、部分的に定義された定数写像を、その定義域に収まる論理式へ適用できるようにする。
本章はその証明書そのものである。BoundedFo P φ は、φ に現れるすべての定数の出現ごとに P を満たすことを記録する。証明書は検査対象の論理式と同じ場合分けで定義されるため、パターン照合の下で自動的に分解され、いかなる証明も「論理式の定数のリスト」について推論する必要はない。純粋な構文だけを扱うので、本章は階層も段階も言及せず、追加のコストも生じない。
これに伴うのが単調性である。より狭い述語に対する証明書は、より広い述語に対する証明書でもある。異なる段階に対して書かれた証明書を、共通の段階へ移してから併せて使うのが、まさにこの仕組みである。
なぜ論理式は定数についての証明書を伴うべきなのであろうか。部分的にしか定義されていない定数上の写像を考えてみてほしい。定数 c が述語 P を満たすときに限り、その写像は c を新しい定数へ送る。このような写像は任意の論理式に適用できるとは限らない。式が定義域の外の定数を含むかもしれないからである。しかし、式の中の各定数の出現について「この出現は定義域に収まる」という証明が揃っていれば、写像は式が必要とするすべての場所で作用できる。本章が答える問いは、この出現ごとの証拠はどのような形をすべきか、そしてそれから何が得られるか、ということである。
その答えが、構文の形そのものに沿った定義である。項は定数であるなら P の証明を伴わねばならず、変数なら定数を含まないので条件を課さない。論理式はこれらから組み立てられ、その証明書も各部分の証明書から組み上がる。証明書は Term K n と Formula K n の構成子構造を写しているので、それに対する照合は各定数の出現箇所で定義域の証明をちょうど届けてくれる。設計を形づくるのは二つの後の用途である。単調性の節は述語の含意に沿って証明書を移し、改名の節は証明書を部分写像に渡す。Δ₀ の構成子は、改名後の論理式が Lévy 階層の証拠を保てるように読み込まれ、⊤* は定数を含まないものが持つ自明な証明書を供給する。
証明書
BoundedTm P と BoundedFo P は構文をそのまま映する。定数は P の証明を持ち、変数は自明なデータを持ち、複合論理式は各部分の証明書を組にする。そのため、パターン照合によって各定数の出現箇所で必要な証拠だけが得られる。
条件が最も単純な項から始めよう。定数上の述語 P と、定数 c と変数からなる c ∈̇ var i のような項を取る。証明書 BoundedTm P t は t に対する再帰で定義される。con c に対しては証明書は P c そのものであり、これがその出現での定義域の証明である。var i に対しては ⊤*、すなわち P c と同じレベルへ持ち上げた単元型であり、両方の場合が型 Type ℓp を持つようにする。変数は何も要求しないので、その自明な証明書が空所を埋めるだけである。
BoundedTm : ∀ {ℓk ℓp} {K : Type ℓk} (P : K → Type ℓp) {n} → Term K n → Type ℓp
BoundedTm P (con c) = P c
BoundedTm P (var i) = ⊤*
BoundedFo : ∀ {ℓk ℓp} {K : Type ℓk} (P : K → Type ℓp) {n} → Formula K n → Type ℓp
BoundedFo P (t ∈̇ u) = BoundedTm P t × BoundedTm P u
再帰のパターンは一様である。構成子が項や論理式の引数を持つなら、その証明書は引数の証明書の積になり、構成子が定数に触れないなら、その証明書は自明である。たとえば (c ∈̇ d) ∧̇ ∃̇ (var 0 ≐ c) では定数 c が二回現れるが、証明書は四重の組であり、その末端に証明 P c が二部、それぞれの出現の位置に対応して入る。逆に ⊥̇ や素の変数が持つのは ⊤* だけである。つまり証明書は抽象的な定数記号ではなく出現に従い、同じ定数が二回現れれば証明も二部になる。
BoundedFo P (t ≐ u) = BoundedTm P t × BoundedTm P u
BoundedFo P (φ ∧̇ ψ) = BoundedFo P φ × BoundedFo P ψ
BoundedFo P (φ ∨̇ ψ) = BoundedFo P φ × BoundedFo P ψ
BoundedFo P (φ ⇒̇ ψ) = BoundedFo P φ × BoundedFo P ψ
BoundedFo P ⊥̇ = ⊤*
量化子は変数を束縛するので定数には触れず、非有界の形式は本体の証明書をそのまま通す。しかし有界量化子は定数を含みうる界の項を伴うので、∀̇∈ t φ の証明書は t の項の証明書と φ の論理式の証明書の組になる。例の式 ∃̇ (var 0 ≐ c) が示すとおり、その本体の証明書は var 0 ≐ c の証明書にほかならない。これらの節は Formula K n の全構成子を尽くし、各節は式の形から直接読み取られるのであって、探索によって計算されるのではない。
BoundedFo P (∃̇ φ) = BoundedFo P φ
BoundedFo P (∀̇ φ) = BoundedFo P φ
BoundedFo P (∀̇∈ t φ) = BoundedTm P t × BoundedFo P φ
BoundedFo P (∃̇∈ t φ) = BoundedTm P t × BoundedFo P φ
単調性
P が Q を含意するなら、P で有界な項や論理式は Q でも有界である。証明は証明書の構造に従い、後には小さい段階で得た有界性を大きい段階で再利用できる。
証明書は、述語の間で移せてこそ有用である。述語を許される定数の制限と考えれば、各点的含意 P⊆Q に沿って P を Q へ広げても証明書は無効にならない。P が受け入れる出現は Q も受け入れるからである。単一の定数に対してはこれは一度の適用にすぎず、P⊆Q c が証明 P c を Q c へ変える。BoundedTm-mono はこれを項全体へ再帰で拡張する。定数の場合はその一度の適用を行い、変数の場合は素通りする。⊤* は述語にかかわらず要素を持つからである。
module _ {ℓk ℓp ℓq} {K : Type ℓk} {P : K → Type ℓp} {Q : K → Type ℓq}
(P⊆Q : (c : K) → P c → Q c) where
BoundedTm-mono : ∀ {n} (t : Term K n) → BoundedTm P t → BoundedTm Q t
BoundedTm-mono (con c) p = P⊆Q c p
BoundedTm-mono (var i) _ = tt*
同じ議論は、証明書の積を通じて論理式へ持ち上がる。例の (c ∈̇ d) ∧̇ ∃̇ (var 0 ≐ c) では、P の証明書は P についての四つの証明である。各項の空所に BoundedTm-mono を、各部分式に再帰を適用すれば、それらは Q についての四つの証明になり、式の形は终始変わらない。
BoundedFo-mono : ∀ {n} (φ : Formula K n) → BoundedFo P φ → BoundedFo Q φ
BoundedFo-mono (t ∈̇ u) (ht , hu) = BoundedTm-mono t ht , BoundedTm-mono u hu
BoundedFo-mono (t ≐ u) (ht , hu) = BoundedTm-mono t ht , BoundedTm-mono u hu
BoundedFo-mono (φ ∧̇ ψ) (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ
BoundedFo-mono (φ ∨̇ ψ) (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ
この変換はどの接続詞にとっても特別ではない。原子式と命題接続詞の場合はいずれも証明書を二つの因子に分け、因子を変換してから組み直すだけで、⊥̇ は自明な証拠を渡すだけである。連言、選言、含意は同じ一歩を三通りに綴ったものである。
BoundedFo-mono (φ ⇒̇ ψ) (hφ , hψ) = BoundedFo-mono φ hφ , BoundedFo-mono ψ hψ
BoundedFo-mono ⊥̇ _ = tt*
BoundedFo-mono (∃̇ φ) hφ = BoundedFo-mono φ hφ
量化子の場合で帰納が終わる。∃̇ や ∀̇ の下では本体が再帰的に変換され、有界量化子の下では界の項が自らの定数を持ちうるため、その証明書も変換される。結論として、述語を広げればすべての証明書が広がり、ある段階で示した有界性を別の段階で引用できるのはこのためである。
BoundedFo-mono (∀̇ φ) hφ = BoundedFo-mono φ hφ
BoundedFo-mono (∀̇∈ t φ) (ht , hφ) = BoundedTm-mono t ht , BoundedFo-mono φ hφ
BoundedFo-mono (∃̇∈ t φ) (ht , hφ) = BoundedTm-mono t ht , BoundedFo-mono φ hφ
部分的な定数の改名
部分写像は、有界性の証明書から各定数の出現箇所で定義域の証明を受け取り、有界な論理式の定数を改名できる。始域と終域を共通の型へ写せば結果は元の論理式と一致し、Lévy の証人も保存される。
このインターフェイスは、利用者が必要とする一般性で述べられている。二つの定義域、両者がともに写し込まれる共通の世界、始域上の述語、その述語の下で定義された部分写像、そして部分写像が二つの射影と一致することを言う等式である。意図された具体例では、始域はモデルの台、終域はある段階のメンバー型、世界は階層であり、等式は「段階のメンバーを集合として見れば、それは元の集合そのものである」という事実である。
いま証明書がその利用者に出会う。部分的な定数写像は、源の定数集合 K 上の定義域述語 P と、P の上でのみ定義された割り当て down で与えられる。論理式全体を改名するには、さらに先の定数集合 K' と、K と K' の双方が写し込まれる世界 W が必要である。このデータへの数学的な条件は可換な三角形である。p : P c を満たす各源の定数 c は、down を経て先の写像に渡った先が、c が源の写像で到達する世界の要素と一致しなければならない。この三角形が与えられれば、そこから誘導される改名は、元の式とともに W で読んだとき一致すると検証できる。
module Relabel
{ℓk ℓk' ℓv ℓp : Level}
{K : Type ℓk}
{K' : Type ℓk'}
{W : Type ℓv}
(proj : K → W)
(up : K' → W)
(P : K → Type ℓp)
(down : (c : K) → P c → K')
(down-correct : (c : K) (p : P c) → up (down c p) ≡ proj c)
where
この三角形はここではパラメータ down-correct として現れる。すべての c と p : P c に対するパス up (down c p) ≡ proj c である。これがデータへの唯一の正しさの義務であり、改名に関するそれ以外のことはすべて、出現ごとにここから従う。down が証明 p を引数として要求する点に注意してほしい。部分写像を適用可能にするのは証明書であり、式が定数に触れるその箇所で定義域の条件を供給するのである。
項の改名は、証明書を通して配線するだけである。liftTm は t と h : BoundedTm P t を受け取り、定数の節点で h を照合すれば、down c が必要とする証明 p : P c がちょうど渡され、節点は con (down c p) になる。変数では h は自明で、節点はそのまま通る。部分写像は全域的になるが、それは定義域の証明を提示する項の上でのみである。
liftTm : ∀ {n} (t : Term K n) → BoundedTm P t → Term K' n
liftTm (con c) p = con (down c p)
liftTm (var i) _ = var i
liftFo : ∀ {n} (φ : Formula K n) → BoundedFo P φ → Formula K' n
論理式に対しては、liftFo が項の空所に liftTm を適用し、その他の場所では再帰する。先の例では、c の二つの出現がその二つの証明における down c の値に置き換えられ、d も同様で、束縛変数の構造はそのままである。改名が書き換えるのは定数だけで、de Bruijn 指標には触れないので、自由変数の個数は n のままである。
liftFo (t ∈̇ u) (ht , hu) = liftTm t ht ∈̇ liftTm u hu
liftFo (t ≐ u) (ht , hu) = liftTm t ht ≐ liftTm u hu
liftFo (φ ∧̇ ψ) (hφ , hψ) = liftFo φ hφ ∧̇ liftFo ψ hψ
liftFo (φ ∨̇ ψ) (hφ , hψ) = liftFo φ hφ ∨̇ liftFo ψ hψ
liftFo (φ ⇒̇ ψ) (hφ , hψ) = liftFo φ hφ ⇒̇ liftFo ψ hψ
有界量化子は同じ二部構成を繰り返し、界の項の定数を改名して本体に再帰する。⊥̇ と非有界量化子は改名すべき定数を持たない。したがって証明書を持つ論理式に対しては liftFo φ h はつねに定義され、次の節の一致定理が、それがどの意味で φ と同じ論理式なのかを正確に述べる。
liftFo ⊥̇ _ = ⊥̇
liftFo (∃̇ φ) hφ = ∃̇ liftFo φ hφ
liftFo (∀̇ φ) hφ = ∀̇ liftFo φ hφ
liftFo (∀̇∈ t φ) (ht , hφ) = ∀̇∈ (liftTm t ht) (liftFo φ hφ)
liftFo (∃̇∈ t φ) (ht , hφ) = ∃̇∈ (liftTm t ht) (liftFo φ hφ)
正しさとは、定数の改名が本質的な何も変えていないことを言う。up に沿って結果を共通の世界 W へ押し込んだものが、proj に沿って元の論理式を押し込んだものと同じ論理式になる、ということである。これは絶対性の議論で二つの経路が合流する等式であり、各出現ごとに、インターフェース down-correct が要求した理由によってまさに成立する。Δ₀ の証拠もまた保存される。この証拠が記録するのは量化子構造だけなので、定数の改名の下でそのまま移る。
三角形の物語を閉じるのは二つの事実である。第一に、持ち上げた項を up に沿って共通の定数域 W へ改名したものは、元の項を proj に沿って改名した項と一致する。第二に、改名は Δ₀ の証明書を保存する。変わるのは定数であって量化子構造ではないからである。基底は項である。定数 con c では証明書が p : P c を供給し、求めるパスは三角形の辺 down-correct c p を cong con の下に置いたものである。var i では両辺とも同じ変数に対する mapTm _ (var i) に計算されるので、パスは refl である。
liftTm-correct : ∀ {n} (t : Term K n) (h : BoundedTm P t)
→ mapTm up (liftTm t h) ≡ mapTm proj t
liftTm-correct (con c) p = cong con (down-correct c p)
liftTm-correct (var i) _ = refl
liftFo-correct : ∀ {n} (φ : Formula K n) (h : BoundedFo P φ)
論理式の水準での主張は、φ に適用された二つの合成 mapFo up ∘ liftFo と mapFo proj を比べるものである。t ∈̇ u のような原子式がすでに仕組みを示す。目標は t と u に対する二つの項の目標に分かれ、それらは基底の場合が供給し、cong₂ _∈̇_ が所属記号の下に置く。
→ mapFo up (liftFo φ h) ≡ mapFo proj φ
liftFo-correct (t ∈̇ u) (ht , hu) =
cong₂ _∈̇_ (liftTm-correct t ht) (liftTm-correct u hu)
liftFo-correct (t ≐ u) (ht , hu) =
cong₂ _≐_ (liftTm-correct t ht) (liftTm-correct u hu)
複合論理式で新しいことは何も起きない。各二項接続詞の場合は記号に cong₂ を適用し、部分式からの二つの再帰パスを渡すだけである。帰納は証明書自身の組の構造をたどるだけで、証明書を構文の鏡として設計したのはこのためである。
liftFo-correct (φ ∧̇ ψ) (hφ , hψ) =
cong₂ _∧̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ)
liftFo-correct (φ ∨̇ ψ) (hφ , hψ) =
cong₂ _∨̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ)
liftFo-correct (φ ⇒̇ ψ) (hφ , hψ) =
定数を含まない形式はさらに容易である。⊥̇ はどちらの経路でも自身に写るので refl となり、非有界量化子の場合は前置が定数を導入しないため、唯一の再帰パスを量化子記号の cong で包むだけである。
cong₂ _⇒̇_ (liftFo-correct φ hφ) (liftFo-correct ψ hψ)
liftFo-correct ⊥̇ _ = refl
liftFo-correct (∃̇ φ) hφ = cong ∃̇_ (liftFo-correct φ hφ)
liftFo-correct (∀̇ φ) hφ = cong ∀̇_ (liftFo-correct φ hφ)
liftFo-correct (∀̇∈ t φ) (ht , hφ) =
有界量化子は二種類の場合を結合する。項のパスと本体のパスを量化子の構成子の下で cong₂ によってつなげば帰納は完了である。宣言 Δ₀-liftFo はここから二つ目の事実に向かう。その主張は転送である。φ の有界性の証明書 h と φ の Δ₀ 証拠を受け取り、liftFo φ h に対する Δ₀ 証拠を返す。基底は原子の証拠 δ-∈ で、データを持たないためそのまま生き残る。
cong₂ ∀̇∈ (liftTm-correct t ht) (liftFo-correct φ hφ)
liftFo-correct (∃̇∈ t φ) (ht , hφ) =
cong₂ ∃̇∈ (liftTm-correct t ht) (liftFo-correct φ hφ)
Δ₀-liftFo : ∀ {n} {φ : Formula K n} (h : BoundedFo P φ) → Δ₀ φ → Δ₀ (liftFo φ h)
Δ₀-liftFo (ht , hu) δ-∈ = δ-∈
再帰は論理式ではなく Δ₀ の証拠の上を走る。証明書を分解するのは、各下位の証拠と組になった下位の証明書に届くためだけである。接続詞は転送された下位の証拠から自身の構成子を組み立て直し、偽は δ-⊥ を直接返す。
Δ₀-liftFo (ht , hu) δ-≐ = δ-≐
Δ₀-liftFo (hφ , hψ) (δ-∧ c d) = δ-∧ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d)
Δ₀-liftFo (hφ , hψ) (δ-∨ c d) = δ-∨ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d)
Δ₀-liftFo (hφ , hψ) (δ-⇒ c d) = δ-⇒ (Δ₀-liftFo hφ c) (Δ₀-liftFo hψ d)
Δ₀-liftFo _ δ-⊥ = δ-⊥
有界量化子の証拠が再帰を閉じる。それぞれ転送された下位の証拠を δ-∀∈ か δ-∃∈ で包む。Δ₀ の全構成子が扱われたので転送は全域的であり、論理式の Δ₀ であることは定数の改名によって損なわれない。
Δ₀-liftFo (ht , hφ) (δ-∀∈ c) = δ-∀∈ (Δ₀-liftFo hφ c)
Δ₀-liftFo (ht , hφ) (δ-∃∈ c) = δ-∃∈ (Δ₀-liftFo hφ c)
まとめ
定数有界な構文は、部分的な定数写像に必要な証拠をまとめる。単調性は述語間の各点的含意に沿ってその証拠を移す。続いて liftTm と liftFo、それらの一致補題、Δ₀-liftFo が、ここで述べた構文上の性質を保ちながら、証明書付きの定数改名を実行する。