Bedrock定数の有界性
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ論理式に現れる定数がすべて与えられた述語を満たすとき、その論理式はその述語で有界です。この構造的な証明書は述語の含意に沿って弱められ、部分的に定義された定数写像を、その定義域に収まる論理式へ適用できるようにします。
本章はその証明書そのものです。BoundedFo P φ は、φ に現れるすべての定数の出現ごとに P を満たすことを記録します。証明書は検査対象の論理式と同じ場合分けで定義されるため、パターン照合の下で自動的に分解され、いかなる証明も「論理式の定数のリスト」について推論する必要はありません。純粋な構文だけを扱うので、本章は階層も段階も言及せず、追加のコストも生じません。
これに伴うのが単調性です。より狭い述語に対する証明書は、より広い述語に対する証明書でもあります。異なる段階に対して書かれた証明書を、共通の段階へ移してから併せて使うのが、まさにこの仕組みです。
なぜ論理式は定数についての証明書を伴うべきなのでしょうか。部分的にしか定義されていない定数上の写像を考えてみてください。定数 c が述語 P を満たすときに限り、その写像は c を新しい定数へ送ります。このような写像は任意の論理式に適用できるとは限りません。式が定義域の外の定数を含むかもしれないからです。しかし、式の中の各定数の出現について「この出現は定義域に収まる」という証明が揃っていれば、写像は式が必要とするすべての場所で作用できます。本章が答える問いは、この出現ごとの証拠はどのような形をすべきか、そしてそれから何が得られるか、ということです。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module FOL.Manipulation.ConstantBounding where open import FOL.Syntax using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
その答えが、構文の形そのものに沿った定義です。項は定数であるなら P の証明を伴わねばならず、変数なら定数を含まないので条件を課しません。論理式はこれらから組み立てられ、その証明書も各部分の証明書から組み上がります。証明書は Term K n と Formula K n の構成子構造を写しているので、それに対する照合は各定数の出現箇所で定義域の証明をちょうど届けてくれます。設計を形づくるのは二つの後の用途です。単調性の節は述語の含意に沿って証明書を移し、改名の節は証明書を部分写像に渡します。Δ₀ の構成子は、改名後の論理式が Lévy 階層の証拠を保てるように読み込まれ、Unit 型は定数を含まないものが持つ自明な証明書を供給します。
; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ) open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo ) open import Cubical.Data.Unit using ( Unit )
証明書
BoundedTm P と BoundedFo P は構文をそのまま映します。定数は P の証明を持ち、変数は自明なデータを持ち、複合論理式は各部分の証明書を組にします。そのため、パターン照合によって各定数の出現箇所で必要な証拠だけが得られます。
条件が最も単純な項から始めましょう。定数上の述語 P と、定数 c と変数からなる c ∈̇ var i のような項を取ります。証明書 BoundedTm P t は t に対する再帰で定義されます。con c に対しては証明書は P c そのものであり、これがその出現での定義域の証明です。var i に対しては Lift Unit、すなわち 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) = Lift Unit 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 が二部、それぞれの出現の位置に対応して入ります。逆に ⊥̇ や素の変数が持つのは Lift Unit だけです。つまり証明書は抽象的な定数記号ではなく出現に従い、同じ定数が二回現れれば証明も二部になります。
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 ⊥̇ = Lift Unit
量化子は変数を束縛するので定数には触れず、非有界の形式は本体の証明書をそのまま通します。しかし有界量化子は定数を含みうる界の項を伴うので、∀̇∈ 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 はこれを項全体へ再帰で拡張します。定数の場合はその一度の適用を行い、変数の場合は素通りします。Lift Unit は述語にかかわらず要素を持つからです。
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) _ = _
同じ議論は、証明書の積を通じて論理式へ持ち上がります。例の (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 ⊥̇ _ = _ 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}
この三角形はここではパラメータ down-correct として現れます。すべての c と p : P c に対するパス up (down c p) ≡ proj c です。これがデータへの唯一の正しさの義務であり、改名に関するそれ以外のことはすべて、出現ごとにここから従います。down が証明 p を引数として要求する点に注意してください。部分写像を適用可能にするのは証明書であり、式が定数に触れるその箇所で定義域の条件を供給するのです。
(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)
項の改名は、証明書を通して配線するだけです。liftTm は t と h : BoundedTm P t を受け取り、定数の節点で h を照合すれば、down c が必要とする証明 p : P c がちょうど渡され、節点は con (down c p) になります。変数では h は自明で、節点はそのまま通ります。部分写像は全域的になりますが、それは定義域の証明を提示する項の上でのみです。
where 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 が、ここで述べた構文上の性質を保ちながら、証明書付きの定数改名を実行します。