再帰的定義のグラフ

module PairFo (φ : Formula S ) where

順序対の論理式

値と添字の関係として読む二変数の論理式 φ を固定する。モジュール PairFo は別の二変数の論理式を作る。順序対の候補 e と添字 p に対し、φ(z,p) を満たす値 z が存在し、e が順序対 pr(p,z) であることを述べる。

ρ : Fin  → Fin 
ρ zero       = zero
ρ (suc zero) = suc (suc zero)

改名写像は、φ の二つの自由変数が存在量化子の下でどこに現れるかを記録する。値の変数は位置 0 に残って量化子に束縛され、添字の変数は位置 2 へ移る。pairFo は不透明なので、以後は定義を展開せず、証明された意味論的特徴づけを用いる。

opaque
  pairFo : Formula S 

この論理式は、存在量化子の下で二つの主張を連言する。第一は 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

二つの意味論的等式が外向きの読みを準備する。順序対の論理式の正しさにより、その充足は周囲の等式 e .fst ≡ pr (p .fst) (z .fst) と同一視される。改名定理により、改名後の論理式の充足は、値 z と添字 p における元の φ の充足と同一視される。

    at : (z e p : S)
       → ⟨ (z ∷ e ∷ p ∷ []) ⊨ prAtL (suc zero) (suc (suc zero)) zero ⟩
       ≡ (e .fst ≡ pr (p .fst) (z .fst))
    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 ] ((e .fst ≡ pr (p .fst) (z .fst)) × ⟨ (z ∷ p ∷ []) ⊨ φ ⟩) ∥₁
  pair-out e p = map₁ (λ { (z , (q , h)) →

内向きの補題で意味論的同値が完成し、ここから一つの再帰を固定する。もとの定義域と値の関係は保たれる。変わるのは置換へ渡す値だけで、出力そのものから入力と出力の順序対へ変わる。

    z , (transport (at z e p) q , transport (gr z e p) h) })

  pair-in : (e p z : S) → e .fst ≡ pr (p .fst) (z .fst) → ⟨ (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 = ⟨ x .fst ∈ dom .fst ⟩

isPropMem : (x : S) → isProp (Mem x)
isPropMem x = (x .fst ∈ dom .fst) .snd

集合への所属は命題値なので、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 (λ p → p .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 (x .fst) ((fn x m) .fst) である。

  uniq : (x : S) (m : Mem x) (p : S) → ⟨ (p ∷ x ∷ []) ⊨ Fo.fo ⟩ → p ≡ pairOf x m
  uniq x m p h = rec₁ (isSetS p (pairOf x m))
    (λ { (z , (e , g)) → Σ≡Prop (λ v → (isL v) .snd)
      (e ∙ cong (λ w → pr (x .fst) (w .fst)) (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 → ((w ∷ x ∷ []) ⊨ Fo.fo) .snd) (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 (x .fst) ((fn x m) .fst) ∈ F .fst ⟩
F-in x m = subst (λ w → ⟨ w ∈ F .fst ⟩) (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 ∈ F .fst ⟩
      → ∥ Σ[ x ∶ S ] Σ[ m ∶ Mem x ] (p ≡ pr (x .fst) ((fn x m) .fst)) ∥₁
F-out p h = rec₁ squash₁ step (T.table-out pS h)
  where
  pS : S

所属の内向きは置換の仕様から直ちに得られる。定義域の証人 m に対し、構成可能な順序対 pairOf x m は順序対の論理式を満たすので、置換の値域に属する。prʟ-fst に沿って輸送すると、周囲の符号 pr (x .fst) ((fn x m) .fst) が F の基礎集合に属するという形になる。

  pS = p , isL-trans {x = F .fst} {y = p} h (F .snd)

  step : Σ[ x ∶ S ] (Mem x × ⟨ (pS ∷ x ∷ []) ⊨ Fo.fo ⟩)
       → ∥ Σ[ x ∶ S ] Σ[ m ∶ Mem x ] (p ≡ pr (x .fst) ((fn x m) .fst)) ∥₁
  step (x , (m , g)) = map₁
    (λ { (z , (e , gz)) →

外向きには、周囲の集合 p ∈ F .fst から始める。構成可能性の下方閉性により、p を L の要素 pS として包む。置換の仕様からまず、添字 x、定義域の証明 m、および pS が順序対の論理式を満たすことが、単に得られる。

      x , m , (e ∙ cong (λ w → pr (x .fst) (w .fst)) (only x m z gz)) })
    (Fo.out pS x g)
Fib : S → S → Type (ℓ-suc ℓ)
Fib x y = Σ[ m ∶ Mem x ] (y .fst ≡ (fn x m) .fst)

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 (y .fst) ((fn x m) .fst))

pair-out : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → Fib x y
pair-out x y h = rec₁ (isPropFib x y) step (F-out (pr (x .fst) (y .fst)) h)
  where
  step : Σ[ x' ∶ S ] Σ[ m' ∶ Mem x' ] (pr (x .fst) (y .fst) ≡ pr (x' .fst) ((fn x' m') .fst))

二つの座標を復元する

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 → (isL v) .snd) (sym (pr-inj e .fst))) (m' , pr-inj e .snd)

γ : Vec S 
γ = F ∷ dom ∷ []

順序対の符号 pr(x,fst .fst y) が F に属するなら、外向きの特徴づけから x'、m'、および pr(x',fst .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 (λ p → p .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 (x .fst) (y .fst) ∈ F .fst) ⟩ → Mem x
  fwd x = rec₁ (isPropMem x) (λ { (y , p) → (pair-out x y p) .fst })

最後に、定義域の論理式を両方向に証明する。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 (x .fst) (y .fst) ∈ F .fst) ⟩
  bwd x m = ∣ fn x m , F-in x m ∣₁