Bedrockパラメータ抽象
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ定数を含む論理式は、定数の各出現を新しい変数で置き換え、その定数をベクトルに記録することで、パラメータを持たない論理式へ変換できます。そのベクトルを環境から与えても充足関係は保存されるため、パラメータ付き論理式を後の符号化に利用できます。
本章ではこの置換そのものを構成します。FOL.Manipulation.ConstantOccurrences の出現数え上げが新しく必要な変数の個数を決め、配置が各出現にどの変数の枠を与えるかを決めます。置換は構造的な一回の走査で済み、章末の妥当性定理が置換前後の充足関係を同一視します。これが後で論理式を符号化するときに用いる事実です。
論理式を使う議論では定数が要ります。集合 $a$ がパラメータ付きで定義可能だと言うには、$a$ を名前で言及する論理式を書くからです。しかし符号化の議論では、パラメータを持たない論理式だけを扱えると便利です。パラメータ抽象はそれを可能にする翻訳です。定数の各出現を新しい変数に置き換え、定数をベクトルに記録して環境から供給できるようにします。
この置き換えは定数ごとではなく、出現ごとに行われます。定数 $c$ が二度現れれば、二度記録され、二つの変数を受け取ります。出現単位で記録するため、翻訳は二つの名前が等しいかを判定する必要がなく、アルファベット K に可判定な等式は要りません。定数の出現を数える章の位置的な数え上げが簿記のすべてを担います。
{-# OPTIONS --cubical --safe --guardedness #-} module FOL.Manipulation.ParameterAbstraction where open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure )
具体的には、この翻訳は前の章で用意された二つのデータを使います。定数の出現の個数は新しく必要な変数の数を決め、記録された定数のベクトルは、解釈の後でそれらの変数が何を表すかを決めます。置き換えそのものは配置と呼ばれる関数で記述され、各出現がどの変数の枠を受け取るかを決めます。
構成全体は論理式の上の一度の構造的な走査です。章の末尾で証明される妥当性の定理は、定数解釈の下での元の論理式の充足と、拡張された環境の下での抽象化の充足を同一視します。後の符号化の議論が依拠するのはまさにこの同一視です。
open import FOL.Syntax using ( Term; con; var ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Semantics open import FOL.Manipulation.ConstantOccurrences using
定数の出現はすべて変数になるため、翻訳後の論理式には定数がまったく含まれません。つまり、元をひとつも持たないアルファベットの上にあります。コードでは空の型 ⊥* がこのアルファベットの役を担います。解釈すべきものがないので、この解釈が実際に要求されることはなく、型が存在して翻訳後の構文に well-formed な台を与えるだけで十分です。
( countTm; countFo; constantsTm; constantsFo; padRight; padLeft ; lookup-padRight; lookup-padLeft; lookup-map ) open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.Vec using ( _++_; map ) import Cubical.Data.Empty as Empty
抽象化
配置は定数の各出現に、より大きな文脈の変数を割り当てます。placeFo はこの置換を構造的に行い、absFo は元の自由変数の直後にある、出現回数と同じ長さの連続した領域を選びます。
走査は任意の配置 θ に対して述べられます。この一般性は再帰から強制されます。部分論理式で用いられる配置は走査の内部で作られるため、帰納法の仮定はすべての配置について成り立つ必要があります。θ を抽象的なまま保つことで、妥当性の証明もモジュール的に保たれます。本節では項について、次に論理式について、この二つの走査を構成します。
置き換えの一般形は走査で、論理式のほかに配置 θ : Fin (countTm t) → Fin (n + k) を受け取ります。θ は数え上げの章で列挙された順に t の出現の枠を読み、それぞれに対して利用可能な n + k 個の枠の一つを指名します。このうち n 個は元の自由変数、k 個は新しいパラメータの枠です。出力は空のアルファベット ⊥* の上の項です。生き残る定数はないからです。
placeTm : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (t : Term K n) → (Fin (countTm t) → Fin (n + k)) → Term (⊥* {ℓz}) (n + k) placeTm (con c) θ = var (θ zero) placeTm {k = k} (var i) θ = var (padRight k i) placeFo : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (φ : Formula K n)
項の二つの場合が、二つの基本的な動きを示します。定数 con c は出現をちょうど一つ、すなわち第 0 枠に持ち、配置がどの変数で置き換えるかを決めます。それが var (θ zero) です。変数 var i は出現を持たないので配置は使われませんが、文脈は n から n + k へ伸びたため、古い添字を埋め込み直す必要があります。padRight k は i を先頭 n 枠の中の同じ位置へ送り、参照法則により連結された環境でも値は保たれます。
→ (Fin (countFo φ) → Fin (n + k)) → Formula (⊥* {ℓz}) (n + k) placeFo (t ∈̇ u) θ = placeTm t (λ i → θ (padRight (countTm u) i)) ∈̇ placeTm u (λ j → θ (padLeft (countTm t) j)) placeFo (t ≐ u) θ = placeTm t (λ i → θ (padRight (countTm u) i)) ≐ placeTm u (λ j → θ (padLeft (countTm t) j))
二項ノードでは出現リストが分裂し、ここで配置の算術が現れます。原子 t ∈̇ u を、t = con c、u = con d とすると、出現リストは c ∷ d ∷ [] で、c は添字 0、d は添字 1 にあります。そこで左の項は padRight を通して配置を読み、u に属する countTm u 個の枠を飛び越えます。右の項は padLeft を通して読み、t に属する countTm t 個の枠をまたぎます。こうして各部分項は自分の出現の枠だけに働く配置を受け取り、翻訳された二つの部分項が元の接続詞で再結合されます。
placeFo (φ ∧̇ ψ) θ = placeFo φ (λ i → θ (padRight (countFo ψ) i)) ∧̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j)) placeFo (φ ∨̇ ψ) θ = placeFo φ (λ i → θ (padRight (countFo ψ) i)) ∨̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j)) placeFo (φ ⇒̇ ψ) θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
論理式の走査は、この例を構造的再帰で一般化したものです。二つの部分からなる構成子は、原子であれ命題的な接続詞であれ、出現リストをまさにこの方法で分割します。第一因子の出現が第二因子の出現に先立ち、左の走査は θ に右側の個数を越える padRight を、右の走査は左側の個数を越える padLeft を合成します。偽 ⊥̇ は出現をまったく持たず、自分自身に翻訳されます。どの節も二度目の走査や改名の補題を要しません。再帰の前に配置を合成しておくことで、翻訳全体が一度の構造的走査に保たれます。
⇒̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j)) placeFo ⊥̇ θ = ⊥̇ placeFo (∃̇ φ) θ = ∃̇ placeFo φ (λ j → suc (θ j)) placeFo (∀̇ φ) θ = ∀̇ placeFo φ (λ j → suc (θ j)) placeFo (∀̇∈ t φ) θ = ∀̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
束縛子の下では文脈が一つ伸びます。これが二つ目の繰り返し現れる動きです。∃̇∈ t φ では、意味論が本体を評価するときに束縛変数を環境の左に追加するため、パラメータの枠はすべて一つずれます。本体は配置 suc ∘ θ の下で走査され、さらに項の出現を越える padLeft で調整されます。項そのものは本体の出現を越える padRight で前の方に配置されます。非有界の量化子 ∃̇ と ∀̇ はずらしだけを持ちます。これらの節で十個の論理式の構成子がすべてカバーされます。
(placeFo φ (λ j → suc (θ (padLeft (countTm t) j)))) placeFo (∃̇∈ t φ) θ = ∃̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i))) (placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))
本の残りの部分で使うのは次のインスタンスです。予算を出現回数ちょうどにとり、配置は変数の直後に続く領域とします。これが求める抽象化であり、その型が本章の主結果を述べます。K 上の自由変数 n 個の論理式が、自由変数 n + countFo φ 個の無パラメータ論理式になります。
padLeft n は出現 j を枠 n + j へ送る配置そのものなので、記録された各定数は、constantsFo φ が並べる順に、元の変数の後ろの最初の空き枠を受け取ります。他に選ぶべきものはありません。
定義は一度の呼び出しだけです。absFo φ = placeFo φ (padLeft n)。添字の算術はすべて走査の内側に繰り込まれているため、抽象化自身は場合分けを持ちません。予算が数え上げと一致するため、配置は事実上、出現の枠とパラメータの枠の間の全単射になりますが、コードがそのことを述べる必要はありません。
absFo : ∀ {ℓz ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Formula (⊥* {ℓz}) (n + countFo φ) absFo {n = n} φ = placeFo φ (padLeft n)
妥当性
妥当性は、定数解釈の下にある元の論理式と、拡張した変数環境の下にある抽象化後の論理式を比較します。配置された各変数が記録済みの定数の解釈を持つなら、項の表示と論理式の充足関係は構造帰納法で一致します。
この比較は、台が S である構造 𝒮 の中で、元の定数の一つの解釈 ι : K → S の下に述べられます。二つの意味論の読み方が並べて用意されます。_⊨_ と ⟦_⟧ は K 上、ι の下の論理式と項に対応し、その改名されたコピー _⊨₀_・⟦_⟧₀ は抽象化の定数域 ⊥* に対応します。⊥* は空なので無パラメータの側に本物の解釈は要りませんが、意味論のモジュールはこのデータを要求するため、Empty.rec* が空虚にそれを供給します。
妥当性とは、抽象化が意味を変えないという主張です。同じ論理式の二つの評価を比較します。一方は K 上の元の構文で、定数は写像 ι : K → S によって解釈されます。他方は空のアルファベット上の翻訳後の構文で、連結された環境 γ ++ σ の中で評価されます。γ は元の自由変数の値を、σ は記録された定数の解釈を保持します。ここで S は命題値の構造 𝒮 の台であり、S ^ n は長さ n の環境の型です。
module _ {ℓ} (𝒮 : ZFStructure ℓ) where open ZFStructure 𝒮 private module Sem = FOL.Semantics 𝒮 open Sem using ( _^_ )
この比較は、両側をつなぐただ一つの仮定に依存します。各出現について、配置の指名した変数がそこに記録された定数の解釈を保持する、すなわち lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ)) というものです。この後のすべては、この仮定を保ちながら構文に対する構造的帰納法です。翻訳後の構文は空のアルファベットの上にあるため、その読み方 _⊨₀_ と ⟦_⟧₀ には本物の定数解釈は要りません。ただし意味論のモジュールはこのデータを要求するため、空の型の消去が空虚にそれを供給します。
module _ {ℓz ℓc} {K : Type ℓc} (ι : K → S) where open Sem.At K ι using ( _⊨_; ⟦_⟧ ) open Sem.At (⊥* {ℓz}) Empty.rec* using () renaming ( _⊨_ to _⊨₀_ ; ⟦_⟧ to ⟦_⟧₀ )
この主張は配置 θ に関して汎用的です。しかも汎用的でなければなりません。再帰における配置は再帰呼び出しの箇所で作られるからです。主張は変数に依存しない形で与えた環境 γ とパラメータ環境 σ の上で述べられ、ただ一つの仮定で制約されます。すなわち、出現のたびに、配置の指す位置にはその位置に記録された定数の解釈が入っている、というものです。この仮定こそ「定数が環境から供給される」の全内容であり、具体的な環境を代入するのではなく仮定として述べることで、どの節もベクトルを正規化する必要がなくなります。
二つの部分からなる構成子に必要な準備は、この仮定を二つに分けることだけです。分かれた各半分は、それぞれ補埋の法則との一度の合成になります。
帰納法の不変条件は、出現ベクトル全体に関する仮定 h です。新しく必要な仕事は、二項の構成子がこのベクトルを左の部分 p と右の部分 q に分けるときに、それを分割することだけです。h が、γ ++ σ の中の枠 θ j に p ++ q の第 j 項の解釈が入っていると述べているとします。左の被演算子に必要なのは p の長さより小さい添字 j だけで、そのような添字を q を越える padRight を通して読めば、p の対応する項がちょうど回復します。それが法則 lookup-padRight です。これを h と合成し、続けて ι を施せば、再帰呼び出しの左の前提が得られます。
private leftHalf : ∀ {n k a b} (θ : Fin (a + b) → Fin (n + k)) (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b) → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q))) → (∀ i → lookup (θ (padRight b i)) (γ ++ σ) ≡ ι (lookup i p))
右半分はその鏡像です。q の添字は padLeft を通して読まれ、これは p の a 個の枠をちょうどまたぎます。そして lookup-padLeft が、連結の中で読み取った項を q の対応する項と同一視します。a が rightHalf では明示的な引数で leftHalf では暗黙だったことに注意してください。配置の定義域 Fin (a + b) だけでは a は定まりませんが、padLeft はいくつの枠をまたぐかを正確に知らされる必要があるからです。
leftHalf θ γ σ p q h i = h (padRight _ i) ∙ cong ι (lookup-padRight p q i) rightHalf : ∀ {n k} a {b} (θ : Fin (a + b) → Fin (n + k)) (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b) → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q))) → (∀ j → lookup (θ (padLeft a j)) (γ ++ σ) ≡ ι (lookup j q))
leftHalf と rightHalf が揃えば、分割の不変条件は一度限り確立されます。以下の帰納法の二項の節はすべて、この二つの補題のどちらかを通して結合仮定を制限するだけで、どの節も再び連結された環境の内部を見ることはありません。
rightHalf a θ γ σ p q h j = h (padLeft a j) ∙ cong ι (lookup-padLeft a p q j)
まず項から始めます。二つの場合はいずれもすぐに示せます。定数の値は、仮定がその位置に述べている解釈そのものです。変数の値は変化せず、補埋の法則が拡張された環境の中でそれを再び見つけ出します。
帰納法は項から始まります。ここでは不変条件がすでにすべての仕事をしています。主張はこうです。h が配置された枠を正しく埋めているなら、解釈 ι の下で t の γ における値は、空のアルファベットの上で翻訳後の項の γ ++ σ における値に等しい。定数 con c の翻訳は var (θ zero) で、その γ ++ σ での値は lookup (θ zero) (γ ++ σ) です。仮定 h zero がこれを ι c と同一視します。これはまさに主張であり、等式の向きが逆なだけです。
⟦⟧-place : ∀ {n k} (t : Term K n) (θ : Fin (countTm t) → Fin (n + k)) (γ : S ^ n) (σ : S ^ k) → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsTm t))) → ⟦ t ⟧ γ ≡ ⟦ placeTm t θ ⟧₀ (γ ++ σ) ⟦⟧-place (con c) θ γ σ h = sym (h zero)
変数 var i では何も置き換えられず、付け替えられただけです。翻訳はそれを padRight k i、すなわち広い文脈の中の同じ枠へ移し、補埋の法則により γ ++ σ で調べれば元の値が回復します。定数と変数の場合が済むと、残りの構成子は分割の不変条件で扱われる二項ノードか束縛子のどちらかで、論理式レベルの帰納法も同じ型に従います。
⟦⟧-place (var i) θ γ σ h = sym (lookup-padRight γ σ i)
続いて帰納法の十二の場合です。ここで十個の論理式の場合を扱い、二つの項の場合は先ほど証明済みです。命題の各原始節はすべて合同です。意味論が各構成子に割り当てるのは対応する論理演算そのものであり、間に変換の層がないからです。四つの束縛節は環境に値を一つ追加し、拡張後の環境で帰納法の仮定を用いますが、パラメータ位置に関する仮定はそのまま通用します。左側への要素の追加と配置の suc による移し替えは計算によって打ち消し合うので、束縛子は固有の補題を必要としません。二つの有界節は、その構成子と同じく左に項、右に本体という形で二分割されます。
論理式レベルの主張 ⊨-place は項の補題と同じ形をしています。表示の代わりに充足が現れます。配置された枠に関する仮定 h の下で、(γ ⊨ φ) は ((γ ++ σ) ⊨₀ placeFo φ θ) に等しい。代表的な原子は所属 t ∈̇ u です。原子の充足は二つの項の値の、構造の所属関係に沿った合同なので、この節は走査が実際に用いた配置で各被演算子に項の補題を適用します。
⊨-place : ∀ {n k} (φ : Formula K n) (θ : Fin (countFo φ) → Fin (n + k)) (γ : S ^ n) (σ : S ^ k) → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ))) → (γ ⊨ φ) ≡ ((γ ++ σ) ⊨₀ placeFo φ θ) ⊨-place (t ∈̇ u) θ γ σ h = cong₂ _∈ˢ_
各被演算子の仮定は、分割の不変条件が供給するものそのものです。constantsTm t ++ constantsTm u に対する結合仮定 h を、左では padRight で、右では padLeft で制限したものです。等号の原子 t ≐ u もまったく同様に扱われ、所属の代わりに構造の等号 ≈ˢ が現れます。続く命題的な接続詞では、項の補題を論理式レベルの帰納に置き換えるだけです。
(⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ (leftHalf θ γ σ (constantsTm t) (constantsTm u) h)) (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h)) ⊨-place (t ≐ u) θ γ σ h = cong₂ _≈ˢ_
連言が最初の純粋に命題的な節です。意味論は φ ∧̇ ψ の充足を、二つの充足値に命題の連言 _⊓_ を施したものとして定義するので、この節は二つの帰納法の仮定の下での cong₂ _⊓_ になり、h は constantsFo φ と constantsFo ψ の間で分割されます。証明は (γ ⊨ φ) ⊓ (γ ⊨ ψ) を単に hProp ℓ の命題として扱い、合同だけを用います。対による表現を仮定することも、それを分解することもありません。
(⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ (leftHalf θ γ σ (constantsTm t) (constantsTm u) h)) (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h)) ⊨-place (φ ∧̇ ψ) θ γ σ h = cong₂ _⊓_
選言は命題の選言 ⊔ で、含意はその含意の演算 ⇒ で同じパターンを繰り返します。三つの命題的な節が違うのは、cong₂ が施される論理演算だけです。分割された仮定を含め、その他の部分はまったく同じです。
(⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h)) (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h)) ⊨-place (φ ∨̇ ψ) θ γ σ h = cong₂ _⊔_
ここでパターンを一度まとめておきます。残りの各節は、その構成子に意味論が割り当てた論理演算で合同を取るか、環境に値を一つ追加して再帰するかのどちらかであり、新しい発想を必要とする節はありません。
(⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h)) (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h)) ⊨-place (φ ⇒̇ ψ) θ γ σ h = cong₂ _⇒_
偽がこれを裏付けます。環境や配置がどうであれ、等式の両辺は偽命題 ⊥なので、この節は refl で済みます。翻訳がパラメータ領域にまったく言及しない唯一の構成子でもあります。
(⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h)) (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h)) ⊨-place ⊥̇ θ γ σ h = refl
非有界の量化子 ∃̇ φ が束縛子の場合で、その内容はずらしが打ち消し合うことです。走査は本体を suc ∘ θ の下に置きました。束縛値を左に追加するとすべてのパラメータ枠が一つずれるからです。一方、意味論は x ∷ γ の上で量化します。そこで再帰的主張は x ∷ γ で用いられ、そこでは lookup (suc (θ j)) (x ∷ γ ++ σ) が計算によって lookup (θ j) (γ ++ σ) に化け、これはちょうど h です。この打ち消しは定義的なので、証明のどこにもずらしのための補題は現れません。
⊨-place (∃̇ φ) θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h)) ⊨-place (∀̇ φ) θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h)) ⊨-place (∀̇∈ t φ) θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → cong₂ _⇒_
全称量化子 ∀̇ の議論も同じで、代数の存在量化の演算 ∃[ x ] P x の代わりに全称量化の演算 ∀[ x ] P x が現れるだけです。演算が名指しされるのは外側の cong の一点だけで、その下の帰納は同一です。
(cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h))) (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h)))) ⊨-place (∃̇∈ t φ) θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → cong₂ _⊓_
有界量化子は二つの動きを組み合わせます。∀̇∈ t φ では、走査は項 t を文脈の前の方で、本体の出現を越える padRight によって抽象化し、本体の配置は項の出現を越える padLeft との合成によって suc だけずらしました。したがってこの節は cong₂ _⇒_ です。一方は項の補題によって x が抽象化された界に属することを、他方はずらした帰納によって x ∷ γ での再帰的主張を結びます。leftHalf と rightHalf が h を constantsTm t と constantsFo φ の間で分割します。存在形の有界量化子 ∃̇∈ は ⇒ の代わりに ⊓ を用いる鏡像です。これで言語のすべての構成子が同じ不変条件で扱われました。
(cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h))) (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))
妥当性そのものは、抽象化が選んだ配置と、収集が指定するパラメータ環境、すなわち解釈済みの定数そのものを選べば直ちに従います。仮定は二つの補埋め法則を順につなげたものになり、定理はまさにこの主張を述べます。元の論理式の γ での充足は、収集された定数で γ を拡張した後の抽象化の充足と一致します。
主定理は帰納法を一度だけ具体化します。absFo φ は配置 padLeft n での走査によって作られたので、⊨-place はまさにその配置で用い、パラメータ環境は map ι (constantsFo φ)、すなわち記録された定数を順に解釈したものと取ります。得られる定理は次を述べています。元の論理式の γ での充足は、これらの解釈済み定数で γ を拡張した後の抽象化の充足と一致する。
⊨-abs : ∀ {n} (φ : Formula K n) (γ : S ^ n) → (γ ⊨ φ) ≡ ((γ ++ map ι (constantsFo φ)) ⊨₀ absFo φ) ⊨-abs {n} φ γ = ⊨-place φ (padLeft n) γ (map ι (constantsFo φ)) hyp where hyp : ∀ j → lookup (padLeft n j) (γ ++ map ι (constantsFo φ))
残るのは、この σ の選択が仮定を果たすことを見ることです。配置 padLeft n は出現 j を項 n + j へ送りますが、これは連結の後半に落ちます。lookup-padLeft がその項を lookup j (map ι (constantsFo φ)) と同一視し、lookup-map が解釈を引き抜いて、ちょうど ι (lookup j (constantsFo φ)) を与えます。二つの法則を合成したものが仮定であり、それを満たせば ⊨-place が定理を与えます。数学的に言えば、パラメータを持たない論理式と有限で順序づけられたパラメータのベクトルの組は、定数付きの元の論理式と同じ外延を持ちます。
≡ ι (lookup j (constantsFo φ)) hyp j = lookup-padLeft n γ (map ι (constantsFo φ)) j ∙ lookup-map ι (constantsFo φ) j
定義可能な部分集合とは何か
パラメータ抽象は、定義可能な部分集合を与えるデータを分離します。すなわち、パラメータを持たない論理式、有限なパラメータベクトル、そして所属を判定する変数です。妥当性により、この提示は元の定数付き論理式とまったく同じ外延を持ちます。
ここには形状上の要点が一つあり、それがアリティ 1 の場合をわざわざ書き下す理由です。アリティ 1 では拡張後の環境は x ∷ map ι p、つまり一つの要素の後にパラメータが続く形になり、これは本書の他のどこでも一項環境が持つのと同じ形です。
一変数の定義可能な部分集合のために、この系は環境を x ∷ [] と固定します。アリティ 1 の論理式はただ一つの要素 x で判定され、定理は x に解釈済みのパラメータを続けた環境での抽象化の判定を与えます。この主張は命題の間の道の等式なので、所属の二つの読み方は取り替えて使えます。定義可能な部分集合を符号化する後の章は、定数の改名も論理式の変更もせず、パラメータを持たない論理式とパラメータベクトル map ι (constantsFo φ) を直接扱って構いません。
⊨-abs₁ : (φ : Formula K 1) (x : S) → ((x ∷ []) ⊨ φ) ≡ ((x ∷ map ι (constantsFo φ)) ⊨₀ absFo φ) ⊨-abs₁ φ x = ⊨-abs φ (x ∷ [])
まとめ
absFo は定数の出現ごとに変数を一つ加えて定数を除き、⊨-abs は記録した定数を環境へ付け加えた後の充足関係を同定します。これは論理式そのものを符号化するときに使う有限パラメータの提示です。