Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ宇宙レベル ℓ を固定する。このレベルをパラメータとして保つことで、異なる宇宙を同一視せずに、必要な大きさで構成を具体化できる。
module L.Coding.Closure {ℓ : Level} where
論理式の符号の定義域は、そこに含まれる各構成子のキーが、その構成子の要求する部分論理式符号を伴うとき、直下の部分論理式符号に閉じている。2 つの原子構成子と底はこのような義務を負わない。それらの項や数項の成分は closedAt の義務ではないからである。本章は、この要求がなぜ必要か、そして何を述べているかを説明する。L.Coding.Expressions の部分符号の節は、参照する符号が実際にエントリを持つ場所でしか表を拘束しないため、十個の節すべてを満たす表がほとんど空でありえる。値を定めるのは索引集合自身の性質であり、閉性述語 closedAt はまさにその性質を一つの対象言語の論理式として述べる。本章は、2 項構成子用と 1 項構成子用の 2 つの量化フレームからこの述語を組み立て、3 つのペイロード関係を具体化して七つの節を得て、それらの節の充足とメタレベルの閉性データとの両方向を証明する。充足された節をその要求する部分符号へと読み出す除去と、そのような所属データから充足を組み立てる導入である。これが揃えば、closedAt は L 内に保存された符号についての構造帰納法を支える。
本章は、既存の符号化の節が持つ欠陥から始まる。L.Coding.Expressions では、各複合構成子に、ある符号での表のエントリをその直接の部分符号でのエントリと結びつける節が付いていた。この種の節は、参照する符号が実際にエントリを持つ場所でしか拘束力を持たないため、ほとんど空の表でも十個の節すべてを満たせる。索引集合をただ一つの複合符号とし、そこに任意の値のエントリを一つ置けば、部分符号のエントリを探す節はすべて空洞に成立する。部分符号がエントリを持たないからである。節だけでは値は定まらない。値を定めるのは索引集合自身への要求、すなわちその各メンバーの直接の部分論理式符号を含むという要求である。この要求を対象言語の論理式として述べたものが、本章で構成する閉性述語 closedAt である。
この反例は、修復しなければ何が誤るかも示す。エントリは複合符号に置かれており、閉性こそが空の部分符号では偽れない性質である。索引集合がある複合符号を含めば、その符号が解読される部分符号も含まねばならない。「複合」であることがここで要になる。その一つのエントリを底の論理式 ⊥̇ の符号に置き換えると、⊥̇ の節は部分符号の参照をまったく行わないため、値が即座に確定する。この小さな失敗が、議論全体の縮図である。
修復は量化のパターンであり、それを述べるのに必要なのは、節と同じ 2 つのフレームから表を取り除いたものである。残るのは形状の読み手と含意である。その形状の鍵が集合にあるならば、かような鍵もまた集合にある、と。鍵はアリティと符号の対なので、部分鍵は同じアリティから、あるいは変数を束縛する 4 つの構成子についてはその後者から作られる。有界全称は集合のメンバーを走り、さらに全称は解読された各部分を走り、含意が要求を形状の検査の後ろに置く。
要求は 2 つの形に分かれる。3 つの二項結合子はそれぞれ同じアリティの論理式の子を 2 つ要求し、2 つの非有界量詞は後続アリティで 1 つの子を要求し、2 つの有界量詞はその同じ高いアリティで第 2 成分 (論理式) だけを追う。第一成分は項だからである。これで義務を持つ構成子は 7 つである。2 つの原子式と底は何も加えない。それらの項や数項の成分は closedAt の義務ではなく、底は反例で見たとおり自身の節が直接確定させる。
フレームの中で述べられる関係はパラメータであり、七つの具体的な節はそのパラメータの具体化として得られる。上の分類は 3 つの具体化で尽くされる。両成分に対する同アリティの要求、一成分に対する同アリティの要求、そしてより高いアリティを存在量化で与える後続アリティの要求である。いずれも、フレーム自身が開く拡張環境の上の素朴な対象言語の論理式である。
存在量化で与えられる後続こそ、命題的切り詰められた存在が現れる唯一の場所である。アリティを上げる関係の内部では、束縛変数がフレームのアリティの後続であることが証人され、その証人は切り詰めのかたちでだけ残る。残るのは後続が存在することであり、選ばれた証人をデータとして保持しない。後ほど、これらの節の読み手が切り詰めを解消する。入力となる所属の主張が命題であるため、その解消は正当である。
すべては集合と所属のレベルで述べられる。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 個の台の要素からなる環境 γ : Vec S n の中で評価される。ここでの充足は L 上の制限された構造での充足を意味し、周囲の階層の充足関係は別の名前を保つため、二つの読み方が混ざることはない。各フレームは自分が束縛するスロットで環境を延長するため、そのアリティは 4 + n のようなずらした和になる。
open hPropView 𝒮ʟ 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 つのペイロード成分のタグ付きの対であることを確認し、一つは保存されたアリティの後続をペイロードとして持つことを表す。形状・所属・後続がすべて対象言語の内部で読めるようになれば、閉性の要求全体が一つの論理式に収まる。本章の残りは、この論理式が何を言うか、そしてどう充足するかを展開する。
部分符号に閉じた定義域
前節で得た閉性の要求は、解読されたキーについての量化された主張であり、本節はそれを表す 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)) (γ : Vec S n)
→ ⟨ γ ⊨ binShapeAt C k rel ⟩
→ (c ar a b : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
残りの仮定は形状の等式で、c が実際にタグ k とペイロード a、b を組んだ対 ar であることを述べる。これらの仮定のもとで、帰結は拡張環境における rel の実例であり、束縛されたスロットには b ∷ a ∷ ar ∷ c ∷ γ の順でまさにこれらの値が満たされる。
→ c .fst ≡ pr (ar .fst) (pr (# k) (pr (a .fst) (b .fst)))
→ ⟨ (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)) (γ : Vec S n)
→ ⟨ γ ⊨ unShapeAt C k rel ⟩
→ (c ar a : S)
形状の等式は、一元の形状読み手 arityTagAtL を通して、c をタグ k と唯一のペイロード a を組んだ対 ar として読む。帰結はより短い拡張環境 a ∷ ar ∷ c ∷ γ の中で成り立ち、束縛されたスロットにはまさにこれらの値が満たされる。
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (a .fst))
→ ⟨ (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 : ℕ) (γ : Vec S n)
→ ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
→ (c ar a b : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (pr (a .fst) (b .fst)))
帰結は構成子が要求する連言である。同じアリティ ar を a および b と対にした 2 つの部分論理式キーが集合の要素になる。証明は一般的なフレーム除去を走らせた後、妥当性を適用する。これは符号化された所属の読み手についての充足の主張を、それが意味する通常の所属の主張へ変換するもので、4 つの読み手すべてに共通する唯一の証明の一段である。
→ ⟨ pr (ar .fst) (a .fst) ∈ (lookup C γ) .fst ⟩
× ⟨ pr (ar .fst) (b .fst) ∈ (lookup C γ) .fst ⟩
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
δ : Vec 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 : ℕ) (γ : Vec S n)
帰結は単一の所属、すなわち ar と a の対の所属である。oneSameAt はアリティを上げないため切り詰めは現れず、証明は 1 項フレームの除去に妥当性の変換が続くだけである。3 番目の読み手は後続アリティに移る。unSuccClosed-out が oneSuccAt から作られる節を読む。
→ ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩
→ (c ar a : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (a .fst))
→ ⟨ pr (ar .fst) (a .fst) ∈ (lookup C γ) .fst ⟩
仮定は前の 1 項の読み手と一致するが、帰結は後続に言及する。要求される部分論理式キーは、ar 自身ではなくキーのアリティの後続 sucV (ar .fst) と 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 : ℕ) (γ : Vec S n)
→ ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩
3 つ目の読み出しは非有界量詞のもので、アリティを上げる。仮定は通常の 1 項のものである。unShapeAt C k (oneSuccAt C) の充足、キーの各部 c、ar、a、c の所属、そして形状の等式である。帰結はアリティ ar をその後続に置き換える。要求される部分論理式キーは、ar 自身ではなくキーのアリティの後続 sucV (ar .fst) と a を対にする。これは変数を束縛し、本体を一つ高いアリティの下に保存する非有界量詞に適した読み出しである。
→ (c ar a : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (a .fst))
→ ⟨ pr (sucV (ar .fst)) (a .fst) ∈ (lookup C γ) .fst ⟩
unSuccClosed-out C k γ h c ar a c∈ shape =
ここで oneSuccAt 内部の存在量化が効いてくる。後続は命題的に切り詰められた形でしか要求されない。フレーム除去が渡すのは命題的に切り詰められた証人と、それがアリティの後続であること、また a と対になって集合に入ることの 2 つの証明書である。この切り詰めがここで除却できるのは、帰結が命題だからである。集合への所属は hProp なので、rec₁ は命題的切り詰められた存在を具体的な所属の主張へ変換でき、標準的な証人を選ぶ必要はない。
rec₁ (target .snd)
(λ { (z , (sz , ap)) →
subst (λ w → ⟨ pr w (a .fst) ∈ (lookup C γ) .fst ⟩)
(subst ⟨_⟩ (sucAtL-adequate (suc n3) zero (z ∷ δ)) sz)
(subst ⟨_⟩ (appAt-adequate (suc (sh3 C)) zero (suc a3) (z ∷ δ)) ap) })
2 つの読み手の妥当性補題は、これらの充足をモデルの実際の値についての等式と所属へ変え、最初の等式に沿う輸送が証人での所属を sucV (ar .fst) での所属として表し直す。こうして読み出しはあるべき場所で終わる。すなわち後続キーの所属で締めくくられるのである。
(unShape-out C k (oneSuccAt C) γ h c ar a c∈ shape)
where
δ : Vec S (3 + n)
δ = a ∷ ar ∷ c ∷ γ
target = pr (sucV (ar .fst)) (a .fst) ∈ (lookup C γ) .fst
4 つ目の読み出しは有界量詞を担う。仮定は 2 項のパターンをそのまま写す。binShapeAt C k (succSndAt C) の充足、4 つのモデル値 c、ar、a、b、c の所属、そして c を「ar と a、b への符号化された適用の対」として呈示する形状の等式である。
binSuccClosed-out : (C : Fin n) (k : ℕ) (γ : Vec S n)
→ ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩
→ (c ar a b : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (pr (a .fst) (b .fst)))
帰結は第二成分だけを問う。sucV (ar .fst) と b の対が集合に属さねばならない。第一スロットが載せるのは部分論理式ではなく有界の項だからである。非有界の場合と同様、succSndAt 内部の存在量化は後続を命題的に切り詰められた形で与え、所属の帰結が命題であるため、その切り詰めの除却は正当である。
→ ⟨ pr (sucV (ar .fst)) (b .fst) ∈ (lookup C γ) .fst ⟩
binSuccClosed-out C k γ h c ar a b c∈ shape =
rec₁ (target .snd)
(λ { (z , (sz , ap)) →
subst (λ w → ⟨ pr w (b .fst) ∈ (lookup C γ) .fst ⟩)
証明の本体は前の読み出しの 2 項版である。2 つの証明書は sucAtL-adequate と appAt-adequate によって変換され、後続の等式に沿う輸送が対の所属を sucV (ar .fst) のもとで表し直す。
(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
δ : Vec S (4 + n)
所属の帰結の命題性こそが、各後続アリティの読み出しにおける切り詰めの除却を許すものである。同アリティの 2 つと後続アリティの 2 つ、この 4 つの読み出しが利用者に必要なすべてであり、どの閉性節も具体的な所属データへ展開できる。
δ = b ∷ a ∷ ar ∷ c ∷ γ
target = pr (sucV (ar .fst)) (b .fst) ∈ (lookup C γ) .fst
七つの節と、その連言である。消去の側では、充足された 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)) (γ : Vec S n)
→ ((c ar a b : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (pr (a .fst) (b .fst)))
→ ⟨ (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)) (γ : Vec S n)
1 項版は成分を一つ減らす。g は c、ar、a を受け取り、1 項フレームの拡張環境での rel の充足を返す。目標は unShapeAt C k rel の充足である。以下の具体的な導入は rel を 4 つの関係に具体化する。アリティを上げる 2 つの関係では、節が後続を存在量化でしか要求しないため、数項の章の L 数項 sucŀ ar が具体的な証人として働き、その証明書とともに切り詰めへ注入される。
→ ((c ar a : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (a .fst))
→ ⟨ (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 : ℕ) (γ : Vec S n)
→ ((c ar a b : S)
ここで g はデータとして述べられた閉性の義務そのものである。与えられた形状のキーから、2 つの部分論理式キー、すなわちアリティ ar を a および b と組んだ 2 つの対の所属を生み出さねばならない。補題がこのデータを節全体の充足へ変換するので、符号上の再帰はこの所属データを供給するだけで 2 項結合子の閉性の義務を果たせる。
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (pr (a .fst) (b .fst)))
→ ⟨ pr (ar .fst) (a .fst) ∈ (lookup C γ) .fst ⟩
× ⟨ pr (ar .fst) (b .fst) ∈ (lookup C γ) .fst ⟩)
→ ⟨ γ ⊨ 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 : ℕ) (γ : Vec S n)
→ ((c ar a : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (a .fst))
1 項の同アリティの節では、単一の所属の主張で足りる。g が唯一の部分論理式キーの所属を返し、rel を oneSameAt C に固定した一般的な 1 項導入と合成すれば、それが節の充足になる。
→ ⟨ pr (ar .fst) (a .fst) ∈ (lookup C γ) .fst ⟩)
→ ⟨ γ ⊨ 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 (ar .fst) と a の対の所属である。
(g c ar a c∈ sh))
unSuccClosed-in : (C : Fin n) (k : ℕ) (γ : Vec S n)
→ ((c ar a : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (a .fst))
関係 oneSuccAt は後続を命題的に切り詰められた存在の形でしか要求しないので、2 つの証明書を備えた証人ならどれでも構わない。証明は具体的な証人として L 数項 sucʟ ar を与える。これが証人として適格なのは、第一射影の法則 sucʟ-fst ar がその第 1 成分を sucV (ar .fst) と同一視するからで、sucAtL の妥当性補題がこの定義等式を節の読む充足へ変換する。
→ ⟨ pr (sucV (ar .fst)) (a .fst) ∈ (lookup C γ) .fst ⟩)
→ ⟨ γ ⊨ 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) (a .fst) の所属として表し、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 (a .fst) ∈ (lookup C γ) .fst ⟩)
(sym (sucʟ-fst ar)) (g c ar a c∈ sh)) ) ∣₁)
最後の導入 binSuccClosed-in は有界量詞を担当する。仮定 g は 2 項キーの 4 つの値を受け取り、後続アリティの下での第 2 成分の所属を生み出す。すなわち sucV (ar .fst) と b の対である。第 1 スロットが載せるのは部分論理式ではなく有界の項だからである。
binSuccClosed-in : (C : Fin n) (k : ℕ) (γ : Vec S n)
→ ((c ar a b : S)
→ ⟨ c .fst ∈ (lookup C γ) .fst ⟩
→ c .fst ≡ pr (ar .fst) (pr (# k) (pr (a .fst) (b .fst)))
→ ⟨ pr (sucV (ar .fst)) (b .fst) ∈ (lookup C γ) .fst ⟩)
この構成は 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 (b .fst) ∈ (lookup C γ) .fst ⟩)
(sym (sucʟ-fst ar)) (g c ar a b c∈ sh)) ) ∣₁)
まとめ
closedAt は、定義域の各複合符号が、その節が読み取る部分論理式の符号を伴うことを要求する。消去補題はこれらの部分符号を取り出し、導入補題は同じ七つの義務をメタ言語側の所属事実から構成する。