L における再帰的定義の内部化

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

読書案内 · 依存マップ

再帰的定義をまずメタ理論で与え、その値を後に L の集合として必要とすることがあります。この移行を与えるのが置換定理です。L の定義域と、その各点で値をただ一つもつ対象言語の論理式から、置換はすべての値からなる集合を作ります。添字への依存はグラフの論理式が保持します。置換で得られる集合は値域なので、異なる添字から同じ値が生じても一度だけ現れます。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Recursion {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

値を定める関係は、二つの自由変数をもつ対象言語の論理式で書き、値、添字の順に読みます。その充足関係は構成可能構造で解釈されます。これにより、置換は L の内部の関係を扱いながら、一意性の証明はメタ理論で利用できます。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

構成には L の段階構造も用います。各構成可能集合はある段階に現れ、Type ℓ の型で添字づけられた族の各段階は一つの順序数で抑えられます。共通の定義域の上界が必要なとき、これにより族全体を含む一つの集合が得られます。

open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset-mono )
open import L.Ordinal {ℓ} using ( boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )

L の置換は、必要な項数をもつ任意の論理式に適用できます。ここでそれを用いる側は、論理式が Δ₀ であることや、すべての定数が選んだ段階に属することを別に証明する必要はありません。それらは一般の置換定理の証明で処理されています。第二成分が命題である依存対の間のパスを用いて、値の一意性を表します。

open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.Prelude using ( isPropIsContr )
import Cubical.HITs.PropositionalTruncation as PT

構成可能な領域上の述語に対して、SetOf は、その述語を実現する集合と所属の仕様からなる型です。置換はこの形で値域を返します。命題的切り詰めは、元となる添字の存在を、特定の一つを選ばずに記録します。

open PT using ( ∣_∣₁; ∥_∥₁ )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

以下の充足記号は、𝒮ʟ における論理式の意味論を表します。一般の置換定理は、この意味論と置換の証明で用いた段階ごとの議論をすでに結びつけています。本章はその定理を用いるのであり、任意の論理式が L と周囲の階層の間で絶対的だと仮定するものではありません。

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

再帰が与えるべきもの

三つです。定義域は添字の集合であり、それ自身モデルの要素です。したがって各添字は L の集合であり、添字全体も一つの集合です。グラフは二変数の論理式で、値が先、添字が後という、モデルの置換のフィールドと同じ順です。その定数は L の任意の要素でよく、すでに内部化された表を読む再帰は、ここでその表を名指します。複雑さの上限も、定数の属する段階の制限もありません。

record Recursion : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom   : S
    graph : Formula S 2

ここでの関数性は、存在と一意性の両方を含みます。定義域の各添字で、値と、それがグラフを満たす証明との対からなる型が可縮でなければなりません。その中心が値を与え、収縮が、グラフを満たす他の値はすべてそれと一致することを証明します。

    funct : (x : S) → ⟨ x ∈ˢ dom ⟩
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)

補題 smallDom は、X : Type ℓ で添字づけられた族 f : X → S を共通に含む集合を与えます。その集合が f の像と一致するとは主張せず、すべての再帰の定義域を自動的に与えるものでもありません。より大きな段階を定義域に用いるなら、そのすべての要素で値の存在と一意性をなお証明する必要があります。

smallDom : (X : Type ℓ) (f : X → S) → Σ[ d ∈ S ] ((x : X) → ⟨ f x ∈ˢ d ⟩)
smallDom X f = LsetS β oβ , mem
  where

界定の原理は値の段階に施します。各 f x は構成可能なのである段階に現れ、すべての f x の段階はただ一つの順序数 β の下にあります。順序数であることが証明されたこの順序数が、定義域として使う段階の集合を名指します。

  b = boundingOrd X (λ x → stage (fst (f x)) (f x .snd))
        (λ x → stage-ord (fst (f x)) (f x .snd))
  β = b .fst
  oβ : IsOrd β
  oβ = b .snd .fst

所属は二段階で従います。各値は自分の段階に現れ、段階は単調なので、段階の順序で β より下にある値は β における段階の要素です。こうしてすべての f x が定義域の集合の要素になります。

  mem : (x : X) → ⟨ f x ∈ˢ LsetS β oβ ⟩
  mem x = Lset-mono {α = β} {β = stage (fst (f x)) (f x .snd)} (b .snd .snd x)
            (stage-mem (fst (f x)) (f x .snd))

値域

再帰 R に対して、Image y を、定義域に属する添字 x が存在してグラフが x と y を関係づけること、とします。この存在は命題的に切り詰められるので、y が値として現れることだけを記録します。置換はこの述語を集合として実現し、添字と値の対の集合を作るわけではありません。

module Of (R : Recursion) where
  open Recursion R public

  private
    Image : S → hProp (ℓ-suc ℓ)
    Image y = ∃[ x ∶ S ] (x ∈ˢ dom) ⊓ ((y ∷ x ∷ []) ⊨ graph)

定義域、グラフ、関数性の証明に置換を適用すると、Image を実現する集合が得られます。その結果は、値域の集合と、そこへの所属を正確に記述する命題の両方を含みます。

    r : SetOf Image
    r = hasReplacementL dom graph funct .fst

値域はこの結果の第一成分です。その所属の仕様は、定義域のある添字でグラフが値 y をとることが単に存在するとき、かつそのときに限り y が値域に属する、と述べます。

  table : S
  table = r .fst

  table-mem : (y : S) → (y ∈ˢ table) ≡ Image y
  table-mem = r .snd

仕様の二つの向きは別々に利用できます。具体的なグラフの証人から、その値が値域に属することが従います。逆に、値域への所属から得られるのは、元となる添字とグラフの証人の切り詰められた存在だけであり、その添字を選ぶことはできません。

  table-in : (x y : S) → ⟨ x ∈ˢ dom ⟩ → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
           → ⟨ y ∈ˢ table ⟩
  table-in x y x∈ h = subst ⟨_⟩ (sym (table-mem y)) ∣ x , (x∈ , h) ∣₁

  table-out : (y : S) → ⟨ y ∈ˢ table ⟩ → ⟨ Image y ⟩
  table-out y h = subst ⟨_⟩ (table-mem y) h

関数性は、定義域の各要素におけるメタ理論上の値も定めます。それは可縮な型の中心の第一成分です。同じ添字で別の y がグラフを満たすなら、再帰データが与える収縮によってこの値と等しくなります。

  val : (x : S) → ⟨ x ∈ˢ dom ⟩ → S
  val x x∈ = funct x x∈ .fst .fst

  val-uniq : (x : S) (x∈ : ⟨ x ∈ˢ dom ⟩) (y : S)
           → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → val x x∈ ≡ y
  val-uniq x x∈ y h = cong fst (funct x x∈ .snd (y , h))

一意存在から関数性へ

構成によっては、グラフを満たす一意な値が単に存在することだけが自然に得られます。補題 mereFunct は、この命題的に切り詰められた一意存在を、Recursion が要求する可縮性へ変換します。決定可能性を仮定せず、一意性の証明とは独立に値を選ぶこともありません。

mereFunct : (graph : Formula S 2) (x : S)
          → ∥ (Σ[ y ∈ S ] (⟨ (y ∷ x ∷ []) ⊨ graph ⟩
                          × ((y' : S) → ⟨ (y' ∷ x ∷ []) ⊨ graph ⟩ → y' ≡ y))) ∥₁
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)

可縮性は命題なので、切り詰めをこの目標へ消去できます。一つの一意な値が収縮の中心を与え、その一意性の条項が他の各対を中心と同一視します。グラフの証明成分は命題なので、値の等式から依存対全体の等式が定まります。

mereFunct graph x = PT.rec isPropIsContr
  (λ { (y , (hy , uniq)) → (y , hy)
     , (λ { (y' , hy') → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph))
                           (sym (uniq y' hy')) }) })

メタ理論の関数から始める

メタ理論に全域関数 fn : S → S がすでにある場合には、Definition の形が便利です。定義域とグラフの論理式に加え、定義域上で論理式が fn x について成り立つこと、また論理式が許す各値が fn x に等しいことを証明します。

record Definition : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom     : S
    fn      : S → S
    graph   : Formula S 2

論理式が関数を定義する、と言うのは二つの含意です。一つは、各添字でその論理式が関数自身の値について成り立つこと。もう一つは、他に満たすものがないこと、すなわちグラフがある添字で許すどんな値も、そこでの関数の値と等しいこと。両者合わせて、グラフの妥当性の二方向です。

    defines : (x : S) → ⟨ x ∈ˢ dom ⟩ → ⟨ (fn x ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) → ⟨ x ∈ˢ dom ⟩ → (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x

この二つの含意から再帰構造が定まります。定義域とグラフはそのまま受け継がれ、残るのは、定義域の各点でグラフを満たす値のファイバーが可縮であることの証明です。

asRecursion : Definition → Recursion
asRecursion D = record
  { dom   = D.dom
  ; graph = D.graph

関数性は仮定されるのではなく、導かれます。中心は、関数の値と、グラフがそれについて成り立つことの証明の対です。競合する対は、第二の含意を通して中心と同一視されます。その含意が、対の値を関数の値に等しく強めるからです。同一視は対に沿って輸送され、その充足の成分は命題です。したがって、指定した定義域上でグラフの値のファイバーは可縮です。

  ; funct = λ x x∈ → (D.fn x , D.defines x x∈)
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ D.graph))
                            (sym (D.only x x∈ y h)) } }
  where module D = Definition D

定義可能な関数の像

先の変換を Definition に適用すると、その値域が L の集合として得られます。関数はメタ理論上の記述のままですが、グラフの論理式と置換により、指定した定義域上のすべての値が内部集合をなすことが証明されます。

module Image (D : Definition) where
  open Definition D public
  private
    module R = Of (asRecursion D)

このモジュールは、この値域を table という名で与えます。ここでは所属に関する補題を別に公開しません。完全な仕様が必要なら、基礎となる Recursion について証明されたものを用います。

  table : S
  table = R.table

構成の適用範囲

この結果には三つの条件があります。定義域が L の集合であること、関係が構成可能構造上の二変数の論理式で表されること、そして定義域の各点で値が一意に存在することです。Definition の形では、メタ理論上の全域関数と二つの妥当性の証明から最後の条件を導きます。補題 smallDom は、Type ℓ の型で添字づけられた族に共通の包含段階を与えますが、その段階を定義域にするなら、余分な各要素についても関数性を証明しなければなりません。

ここで置換を用いる際には、グラフの論理式の複雑さを制限したり、定数が同じ段階に属することを別に証明したりする必要はありません。この利便性は、すでに証明された一般の置換定理によるものです。任意の論理式が絶対的だと主張するものではなく、各適用ではなお論理式とその妥当性の証明を与える必要があります。

まとめ

置換は、内部の定義域上の関数的な論理式を L の値域へ変えます。Recursion は関数性を可縮性として直接述べ、mereFunct は切り詰められた一意存在からそれを導き、Definition はメタ理論上の全域関数とグラフの妥当性の二方向からそれを導きます。得られる集合はどの値が現れるかを記録し、どの添字がどの値を生むかは引き続きグラフの論理式が記録します。