構成可能な段階における最小の証人の写像

周囲の段階 Lset γ を、構成可能な台の要素 Lγ としてまとめる。この包みはグラフ論理式の定数として現れ、探索範囲を固定された候補の段階に正確に制限できる。

opaque
  Lγ : S
  Lγ = LsetS γ oγ

等式 Lγ-fst は、この不透明な包みの底の集合を Lset γ と同一視する。後でホスト側の段階と論理式が使う定数との間を移るとき、所属の証明はこの等式に沿って輸送される。

  Lγ-fst : Lγ .fst ≡ Lset γ
  Lγ-fst = refl

内部関係を符号化するには、順序数の添字自体も構成可能宇宙の要素でなければならない。すべての順序数は構成可能であり、oγ は γ についてその事実を得るために必要な順序数性を与える。

  hγ : ⟨ isL γ ⟩
  hγ = isL-ord γ oγ

段階の順序の内部実装は、符号化された対からなる構成可能な集合であり、最小性はこの関係の中で表現される。

Rγ : S
Rγ = relL γ hγ oγ

述語 Mem x は入力への制約、すなわち x ∈ X の証拠を記録する。証人候補には条件を課さない。候補の別の台は、次に Lset γ の要素の型として定める。

Mem : S → Type (ℓ-suc ℓ)
Mem x = ⟨ x .fst ∈ X .fst ⟩

順序 orderAt γ oγ が作用するのは段階の要素であり、S の任意の要素ではない。部分型 Mγ は、比較される各対象に境界 c ∈ Lset γ を組み込むので、最小要素の探索が固定された候補の段階の外へ出ることはない。

private
  Mγ : Type (ℓ-suc ℓ)
  Mγ = MemOf (Lset γ)

Mγ の要素は、底の集合と、その集合が Lset γ に属するという証明を含む。構成可能な段階の各要素は構成可能なので、memS はその底の集合を台 S へ移せる。もとの所属の証明は、候補に対する段階の境界としてそのまま残る。

  memS : Mγ → S
  memS c = c .fst , Lset→isL γ oγ (c .fst) (c .snd)

候補と入力のもとでの述語とは、P が、候補を先に、入力を後に置いた環境の中で充足されることである。

  At : S → S → hProp (ℓ-suc ℓ)
  At w x = (w ∷ x ∷ []) ⊨ P

述語 Good x は、もとの関係を orderAt γ oγ が整列する台へ移す。段階の要素が良い候補であるのは、それに対応する S の要素が入力 x とともに P を満たすとき、ちょうどそのときである。したがって後の探索が並べるのは Lset γ の候補であり、X の入力を並べたり、候補を X に制限したりはしない。

  Good : S → Mγ → hProp (ℓ-suc ℓ)
  Good x c = At (memS c) x

固定した各入力について、この述語の論理式に面する形は、もとの二項論理式 P を使う。段階の要素が memS を通して環境の第一成分を、固定入力が第二成分を与える。検査済みの読みは反射的なので、このパッケージは新しい数学的仮定を加えず、Good にすでにある構文を露出させるだけである。

  definedGood : (x : S) → FOL.Semantics.FormulaPredicate 𝒮ʟ Mγ S id (Good x)
  definedGood x = FOL.Semantics.presented  P (λ c → memS c ∷ x ∷ []) (λ c → refl)

同じ底の集合が、構成可能性の二つの証明を伴って現れることがある。構成可能性は命題なので、S≡ は二つの包まれた S の要素を同一視する。得られたパスに沿って充足の証明を輸送すれば、組み直した段階の要素が、もとの証人と同じ P の実例を満たすと分かる。

  toMem : (x w : S) (hw : ⟨ w .fst ∈ Lset γ ⟩) → ⟨ At w x ⟩ → ⟨ Good x (w .fst , hw) ⟩
  toMem x w hw = subst (λ v → ⟨ At v x ⟩) (S≡ refl)

選択は、入力 x と証拠 m : x ∈ X を固定してから各点で行う。この証拠によって各点の存在仮定 have を使えるが、候補が X に属することも、X に順序が入ることも意味しない。

module Sel (x : S) (m : Mem x) where

private
  nonempty : ∥ Σ[ c ∶ Mγ ] ⟨ Good x c ⟩ ∥₁
  nonempty = map₁ (λ { (w , hw , hp) → (w .fst , hw) , toMem x w hw hp }) (have x m)

opaque
  c : Mγ
  c = (leastOfFormula (orderAt γ oγ) (definedGood x) lem nonempty) .fst

  c-good : ⟨ Good x c ⟩
  c-good = ((leastOfFormula (orderAt γ oγ) (definedGood x) lem nonempty) .snd) .fst

  minimal : (c' : Mγ) → ⟨ Good x c' ⟩ → relOf (orderAt γ oγ) c' c → ⊥₀
  minimal = ((leastOfFormula (orderAt γ oγ) (definedGood x) lem nonempty) .snd) .snd

e : S
e = memS c

e-holds : ⟨ (e ∷ x ∷ []) ⊨ P ⟩
e-holds = c-good

e∈Lγ : ⟨ e .fst ∈ Lset γ ⟩
e∈Lγ = c .snd

証拠 m : x ∈ X を伴う入力 x に対して、関数 fn はこの選ばれた候補を返す。存在仮定を使えるのは X 上だけなので、定義域の証拠が明示されている。

fn : (x : S) → Mem x → S
fn x m = Sel.e x m

そのような定義域の各入力について、選ばれた値は環境 (fn(x),x) でもとの論理式を満たす。

fn-holds : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ P ⟩
fn-holds x m = Sel.e-holds x m

同じ値は Lset γ に属する。この独立した値域の主張によって、後で定義可能な写像の終域を Lγ にできるが、値が入力集合 X に属するという意味ではない。

fn-in : (x : S) (m : Mem x) → ⟨ (fn x m) .fst ∈ Lset γ ⟩
fn-in x m = Sel.e∈Lγ x m

L の内部でも表せる形で最小性を述べるため、比較候補 w' が fn(x) より小さいことを内部関係 Rγ が記録していると仮定する。読み出し補題 relL-rep は、この符号化された項目を orderAt γ oγ が使うホスト側の比較へ移し、選ばれた要素の最小性がそれを反駁する。結論が排除するのは Lset γ にある充足候補だけであり、しかもこの固定された順序に関してだけである。

fn-least : (x : S) (m : Mem x) (w' : S) → ⟨ w' .fst ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
         → ⟨ pr (w' .fst) ((fn x m) .fst) ∈ Rγ .fst ⟩ → ⊥₀
fn-least x m w' hw' hp hr = Sel.minimal x m (w' .fst , hw') (toMem x w' hw' hp)
  (relL-rep γ hγ oγ (w' .fst , hw') (Sel.c x m) hr)

ホスト側の仕様 TWit w x は、グラフ論理式が表すべき三つの事実をまとめる。すなわち P(w,x)、w が固定された段階に属すること、そして orderAt γ oγ において w より真に小さく P を満たす段階の要素がないことである。これはグラフの値の仕様であり、この時点ではグラフはまだ内部の表として集められていない。

TWit : (w x : S) → Type (ℓ-suc ℓ)
TWit w x =
    ⟨ (w ∷ x ∷ []) ⊨ P ⟩
  × ⟨ w .fst ∈ Lset γ ⟩
  × ((w' : S) → ⟨ w' .fst ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩

最後の成分は、w' ∈ Lset γ と P(w',x) を満たす任意の w' を調べる。符号化対 (w',w) が Rγ に属するなら、w' が固定された段階順序で真に小さいことを意味し、仕様はまさにその可能性を退ける。

      → ⟨ pr (w' .fst) (w .fst) ∈ Rγ .fst ⟩ → ⊥₀)

一意性を示す範囲は、完全な TWit の仕様を満たす候補に限られる。もとの述語 P は段階の中に多数の証人をもってよいのである。狭義全順序が排除するのは、異なる二つの候補がともに P を満たし、しかも両方により小さい充足候補がないという状況である。三分性により、任意の候補と選ばれた値との比較は、次の三場合に分かれる。

fn-unique : (x : S) (m : Mem x) (w : S) → TWit w x → w .fst ≡ (fn x m) .fst
fn-unique x m w (hp , hw , mn) = go (SWO.tri∙ (orderAt γ oγ) c' (Sel.c x m))
  where
  c' : Mγ
  c' = w .fst , hw

代替の候補が選ばれたものより真に下なら、最小性と矛盾する。二つの段階の要素が一致すれば、底の集合が等しくなる。

  go : Tri∙ (relOf (orderAt γ oγ) c' (Sel.c x m)) (c' ≡ Sel.c x m)
            (relOf (orderAt γ oγ) (Sel.c x m) c')
     → w .fst ≡ (fn x m) .fst
  go (lt k) = ⊥₀-rec (Sel.minimal x m c' (toMem x w hw hp) k)
  go (eq q) = cong (λ p → p .fst) q

選ばれた候補が代替の候補より真に下なら、代替の候補自身の最小性と矛盾する。欠けていた比較は、内部の関係の埋めの方向によって供給される。

  go (gt k) = ⊥₀-rec (mn (fn x m) (fn-in x m) (fn-holds x m)
    (relL-fill γ hγ oγ (Sel.c x m) c' k))

有界量化子の内側では環境が (w',w,x) となるが、P が期待するのは (候補,入力) である。そこで名前替えは変数 0 を、引き続き w' であるスロット 0 へ送り、変数 1 を、いま x であるスロット 2 へ送る。スロット 1 は、w' と比較される値の候補 w のために残す。

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

環境の一致は、この二つの対応を正確に記録する。(w',w,x) から変数 0 を読むと (w',x) の第一項になり、名前替え後に変数 1 を読むとその第二項になる。この変数ごとの一致が、論理式 P 全体の充足を輸送するための前提である。

  ag : (w' w x : S) → Ren.Agrees ρ (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ [])
  ag w' w x zero       = refl
  ag w' w x (suc zero) = refl

最小性の論理式は w' ∈ Lγ の上を動き、二つの主張の連言を否定する。すなわち、符号化対 (w',w) が Rγ に属することと、P(w',x) が成り立つことである。その意味は、固定された段階の候補で、orderAt γ oγ において w より小さく、同じ入力についてもとの述語を証言するものはない、ということである。

opaque
  private
    leastFo : Formula S 
    leastFo = ∀̇∈ (con Lγ) (¬̇ (appC Rγ i0 i1 ∧̇ renameFo ρ P))

名前替えとの両立性により、P の二つの読みが一致する。(w',w,x) で renameFo ρ P を評価することは、(w',x) で P を直接評価することと同じである。現在の値の候補 w は、比較候補についての述語の検査には意図的に現れず、順序比較 (w',w) にだけ現れる。

    ren : (w' w x : S)
        → ⟨ (w' ∷ w ∷ x ∷ []) ⊨ renameFo ρ P ⟩ ≡ ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
    ren w' w x = cong ⟨_⟩ (Ren.⊨-rename ρ P (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ []) (ag w' w x))

完全なグラフの論理式は、もとの述語に、段階への所属と最小性の節を連言する。値が記録されるのは、述語を充足し、固定された段階に属し、そしてそうする段階の要素の中で最小のとき、ちょうどそのときである。

  fo : Formula S 
  fo = P ∧̇ ((var i0 ∈̇ con Lγ) ∧̇ leastFo)

fo を外向きに読むと、意味論的な仕様の三部分が得られる。すなわち P(w,x)、所属 w ∈ Lset γ、そして同じ段階に、条件を満たし、内部順序によって w より小さいと記録される要素がないことである。論理式 fo 自体は条件 x ∈ X を含まない。この制限は、fo を Dmap のグラフ論理式として使うときに課される。したがって X は値を定めるべき入力を制御し、Lset γ はその入力について比較される候補を制御する。

  fo-out : (w x : S) → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩ → TWit w x
  fo-out w x (hp , (hl , hm)) =
      hp
    , subst (λ v → ⟨ w .fst ∈ v ⟩) Lγ-fst hl
    , λ w' hw' hp' hr → lower (hm w' (subst (λ v → ⟨ w' .fst ∈ v ⟩) (sym Lγ-fst) hw')

TWit の最小性の成分を得るため、比較候補 w' を固定し、意味論的な事実 pr(w',w) ∈ Rγ と P(w',x) を仮定する。証明は appC-adequate と名前替えを内向きに用いて、この二つの事実を fo が否定する二つの連言の充足へ移す。すると有界な条項から矛盾が得られる。この関係の項目は段階順序による比較の対象言語での符号化であり、relOf (orderAt γ oγ) と定義的に等しいわけではない。

        ( subst ⟨_⟩ (sym (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ []))) hr
        , transport (sym (ren w' w x)) hp' ))

逆に、TWit を満たす証人からグラフ論理式の証明が定まる。最初の二つの成分は P(w,x) と w ∈ Lset γ を与える。有界な最小性の条項については、同じ段階の任意の w' を取り、符号化された順序で w' が w より前にあり、かつ P(w',x) が成り立つと仮定する。TWit の最後の成分が、まさにこの連言を排除する。

  fo-in : (w x : S) → TWit w x → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩
  fo-in w x (hp , hl , mn) =
      hp
    , subst (λ v → ⟨ w .fst ∈ v ⟩) (sym Lγ-fst) hl
    , λ w' hw' hc → lift (mn w' (subst (λ v → ⟨ w' .fst ∈ v ⟩) Lγ-fst hw')

改名と適用の妥当性によって、この二つの仮定は意味論的な最小性が受け取る形になる。fo-out と fo-in を合わせると、fo が固定された段階における最小証人の仕様を正確に表すことが分かる。もとの述語の証人が一意であることも、Lset γ の外にある候補との比較も、ここには加えられていない。

        (transport (ren w' w x) (hc .snd))
        (subst ⟨_⟩ (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ [])) (hc .fst)))

この正確な対応により、選択は定義可能な写像になる。入力集合は X、終域は Lγ である。x ∈ X の各証明に対する値は fn x m であり、先に示した段階への所属によって、その値は Lγ に入る。グラフ論理式は環境 (値,入力) で読まれるので、第一変数が選ばれた証人を、第二変数が入力を表す。

Dmap : DefinableMap
Dmap = record
  { dom = X ; cod = Lγ ; fn = fn
  ; into = λ x m → subst (λ v → ⟨ (fn x m) .fst ∈ v ⟩) (sym Lγ-fst) (fn-in x m)
  ; graph = fo

選ばれた値については、すでに示した三つの事実から fo の証明が得られる。その値は P を満たし、候補の段階に属し、その段階にはそれより小さく P を満たす候補がない。逆に、fo を満たす値はこの最小証人の仕様をすべて備えるので、選ばれた値と等しくなる。この一意性は二つの候補がともに最小であることと orderAt γ oγ の三分律から従うのであり、P の証人の一意性から従うのではない。構成可能性の証拠は命題なので、基礎となる集合の等しさは S での等しさへ持ち上がる。

  ; defines = λ x m → fo-in (fn x m) x (fn-holds x m , fn-in x m , fn-least x m)
  ; only = λ x m w h → S≡ (fn-unique x m w (fo-out w x h)) }

一つの論理式が X の各入力にただ一つの値を定めれば、置換によってそれらの値を L の内部に集められる。グラフの構成を Dmap に適用すると、順序対からなる構成可能集合と、その所属関係を利用するための二方向の読みが得られる。

private module Gr = Graph Dmap using ( F; F-in; pair-out )

こうして集めた集合を T と呼ぶ。その項目は順序対 (x,fn(x)) であり、入力が先、選ばれた値が後である。これは論理式の充足に用いた環境 (値,入力) と逆の順序である。二つの規約を区別することで、グラフ論理式を内部の表そのものと取り違えずに済む。

T : S
T = Gr.F

各 x ∈ X について、表は順序対 (x,fn(x)) を含む。したがって後の議論では、入力ごとに単に非空な族から別々に選ぶのではなく、一つの構成可能集合への所属を通して、これらの選択を参照できる。

T-in : (x : S) (m : Mem x) → ⟨ pr (x .fst) ((fn x m) .fst) ∈ T .fst ⟩
T-in = Gr.F-in

逆に、項目 (x,w) ∈ T からは、証拠 x ∈ X と、w の底の集合が選ばれた値 fn(x) の底の集合に等しいことが得られる。表への所属そのものは、最小性の証明を返さない。HullCounting では、この表を使って、それまでは命題的切り詰めのもとでしか得られなかった選択をそろえる。単射が必要な場合には、基礎となる関係について逆向きの関数性を別に仮定し、一つの関係する候補が異なる二つの入力に対応しないことを示す。単射性は最小選択だけから従うものではない。

T-out : (x w : S) → ⟨ pr (x .fst) (w .fst) ∈ T .fst ⟩
      → Σ[ m ∶ Mem x ] (w .fst ≡ (fn x m) .fst)
T-out = Gr.pair-out