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

宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

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

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

open import Cubical.Foundations.Prelude using ( isPropIsContr )

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

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

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

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

open hPropView 𝒮ʟ

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 

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

    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 ((f x) .fst) (f x .snd))
        (λ x → stage-ord ((f x) .fst) (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 ((f x) .fst) (f x .snd)} (b .snd .snd x)
            (stage-mem ((f x) .fst) (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)

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

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

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 (λ p → p .fst) (funct x x∈ .snd (y , h))

一意存在から関数性へ

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

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

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

mereFunct graph x = rec₁ isPropIsContr
  (λ { (y , (hy , uniq)) → (y , hy)
     , (λ { (y' , hy') → Σ≡Prop (λ w → ((w ∷ x ∷ []) ⊨ graph) .snd)
                           (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 

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

    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 → ((w ∷ x ∷ []) ⊨ D.graph) .snd)
                            (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 : S
table = R.table

構成の適用範囲

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

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

まとめ

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