狭義整列順序と最小要素の探索

順序の台と順序関係そのものは、同じ宇宙レベルに住む必要はない。関係は固定レベル ℓₚ で値をとり、台は任意のレベルに住んでいてよい。この区別は一般性の問題であって探索の数学とは無関係であり、以下の最小要素の議論がレベルを比較することはない。

そのうえで、実際に働くのは二つの数学的概念である。整礎性は到達可能性の述語 Acc で表す。ある要素が到達可能とは、真に小さい各要素がさらに到達可能であることであり、すべての要素が到達可能なとき関係は整礎である。この到達可能性の証明書こそが、探索の再帰的降下を許すものである。三分性はその一方で、最小証人の一意性を支える比較データである。自然数上の順序はこの二つをすでに備えているため、その実例は組み立てだけで新たな証明を要しない。

module L.WellOrder.Base {ℓₚ : Level} where

自然数のある性質が少なくとも一つの数で成り立つとする。すると、その性質は最小の数で成り立つ。証人のうちには最小のものがあるからである。一般の狭義整列順序に対して、本章は既知の証人からの降下を用いる。まだ真に小さい要素が性質を満たすならそこへ移って繰り返し、満たさなければ現在の要素が最小である。順序の整礎性がこの降下は永遠に続かないことを保証し、探索は最小証人で止まる。

本章は、この議論を自然数だけでなく任意の狭義整列順序に対する定理にする。証明を支えるのは二つの順序のデータである。第一に、二つの要素の比較には真に小さい・等しい・真に大きいという三つの結果があり、これらを明示的なデータとして表せば証明は場合分けで推論できる。これが最小証人の一意性を示すもので、二つの最小証人は互いに真に小さいことはあり得ない。第二に、整礎性は各要素への到達可能性の証明書として表され、この証明書を一歩ごとに受け渡すことで、降下を型理論の中で実行できる。本章のこの証明には古典的な成分が一つある。各段階で、より小さい証人がまだ存在するかどうかを判定し、この単なる存在の問いを、それが問われるレベルでの排中律によって決着する。結果の一意性を含め、それ以外はすべて構成的である。

本章はまず比較データを定義し、次に順序の法則をまとめて述べ、さらに「最小であること」が命題であることと最小証人の存在を示し、最後に自然数上の狭義順序を実例として組み立てて、探索がそこで具体的に使えるようにする。

探索はさらに、不完全な情報のもとで行われなければならない。仮定が言うのは、証人の集合が「単に非空」であること、つまり ∥_∥₁ の住人が存在することだけである。また各降下段階で問われる「真に小さい証人がまだ残っているか」も、やはり単なる存在文である。どちらも選ばれた証人を手渡すわけではなく、手渡す必要もない。命題的な切り捨ての除去が許されるのは、目標である「最小要素であること」が命題だからであり、これは本章で示す。排中律が入るのはまさに、そのような存在の問いを証明か反証かへの二路判定に変える箇所である。

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder

この論理的状況が証明の順序を定める。いずれかの切り捨てを除去する前に、まず固定した点での最小性が命題であり、最小証人の全体型も命題であることを示す。三分性が任意の二候補の間のパスを与え、最小性と両立しない狭義比較は排除される。この一意性の議論を終えて初めて、降下は単に非空であるという仮定を消費できる。

データとしての三分性

狭義整列順序の二つの要素の比較には三つの可能的な結果があり、後の証明はどの結果が起きたかで場合分けして推論する必要がある。そこで比較を、三つの構成子をもつ帰納型として表す。各構成子はそれぞれの証拠、すなわち一方方向の狭義関係の証明、等式、あるいは他方方向の証明をデータとしてもたせる。三つの選択肢は入れ子の直和ではなく構成子のタグとして表されるため、証明は比較を直接検査し、自分がどの場合にいるかを名指せる。三つの型はそれぞれ独自の宇宙レベルに住んでよく、比較型は三つの最大値に住む。

三つの構成子 lt、eq、gt が三つの結果に対応する。等号の分岐は、等しいと報告するだけのタグではなく、台の要素間のパス a ≡ b の証明を運ぶ。自然数の例では、この型はライブラリの a ≟ b に対する三路判定を構成子ごとに翻訳して埋められる。

data Tri {ℓ₁ ℓ₂ ℓ₃ : Level} (A : Type ℓ₁) (B : Type ℓ₂) (C : Type ℓ₃)
       : Type (ℓ-max ℓ₁ (ℓ-max ℓ₂ ℓ₃)) where
  lt : A → Tri A B C
  eq : B → Tri A B C
  gt : C → Tri A B C

狭義整列順序の構造

狭義整列順序は単なる関係ではない。最小要素探索を機能させる法則を伴った関係である。関係、三分性、非反射性、推移性、整礎性を、台 A の上の単一のレコード SWO にまとめる。このインターフェースに名前を与えることで、以後の構成は特定の順序の作られ方に依存しなくなる。本章の後半で与える自然数の順序も他の実例も、同じ五つのフィールドを供給する。台と関係は異なる宇宙レベルに住んでよく、A はレベル ℓc に住み、関係は Type ℓₚ に値をとる。このような関係値の型そのものは一つ上の宇宙に住むため、レコードは ℓ-max ℓc (ℓ-suc ℓₚ) に住む。

最初の二つのフィールドは関係とその三分性である。任意の二要素 a と b に対し、tri∙ は比較データを返す。a <∙ b、パス a ≡ b、または b <∙ a のいずれかである。三分性は後で最小要素の一意性を支えるもので、二人の候補が互いに真に小さいことはあり得ない。

record SWO {ℓc : Level} (A : Type ℓc) : Type (ℓ-max ℓc (ℓ-suc ℓₚ)) where
  field
    _<∙_   : A → A → Type ℓₚ
    tri∙   : (a b : A) → Tri (a <∙ b) (a ≡ b) (b <∙ a)
    irr∙   : (a : A) → a <∙ a → ⊥₀

残りの三つのフィールドは順序の法則である。irr∙ はどの要素も自分自身より小さくないことを言い、trans∙ は推移性、そして wf∙ は A のすべての要素がこの関係について到達可能であると主張する。到達可能性は整礎再帰の背後にある帰納原理である。a における acc rs が与えられると、関数 rs はより小さい各要素に対して到達可能性のデータを生み出す。段階ごとに受け渡されるこの供給こそが、探索の降下を停止させるものである。

    trans∙ : (a b c : A) → a <∙ b → b <∙ c → a <∙ c
    wf∙    : WellFounded _<∙_

最小要素

A 上の狭義整列順序 w を固定する。命題値をとる述語 P に対し、要素 a が P の最小要素であるとは、P を満たし、かつ P を満たす要素で真に a より小さいものが存在しないことである。最小であることは命題であり、「最小要素」の型全体もそうである。二つ与えられれば、三分性が両方の真のケースを排除し、等しさを強制する。この二つの命題性の事実が本章の要である。命題値の目標は命題的な切り捨てを吸収できるからである。これにより後の探索が、単に非空なだけの部分集合から実際の最小要素を取り出せるようになる。

定義では P を hProp 値の族として取る。各ファイバーは「それが命題である」という証明書とともに梱包されている。⟨ P a ⟩ が基礎型を射影するので、IsLeast P a は、a が P を満たすことの証人と、他の各証人 b をその証明書 ⟨ P b ⟩ とともに b <∙ a の反証へ送る関数との対である。最小性の条件が要求されるのは実際に述語を満たす要素についてだけであり、部分集合の外の要素はどこにあってもよいことに注意してほしい。

module _ {ℓc : Level} {A : Type ℓc} (w : SWO {ℓc} A) where

open SWO w

IsLeast : {ℓ'' : Level} → (A → hProp ℓ'') → A → Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
IsLeast P a = ⟨ P a ⟩ × ((b : A) → ⟨ P b ⟩ → b <∙ a → ⊥₀)

isPropIsLeast : {ℓ'' : Level} (P : A → hProp ℓ'') (a : A) → isProp (IsLeast P a)

isPropIsLeast P a = isProp× ((P a) .snd) (isPropΠ λ b → isPropΠ λ _ → isProp→ isProp⊥)

isPropLeastOf : {ℓ'' : Level} (P : A → hProp ℓ'')
              → isProp (Σ[ a ∶ A ] IsLeast P a)
isPropLeastOf P (m , pm , minm) (m' , pm' , minm') =
  Σ≡Prop (isPropIsLeast P) (decide (tri∙ m m'))

  where
  decide : Tri (m <∙ m') (m ≡ m') (m' <∙ m) → m ≡ m'
  decide (lt m<m') = ⊥₀-rec (minm' m pm m<m')
  decide (eq e)    = e
  decide (gt m'<m) = ⊥₀-rec (minm m' pm' m'<m)

hostLeastOf : {ℓ'' : Level} → LEM (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
        → (P : A → hProp ℓ'')
        → ∥ Σ[ a ∶ A ] ⟨ P a ⟩ ∥₁ → Σ[ a ∶ A ] IsLeast P a
hostLeastOf {ℓ''} lem P =
  rec₁ (isPropLeastOf P) (λ { (a₀ , pa₀) → go a₀ (wf∙ a₀) pa₀ })

  where
  go : (a : A) → Acc _<∙_ a → ⟨ P a ⟩ → Σ[ m ∶ A ] IsLeast P m
  go a (acc rs) pa = decide (lem (Smaller , squash₁))
    where
    Smaller : Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))

    Smaller = ∥ Σ[ b ∶ A ] ((b <∙ a) × ⟨ P b ⟩) ∥₁
    decide : Dec Smaller → Σ[ m ∶ A ] IsLeast P m
    decide (yes q) = rec₁ (isPropLeastOf P)
      (λ { (b , (b<a , pb)) → go b (rs b b<a) pb }) q
    decide (no ¬q) = a , (pa , λ b pb b<a → ¬q ∣ b , (b<a , pb) ∣₁)

leastOfFormula : ∀ {ℓs ℓk} {𝒮 : ZFStructureₕ ℓs}
    {K : Type ℓk} {ι : K → ZFStructure.S 𝒮}
    {P : A → hProp ℓs} → Semantics.FormulaPredicate 𝒮 A K ι P
    → LEM (ℓ-max ℓc (ℓ-max ℓₚ ℓs))
    → ∥ Σ[ a ∶ A ] ⟨ P a ⟩ ∥₁ → Σ[ a ∶ A ] IsLeast P a
leastOfFormula {P = P} defined lem = hostLeastOf lem P

制限のない演算は HostLeast 名前空間を通してのみ公開する。これにより、呼び出し側はホスト層の探索を行っていることを明示する。モデルに面するコードは代わりに、対象論理式と検査済みの意味論的読みを入力に含む leastOfFormula を使うべきである。

module HostLeast {ℓc : Level} {A : Type ℓc} (w : SWO {ℓc} A) where

leastOf = hostLeastOf w

自然数の整列順序

自然数上の通常の狭義順序は束の四つの法則をすべて満たし、その整礎性は上側の自然数についての帰納で従う。この節では natOrder : SWO {ℓ-zero} ℕ を組み立てる。具体的な利用箇所である L.Choice.FiniteStageOrders は leastOfFormula natOrder を呼び、自然数で番号づけられた有限段階のうち、表示された性質を満たす最も早いものを選び出す。通常の順序について必要な材料はすべてライブラリが供給するため、この束は証明するのではなく組み立てるだけである。関係・非反射性・推移性・整礎性はライブラリのものをそのまま使い、三分性はライブラリの三路判定の手続きの答えを本章の構成子に名前を変えたものである。

残る真の調整が一つある。自然数の順序は最下層の宇宙レベルに住む一方、束の関係は固定レベル ℓₚ で値をとる。そこで各比較を Lift で包む。これは型の住むレベルを変えるだけで、住人については何も変えない。

liftAcc は到達可能性のデータを元の順序からその持ち上げられたコピーへ運ぶ。n における acc r が与えられると、持ち上げられた順序で n より下の m に対し、まず lower で持ち上げられた証明をほどいてから m で再帰する関数の acc を返す。これは到達可能性の引数に対する構造的再帰であり、最小証人の探索を駆動するのと同じパターンである。Lift が二つの宇宙引数をもつことに注意してほしい。ソースはゼロのままで、ターゲットだけが ℓₚ である。

liftAcc : (n : ℕ) → Acc _<_ n → Acc (λ a b → Lift {ℓ-zero} {ℓₚ} (a < b)) n
liftAcc n (acc r) = acc (λ m h → liftAcc m (r m (lower h)))

natOrder : SWO {ℓ-zero} ℕ
natOrder = record
  { _<∙_   = λ a b → Lift (a < b)

持ち上げられた到達可能性が手に入れば、natOrder はフィールドごとに埋められる。関係は a と b を Lift (a < b) に送り、非反射性は仮定をほどいてライブラリの ¬m<m を適用し、推移性は二つの証明をほどいてライブラリの <-trans で合成してから結果を再度持ち上げ、整礎性は各 n に対し liftAcc n (<-wellfounded n) を与える。ここで自然数の順序について新しい数学が証明されるわけではなく、行われるのはレベルの調整と束のフィールド名への名前の付け替えだけである。

  ; tri∙   = triOf
  ; irr∙   = λ a h → ¬m<m (lower h)
  ; trans∙ = λ a b c h k → lift (<-trans (lower h) (lower k))
  ; wf∙    = λ n → liftAcc n (<-wellfounded n) }
  where

三分性のフィールドは where ブロックの triOf である。ライブラリの判定手続き a ≟ b は、ライブラリ自身の三路型 NatOrder.Trichotomy a b の値を返す。その構成子 lt、eq、gt は本章の Tri と同じ三種類の証拠を運ぶ。そこで fromNat は構成子ごとに写す。どちらの方向の真に小さいことの証明も持ち上げられ、等式はそのまま通る。自然数の等しさにはレベルの調整が要らないからである。

  triOf : (a b : ℕ) → Tri (Lift (a < b)) (a ≡ b) (Lift (b < a))
  triOf a b = fromNat (a ≟ b)
    where
    fromNat : NatOrder.Trichotomy a b → Tri (Lift (a < b)) (a ≡ b) (Lift (b < a))
    fromNat (NatOrder.lt h) = lt (lift h)

fromNat の三つの節が翻訳を完成させる。合わせて読めば、名前の付け替えだけで足りる理由が分かる。ライブラリの比較データと本章のものは同じ形をしており、違いは二つの真に小さいことを表す型の住むレベルだけである。このフィールドが埋まれば、natOrder は完全に組み立てられた束となり、前節までの結果が適用される。排中律が与えられれば、ℕ 上の証人をもつ命題値述語には一意な最小の証人が存在する。

    fromNat (NatOrder.eq h) = eq h
    fromNat (NatOrder.gt h) = gt (lift h)

まとめ

これで狭義整列順序を一つの構造として受け渡し、三分性で比較し、最小の証人を探索できるようになった。SWO は関係と四つの法則をまとめる。HostLeast.leastOf は制限のないホスト述語の探索を明示し、leastOfFormula は論理式、環境、読み取り定理を要求してから、モデルに面するコードに同じ降下を許す。自然数の実例 natOrder は自然数による添字上の探索を可能にする。例えば後の章では、論理式で定義された性質を証明する L の最も早い有限段階を選ぶために使われる。排中律が入るのは探索の各降下段階で問われる判定のところだけである。束の定義、その法則、そして自然数の順序は構成的なままである。