Bedrock再帰的定義のグラフ
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップL の再帰は、内部の定義域の各点で一意な値を与えます。集合論の関数は、そのグラフ、すなわち入力を先、出力を後に置く順序対 pr(x , y) の集合で表されます。本章は再帰の値の関係をそのような集合 F に変え、F が関数的で、もとの定義域をちょうどもつことを証明します。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Recursion.Graph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure )
グラフ自体を対象言語で記述する必要があります。利用する構文は連言と存在文を作り、改名によって既存の二変数の値関係を新しい量化子の下に置きます。周囲の演算 pr が順序対の符号を与え、その単射性により、後で符号の等式から両方の座標を復元できます。
open import FOL.Syntax using ( Formula; _∧̇_; ∃̇_ ) open import FOL.Manipulation.Renaming using ( renameFo; module Sat ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; pr-inj )
構成可能な順序対の演算は、その基礎集合が周囲の順序対の符号である L の要素を作ります。そこで一般の再帰定理を、これらの順序対を記述する論理式に適用できます。構成可能性の証明は命題なので、構成可能な要素の等式は基礎集合の等式に帰着します。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Recursion {ℓ} lem using ( Recursion; module Of ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; domAt; domAt-intro ) open import Cubical.Data.Sigma using ( Σ≡Prop )
以下では、切り詰められた存在からいくつかの命題を得ます。切り詰めを消去できるのは命題である目標に限られます。累積階層の所属と等式はこの性質をもつため、大域的な選択を行わずに存在の証人を利用できます。
open import Cubical.Foundations.HLevels using ( isPropΣ ) open import Cubical.Functions.Logic using ( ∃[∶]-syntax ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
論理式は構成可能構造で解釈されます。局所的な充足記号と改名定理が、構文的な代入と環境の変化を結びつけます。以下の関数グラフに関する主張は、すべてこの意味論で述べられます。
open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename ) module PairFo (φ : Formula S 2) where
順序対の論理式
値と添字の関係として読む二変数の論理式 φ を固定します。モジュール PairFo は別の二変数の論理式を作ります。順序対の候補 e と添字 p に対し、φ(z,p) を満たす値 z が存在し、e が順序対 pr(p,z) であることを述べます。
ρ : Fin 2 → Fin 3 ρ zero = zero ρ (suc zero) = suc (suc zero)
改名写像は、φ の二つの自由変数が存在量化子の下でどこに現れるかを記録します。値の変数は位置 0 に残って量化子に束縛され、添字の変数は位置 2 へ移ります。pairFo は不透明なので、以後は定義を展開せず、証明された意味論的特徴づけを用います。
opaque pairFo : Formula S 2
この論理式は、存在量化子の下で二つの主張を連言します。第一は e が p と量化された値との順序対を符号化すること、第二は改名された φ です。したがって、この構文は関数グラフの要素の数学的記述をそのまま表します。
pairFo = ∃̇ (prAtL (suc zero) (suc (suc zero)) zero ∧̇ renameFo ρ φ)
一致の証明は、改名が意図した環境を保つことを確かめます。長い環境 (z ∷ e ∷ p ∷ []) では、改名後の値の位置は z を、添字の位置は p を読み、元の論理式を (z ∷ p ∷ []) で読む場合と正確に一致します。
private ag : (z e p : S) → Ren.Agrees ρ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ []) ag z e p zero = refl ag z e p (suc zero) = refl
二つの意味論的等式が外向きの読みを準備します。順序対の論理式の正しさにより、その充足は周囲の等式 fst e ≡ pr (fst p) (fst z) と同一視されます。改名定理により、改名後の論理式の充足は、値 z と添字 p における元の φ の充足と同一視されます。
at : (z e p : S) → ⟨ (z ∷ e ∷ p ∷ []) ⊨ prAtL (suc zero) (suc (suc zero)) zero ⟩ ≡ (fst e ≡ pr (fst p) (fst z)) at z e p = cong ⟨_⟩ (prAtL-adequate (suc zero) (suc (suc zero)) zero (z ∷ e ∷ p ∷ [])) gr : (z e p : S)
pairFo を外向きに読むと、命題的に切り詰められた値 z と、順序対の等式および φ(z,p) の証明が得られます。内向きにはこれらの輸送を逆に行い、値、等式、グラフの証明から pairFo の充足の証人を作ります。以下ではこの二つの意味論的方向を用います。
→ ⟨ (z ∷ e ∷ p ∷ []) ⊨ renameFo ρ φ ⟩ ≡ ⟨ (z ∷ p ∷ []) ⊨ φ ⟩ gr z e p = cong ⟨_⟩ (Ren.⊨-rename ρ φ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ []) (ag z e p)) pair-out : (e p : S) → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩ → ∥ Σ[ z ∈ S ] ((fst e ≡ pr (fst p) (fst z)) × ⟨ (z ∷ p ∷ []) ⊨ φ ⟩) ∥₁ pair-out e p = PT.map (λ { (z , (q , h)) →
内向きの補題で意味論的同値が完成し、ここから一つの再帰を固定します。もとの定義域と値の関係は保たれます。変わるのは置換へ渡す値だけで、出力そのものから入力と出力の順序対へ変わります。
z , (transport (at z e p) q , transport (gr z e p) h) }) pair-in : (e p z : S) → fst e ≡ pr (fst p) (fst z) → ⟨ (z ∷ p ∷ []) ⊨ φ ⟩ → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩ pair-in e p z q h = ∣ z , (transport (sym (at z e p)) q , transport (sym (gr z e p)) h) ∣₁ module Graph (R₀ : Recursion) where
定義域と値
再帰は、定義域、もとの値のグラフを表す論理式、および定義域の各要素におけるグラフの値ファイバーの可縮性を与えます。そこから得られる値を fn と記します。局所的な述語 Mem x は、fn が必要とする基礎の所属の主張です。
open Of R₀ public using ( dom; graph; funct ) renaming ( val to fn ) Mem : S → Type (ℓ-suc ℓ) Mem x = ⟨ fst x ∈ fst dom ⟩ isPropMem : (x : S) → isProp (Mem x) isPropMem x = snd (fst x ∈ fst dom)
集合への所属は命題値なので、Mem x は命題です。したがって、x が定義域に属することの任意の二つの証明は等しくなります。この証明無関係性により、値 fn x m は選んだ所属の証明に依存しません。
private defines : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩ defines x m = funct x m .fst .snd only : (x : S) (m : Mem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m only x m y h = sym (cong fst (funct x m .snd (y , h)))
可縮性から、もとの値関係について二つの事実が得られます。選ばれた中心は、環境 (fn x m ∷ x ∷ []) で論理式 graph が満たされることを証明します。収縮は、x でこの論理式を満たす他の任意の y が fn x m に等しいことを証明します。
module Fo = PairFo graph renaming ( pairFo to fo; pair-out to out; pair-in to into ) fn-irr : (x : S) (m m' : Mem x) → fn x m ≡ fn x m' fn-irr x m m' = cong (fn x) (isPropMem x m m') pairOf : (x : S) → Mem x → S pairOf x m = prʟ x (fn x m)
ここで順序対の論理式をもとの値関係に適用します。Mem x の証明無関係性から fn-irr が得られ、pairOf x m は x とその値との構成可能な順序対です。その基礎集合は pr (fst x) (fst (fn x m)) です。
uniq : (x : S) (m : Mem x) (p : S) → ⟨ (p ∷ x ∷ []) ⊨ Fo.fo ⟩ → p ≡ pairOf x m uniq x m p h = PT.rec (isSetS p (pairOf x m)) (λ { (z , (e , g)) → Σ≡Prop (λ v → snd (isL v)) (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z g) ∙ sym (prʟ-fst x (fn x m))) }) (Fo.out p x h)
候補 p が x で特殊化した順序対の論理式を満たすとします。外向きの補題は、値 z、p の基礎集合と pr(x,z) との等式、および z がもとのグラフを満たす証明を単に与えます。もとの値の一意性により z は fn x m と同一視され、得られた等式を合成すると p ≡ pairOf x m が従います。
R : Recursion R = record { dom = dom ; graph = Fo.fo ; funct = λ x m →
関数グラフを集める
もとの定義域を保ち、順序対の論理式を値関係とする新しい再帰を作ります。x における中心は pairOf x m です。内向きの意味論的補題がこの順序対による式の充足を証明し、uniq が他のすべての候補はそれと等しいことを証明します。
( pairOf x m , Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m) ) , λ { (p , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ Fo.fo)) (sym (uniq x m p h)) } } module T = Of R using ( table; table-in; table-out ) F : S
依存対の収縮は、候補の値とその充足の証明を、選ばれた中心と比較します。第一成分の等式は uniq が与え、充足の証明は命題なので、この等式から依存対全体のパスが定まります。これにより、順序対についての正しい Recursion が得られます。
F = T.table F-in : (x : S) (m : Mem x) → ⟨ pr (fst x) (fst (fn x m)) ∈ fst F ⟩ F-in x m = subst (λ w → ⟨ w ∈ fst F ⟩) (prʟ-fst x (fn x m)) (T.table-in x (pairOf x m) m (Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m)))
この再帰に置換を適用すると、順序対としての値の値域ができます。この値域が求める関数グラフ F です。したがって F は L の要素であり、そこに入る各要素は、定義域の要素と再帰で定まる値との順序対です。
F-out : (p : V ℓ) → ⟨ p ∈ fst F ⟩ → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁ F-out p h = PT.rec squash₁ step (T.table-out pS h) where pS : S
所属の内向きは置換の仕様から直ちに得られます。定義域の証人 m に対し、構成可能な順序対 pairOf x m は順序対の論理式を満たすので、置換の値域に属します。prʟ-fst に沿って輸送すると、周囲の符号 pr (fst x) (fst (fn x m)) が F の基礎集合に属するという形になります。
pS = p , isL-trans {x = fst F} {y = p} h (snd F) step : Σ[ x ∈ S ] (Mem x × ⟨ (pS ∷ x ∷ []) ⊨ Fo.fo ⟩) → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁ step (x , (m , g)) = PT.map (λ { (z , (e , gz)) →
外向きには、周囲の集合 p ∈ fst F から始めます。構成可能性の下方閉性により、p を L の要素 pS として包みます。置換の仕様からまず、添字 x、定義域の証明 m、および pS が順序対の論理式を満たすことが、単に得られます。
x , m , (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z gz)) }) (Fo.out pS x g) Fib : S → S → Type (ℓ-suc ℓ) Fib x y = Σ[ m ∈ Mem x ] (fst y ≡ fst (fn x m)) isPropFib : (x y : S) → isProp (Fib x y)
次に意味論的な外向きの補題が第二の切り詰めを開き、値 z、順序対の等式、もとの値関係の証明を与えます。もとの値の一意性により z を fn x m に置き換えます。その結果、ある定義域の要素 x に対して p が符号 pr(x,fn x m) であることが単に示されます。
isPropFib x y = isPropΣ (isPropMem x) (λ m → setIsSet (fst y) (fst (fn x m))) pair-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → Fib x y pair-out x y h = PT.rec (isPropFib x y) step (F-out (pr (fst x) (fst y)) h) where step : Σ[ x' ∈ S ] Σ[ m' ∈ Mem x' ] (pr (fst x) (fst y) ≡ pr (fst x') (fst (fn x' m')))
二つの座標を復元する
x と y を固定すると、ファイバー Fib x y は二つの成分からなります。定義域の証明 m : Mem x と、y の基礎集合と fn x m の基礎集合との等式です。定義域への所属は命題値であり、V の等式も命題なので、両方の成分が命題です。したがってファイバー全体も命題です。
→ Fib x y step (x' , m' , e) = subst (λ z → Fib z y) (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj e .fst))) (m' , pr-inj e .snd) γ : S ^ 2 γ = F ∷ dom ∷ []
順序対の符号 pr(fst x,fst y) が F に属するなら、外向きの特徴づけから x'、m'、および pr(fst x',fst(fn x' m')) との等式が得られます。pr の単射性が両方の座標の等式を与えます。入力座標の等式に沿って m' を輸送すると x が定義域に属する証明となり、出力座標の等式が Fib x y の第二成分となります。
sv : ⟨ γ ⊨ svAt zero ⟩ sv = svAt-in zero γ (λ x y y' p q → let (m , e) = pair-out x y p (m' , e') = pair-out x y' q in e ∙ cong fst (fn-irr x m m') ∙ sym e')
環境 γ = F ∷ dom ∷ [] は、単値性と定義域を表す論理式の二つの自由変数に値を割り当てます。単値性を示すため、第一座標が同じ x である二つの順序対が F に属するとします。それぞれのファイバーから所属の証明 m、m' と、二つの出力が fn x m、fn x m' に等しいことが得られます。証明無関係性により二つの関数値が等しくなり、したがって出力も等しくなります。
dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩ dm = domAt-intro zero (suc zero) γ (λ x → fwd x , bwd x) where fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩ → Mem x fwd x = PT.rec (isPropMem x) (λ { (y , p) → fst (pair-out x y p) })
最後に、定義域の論理式を両方向に証明します。x が F のある順序対の第一座標として現れるなら、pair-out がファイバーを返し、そこから Mem x の証明が得られます。逆に m : Mem x なら、F-in により順序対 pr(x,fn x m) が F に属するので、x は第一座標として現れます。したがって、構成した関数グラフの定義域はちょうど dom です。
bwd : (x : S) → Mem x → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩ bwd x m = ∣ fn x m , F-in x m ∣₁