部分式についての閉包

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

論理式コード上の再帰には、各構成子が要求する直接の部分式の鍵を含む添字集合が必要です。本章では、まず 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.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
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.Coding.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in )
open import L.Coding.CodeConstructibility {ℓ}
  using ( closure; closureL; closure-inv; byTag; Concl; key )

open import Cubical.Foundations.HLevels using ( isProp× )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

open hPropStructure 𝒮ʟ 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 (fst D)) where
    private
      C : V ℓ
      C = fst D

      viaKey : (k : ℕ) (c : S) (ar p : V ℓ)
             → ⟨ fst c ∈ C ⟩ → fst c ≡ 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 = PT.rec pT
        (λ { (m , ψ , q , incl) →
          g (byTag f h C ψ k ar p incl (sym q ∙ sh)) })
        (peel (fst c) c∈)

      same : ∀ {m} (γ : 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 (fst ar) (pr (fst a) (fst b)) c∈ sh _
            (isProp× (snd (pr (fst ar) (fst a) ∈ C))
                     (snd (pr (fst ar) (fst b) ∈ C)))
            (use (fst ar) (fst a) (fst b)))

      one : ∀ {m} (γ : 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 (fst ar) (fst a) c∈ sh _
            (snd (pr (fst ar) (fst a) ∈ C)) (use (fst ar) (fst a)))

      up : ∀ {m} (γ : 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 (fst ar) (fst a) c∈ sh _
            (snd (pr (sucV (fst ar)) (fst a) ∈ C)) (use (fst ar) (fst a)))

      sndUp : ∀ {m} (γ : 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 (fst ar) (pr (fst a) (fst b)) c∈ sh _
            (snd (pr (sucV (fst ar)) (fst b) ∈ C))
            (use (fst ar) (fst a) (fst b)))

七つの節の連言

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} (γ : 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) (γ : 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.