Bedrock部分符号に閉じた定義域
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ論理式の符号の定義域は、そこに含まれる各構成子のキーが、その構成子の要求する部分論理式符号を伴うとき、直下の部分論理式符号に閉じています。2 つの原子構成子と底はこのような義務を負いません。それらの項や数項の成分は closedAt の義務ではないからです。本章は、この要求がなぜ必要か、そして何を述べているかを説明します。L.Coding.Expressions の部分符号の節は、参照する符号が実際にエントリを持つ場所でしか表を拘束しないため、十個の節すべてを満たす表がほとんど空でありえます。値を定めるのは索引集合自身の性質であり、閉性述語 closedAt はまさにその性質を一つの対象言語の論理式として述べます。本章は、2 項構成子用と 1 項構成子用の 2 つの量化フレームからこの述語を組み立て、3 つのペイロード関係を具体化して七つの節を得て、それらの節の充足とメタレベルの閉性データとの両方向を証明します。充足された節をその要求する部分符号へと読み出す除去と、そのような所属データから充足を組み立てる導入です。これが揃えば、closedAt は L 内に保存された符号についての構造帰納法を支えます。
本章は、既存の符号化の節が持つ欠陥から始まります。L.Coding.Expressions では、各複合構成子に、ある符号での表のエントリをその直接の部分符号でのエントリと結びつける節が付いていました。この種の節は、参照する符号が実際にエントリを持つ場所でしか拘束力を持たないため、ほとんど空の表でも十個の節すべてを満たせます。索引集合をただ一つの複合符号とし、そこに任意の値のエントリを一つ置けば、部分符号のエントリを探す節はすべて空洞に成立します。部分符号がエントリを持たないからです。節だけでは値は定まりません。値を定めるのは索引集合自身への要求、すなわちその各メンバーの直接の部分論理式符号を含むという要求です。この要求を対象言語の論理式として述べたものが、本章で構成する閉性述語 closedAt です。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude
この反例は、修復しなければ何が誤るかも示します。エントリは複合符号に置かれており、閉性こそが空の部分符号では偽れない性質です。索引集合がある複合符号を含めば、その符号が解読される部分符号も含まねばなりません。「複合」であることがここで要になります。その一つのエントリを底の論理式 ⊥̇ の符号に置き換えると、⊥̇ の節は部分符号の参照をまったく行わないため、値が即座に確定します。この小さな失敗が、議論全体の縮図です。
module L.Coding.Closure {ℓ : Level} where
修復は量化のパターンであり、それを述べるのに必要なのは、節と同じ 2 つのフレームから表を取り除いたものです。残るのは形状の読み手と含意です。その形状の鍵が集合にあるならば、かような鍵もまた集合にある、と。鍵はアリティと符号の対なので、部分鍵は同じアリティから、あるいは変数を束縛する 4 つの構成子についてはその後者から作られます。有界全称は集合のメンバーを走り、さらに全称は解読された各部分を走り、含意が要求を形状の検査の後ろに置きます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∧̇_; _⇒̇_; ∀̇_; ∀̇∈; ∃̇_ )
要求は 2 つの形に分かれます。3 つの二項結合子はそれぞれ同じアリティの論理式の子を 2 つ要求し、2 つの非有界量詞は後続アリティで 1 つの子を要求し、2 つの有界量詞はその同じ高いアリティで第 2 成分 (論理式) だけを追います。第一成分は項だからです。これで義務を持つ構成子は 7 つです。2 つの原子式と底は何も加えません。それらの項や数項の成分は closedAt の義務ではなく、底は反例で見たとおり自身の節が直接確定させます。
import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
フレームの中で述べられる関係はパラメータであり、七つの具体的な節はそのパラメータの具体化として得られます。上の分類は 3 つの具体化で尽くされます。両成分に対する同アリティの要求、一成分に対する同アリティの要求、そしてより高いアリティを存在量化で与える後続アリティの要求です。いずれも、フレーム自身が開く拡張環境の上の素朴な対象言語の論理式です。
open import Cubical.Data.Nat using ( _+_ )
存在量化で与えられる後続こそ、命題的切り詰められた存在が現れる唯一の場所です。アリティを上げる関係の内部では、束縛変数がフレームのアリティの後続であることが証人され、その証人は切り詰めのかたちでだけ残ります。残るのは後続が存在することであり、選ばれた証人をデータとして保持しません。後ほど、これらの節の読み手が切り詰めを解消します。入力となる所属の主張が命題であるため、その解消は正当です。
import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁ )
すべては集合と所属のレベルで述べられます。L に保存された符号は累積階層の要素として読まれ、部分符号の要求は文字通り所属の主張の並びです。pr がアリティとペイロードを組んだ対が定義域の集合に属する、という主張です。これが述語を輸送可能にする理由です。所属についての対象言語の論理式の充足、それだけです。
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; sucV )
論理式は L の台 S の上で、アリティ n の論理式のための n 個の台の要素からなる環境 γ : S ^ n の中で評価されます。ここでの充足は L 上の制限された構造での充足を意味し、周囲の階層の充足関係は別の名前を保つため、二つの読み方が混ざることはありません。各フレームは自分が束縛するスロットで環境を延長するため、そのアリティは 4 + n のようなずらした和になります。
open hPropStructure 𝒮ʟ using ( S )
拡張環境の中では、各フレームは自分のスロットを内側から外側へ数える de Bruijn のインデックスで名指します。2 項フレームはペイロード、ペイロード、アリティ、符号の 4 スロットを束縛し、符号は最も外側のインデックスにあります。1 項フレームは 3 スロットです。シフト写像は元の n 個の環境変数を束縛スロットの先へ押しやり、フレームの外で値を指していた変数が量化された本体の中でも同じ値を指すようにします。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
4 つの対象言語の読み手が構成要素を供給し、それぞれに、その充足を読み取り先のメタレベルの主張と同一視する妥当性証明が付きます。一つは環境スロットに保存された集合への所属を読み、二つはある符号がアリティとその 1 つまたは 2 つのペイロード成分のタグ付きの対であることを確認し、一つは保存されたアリティの後続をペイロードとして持つことを表します。形状・所属・後続がすべて対象言語の内部で読めるようになれば、閉性の要求全体が一つの論理式に収まります。本章の残りは、この論理式が何を言うか、そしてどう充足するかを展開します。
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate ) open import L.Coding.Expressions {ℓ} using ( arityTagAtL; arityTagAtL-adequate; arityTagPairAtL; arityTagPairAtL-adequate ; sucAtL; sucAtL-adequate )
部分符号に閉じた定義域
前節で得た閉性の要求は、解読されたキーについての量化された主張であり、本節はそれを表す 2 つの論理式を構成します。必要な分類は形によるものだけです。1 項構成子の解読されたキーは、符号・アリティ・一つのペイロード成分という 3 つの証人を示し、2 項構成子のキーは第 2 成分を加えた 4 つを示します。したがって解読されたキーを量化するフレームは、1 項では 3 つの値を、2 項では 4 つの値を量化することになり、有効な 7 つの構成子の義務はこの 2 つのフレームに掛かります。
形式化すべき閉性の要求は、解読されたキーについての量化された主張です。インデックス C を固定し、そこに保存された集合を Cset とします。これは次のように読めます。Cset の各符号 c について、c が構成子の数 k をタグに持つアリティ ar として解読され、ペイロード成分を伴うならば、関係 rel がこれらのデータについて成り立つ、と。ペイロード成分の個数は構成子の形で決まります。1 項構成子の解読されたキーは符号・アリティ・一つの成分という 3 つの証人を示し、2 項構成子のキーは第 2 成分を加えた 4 つを示します。そこで、3 つの値を量化するフレームと 4 つの値を量化するフレームの 2 つが要ります。
module _ {n : ℕ} where
両方のフレームは周囲の自由変数の個数 n のもとで働きます。長さ n の環境の中で量化し、自分が束縛するスロットを追加します。2 項フレームで 4 つ、1 項フレームで 3 つです。周囲の変数はこの拡張で不変のままでなければならないため、sh4 のようなシフトは n 個のインデックスをそれぞれ新しく束縛されたスロットの先へ送ります。量化された本体の中でも、それは外で指していたのと同じ値を指します。
private sh4 : Fin n → Fin (4 + n) sh4 i = suc (suc (suc (suc i)))
拡張された環境の中では、フレーム自身の値が参照可能でなければなりません。de Bruijn 番号は最内の変数を 0 とすることでこれを実現します。2 項フレームでは、2 つのペイロード成分が最内の 2 スロットを占め、次がアリティ、符号が 4 つのうち最も外側です。この 4 つの名前があるからこそ、フレームの本体は、フレームがどれほど深くネストしていても、各役割を担う値そのものを正確に指せるのです。
c4 n4 a4 b4 : Fin (4 + n)
c4 = suc (suc (suc zero))
n4 = suc (suc zero)
a4 = suc zero
b4 = zero
1 項フレームは束縛スロットが一つ少ないため、そのシフトは周囲の変数を 4 つではなく 3 つのスロットの先へ動かします。拡張のそれ以外の部分は同じです。
sh3 : Fin n → Fin (3 + n)
sh3 i = suc (suc (suc i))
その 3 つの束縛スロットも同じ内側から外側への順序に従います。唯一のペイロード成分が最内、次がアリティ、そして符号です。両方のフレームを一度ずつ固定すれば、2 項の形に基づく節はすべて 4 スロットの配置を、1 項の形に基づく節はすべて 3 スロットの配置を再利用します。閉性の主張の量化構造は合計 2 回書かれるだけで済みます。
c3 n3 a3 : Fin (3 + n)
c3 = suc (suc zero)
n3 = suc zero
a3 = zero
binShapeAt は 2 項フレームそのものであり、表を除いた閉性の要求です。量詞の構造は正確に次のとおりです。まず有界全称が定義域 C から c を選び、続いてさらに 3 つの値 ar、a、b が量化されます。対の読み手が c が実際にアリティ ar をタグ k とペイロード a、b と組んだタグ付きの対であると証明するという仮定のもとで、関係 rel が拡張された環境 b ∷ a ∷ ar ∷ c ∷ γ の中で成り立たねばなりません。関係はパラメータなので、各節は同じフレームを自分のペイロードの要求で具体化します。
binShapeAt : Fin n → ℕ → Formula S (4 + n) → Formula S n binShapeAt C k rel = ∀̇∈ (var C) (∀̇ (∀̇ (∀̇ ( arityTagPairAtL c4 n4 k a4 b4 ⇒̇ rel))))
unShapeAt は 1 項構成子のための同じフレームです。ペイロード成分が 2 つではなく 1 つであるため、束縛されるスロットが 1 つ減り、形状の読み手は対の版の代わりに arityTagAtL を使います。それ以外、定義域上の有界全称と rel への含意は同一です。
unShapeAt : Fin n → ℕ → Formula S (3 + n) → Formula S n unShapeAt C k rel = ∀̇∈ (var C) (∀̇ (∀̇ ( arityTagAtL c3 n3 k a3 ⇒̇ rel)))
binShape-out は 2 項フレームの除去方向です。その型は、環境 γ が任意の関係 rel についてフレームを充足するという証明を取り、続いて選ばれた符号 c、アリティ ar、成分 a、b、そして c が定義域に属するという所属の仮定を受け取ります。
binShape-out : (C : Fin n) (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) → ⟨ γ ⊨ binShapeAt C k rel ⟩ → (c ar a b : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩
残りの仮定は形状の等式で、c が実際にタグ k とペイロード a、b を組んだ対 ar であることを述べます。これらの仮定のもとで、帰結は拡張環境における rel の実例であり、束縛されたスロットには b ∷ a ∷ ar ∷ c ∷ γ の順でまさにこれらの値が満たされます。
→ fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b))) → ⟨ (b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
証明は短いです。フレームがこの読み方のために設計されているからです。仮説 h は関数であり、c において所属と形状とともに適用すれば求めるものが得られます。ただし形状の引数は、拡張環境における arityTagPairAtL の妥当性のパスに沿って移送される必要があります。妥当性は命題間のパスとして述べられ、それに沿う subst が証明を結論の必要とする形へ移します。
binShape-out C k rel γ h c ar a b c∈ shape = h c c∈ ar a b (subst ⟨_⟩ (sym (arityTagPairAtL-adequate c4 n4 k a4 b4 (b ∷ a ∷ ar ∷ c ∷ γ))) shape)
unShape-out は 1 項フレームに対する同じ除去です。γ による unShapeAt C k rel の充足、唯一のペイロード成分 a とアリティ ar を持つ符号 c、そして c の所属の仮定を受け取ります。
unShape-out : (C : Fin n) (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) → ⟨ γ ⊨ unShapeAt C k rel ⟩ → (c ar a : S)
形状の等式は、一元の形状読み手 arityTagAtL を通して、c をタグ k と唯一のペイロード a を組んだ対 ar として読みます。帰結はより短い拡張環境 a ∷ ar ∷ c ∷ γ の中で成り立ち、束縛されたスロットにはまさにこれらの値が満たされます。
→ ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (fst a)) → ⟨ (a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
2 項の場合と同様に、証明は選ばれた成分においてフレームの関数を適用し、arityTagAtL の妥当性のパスに沿って形状の証明を移送します。この 2 つの除去が利用者に必要なすべてです。以下の 7 つの具体的な閉性節は、関係を具体化することでこれらから得られます。
unShape-out C k rel γ h c ar a c∈ shape = h c c∈ ar a (subst ⟨_⟩ (sym (arityTagAtL-adequate c3 n3 k a3 (a ∷ ar ∷ c ∷ γ))) shape)
四つの一般関係が各種のペイロード形状を担当し、有効な七つの閉性節はそのうち三つを使います。三つの二項結合子は両方の成分が現在のアリティで定義域に属することを要求し、二つの非有界量詞は唯一の成分が一つ高いアリティで属することを要求しますが、その後続アリティは存在量化で与えられます。二つの有界量詞は第二成分だけが同じく一つ高いアリティで属することを要求します。第一成分は項だからです。
アリティを保つ二つの関係は、部分符号の所属の単純な連言です。二項フレームの四つの新規エントリの下で、bothSameAt C はインデックス a4 と b4 が指す二つの部分論理式スロットが、エントリ sh4 C の指す集合に既に属することを主張します。その一項版 oneSameAt C は、一項フレームの三つの新規エントリの下で単一の所属主張を与え、唯一の成分が同じアリティに置かれる構成子に対応します。
bothSameAt : Fin n → Formula S (4 + n) bothSameAt C = appAt (sh4 C) n4 a4 ∧̇ appAt (sh4 C) n4 b4 oneSameAt : Fin n → Formula S (3 + n) oneSameAt C = appAt (sh3 C) n3 a3 oneSuccAt : Fin n → Formula S (3 + n)
アリティを上げる二つの関係は、後続を存在量化で与えます。位置 zero の束縛変数は sucAtL によってフレームのアリティの後続 sucV であると証人され、同じ証人が成分スロットとの対にも要求されます。スロットは拡張された環境の中で suc a3 ないし suc b4 へとずれます。succSndAt の対は第二スロット b4 だけに言及します。有界量詞では二項キーの第一スロットは部分論理式ではなく項を載せるからです。
oneSuccAt C = ∃̇ (sucAtL (suc n3) zero ∧̇ appAt (suc (sh3 C)) zero (suc a3)) succSndAt : Fin n → Formula S (4 + n) succSndAt C = ∃̇ (sucAtL (suc n4) zero ∧̇ appAt (suc (sh4 C)) zero (suc b4))
これらの関係の逆方向の読み出しは利用者が行うので、各版は節の位置で、フレームと既に合成された形で述べられます。集合がその形状のキーを含むなら、構成子が要求する子キーも集合に属します。アリティを変える二つの読み出しは途中で命題的切り詰めを一つ解消します。帰結が所属命題なので、その解消が許されます。
4 つの読み手が各節を具体的な所属データへ展開し直します。ペイロードの形ごとに一つです。最初のものは同アリティの 2 項結合子を扱います。入力は節全体 binShapeAt C k (bothSameAt C) の充足証明と、正しい形のキーです。すなわちモデルの要素 c、ar、a、b、C の集合への c の所属、そして c を「アリティ ar と a、b への符号化された適用の順序対」として呈示する形状の等式です。
binSameClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩ → (c ar a b : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
帰結は構成子が要求する連言です。同じアリティ ar を a および b と対にした 2 つの部分論理式キーが集合の要素になります。証明は一般的なフレーム除去を走らせた後、妥当性を適用します。これは符号化された所属の読み手についての充足の主張を、それが意味する通常の所属の主張へ変換するもので、4 つの読み手すべてに共通する唯一の証明の一段です。
→ ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩ × ⟨ pr (fst ar) (fst b) ∈ fst (lookup C γ) ⟩ binSameClosed-out C k γ h c ar a b c∈ shape = subst ⟨_⟩ (appAt-adequate (sh4 C) n4 a4 δ) (r .fst) , subst ⟨_⟩ (appAt-adequate (sh4 C) n4 b4 δ) (r .snd)
2 番目の読み手は同アリティの 1 項構成子を扱います。仮定は最初のものを一成分分減らして写したものです。oneSameAt から作られる節の充足証明、キーの各部 c、ar、a、c の所属、そして c を「アリティ ar と、符号化された数 k の a への適用」の対として呈示する形状の等式です。
where δ : S ^ (4 + n) δ = b ∷ a ∷ ar ∷ c ∷ γ r = binShape-out C k (bothSameAt C) γ h c ar a b c∈ shape unSameClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
帰結は単一の所属、すなわち ar と a の対の所属です。oneSameAt はアリティを上げないため切り詰めは現れず、証明は 1 項フレームの除去に妥当性の変換が続くだけです。3 番目の読み手は後続アリティに移ります。unSuccClosed-out が oneSuccAt から作られる節を読みます。
→ ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩ → (c ar a : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (fst a)) → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩
仮定は前の 1 項の読み手と一致しますが、帰結は後続に言及します。要求される部分論理式キーは、ar 自身ではなくキーのアリティの後続 sucV (fst ar) と a を対にします。これは非有界量詞に合います。変数を束縛するため、本体は一つ高いアリティの下に保存されるからです。次の三段落で、存在証人とその妥当性証明がこの帰結をどのように導くかを説明します。
unSameClosed-out C k γ h c ar a c∈ shape = subst ⟨_⟩ (appAt-adequate (sh3 C) n3 a3 (a ∷ ar ∷ c ∷ γ)) (unShape-out C k (oneSameAt C) γ h c ar a c∈ shape) unSuccClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n) → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩
3 つ目の読み出しは非有界量詞のもので、アリティを上げます。仮定は通常の 1 項のものです。unShapeAt C k (oneSuccAt C) の充足、キーの各部 c、ar、a、c の所属、そして形状の等式です。帰結はアリティ ar をその後続に置き換えます。要求される部分論理式キーは、ar 自身ではなくキーのアリティの後続 sucV (fst ar) と a を対にします。これは変数を束縛し、本体を一つ高いアリティの下に保存する非有界量詞に適した読み出しです。
→ (c ar a : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (fst a)) → ⟨ pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ) ⟩ unSuccClosed-out C k γ h c ar a c∈ shape =
ここで oneSuccAt 内部の存在量化が効いてきます。後続は命題的に切り詰められた形でしか要求されません。フレーム除去が渡すのは命題的に切り詰められた証人と、それがアリティの後続であること、また a と対になって集合に入ることの 2 つの証明書です。この切り詰めがここで除却できるのは、帰結が命題だからです。集合への所属は hProp なので、PT.rec は命題的切り詰められた存在を具体的な所属の主張へ変換でき、標準的な証人を選ぶ必要はありません。
PT.rec (snd target) (λ { (z , (sz , ap)) → subst (λ w → ⟨ pr w (fst a) ∈ fst (lookup C γ) ⟩) (subst ⟨_⟩ (sucAtL-adequate (suc n3) zero (z ∷ δ)) sz) (subst ⟨_⟩ (appAt-adequate (suc (sh3 C)) zero (suc a3) (z ∷ δ)) ap) })
2 つの読み手の妥当性補題は、これらの充足をモデルの実際の値についての等式と所属へ変え、最初の等式に沿う輸送が証人での所属を sucV (fst ar) での所属として表し直します。こうして読み出しはあるべき場所で終わります。すなわち後続キーの所属で締めくくられるのです。
(unShape-out C k (oneSuccAt C) γ h c ar a c∈ shape) where δ : S ^ (3 + n) δ = a ∷ ar ∷ c ∷ γ target = pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ)
4 つ目の読み出しは有界量詞を担います。仮定は 2 項のパターンをそのまま写します。binShapeAt C k (succSndAt C) の充足、4 つのモデル値 c、ar、a、b、c の所属、そして c を「ar と a、b への符号化された適用の対」として呈示する形状の等式です。
binSuccClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n) → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → (c ar a b : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
帰結は第二成分だけを問います。sucV (fst ar) と b の対が集合に属さねばなりません。第一スロットが載せるのは部分論理式ではなく有界の項だからです。非有界の場合と同様、succSndAt 内部の存在量化は後続を命題的に切り詰められた形で与え、所属の帰結が命題であるため、その切り詰めの除却は正当です。
→ ⟨ pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ) ⟩ binSuccClosed-out C k γ h c ar a b c∈ shape = PT.rec (snd target) (λ { (z , (sz , ap)) → subst (λ w → ⟨ pr w (fst b) ∈ fst (lookup C γ) ⟩)
証明の本体は前の読み出しの 2 項版です。2 つの証明書は sucAtL-adequate と appAt-adequate によって変換され、後続の等式に沿う輸送が対の所属を sucV (fst ar) のもとで表し直します。
(subst ⟨_⟩ (sucAtL-adequate (suc n4) zero (z ∷ δ)) sz) (subst ⟨_⟩ (appAt-adequate (suc (sh4 C)) zero (suc b4) (z ∷ δ)) ap) }) (binShape-out C k (succSndAt C) γ h c ar a b c∈ shape) where δ : S ^ (4 + n)
所属の帰結の命題性こそが、各後続アリティの読み出しにおける切り詰めの除却を許すものです。同アリティの 2 つと後続アリティの 2 つ、この 4 つの読み出しが利用者に必要なすべてであり、どの閉性節も具体的な所属データへ展開できます。
δ = b ∷ a ∷ ar ∷ c ∷ γ target = pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ)
七つの節と、その連言です。消去の側では、充足された closedAt の連言を読む利用者は必要な節を選び、それに対応する読み出しを適用します。引入の方向は次の節で与えられます。
まず七つの節の名前を宣言します。型はすべて同じで、各インデックス C において n 環境上の論理式であり、そこに保存されるキーのアリティそのものです。各フレームが新しくずらしたインデックスで内部的に適用されるため、型には環境の拡張は現れません。
andClosedAt orClosedAt impClosedAt : Fin n → Formula S n existClosedAt forallClosedAt allInClosedAt exInClosedAt : Fin n → Formula S n andClosedAt C = binShapeAt C 2 (bothSameAt C) orClosedAt C = binShapeAt C 3 (bothSameAt C) impClosedAt C = binShapeAt C 4 (bothSameAt C)
各定義は構成子のキーと適切な関係を対にします。数 2、3、4 は二項結合子で、その節は bothSameAt を使い、6 と 7 は非有界量詞で oneSuccAt を、8 と 9 は有界量詞で succSndAt を使います。フレーム binShapeAt か unShapeAt かは、構成子の符号がペイロード成分を 2 つ持つか 1 つ持つかで選ばれます。二項結合子と有界量詞は 2 つ持つので binShapeAt を、非有界量詞は 1 つしか持たないので unShapeAt を使います。量詞の本体は後続アリティに置かれ、有界量詞では第 2 のペイロード成分だけが論理式なので、その関係はその成分だけを追います。
existClosedAt C = unShapeAt C 6 (oneSuccAt C) forallClosedAt C = unShapeAt C 7 (oneSuccAt C) allInClosedAt C = binShapeAt C 8 (succSndAt C) exInClosedAt C = binShapeAt C 9 (succSndAt C) closedAt : Fin n → Formula S n
closedAt C は単一のインデックス C で七つの節すべてを連言します。これが後に L へ輸送される対象言語の述語です。この連言が充足されるとき集合は C で部分符号に対して閉じており、符号上の構造帰納法は連言項ごとに、それぞれ専用の読み出しとともに進みます。
closedAt C = andClosedAt C ∧̇ (orClosedAt C ∧̇ (impClosedAt C ∧̇ (existClosedAt C ∧̇ (forallClosedAt C ∧̇ (allInClosedAt C ∧̇ exInClosedAt C)))))
逆方向は、メタレベルで実際に与えられた部分符号の閉性から出発し、それを各対象言語フレームの充足へ移します。同じアリティの節では、与えられた所属事実が必要なペイロードの所属を直接示します。アリティを上げる節では、L 数項 sucʟ ar が存在量化された後続の証人と、フレームが要求する等式および所属の証明を与えます。
導入の方向は逆向きの需要に答えます。メタレベルの閉性データから、節の充足を作るのです。2 項フレームでは、binShape-in は関数 g を受け取ります。g はキーの各部 c、ar、a、b、c の所属、そして形状の等式から、任意の関係 rel の拡張環境での充足を返します。結論は形状全体 binShapeAt C k rel の充足です。
binShape-in : (C : Fin n) (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) → ((c ar a b : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b))) → ⟨ (b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
これは量詞の意味論を逆向きに読んだものです。有界全称の充足は集合の要素上で定義された関数であり、含意の充足はその前提の証明上の関数です。したがって g をキーのデータに適用すれば求める充足が得られます。必要な変換は arityTagPairAtL-adequate に沿うものだけで、フレームの読むタグの等式を g に渡された形状の等式と整列させます。
→ ⟨ γ ⊨ binShapeAt C k rel ⟩ binShape-in C k rel γ g c c∈ ar a b sh = g c ar a b c∈ (subst ⟨_⟩ (arityTagPairAtL-adequate c4 n4 k a4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)) sh) unShape-in : (C : Fin n) (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n)
1 項版は成分を一つ減らします。g は c、ar、a を受け取り、1 項フレームの拡張環境での rel の充足を返します。目標は unShapeAt C k rel の充足です。以下の具体的な導入は rel を 4 つの関係に具体化します。アリティを上げる 2 つの関係では、節が後続を存在量化でしか要求しないため、数項の章の L 数項 sucŀ ar が具体的な証人として働き、その証明書とともに切り詰めへ注入されます。
→ ((c ar a : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (fst a)) → ⟨ (a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩) → ⟨ γ ⊨ unShapeAt C k rel ⟩
同アリティの導入は、一般的なフレームの導入と具体的な関係を合成して作られます。1 項フレームでは、arityTagAtL-adequate が与えるタグの等式が、フレームの読む形状と利用者が渡すデータを整列させます。最初の合成導入 binSameClosed-in は 2 項フレームを bothSameAt C で具体化します。任意の関係の代わりに、利用者が負うのはメタレベルの所属データであり、この補題がそのデータを節の充足として組み直します。
unShape-in C k rel γ g c c∈ ar a sh = g c ar a c∈ (subst ⟨_⟩ (arityTagAtL-adequate c3 n3 k a3 (a ∷ ar ∷ c ∷ γ)) sh) binSameClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n) → ((c ar a b : S)
ここで g はデータとして述べられた閉性の義務そのものです。与えられた形状のキーから、2 つの部分論理式キー、すなわちアリティ ar を a および b と組んだ 2 つの対の所属を生み出さねばなりません。補題がこのデータを節全体の充足へ変換するので、符号上の再帰はこの所属データを供給するだけで 2 項結合子の閉性の義務を果たせます。
→ ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b))) → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩ × ⟨ pr (fst ar) (fst b) ∈ fst (lookup C γ) ⟩) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
連言の充足を作るには、g が返す 2 つの所属の主張を、appAt の 2 つの連言項の充足として言い換えねばなりません。appAt の妥当性補題は両者の形を同一視するもので、ここでは除却の側とは逆向きに使われます。帰結が今度はデータから充足へと読まれるからです。
binSameClosed-in C k γ g = binShape-in C k (bothSameAt C) γ (λ c ar a b c∈ sh → subst ⟨_⟩ (sym (appAt-adequate (sh4 C) n4 a4 (b ∷ a ∷ ar ∷ c ∷ γ))) (g c ar a b c∈ sh .fst) , subst ⟨_⟩ (sym (appAt-adequate (sh4 C) n4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)))
2 つの成分は同じ読み方で、連言項ごとに扱われます。続く 1 項の同アリティ導入 unSameClosed-in は、単一成分の関係に対して同じ構成を繰り返すもので、データの形は第 2 成分を除いて同じです。
(g c ar a b c∈ sh .snd)) unSameClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n) → ((c ar a : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (fst a))
1 項の同アリティの節では、単一の所属の主張で足ります。g が唯一の部分論理式キーの所属を返し、rel を oneSameAt C に固定した一般的な 1 項導入と合成すれば、それが節の充足になります。
→ ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩) → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩ unSameClosed-in C k γ g = unShape-in C k (oneSameAt C) γ (λ c ar a c∈ sh → subst ⟨_⟩ (sym (appAt-adequate (sh3 C) n3 a3 (a ∷ ar ∷ c ∷ γ)))
残る 2 つの導入はアリティを上げます。まず unSuccClosed-in です。仮定 g はいつもの 1 項キーのデータを受け取りますが、後続キーの所属を結論せねばなりません。すなわちキーのアリティの後続 sucV (fst ar) と a の対の所属です。
(g c ar a c∈ sh)) unSuccClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n) → ((c ar a : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (fst a))
関係 oneSuccAt は後続を命題的に切り詰められた存在の形でしか要求しないので、2 つの証明書を備えた証人ならどれでも構いません。証明は具体的な証人として L 数項 sucʟ ar を与えます。これが証人として適格なのは、第一射影の法則 sucʟ-fst ar がその第 1 成分を sucV (fst ar) と同一視するからで、sucAtL の妥当性補題がこの定義等式を節の読む充足へ変換します。
→ ⟨ pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ) ⟩) → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ unSuccClosed-in C k γ g = unShape-in C k (oneSuccAt C) γ (λ c ar a c∈ sh → ∣ sucʟ ar , ( subst ⟨_⟩ (sym (sucAtL-adequate (suc n3) zero
第 2 の証明書は対の主張です。g は既に後続キーの所属を与えており、数項の射影の法則がそれを pr (sucʟ ar) (fst a) の所属として表し、appAt の妥当性補題が対の連言項の充足へ変換します。証人と証明書を命題的切り詰めへ注入するのに命題性の前提は不要です。その要件は除却に属し、導入には属しません。
(sucʟ ar ∷ a ∷ ar ∷ c ∷ γ))) (sucʟ-fst ar) , subst ⟨_⟩ (sym (appAt-adequate (suc (sh3 C)) zero (suc a3) (sucʟ ar ∷ a ∷ ar ∷ c ∷ γ))) (subst (λ w → ⟨ pr w (fst a) ∈ fst (lookup C γ) ⟩) (sym (sucʟ-fst ar)) (g c ar a c∈ sh)) ) ∣₁)
最後の導入 binSuccClosed-in は有界量詞を担当します。仮定 g は 2 項キーの 4 つの値を受け取り、後続アリティの下での第 2 成分の所属を生み出します。すなわち sucV (fst ar) と b の対です。第 1 スロットが載せるのは部分論理式ではなく有界の項だからです。
binSuccClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n) → ((c ar a b : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b))) → ⟨ pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ) ⟩)
この構成は 1 項の後続の導入と同じもので、rel を succSndAt C に固定した 2 項フレームに適用されます。証人はやはり L 数項 sucʟ ar であり、その射影の法則が後続を証明し、対の主張は今度は第 2 成分 b だけに関わり、これで有界量詞の節が充足されます。
→ ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ binSuccClosed-in C k γ g = binShape-in C k (succSndAt C) γ (λ c ar a b c∈ sh → ∣ sucʟ ar , ( subst ⟨_⟩ (sym (sucAtL-adequate (suc n4) zero (sucʟ ar ∷ b ∷ a ∷ ar ∷ c ∷ γ))) (sucʟ-fst ar)
2 項の後続の場合も同じ証人と同じ 2 つの妥当性の事実を使い、今度は有界量化子の論理式成分に適用します。したがって、有効な各構成子の節には両方向の読みがあります。充足から必要な部分符号の所属が得られ、実際の閉性データから充足が得られます。この両方向により、closedAt C は直下の部分論理式符号に関するメタレベルの閉性を対象言語で表したものになります。
, subst ⟨_⟩ (sym (appAt-adequate (suc (sh4 C)) zero (suc b4) (sucʟ ar ∷ b ∷ a ∷ ar ∷ c ∷ γ))) (subst (λ w → ⟨ pr w (fst b) ∈ fst (lookup C γ) ⟩) (sym (sucʟ-fst ar)) (g c ar a b c∈ sh)) ) ∣₁)
まとめ
closedAt は、定義域の各複合符号が、その節が読み取る部分論理式の符号を伴うことを要求します。消去補題はこれらの部分符号を取り出し、導入補題は同じ七つの義務をメタ言語側の所属事実から構成します。