この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

宇宙レベル ℓ を固定する。このレベルをパラメータとして保つことで、異なる宇宙を同一視せずに、必要な大きさで構成を具体化できる。

module L.Coding.SubformulaClosure {ℓ : Level} where

論理式コード上の再帰には、各構成子が要求する直接の部分式の鍵を含む添字集合が必要である。本章では、まず Peel 性をもつ任意の集合について対象言語の七つの閉包条件を証明し、次に論理式の実際の部分式閉包へ適用する。

英語原文

The proof is short because the two halves it needs were built to meet here. An element of the closure is the key of a formula, and it brings a closure of its own that sits inside; a key of a given constructor shape has known subkeys, and which ones is computed from the shape's tag. So each of the seven clauses is the same four moves: take the element apart, read its tag, ask what that tag demands, and hand back what the formula's own closure already contains.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

open hPropView 𝒮ʟ using ( S )

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )

モデルの要素としての閉包

clo φ は外側で構成した集合 closure f h φ とその構成可能性の証明を組み合わせ、closedAt を評価できる L の要素にする。

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

private
  Cl : ∀ {n} → Formula K n → V ℓ
  Cl = closure f h

clo : ∀ {n} → Formula K n → S
clo φ = closure f h φ , closureL f h φ

部分式の鍵を復元する

Peel C は、C の各要素がある論理式の鍵であり、その論理式自身の閉包が C に含まれることを表す。これは構成子のタグが要求する直接の部分式の鍵を復元するために必要な情報そのものである。

英語原文

Stating it separately is not tidiness. A later chapter cuts a set of codes out of a stage and has to prove the same closedness for it, and that set is not a closure of anything; what it has instead is a characterization of its members as keys, and Peel is what a characterization turns into. So the seven clauses are proved once, for any set that peels, and the closure is the first of the two instances rather than the subject.

Peel : V ℓ → Type (ℓ-suc ℓ)
Peel C = (x : V ℓ) → ⟨ x ∈ C ⟩
       → ∥ (Σ[ m ∶ ℕ ] Σ[ ψ ∶ Formula K m ]
             ((x ≡ key f h ψ) × ((z : V ℓ) → ⟨ z ∈ Cl ψ ⟩ → ⟨ z ∈ C ⟩))) ∥₁

七つの閉包節

補助構成 same、one、up、sndUp は、取り出した論理式の鍵を、二項、単項、アリティを増やす構成子、有界量化子が要求する部分鍵へ変換する。七つのタグへの適用が七つの閉包条件を証明する。

英語原文

The truncation that peeling returns is eliminated straight away, which is allowed because what is being produced is a membership, or a pair of them, and membership is a proposition.

module _ (D : S) (peel : Peel (D .fst)) where

private
  C : V ℓ
  C = D .fst

  viaKey : (k : ℕ) (c : S) (ar p : V ℓ)
         → ⟨ c .fst ∈ C ⟩ → c .fst ≡ pr ar (pr (# k) p)
         → (T : Type (ℓ-suc ℓ)) → isProp T
         → (Concl f h C k ar p → T) → T
  viaKey k c ar p c∈ sh T pT g = rec₁ pT
    (λ { (m , ψ , q , incl) →
      g (byTag f h C ψ k ar p incl (sym q ∙ sh)) })
    (peel (c .fst) c∈)

  same : ∀ {m} (γ : Vec S m) (k : ℕ)
       → ((ar a b : V ℓ) → Concl f h C k ar (pr a b)
          → ⟨ pr ar a ∈ C ⟩ × ⟨ pr ar b ∈ C ⟩)
       → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (bothSameAt zero) ⟩
  same γ k use = binSameClosed-in zero k (D ∷ γ)
    (λ c ar a b c∈ sh →
      viaKey k c (ar .fst) (pr (a .fst) (b .fst)) c∈ sh _
        (isProp× ((pr (ar .fst) (a .fst) ∈ C) .snd)
                 ((pr (ar .fst) (b .fst) ∈ C) .snd))
        (use (ar .fst) (a .fst) (b .fst)))

  one : ∀ {m} (γ : Vec S m) (k : ℕ)
      → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr ar a ∈ C ⟩)
      → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSameAt zero) ⟩
  one γ k use = unSameClosed-in zero k (D ∷ γ)
    (λ c ar a c∈ sh →
      viaKey k c (ar .fst) (a .fst) c∈ sh _
        ((pr (ar .fst) (a .fst) ∈ C) .snd) (use (ar .fst) (a .fst)))

  up : ∀ {m} (γ : Vec S m) (k : ℕ)
     → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr (sucV ar) a ∈ C ⟩)
     → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSuccAt zero) ⟩
  up γ k use = unSuccClosed-in zero k (D ∷ γ)
    (λ c ar a c∈ sh →
      viaKey k c (ar .fst) (a .fst) c∈ sh _
        ((pr (sucV (ar .fst)) (a .fst) ∈ C) .snd) (use (ar .fst) (a .fst)))

  sndUp : ∀ {m} (γ : Vec S m) (k : ℕ)
        → ((ar a b : V ℓ) → Concl f h C k ar (pr a b)
           → ⟨ pr (sucV ar) b ∈ C ⟩)
        → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (succSndAt zero) ⟩
  sndUp γ k use = binSuccClosed-in zero k (D ∷ γ)
    (λ c ar a b c∈ sh →
      viaKey k c (ar .fst) (pr (a .fst) (b .fst)) c∈ sh _
        ((pr (sucV (ar .fst)) (b .fst) ∈ C) .snd)
        (use (ar .fst) (a .fst) (b .fst)))

七つの節の連言

closedOf は七つのタグの適用を、台となる集合が Peel を満たす任意のモデル要素についての連言 closedAt にまとめる。closureClosed は closure-inv を渡して clo φ に対する結果を得る。

英語原文

closureClosed is then the instance at a closure, and its peeling is closure-inv unchanged: the two statements are the same type, because Peel was read off that lemma's conclusion.

closedOf : ∀ {m} (γ : Vec S m) → ⟨ (D ∷ γ) ⊨ closedAt zero ⟩
closedOf γ =
    same γ 2 (λ _ a b r → r a b refl)
  , ( same γ 3 (λ _ a b r → r a b refl)
  , ( same γ 4 (λ _ a b r → r a b refl)
  , ( up γ 6 (λ _ _ r → r)
  , ( up γ 7 (λ _ _ r → r)
  , ( sndUp γ 8 (λ _ a b r → r a b refl)
  , sndUp γ 9 (λ _ a b r → r a b refl) )))))

closureClosed : ∀ {n m} (φ : Formula K n) (γ : Vec S m)
              → ⟨ (clo φ ∷ γ) ⊨ closedAt zero ⟩
closureClosed φ γ = closedOf (clo φ) (closure-inv f h φ) γ

まとめ

任意の Peel 性を持つ集合について closedOf が部分式閉包条件を証明し、closureClosed がそれを論理式の実際の閉包に適用する。内容は満足関係の値ではなく、各コード形が要求する部分鍵の包含である。

英語原文

What it cost is worth recording, because the same shape is what the satisfaction instance will pay. Four readers, seven lines of instantiation, and one lemma per reader; the content is in byTag one chapter earlier, where the ten constructors were matched against the seven demands once and for all rather than ten times seven. byTag was already written against an arbitrary target set, which is why generality here is free: the closure was never the subject, only the first thing handed in.