Bedrock充足関係と再帰の値
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ再帰的構成 Sat は各論理式に符号化された環境の集合を割り当てますが、その再帰方程式が意図した意味をもつためには、それらの符号を B の要素からなる構造の実際の割当てと比較しなければなりません。ここで重要なのは、この制限構造の内側の意味論を使うことです。量化変数はすでに B 上を動き、有界量化子はさらに、限界項の値への所属という別の条件を課します。
{-# OPTIONS --cubical --safe --guardedness #-}
明示的な仮定は、レベル ℓ-suc ℓ における排中律だけです。以下の論理式に関する帰納法そのものは命題について場合分けをしません。この仮定は、すでに構成された環境集合と充足集合を通して入ります。それらの分出は lem をパラメータとしているからです。
open import Base.Prelude open import Base.Classical using ( LEM )
一つの宇宙レベルと、この古典論理の実例を固定します。本章では、同じ真理条件の二つの記述を比較します。符号化された側では、環境が再帰的に定義された集合 Sat B φ に属します。意味論の側では、対応する割当てが、B の要素を論域とする構造で φ を充足します。二つの記述が同じ制限構造で定数を解釈できるように、定数も B の要素を名指すものに限ります。
module L.Coding.SatisfactionBridge {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
証明は論理式の構文に沿って進みます。論理式には二つの原子構成子、三つの命題結合子、偽、二つの非有界量化子、そして項で限界づけられた二つの有界量化子があります。したがって意味論の比較には十の場合があります。項と論理式の定数アルファベットは、それぞれ mapTm と mapFo によって取り替えられ、mapFo-comp は二度続けた取り替えが合成写像による取り替えと一致することを述べます。こうして B の要素を定数とする論理式を、その構文を変えずに周囲の定数アルファベットへ移せます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; con; var; Formula ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo; mapFo-comp )
定数の改名は意味論的に正確です。写像 f に沿って定数を取り替えたとき、解釈 ι のもとで mapFo f φ を評価した真理値は、合成された解釈 ι ∘ f のもとで φ を評価した真理値と一致します。これが ⊨-map です。本章では、小さな要素添字、制限構造の要素、構成可能集合の間を移るときに、この等式を用います。周囲の階層とその順序対演算は、符号化された環境を作る集合を供給します。
open import FOL.Manipulation.Relabelling using ( ⊨-map ) import FOL.Absoluteness import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr )
先行する三つの構成が、この橋で使う数学的データを供給します。集合 B に対して、DefOf は B への所属に制限した構造と、その構造で定義可能な部分集合を与えます。環境の符号化は有限の割当てを値のグラフで表し、一つの値を先頭に加えることで拡張を表します。最後に、環境集合の構成は、固定されたアリティをもつそのようなグラフをすべて集めます。ここで使う推移性はクラス L の推移性です。構成可能集合の要素を再び構成可能とみなすために用いられ、B 自身が推移的であることは主張しません。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Definability {ℓ} using ( module DefOf ) open import L.Coding.Environment {ℓ} using ( env; cons; lookup-spec ) open import L.Coding.Expressions {ℓ} using ( consAtL; consAtL-adequate ) open import L.Coding.EnvironmentSet {ℓ} lem
符号化された側と意味論の側には、すでに相補的なインターフェースがあります。添字族は正準なグラフ envS を与え、envSet-in と envSet-out は正準なグラフと envSet の任意の要素を結びます。集合 Sat B φ はさらに、再帰的条件 cond B φ を充足するグラフを envSet B n から分出して得られます。論理式 tmIs は項の値の関係を表し、その変数の場合を読む補題を伴います。原子論理式と非有界量化子に関する読み出しは、対応する節を両方向に翻訳します。これらの主張が説明するのは cond であり、envSet に属するという追加条件は Sat-mem の別の成分として残ります。
using ( Ix; envS; envSet; envSet-in; envSet-out ) open import L.Coding.Satisfaction {ℓ} lem using ( tmIs; tmIs-var-in; tmIs-var-out; cond; Sat; Sat-mem ; cond∈-in; cond∈-out; cond≐-in; cond≐-out ; cond∃-in; cond∃-out; cond∀-in; cond∀-out
残る読み出しは二つの有界量化子を扱います。先のインターフェースと合わせると、cond の命題結合子以外の各節を両方向に展開できます。有界な節では二つの制限を区別します。新しい値は台 B に属さなければならず、同時に限界項の値にも属さなければなりません。後の帰納法では、これらを制限構造の論域と、内側の意味論に現れる限界とにそれぞれ対応させます。
; cond∃∈-in; cond∃∈-out; cond∀∈-in; cond∀∈-out )
証明は命題値の主張をパスによって比較します。⇔toPath は命題の間の二方向の含意をそのようなパスへ変え、その後は合同性によって比較を論理構成子の内部へ運べます。所属の原子の場合には、二つの候補となる項の値をそれぞれ意味論的な値と同定した後、subst2 が二つの等式に沿って所属関係を輸送します。存在の節と環境の回復には命題的切り詰めを用います。切り詰めは目標が再び命題である場合にだけ除去されるので、選ばれた証人が取り出されることはありません。
open import Cubical.Foundations.Prelude using ( subst2; funExt⁻ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
階層の集合には、その要素の小さな表示が備わっています。a ∈ B の証明から、同値 ∈-asFiber は ⟪ B ⟫ の添字と、その添字が表示する要素から a へのパスを返します。小さな表示での所属と通常の階層での所属の二方向の変換により、証明は二つの見方の間を移れます。この表示が重要なのは、内側の割当てが各項目の B への所属証明をすでに含み、そこから添字族を直接得られるからです。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
有限環境は von Neumann 数項をキーとして用います。したがって位置 i : Fin n は、そのグラフでは集合 # (toℕ i) によって記録されます。ここで数項の構成子を導入することで、項の変数が使う有限添字と、符号化された環境が使う集合論的なキーとが結ばれます。
open InfinitySet using ( #_ )
構成可能宇宙を hProp 値の構造として開くと、構成可能性の証明を備えた集合からなる周囲の台 S が定まります。同時に、命題値の所属を表す _∈ˢ_ と、その基礎の証明型を取り出す括弧 ⟨_⟩ も得られます。したがって以下の等式が比較するのは真理値そのものです。階層の集合の等式でも、追加のデータを運ぶ切り詰められていない同値でもありません。
open hPropStructure 𝒮ʟ
先に導入した対象言語の条件は、すべての構成可能集合が担う構造で解釈されます。一般の絶対性の構成をクラス isL に具体化すると、この周囲の充足関係 _⊨_ と、固定長の環境を表す _^_ が得られます。その変数は構成可能集合を動きます。Sat の所属の等式を開いた後、この周囲の意味論が cond B φ のような符号化された論理式を読みます。これは符号化された側の中間層であり、論域が一つの特定の集合 B の要素だけからなる、さらに小さな構造とは区別しなければなりません。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
台上の制限構造
ここで B : S を固定します。その基礎となる階層の集合に DefOf を適用すると、制限された論域 DB.SM が得られます。その要素は、集合と、それが B に属することの証明との対です。構造 DB.𝒮M は、この論域の上で所属と等号を解釈します。そこで定数の恒等解釈を用いて通常の一階意味論を開くと、_⊨ᴮ_ と ⟦_⟧ᴮ が得られます。これらは DB.defSet の定義に使われる内側の充足と項の評価そのものなので、橋の意味論的な終点と定義可能部分集合は同じ制限構造を共有します。
module _ (B : S) where module DB = DefOf (fst B) module SemB = FOL.Semantics DB.𝒮M open SemB.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
要素 x : DB.SM は、基礎の集合 fst x と、それが B に属することの証明 snd x からすでに成ります。B が構成可能であり、クラス L が推移的なので、fst x も構成可能です。写像 intoL は基礎の集合を保ったまま、この新しい証明書だけを補い、周囲の台 S の要素を作ります。ここでは B が所属について閉じているとは仮定しません。
intoL : DB.SM → S intoL x = fst x , isL-trans {x = fst B} {y = fst x} (snd x) (snd B)
さらにもう一つ、定数アルファベットを結ぶ必要があります。添字 m : ⟪ fst B ⟫ は B の一つの要素を表示します。DB.ι m はその要素と所属証明を組にして DB.SM の要素を作り、intoL は同じ基礎集合を S の要素とみなします。その合成 asConst は、小さな表示で添字づけられた論理式を周囲の意味論で読むときの定数写像です。表示写像 DB.ι と包含 intoL は異なる役割をもちますが、その合成は名指された集合を変えません。
asConst : ⟪ fst B ⟫ → S asConst m = intoL (DB.ι m)
内側の割当てを環境として符号化する
内側の環境 δ : DB.SM ^ n は、各位置に集合とその B への所属証明をともに保存します。符号化された環境が必要とするのは集合だけです。そこで values δ は各項目を第一成分へ射影します。この基礎の値族を明示的に保つのは、項の評価と環境の拡張を、どちらもその有限グラフと比較するためです。
values : ∀ {n} → DB.SM ^ n → Fin n → V ℓ values δ i = fst (lookup i δ)
集合 graph δ は、この値族の有限グラフです。位置 i には、i の数項をキーとし、values δ i を値とする順序対が記録されます。したがって内側のベクトルと階層の集合は、同じ割当てを二つの形で保持します。以下の補題は、この二つの間を移るために必要な正確な等式を与えます。
graph : ∀ {n} → DB.SM ^ n → V ℓ graph δ = env (values δ)
変数を束縛することは、割当ての先頭に新しい値を加えることです。基礎の値族ではこれは cons (fst x) (values δ) であり、内側のベクトルでは x ∷ δ です。補題 cons-values は両者を各点で同定します。新しい先頭ではどちらも fst x を与え、後ろへずれた各位置ではどちらも以前の値を与えます。この一つの整合性の等式が、四つの量化子の場合すべてで再利用されます。
private cons-values : ∀ {n} (x : DB.SM) (δ : DB.SM ^ n) → cons (fst x) (values δ) ≡ values (x ∷ δ) cons-values x δ = funExt (λ { zero → refl ; (suc i) → refl })
ベクトルそのものが、B の小さな表示における添字族を定めます。位置 i では、lookup i δ の第二成分が、その基礎の値が B に属することを証明します。この証明に ∈-asFiber を適用して、添字 index δ i を得ます。この構成はベクトルにすでに保存された所属の証拠を直接使うため、命題的切り詰めも、符号化されたグラフから回復した代表の選択も含みません。
index : ∀ {n} (δ : DB.SM ^ n) → Ix B n index δ i = ∈-asFiber {a = values δ i} {b = fst B} (snd (lookup i δ)) .fst
ファイバーの同値が返すのは添字だけではありません。その添字が表示する要素と、もとの基礎の値との同一視も返します。index-eq δ i は各位置でこのパスを記録します。したがって index δ が表示する値族と values δ は各点で一致し、有限グラフを比較するための正確な入力が得られます。
index-eq : ∀ {n} (δ : DB.SM ^ n) (i : Fin n) → ⟪ fst B ⟫↪ (index δ i) ≡ values δ i index-eq δ i = ∈-asFiber {a = values δ i} {b = fst B} (snd (lookup i δ)) .snd
この添字族を正準な環境の構成子に渡すと、構成可能な周囲の構造の要素 envFor δ が得られます。これは具体的なベクトル δ に対応する、階層における正準な符号です。続く二つの事実が、その基礎のグラフを同定し、さらに環境集合への所属を証明します。任意の環境の代表を選んではいません。
envFor : ∀ {n} → DB.SM ^ n → S envFor δ = envS B (index δ)
envFor δ の基礎となる階層の集合は、ちょうど graph δ です。関数外延性が各点のパス index-eq δ i を値族の等式にまとめ、env の合同性がそれを envFor-graph に変えます。後で使うインターフェースは、この基礎集合のパスです。特に、δ を x ∷ δ へ拡張すると新しい正準な環境が得られ、切り詰めの中に隠れた証人を比較せずに、同じ定理を再び適用できます。
envFor-graph : ∀ {n} (δ : DB.SM ^ n) → fst (envFor δ) ≡ graph δ envFor-graph δ = cong env (funExt (index-eq δ))
最初の帰結は、既知のベクトルから環境集合への所属へ進みます。z : S の基礎集合が graph δ であるとします。正準な環境 envFor δ は envSet-in によって envSet B n に属し、envFor-graph と仮定したパスに沿ってその所属を z へ輸送すれば、graph-envSet が得られます。後の所属の等式が Sat B φ から共通の環境条件を取り除くときに必要とするのは、まさにこの向きです。逆向きは論理的な強さが異なります。envSet-out が回復する添字族は命題的切り詰めの中にあり、後の構成がそれをベクトルへ変換するときも切り詰めを保ちます。この回復は論理式に関する帰納法の外に置かれます。
graph-envSet : ∀ {n} (δ : DB.SM ^ n) (z : S) → fst z ≡ graph δ → ⟨ z ∈ˢ envSet B n ⟩ graph-envSet {n} δ z q = subst (λ w → ⟨ w ∈ fst (envSet B n) ⟩) (envFor-graph δ ∙ sym q) (envSet-in B (index δ))
グラフの等式により、所属の等式から共通の環境条件を取り除けます。Sat-mem は、z が Sat B φ に属すことを、envSet B n への所属と cond B φ の充足との論理積として表します。fst z ≡ graph δ が与えられれば、直前の補題から前者が得られるので、後者は論理積全体と論理的に同値です。⇔toPath はその二方向の含意を真理値の間のパスにします。したがって Sat-cond はまだ論理式の意味を説明せず、次の帰納法で解釈すべき再帰条件だけを取り出します。
Sat-cond : ∀ {n} (φ : Formula S n) (δ : DB.SM ^ n) (z : S) → fst z ≡ graph δ → (z ∈ˢ Sat B φ) ≡ ((z ∷ []) ⊨ cond B φ) Sat-cond φ δ z q = Sat-mem B φ z ∙ ⇔toPath snd (λ h → graph-envSet δ z q , h)
項と環境拡張を読み取る
最初の読み補題は、対象言語の項述語と実際の項評価を比較します。周囲の環境 γ では、スロット ei が符号化された割当てを、スロット viが候補の値を収めます。前者の基礎集合が graph δ なら、tmIs (mapTm intoL t) vi ei の充足から、後者の基礎集合がfst (⟦ t ⟧ᴮ δ) に等しいことが従います。定数の場合、この述語はすでに求める等式です。intoL による定数の改名は台の包装だけを変え、基礎集合はその定数の値のままです。
tmIs-out : ∀ {n k} (t : Term DB.SM n) (δ : DB.SM ^ n) (γ : S ^ k) (vi ei : Fin k) → fst (lookup ei γ) ≡ graph δ → ⟨ γ ⊨ tmIs (mapTm intoL t) vi ei ⟩ → fst (lookup vi γ) ≡ fst (⟦ t ⟧ᴮ δ) tmIs-out (con c) δ γ vi ei qe h = h
変数の場合、tmIs-var-out は充足関係をグラフへの所属として読みます。添字の数項と候補の値との対が、ei に収められたグラフに属すという所属です。その存在証人は命題的に切り詰められていますが、目標の所属は命題なので、ここでの除去によって必要な情報は失われません。qe に沿って輸送するとグラフは graph δ になり、lookup-spec はキー i での所属を、候補の値が δ の第 i項に等しいことと同一視します。符号化グラフのこの関数性が、項評価の変数の場合にほかなりません。
tmIs-out (var i) δ γ vi ei qe h = subst ⟨_⟩ (lookup-spec (values δ) i (fst (lookup vi γ))) (subst (λ w → ⟨ pr (# (toℕ i)) (fst (lookup vi γ)) ∈ w ⟩) qe (tmIs-var-out i γ vi ei h))
逆向きの補題は、意味論的な値の等式から項述語の充足を構成します。定数の場合も直ちに従います。定数を改名した後に対象言語の等式が要求するのは、仮定として与えられた等式そのものです。tmIs-out と tmIs-in を合わせると、項の値をどちらの向きにも読めます。原子の節ではこの二つの補題で評価済みの二項を比較し、有界量化子の節では限界項の値を読みます。
tmIs-in : ∀ {n k} (t : Term DB.SM n) (δ : DB.SM ^ n) (γ : S ^ k) (vi ei : Fin k) → fst (lookup ei γ) ≡ graph δ → fst (lookup vi γ) ≡ fst (⟦ t ⟧ᴮ δ) → ⟨ γ ⊨ tmIs (mapTm intoL t) vi ei ⟩ tmIs-in (con c) δ γ vi ei qe q = q
変数の場合には、先ほどの議論を逆向きにたどります。lookup-spec が仮定された値の等式を、キー付きの対のgraph δ への所属に変えます。次にグラフの等式を逆向きに用いて、その所属を ei に収められたグラフへ輸送し、tmIs-var-in が対象言語の述語の充足として包みます。したがって二方向が表すのは同じ関数的グラフの事実であり、切り詰めから代表を選ぶことはありません。
tmIs-in (var i) δ γ vi ei qe q = tmIs-var-in i γ vi ei (subst (λ w → ⟨ pr (# (toℕ i)) (fst (lookup vi γ)) ∈ w ⟩) (sym qe) (subst ⟨_⟩ (sym (lookup-spec (values δ) i (fst (lookup vi γ)))) q))
第二の一対の読み補題は、割当ての拡張を扱います。consAtL ei mi di では、スロット di が古いグラフを、mi が新しい先頭値を収め、ei が拡張後のグラフの候補になります。最初の二つのスロットがそれぞれ δ と x に対応しているなら、この述語の充足からei の基礎集合が graph (x ∷ δ) であることが従います。量化された論理式が、元の割当てから先頭に一項を加えた割当てへ移るときに必要なのがこの等式です。
consAtL-out : ∀ {n k} (δ : DB.SM ^ n) (x : DB.SM) (γ : S ^ k) (ei mi di : Fin k) → fst (lookup di γ) ≡ graph δ → fst (lookup mi γ) ≡ fst x → ⟨ γ ⊨ consAtL ei mi di ⟩ → fst (lookup ei γ) ≡ graph (x ∷ δ)
証明はまず consAtL-adequate を使います。古いグラフについての仮定のもとで、このパスは拡張スロットの候補をenv (cons (fst (lookup mi γ)) (values δ)) と同一視します。等式 qmがその先頭値を fst x に置き換え、cons-values が得られた族をx ∷ δ の基礎の値の族と同一視します。最後に env の合同性を使えば、求めるグラフの等式が得られます。ここで妥当性の法則が与えるのは拡張グラフとの等式であって、そのグラフへの所属ではありません。
consAtL-out δ x γ ei mi di qd qm h = subst ⟨_⟩ (consAtL-adequate ei mi di γ (values δ) qd) h ∙ cong env (cong (λ w → cons w (values δ)) qm ∙ cons-values x δ)
内向きの読みは三つの意味論的な等式を仮定します。古いスロットがgraph δ を、新しい値のスロットが fst x を、拡張スロットの候補がgraph (x ∷ δ) を収めるという等式です。これらから consAtL の充足を構成します。この向きがあるため、各量化子の節は標準環境envFor (x ∷ δ) を証明済みの拡張として直接使えます。存在表示から切り詰められていない環境を取り出す必要はありません。
consAtL-in : ∀ {n k} (δ : DB.SM ^ n) (x : DB.SM) (γ : S ^ k) (ei mi di : Fin k) → fst (lookup di γ) ≡ graph δ → fst (lookup mi γ) ≡ fst x → fst (lookup ei γ) ≡ graph (x ∷ δ) → ⟨ γ ⊨ consAtL ei mi di ⟩
内向きの証明は、外向きの読みに使ったパスを逆にたどります。graph (x ∷ δ) についての等式から始め、cons-values の逆向きの等式と先頭の値の等式によって、その右辺を mi の値と古い値の族から作ったグラフへ書き換えます。続いて妥当性のパスを逆向きに用い、この等式を consAtL の充足へ輸送します。したがって、各スロットを基礎集合の等式で固定すれば、対象言語の拡張述語と割当てを具体的に前置拡張する操作との間を双方向に移れます。
consAtL-in δ x γ ei mi di qd qm q = subst ⟨_⟩ (sym (consAtL-adequate ei mi di γ (values δ) qd)) (q ∙ sym (cong env (cong (λ w → cons w (values δ)) qm ∙ cons-values x δ)))
再帰の値から内側の充足への帰納法
論理式に関する帰納法は、性質 Adequate によって組織されます。制限構造の各割当て δ、周囲の各構成可能な要素 z、およびその基礎集合をgraph δ と同一視する各等式に対し、この性質は、定数を改名した論理式の充足関係集合への所属から、元の論理式が δ のもとで充足されることへのパスを与えます。すべての z を量化するため、主張はグラフの特定の代表に依存しません。結論は二つの命題を比較し、左辺の mapFo intoL φ は制限された定数から周囲の構成可能な定数への必要な変更を記録します。
Adequate : ∀ {n} → Formula DB.SM n → Type (ℓ-suc (ℓ-suc ℓ)) Adequate {n} φ = (δ : DB.SM ^ n) (z : S) → fst z ≡ graph δ → (z ∈ˢ Sat B (mapFo intoL φ)) ≡ (δ ⊨ᴮ φ)
偽は基底の場合であり、帰納仮定を必要としません。Sat-cond が環境集合についての論理積の項を取り除くと、⊥̇ の再帰条件は偽命題になります。⊥̇ の内側の意味論も同じ偽命題なので、残る比較は定義的に成り立ちます。二つの意味論は、同一の充足不能な条件を課しています。
step⊥ : ∀ {n} → Adequate {n} ⊥̇ step⊥ δ z q = Sat-cond ⊥̇ δ z q
論理積の場合、Sat-cond は二つの再帰的な部分条件の論理積を露わにします。二つの帰納仮定は、同じ割当てと同じグラフの代表のもとで、各部分条件から対応する内側の充足命題へのパスを与えます。真理値の論理積_⊓_ の合同性を二つのパスに施せば、a ∧̇ b に必要なパスが得られます。再帰の節と内側の意味論が同じ命題結合子を使うため、証人を扱う必要はありません。
step∧ : ∀ {n} (a b : Formula DB.SM n) → Adequate a → Adequate b → Adequate (a ∧̇ b) step∧ a b ia ib δ z q = Sat-cond (mapFo intoL (a ∧̇ b)) δ z q ∙ cong₂ _⊓_ (ia δ z q) (ib δ z q)
論理和も同じ構造をもちます。その再帰条件は真理値の論理和 _⊔_ で二つの部分条件を結び、合同性が二つの帰納パスをこの結合子のもとへ運びます。ここでの演算は命題に作用します。証明が比較するのは二つの部分論理式の真理と、その論理和の真理であり、二つの充足関係集合の和集合を作るのではありません。
step∨ : ∀ {n} (a b : Formula DB.SM n) → Adequate a → Adequate b → Adequate (a ∨̇ b) step∨ a b ia ib δ z q = Sat-cond (mapFo intoL (a ∨̇ b)) δ z q ∙ cong₂ _⊔_ (ia δ z q) (ib δ z q)
含意で命題の場合がすべてそろいます。再帰の節は真理値の含意 _⇒_ を使うため、二つの帰納パスに合同性を施すだけで、ここでも比較が得られます。したがって、偽と三つの二項結合子には特別な意味論的変換が要りません。環境の成分を取り除いた後では、それらの再帰条件がすでに内側の意味論と同じ論理的な形をしているからです。
step⇒ : ∀ {n} (a b : Formula DB.SM n) → Adequate a → Adequate b → Adequate (a ⇒̇ b) step⇒ a b ia ib δ z q = Sat-cond (mapFo intoL (a ⇒̇ b)) δ z q ∙ cong₂ _⇒_ (ia δ z q) (ib δ z q)
原子論理式の再帰条件は項の値の候補を量化するため、先ほどの項の読み補題が必要です。所属の場合、その条件は命題的切り詰めのもとで、値 v と w、それらがそれぞれ t と u の評価を表すという証明、および fst v からfst w への所属を与えます。内側の意味論は、実際の評価 T と U の間の所属を直接述べます。この二つの評価に局所的な名前を付けることで、論理的同値の両方向を明示できます。
step∈ : ∀ {n} (t u : Term DB.SM n) → Adequate (t ∈̇ u) step∈ t u δ z q = Sat-cond (mapFo intoL (t ∈̇ u)) δ z q ∙ ⇔toPath fwd bwd where T = ⟦ t ⟧ᴮ δ U = ⟦ u ⟧ᴮ δ
順方向では、cond∈-out が切り詰められた候補を展開します。目標 fst T ∈ fst U は命題なので、PT.rec によって各候補の包みを調べられます。環境 w ∷ v ∷ z ∷ [] で tmIs-out を二度使うと、v は T と、w は U とそれぞれ同一視されます。二変数の輸送subst2 が、記録された関係 fst v ∈ fst w を fst T ∈ fst U へ運びます。これがこの原子の内側の解釈そのものです。
fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ∈̇ u)) ⟩ → ⟨ fst T ∈ fst U ⟩ fwd h = PT.rec (snd (fst T ∈ fst U)) (λ { (v , (w , (ht , (hu , r)))) → subst2 (λ p s → ⟨ p ∈ s ⟩) (tmIs-out t δ (w ∷ v ∷ z ∷ []) (suc zero) (suc (suc zero)) q ht) (tmIs-out u δ (w ∷ v ∷ z ∷ []) zero (suc (suc zero)) q hu)
逆向きの含意では、意味論的な項の値そのものが候補になります。写像intoL は基礎集合を変えずに T と U を周囲の構成可能な要素として包むので、intoL T と intoL U を cond∈-in が要求する二つの証人として入れられます。これは与えられた評価からの直接の構成であり、選択原理を使ったり、命題的切り詰めから証人を取り出したりはしません。
r }) (cond∈-out B (mapTm intoL t) (mapTm intoL u) z h) bwd : ⟨ fst T ∈ fst U ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ∈̇ u)) ⟩ bwd r = cond∈-in B (mapTm intoL t) (mapTm intoL u) z ∣ intoL T , (intoL U
この二つの証人を定めると、tmIs-in の二つの呼び出しにはどちらもrefl を渡せます。intoL T の基礎集合は定義によって fst T であり、U についても同様だからです。したがって、仮定された評価間の所属が、候補間に必要な関係になっています。この一式を命題的切り詰めへ入れると、逆向きの含意が閉じ、所属の原子についての妥当性が完成します。
, ( tmIs-in t δ (intoL U ∷ intoL T ∷ z ∷ []) (suc zero) (suc (suc zero)) q refl , ( tmIs-in u δ (intoL U ∷ intoL T ∷ z ∷ []) zero (suc (suc zero)) q refl , r ))) ∣₁
等号の原子も同じ方針に従い、候補間の関係だけを等号に替えます。再帰条件は命題的切り詰めのもとで、二つの項の値の候補、二つの項の読み、およびそれらの基礎集合の間のパスを与えます。内側の意味論が直接要求するのはfst T ≡ fst U というパスです。所属の場合と同じく、⇔toPath は妥当性を、候補から評価へ輸送する順方向と、評価を候補として使う逆方向とに分けます。
step≐ : ∀ {n} (t u : Term DB.SM n) → Adequate (t ≐ u) step≐ t u δ z q = Sat-cond (mapFo intoL (t ≐ u)) δ z q ∙ ⇔toPath fwd bwd where T = ⟦ t ⟧ᴮ δ U = ⟦ u ⟧ᴮ δ
累積階層の等号は命題なので、順方向の写像は切り詰めを除去できます。項の読みが ht : fst v ≡ fst T と hu : fst w ≡ fst U を与え、候補間の関係が r : fst v ≡ fst w であるとき、求めるパスの向きは正確にsym ht ∙ r ∙ hu です。すなわち、まず t の実際の評価からその候補へ逆向きに進み、記録された候補間の等号を渡り、最後に u の実際の評価へ順向きに進みます。
fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ≐ u)) ⟩ → fst T ≡ fst U fwd h = PT.rec (snd (intoL T ≈ˢ intoL U)) (λ { (v , (w , (ht , (hu , r)))) → sym (tmIs-out t δ (w ∷ v ∷ z ∷ []) (suc zero) (suc (suc zero)) q ht) ∙ r
逆向きの写像でも、intoL T と intoL U を周囲の証人として使います。内向きの項の読みによって二つの項述語が充足され、仮定されたパスfst T ≡ fst U が cond≐-in の要求する候補間の等号をそのまま与えます。したがって、所属の原子と等号の原子との違いは、同じ二つの評価済み項の間にどの関係を運ぶかだけです。候補の値と切り詰めの扱いは一致します。
∙ tmIs-out u δ (w ∷ v ∷ z ∷ []) zero (suc (suc zero)) q hu }) (cond≐-out B (mapTm intoL t) (mapTm intoL u) z h) bwd : fst T ≡ fst U → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ≐ u)) ⟩ bwd r = cond≐-in B (mapTm intoL t) (mapTm intoL u) z ∣ intoL T , (intoL U
tmIs-in に渡す二つの値の等式は、ここでも refl です。証人として選んだのが、intoL で包んだ項の評価そのものだからです。仮定された等号が、切り詰められた条件へ入れる組を完成させます。これで論理式文法の二つの原子の葉について妥当性が得られました。残るのは量化子の場合であり、そこでの中心的な課題は、対象言語の拡張の証人を、内側の割当ての先頭に一つの要素を加える操作と対応させることです。
, ( tmIs-in t δ (intoL U ∷ intoL T ∷ z ∷ []) (suc zero) (suc (suc zero)) q refl , ( tmIs-in u δ (intoL U ∷ intoL T ∷ z ∷ []) zero (suc (suc zero)) q refl , r ))) ∣₁
非有界の存在量化子について、対象言語の条件は命題的に切り詰められた一式のデータを含みます。周囲の要素 x と、その基礎集合が B に属すという証明、拡張環境の候補 e、拡張述語の充足、および e の部分論理式の充足関係集合への所属です。内側の存在量化子は DB.SM 上を動き、その要素は集合とそのB への所属証明をすでに組にしています。この存在量化子自身も命題的に切り詰められています。したがって順方向では、特定の代表を保持せずに、外側の一式を内側の存在証人へ写せます。
step∃ : ∀ {n} (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∃̇ a) step∃ a ia δ z q = Sat-cond (mapFo intoL (∃̇ a)) δ z q ∙ ⇔toPath fwd bwd where fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇ a)) ⟩ → ⟨ δ ⊨ᴮ (∃̇ a) ⟩ fwd h = PT.rec squash₁
切り詰めの内側で、周囲の証人とその証明 x∈B を組にすると、制限された台の要素 (fst x , x∈B) が得られます。非有界の量化変数に課される論域の制限はこれだけであり、限界項の値への所属という追加条件は有界量化子で初めて現れます。続いて consAtL-out は e を、具体的に拡張した割当て (fst x , x∈B) ∷ δ のグラフと同一視します。帰納仮定が、記録された部分論理式の所属をこの割当てでの内側の充足へ輸送し、その値と証明の組が内側の存在量化の命題的切り詰めへ入れられます。
(λ { (x , (x∈B , (e , (hc , he)))) → ∣ (fst x , x∈B) , subst ⟨_⟩ (ia ((fst x , x∈B) ∷ δ) e (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ z ∷ []) zero (suc zero) (suc (suc zero)) q refl hc)) he ∣₁ }) (cond∃-out B (mapFo intoL a) z h)
存在量化の場合の逆向きの含意では、意味論的な証人は ∃[] の内部でのみ与えられます。そこで、この命題的切り詰めの上で構成を写します。証人 x はすでに制限された台の要素なので、第一成分が周囲の集合を与え、第二成分が B への所属を証明します。条件の側では intoL x を新しい値とし、拡張された割当て x ∷ δ の正準な環境 envFor (x ∷ δ) を環境の証人とします。
bwd : ⟨ δ ⊨ᴮ (∃̇ a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇ a)) ⟩ bwd h = cond∃-in B (mapFo intoL a) z (PT.map (λ { (x , ha) → intoL x , (snd x , (envFor (x ∷ δ) , ( consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ z ∷ []) zero (suc zero) (suc (suc zero)) q refl (envFor-graph (x ∷ δ))
consAtL の内向きの読みは、三つの等式からこの環境の拡張を証明します。古い環境は δ のグラフをもち、intoL x の基礎の値は x の基礎の値であり、新しい正準な環境は x ∷ δ のグラフをもちます。続いて帰納法の仮定を逆向きに読み、x ∷ δ での部分論理式の意味論的充足を、正準な環境が再帰的な部分の値に属することへ移します。証人の構成はすべて ∃[] の内部にとどまり、意味論的な証人を命題的切り詰めの外へ選び出すことはありません。
, subst ⟨_⟩ (sym (ia (x ∷ δ) (envFor (x ∷ δ)) (envFor-graph (x ∷ δ)))) ha ))) }) h)
全称量化の場合は証明の形が異なります。内側の ∀[] は、制限された台の任意の x に対して、部分論理式が x ∷ δ で成り立つことを示す関数であり、命題的切り詰めを含みません。Sat-cond が再帰的な条件を展開した後、正向きの含意は任意の x を取り、必要な証明を直接構成します。
step∀ : ∀ {n} (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∀̇ a) step∀ a ia δ z q = Sat-cond (mapFo intoL (∀̇ a)) δ z q ∙ ⇔toPath fwd bwd where fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇ a)) ⟩ → ⟨ δ ⊨ᴮ (∀̇ a) ⟩ fwd h x = subst ⟨_⟩ (ia (x ∷ δ) (envFor (x ∷ δ)) (envFor-graph (x ∷ δ)))
条件の全称の節を使うために、周囲での表示 intoL x、台への所属証明 snd x、そして正準な拡張環境を与えます。consAtL の内向きの読みは、この環境が実際に x の値を古いグラフの先頭に加えたものであることを示します。すると節から再帰的な部分の値への所属が得られ、帰納法の仮定がそれを内側の充足へ運びます。この非有界変数に課される唯一の制限は B への所属であり、その証明はすでに x : DB.SM の組に含まれています。
(cond∀-out B (mapFo intoL a) z h (intoL x) (envFor (x ∷ δ)) (snd x) (consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ z ∷ []) zero (suc zero) (suc (suc zero)) q refl (envFor-graph (x ∷ δ)))) bwd : ⟨ δ ⊨ᴮ (∀̇ a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇ a)) ⟩ bwd k = cond∀-in B (mapFo intoL a) z
逆に条件が要求するのは、B に属すると分かっている周囲の任意の x と、z の拡張であると証明された任意の環境に対する、部分の値への所属です。証明は (fst x , x∈B) を制限された台の要素として組にし、与えられた内側の全称関数を適用します。consAtL の外向きの読みは、証明された環境を拡張された割当てのグラフと同定します。その等式に沿って帰納法の仮定を逆向きに読めば、必要な部分の値への所属が得られます。この向きは終始点ごとの議論であり、命題的切り詰めを使いません。
(λ x e x∈B hc → subst ⟨_⟩ (sym (ia ((fst x , x∈B) ∷ δ) e (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ z ∷ []) zero (suc zero) (suc (suc zero)) q refl hc))) (k (fst x , x∈B)))
有界存在量化では、非有界の場合の議論に限界項の評価が加わります。T = ⟦ t ⟧ᴮ δ を、制限された構造におけるその項の真の値とします。内側の意味論は ∃[] の下で x : DB.SM を探し、x の基礎集合が T の基礎集合に属することと、部分論理式が x ∷ δ で充足されることを同時に要求します。したがって、台への所属と限界への所属は別々の証拠として保たれます。
step∃∈ : ∀ {n} (t : Term DB.SM n) (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∃̇∈ t a) step∃∈ t a ia δ z q = Sat-cond (mapFo intoL (∃̇∈ t a)) δ z q ∙ ⇔toPath fwd bwd where T = ⟦ t ⟧ᴮ δ
正向きの含意では、有界な条件はまず外側の切り詰めの下で、項の値を表す述語を満たす候補 w を与えます。第二の切り詰められた組は、周囲の要素 x、x が B と w に属する証明、拡張環境 e、そして e での部分条件を与えます。外側の切り詰めは命題値である意味論的な目標へ除去し、内側の切り詰めは意味論的な存在証人 (fst x , x∈B) へ写します。
fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇∈ t a)) ⟩ → ⟨ δ ⊨ᴮ (∃̇∈ t a) ⟩ fwd h = PT.rec squash₁ (λ { (w , (hw , hb)) → PT.map (λ { (x , ((x∈B , x∈w) , (e , (hc , he)))) → (fst x , x∈B) , ( subst (λ s → ⟨ fst x ∈ s ⟩)
項の読み tmIs-out は、候補 w の基礎集合を意味論的な値 T の基礎集合と同定します。そのパスに沿って輸送すると、x∈w は内側の意味論が要求する限界への所属、すなわち fst x ∈ fst T になります。一方、consAtL-out は e を (fst x , x∈B) ∷ δ のグラフと同定するので、帰納法の仮定によって e での部分条件を拡張された割当てでの充足へ移せます。この二つの結果が内側の ∃[] の中身になります。
(tmIs-out t δ (w ∷ z ∷ []) zero (suc zero) q hw) x∈w , subst ⟨_⟩ (ia ((fst x , x∈B) ∷ δ) e (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ w ∷ z ∷ []) zero (suc zero) (suc (suc (suc zero))) q refl hc)) he ) }) hb })
逆向きの含意では、真の値 T そのものを条件側の限界の候補として用います。反射的な値の等式とともに tmIs-in を使えば、その項の値を表す述語が得られます。次に意味論的な ∃[] の上で写すと、残る仕事は各意味論的証人 x を組み直すことだけになります。条件の内側の存在は命題的に切り詰められたままです。
(cond∃∈-out B (mapTm intoL t) (mapFo intoL a) z h) bwd : ⟨ δ ⊨ᴮ (∃̇∈ t a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇∈ t a)) ⟩ bwd h = cond∃∈-in B (mapTm intoL t) (mapFo intoL a) z (PT.map (λ { (x , (hx , ha)) → intoL T , ( tmIs-in t δ (intoL T ∷ z ∷ []) zero (suc zero) q refl
意味論的証人 x : DB.SM は二つの制限を別々に与えます。snd x は台への所属を証明し、hx は限界 T への所属を証明します。選んだ候補は実際に intoL T なので、hx はそのまま使えます。拡張環境として envFor (x ∷ δ) を選び、consAtL-in でそれを証明し、帰納法の仮定を逆向きに読んで再帰的な部分の値への所属を得ます。
, ∣ intoL x , ((snd x , hx) , (envFor (x ∷ δ) , ( consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ intoL T ∷ z ∷ []) zero (suc zero) (suc (suc (suc zero))) q refl (envFor-graph (x ∷ δ)) , subst ⟨_⟩ (sym (ia (x ∷ δ) (envFor (x ∷ δ))
これで有界存在量化の両方向が完成します。非有界存在量化に加わった数学的な仕事は、限界項の値を名づけることと、符号化された候補と意味論的な値の間で一つの所属証明を輸送することだけです。二つの存在の組はどちらも命題的切り詰めの下にとどまるため、選択原理は導入されません。排中律のパラメータはすでに Sat の構成に現れており、この妥当性の段階で新たな古典的仮定は加わりません。
(envFor-graph (x ∷ δ)))) ha ))) ∣₁ ) }) h)
有界全称量化は最後の構成子の場合です。T = ⟦ t ⟧ᴮ δ とすると、その内側の意味は、任意の x : DB.SM と証明 fst x ∈ fst T を受け取り、部分論理式が x ∷ δ で充足されることを返す関数です。非有界全称量化の場合と同じく、どちらの向きにも存在の組はないため、二つの含意は命題的切り詰めを使わず点ごとに構成されます。
step∀∈ : ∀ {n} (t : Term DB.SM n) (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∀̇∈ t a) step∀∈ t a ia δ z q = Sat-cond (mapFo intoL (∀̇∈ t a)) δ z q ∙ ⇔toPath fwd bwd where T = ⟦ t ⟧ᴮ δ
正向きの関数を作るには、x とその意味論的な限界への所属証明 hx を取ります。条件の全称の節では、真の限界値 intoL T を使い、その項の読みを tmIs-in から得ます。変数には周囲での表示 intoL x を使います。二つの制限は異なる所から来ます。snd x が x ∈ B を記録し、hx が fst x ∈ fst T を記録します。consAtL-in が正準な拡張を証明し、帰納法の仮定が得られた部分の値への所属を内側の充足へ移します。
fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇∈ t a)) ⟩ → ⟨ δ ⊨ᴮ (∀̇∈ t a) ⟩ fwd h x hx = subst ⟨_⟩ (ia (x ∷ δ) (envFor (x ∷ δ)) (envFor-graph (x ∷ δ))) (cond∀∈-out B (mapTm intoL t) (mapFo intoL a) z h (intoL T) (tmIs-in t δ (intoL T ∷ z ∷ []) zero (suc zero) q refl) (intoL x) (envFor (x ∷ δ)) (snd x) hx
逆向きの関数では、条件は任意の限界候補 w、それが項の値として読めることを示す hw、x∈B と x∈w を伴う周囲の要素 x、そして証明された拡張 e のすべてについて量化します。項の外向きの読みは w の基礎集合を fst T と同定します。このパスに沿って x∈w を輸送すれば、内側の全称関数を (fst x , x∈B) に適用するための限界への所属証明がちょうど得られます。
(consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ intoL T ∷ z ∷ []) zero (suc zero) (suc (suc (suc zero))) q refl (envFor-graph (x ∷ δ)))) bwd : ⟨ δ ⊨ᴮ (∀̇∈ t a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇∈ t a)) ⟩ bwd k = cond∀∈-in B (mapTm intoL t) (mapFo intoL a) z (λ w hw x e x∈B x∈w hc → subst ⟨_⟩
内側の全称関数を適用すると、部分論理式が (fst x , x∈B) ∷ δ で充足されることが得られます。consAtL の外向きの読みは、証明された環境 e をまさにこの割当てのグラフと同定します。したがって帰納法のパスを逆向きに読めば、意味論的充足を条件が要求する部分の値への所属へ移せます。これで有界全称量化の場合が閉じ、台への制限と限界への制限を区別したまま、四つの量化子の議論がすべて完成します。
(sym (ia ((fst x , x∈B) ∷ δ) e (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ w ∷ z ∷ []) zero (suc zero) (suc (suc (suc zero))) q refl hc))) (k (fst x , x∈B) (subst (λ s → ⟨ fst x ∈ s ⟩) (tmIs-out t δ (w ∷ z ∷ []) zero (suc zero) q hw) x∈w)))
個々の場合を論理式の構造に沿って再帰させ、Sat-spec にまとめます。その帰納的不変条件は正確です。任意の割当て δ、任意の周囲の要素 z、そして fst z から graph δ への任意のパスについて、z が Sat B (mapFo intoL φ) に属することと、内側で δ ⊨ᴮ φ が成り立つことは同じ命題です。最初の四つの節は二つの原子の場合を選び、連言と選言について帰納的に得たパスを組み合わせます。
Sat-spec : ∀ {n} (φ : Formula DB.SM n) → Adequate φ Sat-spec (t ∈̇ u) = step∈ t u Sat-spec (t ≐ u) = step≐ t u Sat-spec (a ∧̇ b) = step∧ a b (Sat-spec a) (Sat-spec b) Sat-spec (a ∨̇ b) = step∨ a b (Sat-spec a) (Sat-spec b)
再帰は含意と偽へ進み、続いて二つの非有界量化子と有界全称量化を扱います。複合した構成子が受け取るのは、直接の部分論理式に対する妥当性の証明だけであり、偽の場合には帰納法の仮定は要りません。したがって帰納法の仮定は毎回、その構文の枝における再帰的な条件と内側の意味論を比較するためだけに使われます。
Sat-spec (a ⇒̇ b) = step⇒ a b (Sat-spec a) (Sat-spec b) Sat-spec ⊥̇ = step⊥ Sat-spec (∃̇ a) = step∃ a (Sat-spec a) Sat-spec (∀̇ a) = step∀ a (Sat-spec a) Sat-spec (∀̇∈ t a) = step∀∈ t a (Sat-spec a)
有界存在量化の節によって十の場合の再帰が閉じます。したがって Sat-spec は、定数が制限された台に属する任意の論理式について妥当性を証明します。ここで mapFo intoL はそれらの定数を周囲の言語へ移します。この定理は、外側で構成された各値 Sat B φ に意味論的な読みを与えますが、一様な充足関係表を構成することも、候補の表の一意性を証明することもありません。SatisfactionGraph が候補となるグラフ関係を記述し、PinnedRecursion が必要なキーごとの一意性を証明します。UniformSatisfaction は存在とこの一意性を組み合わせて一様な表を構成し、その後で Sat-spec を使って各値を解釈します。
Sat-spec (∃̇∈ t a) = step∃∈ t a (Sat-spec a)
環境から割当てを復元する
主定理は、あらかじめ選ばれた割当てから出発します。環境集合の任意の要素を読むには、まずその符号化に使われる小さな添字を、制限された台の要素へ変換します。m : ⟪ fst B ⟫ に対して、表示写像は基礎集合 ⟪ fst B ⟫↪ m を与えます。表示における所属の二つの読みから、この集合が fst B に属することが分かります。集合とその証明を組にしたものが inB m : DB.SM です。
private inB : (m : ⟪ fst B ⟫) → ⟨ ⟪ fst B ⟫↪ m ∈ fst B ⟩ inB m = ∈∈ₛ {a = ⟪ fst B ⟫↪ m} {b = fst B} .snd (∈ₛ⟪ fst B ⟫↪ m)
添字族 g : Ix B n は、有限な各位置に小さな要素の添字を一つずつもちます。関数 tab は n に関する再帰によって、これを DB.SM ^ n の割当てへ変えます。先頭は g zero が表示する集合に inB (g zero) を添えたものであり、尾はずらした族 λ i → g (suc i) から得られます。したがって各項目の順序は正確に保たれます。
tab : ∀ {n} → Ix B n → DB.SM ^ n tab {zero} g = [] tab {suc n} g = (⟪ fst B ⟫↪ (g zero) , inB (g zero)) ∷ tab (λ i → g (suc i))
最初の整合性の等式は、tab g から台への所属証明を忘れると、g が表示する集合の族がそのまま得られることを述べます。位置 zero では反射的に成り立ち、後続の位置では、ずらした尾に対する再帰的な等式から従います。関数外延性がこれらの点ごとの等式をまとめ、値の族全体の等式 tab-values を与えます。
tab-values : ∀ {n} (g : Ix B n) → values (tab g) ≡ (λ i → ⟪ fst B ⟫↪ (g i)) tab-values {zero} g = funExt (λ ()) tab-values {suc n} g = funExt (λ { zero → refl ; (suc i) → funExt⁻ (tab-values (λ j → g (suc j))) i })
グラフを作る演算 env を tab-values に施すと、第二の整合性の等式が得られます。これは graph (tab g) を、正準な符号化環境 envS B g の基礎集合と同定します。したがって envSet が使う添字表示と、内側の意味論が使う制限された台の割当ては、項目に異なる補助データを伴いながらも、同じ有限グラフを記述します。
tab-graph : ∀ {n} (g : Ix B n) → graph (tab g) ≡ fst (envS B g)
tab-graph g = cong env (tab-values g)
envSet の外向きの仕様は、要素 z から命題的切り詰めの下で添字族 g と、fst z から envS B g の基礎集合へのパスを復元します。g を tab g へ写し、そのパスを tab-graph の逆向きと合成すると、fst z ≡ graph δ を満たす割当て δ が得られます。結果は切り詰めの下にとどまり、大域的に選ばれた復号も一意性の主張も与えません。後の節の意味論で任意の符号化環境を扱うときにも、まさにこの制限されたインターフェースが使われます。
envSet-vectors : ∀ {n} (z : S) → ⟨ z ∈ˢ envSet B n ⟩ → ∥ Σ[ δ ∈ DB.SM ^ n ] (fst z ≡ graph δ) ∥₁ envSet-vectors {n} z h = PT.map (λ { (g , qg) → tab g , qg ∙ sym (tab-graph g) }) (envSet-out B n z h)
Sat-spec は、特定の割当てとグラフの等式から出発します。Sat-out は、充足の値の任意の要素 z に対応する主張を与えます。すなわち ∃[] のもとで、グラフが fst z であり、制限構造でその論理式を充足する割当て δ が存在します。命題的切り詰めは結論そのものの一部なので、この定理は復号する割当てを選び出さず、そのような割当ての一意性も証明しません。主張するのは、Sat への所属から充足する表示の存在へ進む向きだけです。
Sat-out : ∀ {n} (φ : Formula DB.SM n) (z : S) → ⟨ z ∈ˢ Sat B (mapFo intoL φ) ⟩ → ∥ (Σ[ δ ∈ DB.SM ^ n ] ((fst z ≡ graph δ) × ⟨ δ ⊨ᴮ φ ⟩)) ∥₁ Sat-out {n} φ z h = PT.map (λ { (g , qg) → tab g , (qg ∙ sym (tab-graph g)
最後の二行は、復元されたデータの論理的な強さを増すことなく、外向きの読みを完成させます。もとの Sat への所属証明から、Sat-mem が取り出すのは z が環境集合に属するという成分だけです。続いて envSet-out は、命題的切り詰めの中で添字族 g とそのグラフ等式を返します。PT.map の内部では、tab g が対応する内側の割当てであり、qg ∙ sym (tab-graph g) が z の基礎集合をその割当てのグラフと同一視します。この等式を固定すると、Sat-spec はもとの所属証明 h を直接、内側の充足へ運びます。したがって割当てとその充足証明は同じ切り詰めの中にとどまり、選択も一意性も主張されません。
, subst ⟨_⟩ (Sat-spec φ (tab g) z (qg ∙ sym (tab-graph g))) h) }) (envSet-out B n z (subst ⟨_⟩ (Sat-mem B (mapFo intoL φ) z) h .fst))
定義可能部分集合との一致
この再帰を定義可能部分集合と比較するには、定数を三つの領域の間で移す必要があります。論理式 ψ の定数は、初めは小さな提示 ⟪ fst B ⟫ に属します。DB.ι はそれらを制限された台へ送り、続いて intoL がその台の要素を周囲の台 S へ送ります。定義により、この合成が asConst です。したがって mapFo-comp が表す定数の改名の関手性により、二度改名した論理式 mapFo intoL (mapFo DB.ι ψ) は、直接改名した論理式 mapFo asConst ψ と同一視されます。これは論理式の等式であり、意味論の橋を、再帰が要求する定数の形で使えるようにします。
private mapFo-fuse : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) → mapFo intoL (mapFo DB.ι ψ) ≡ mapFo asConst ψ mapFo-fuse = mapFo-comp DB.ι intoL
第二の正規化は、定義可能部分集合で用いる一項目の割当てに関するものです。正準な環境 envS B (λ _ → m) は、値が常に m である添字族から作られ、その基礎集合はベクトル DB.ι m ∷ [] のグラフです。長さ一の族には添字 zero しかないため、二つのグラフの値の族は一致します。関数外延性がこの添字を確認し、後続の場合は不可能です。さらに合同性がその等式をグラフ演算へ運びます。こうして、この具体的な環境は Sat-spec が必要とするグラフの仮定を満たします。
graph-single : (m : ⟪ fst B ⟫) → fst (envS B (λ _ → m)) ≡ graph (DB.ι m ∷ []) graph-single m = cong env (funExt (λ { zero → refl ; (suc ()) }))
この二つの正規化から、小さな定数アルファベットにおける橋が得られます。z の基礎集合が内側の割当て δ のグラフに等しいとします。このとき、mapFo asConst ψ に対する再帰の値への z の所属は、δ における mapFo DB.ι ψ の内側の充足と等しくなります。右辺の論理式は制限された台に定数を持ち、その構造で恒等写像を解釈として評価されます。言い換えれば、もとの小さな論理式の定数を DB.ι で解釈したものです。証明はまず mapFo-fuse を逆向きに使って左辺に二段の定数の改名を現し、次に Sat-spec を適用します。これにより、下で自由変数が一つの場合へ特殊化する前に、任意のアリティに対する小さなアルファベットでの橋が得られます。
Sat-small-spec : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (δ : DB.SM ^ n) (z : S) → fst z ≡ graph δ → (z ∈ˢ Sat B (mapFo asConst ψ)) ≡ (δ ⊨ᴮ mapFo DB.ι ψ) Sat-small-spec ψ δ z q = cong (λ χ → z ∈ˢ Sat B χ) (sym (mapFo-fuse ψ)) ∙ Sat-spec (mapFo DB.ι ψ) δ z q
ここで自由変数が一つの場合に特殊化します。小さな論理式 ψ と提示の添字 m に対し、defSet-Sat は二つの命題を比較します。m が名指す集合が定義可能部分集合 DB.defSet ψ に属することと、m に対する正準な一項目の環境が mapFo asConst ψ の再帰的な充足関係の値に属することです。証明の最初のパスは DB.defSet-mem です。これは定義可能部分集合の意味を展開し、前者の所属命題を、定数を DB.ι で解釈した ψ の、割当て DB.ι m ∷ [] における内側の充足へ変えます。
defSet-Sat : (ψ : Formula ⟪ fst B ⟫ 1) (m : ⟪ fst B ⟫) → (⟪ fst B ⟫↪ m ∈ DB.defSet ψ) ≡ (envS B (λ _ → m) ∈ˢ Sat B (mapFo asConst ψ)) defSet-Sat ψ m = DB.defSet-mem ψ m
さらに三つのパスをつなぐと、主張された再帰の値に到達します。まず ⊨-map を逆向きに使い、定数を DB.ι で解釈した ψ の充足を、恒等解釈のもとで改名された論理式 mapFo DB.ι ψ の充足へ置き換えます。次に graph-single を用いて Sat-spec を逆向きにたどり、その内側の充足を Sat B (mapFo intoL (mapFo DB.ι ψ)) への所属へ変えます。最後に mapFo-fuse に沿う合同性により、二度改名された論理式を mapFo asConst ψ に置き換えます。各段階は真理値の間のパスです。割当てとそのグラフは明示的に与えられているため、割当ての復元も命題的切り詰めも用いません。この結果が、定義可能冪集合の構成から再帰的な充足関係の値を読むための、一変数のインターフェースになります。
∙ sym (⊨-map DB.𝒮M DB.ι id ψ (DB.ι m ∷ [])) ∙ sym (Sat-spec (mapFo DB.ι ψ) (DB.ι m ∷ []) (envS B (λ _ → m)) (graph-single m)) ∙ cong (λ χ → envS B (λ _ → m) ∈ˢ Sat B χ) (mapFo-fuse ψ)
まとめ
中心的な結果 Sat-spec は、与えられた各割当てについて、再帰的に構成された値への所属を内側の充足と同定します。fst z ≡ graph δ ならば、z が Sat B (mapFo intoL φ) に属することと δ ⊨ᴮ φ は同じ命題です。入力が充足の値の任意の符号化された要素である場合、Sat-out は必要なグラフの等式と充足の証明を備えた割当てを ∃[] のもとで与えるだけです。その割当てを選び出すことも、一意性を証明することもありません。小さな表示の定数を DB.ι、intoL の順に取り替えると、Sat-small-spec が任意のアリティで橋を与え、defSet-Sat はそれを自由変数が一つの場合に特殊化して、定義可能部分集合への所属を正準な一項目環境の所属と同定します。一様な表の構成と候補表の値の一意性には、後の固定された再帰と一様な充足関係の議論が必要です。