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

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

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

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

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

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

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

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

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

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

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

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

open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )
open import Cubical.Relation.Nullary using ( isProp¬ ) renaming ( ¬_ to ¬ᵗ_ )
import Cubical.Data.Empty as Empty

判定 (存在するならば) は証明か反証のどちらかを返します。二つの構成子をもつ直和型はまさにこの形の判定を与え、排中律が降下に渡す選択を担うことになります。

open import Cubical.Data.Sum using ( _⊎_; inl; inr )

データとしての三分性

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

三つの構成子 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)

IsLeast P a の両成分は命題です。第一は P a に梱包された証明書により、第二は命題値を返す否定値関数が命題であることによります。したがって「命題の対は命題」という閉じ方により、IsLeast P a は命題です。最小要素全体の型については、Σ≡Prop は第二成分が命題であるとき、第一成分が一致すれば二つの対を同一視します。この帰着をまさに行うのが補助関数 decide です。

  isPropIsLeast P a = isProp× (snd (P a)) (isPropΠ λ b → 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'))

二つの最小要素 m と m' を比較するために、decide は tri∙ m m' を検査します。m <∙ m' なら、m' は最小であり m は述語を満たすので、m が真に m' より小さいはずがありません。矛盾です。これは不可能な場合から任意の目標を導く Empty.rec によります。対称な場合も同様です。残る場合では、比較そのものがパス e : m ≡ m' を渡してくるので、それを直接返します。Σ≡Prop と合わせて、これが isPropLeastOf を証明します。P の最小証人の型は命題であり、したがって最小性は存在すれば一意です。

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

これが探索そのものです。問いが発せられるレベルでの排中律、述語 P、そして証人の部分集合の単なる住人を受け取り、最小性のデータを伴った実際の最小証人の対を返します。議論は整列順序に沿って降下します。任意の出発点の証人から、「より真に小さく P を満たす要素があるか」を問い、あればそこで再帰します。再帰のたびに真に下へ移動し、到達可能性が受け渡されるため、これは停止します。なければ、現在の要素が定義により最小です。各段階では任意の述語から構成される命題の古典的判定が必要であり、これが排中律が入る唯一の場所です。主張自体と順序の法則は構成的なままです。

仮定の切り捨ての除去が正当なのは、目標 Σ[ a ∈ A ] IsLeast P a が isPropLeastOf によって命題と示されているからです。したがって、単に非空な部分集合から出発点の証人 a₀ とその証明書を取り出し、降下 go a₀ (wf∙ a₀) pa₀ を始められます。束の一部である到達可能性のデータ wf∙ a₀ が再帰の燃料です。出発点の証人は任意であることに注意してください。最小要素を生み出すのは出発点の選択ではなく降下のほうです。

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

補助関数 go は要素 a、その到達可能性のデータ、そして a が P を満たすことの証明書を受け取り、最小証人を返します。各段階で命題 Smaller を構成します。すなわち、真に a より小さく P を満たす要素が「単に存在する」かどうかです。その基礎型は命題的な切り捨てなのでこれは hProp であり、排中律が適用できます。レベルの帳簿づけにより、判定はまさに関係するデータのレベルで行われます。

    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 ℓₚ ℓ''))

lem を Smaller に適用すると証明か反証が得られ、decide はどちらの判定も最小証人に変えます。肯定の場合、切り捨てられた主張は再び命題値の目標へと除去され、真に a より小さく P b を満たす実際の要素 b が渡されます。再帰は到達可能性関数 rs を用いて b で続きます。rs はまさに a より下の要素の上で定義されています。これが降下の一段であり、これが無限に続かないことを保証するのは到達可能性のデータです。

      Smaller = ∥ Σ[ b ∈ A ] ((b <∙ a) × ⟨ P b ⟩) ∥₁
      decide : Smaller ⊎ (Smaller → Empty.⊥) → Σ[ m ∈ A ] IsLeast P m
      decide (inl q) = PT.rec (isPropLeastOf P)
        (λ { (b , (b<a , pb)) → go b (rs b b<a) pb }) q
      decide (inr ¬q) = a , (pa , λ b pb b<a → ¬q ∣ b , (b<a , pb) ∣₁)

自然数の整列順序

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

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

liftAcc は到達可能性のデータを元の順序からその持ち上げられたコピーへ運びます。n における acc r が与えられると、持ち上げられた順序で n より下の m に対し、まず lower で持ち上げられた証明をほどいてから m で再帰する関数の acc を返します。これは到達可能性の引数に対する構造的再帰であり、後に leastOf を駆動するのと同じパターンです。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 は関係と四つの法則をまとめ、leastOf は単に非空なだけの任意の部分集合から最小の証人を取り出します。その一意性は isPropLeastOf の供給するパスによって理解されます。自然数の実例 natOrder は自然数による添字上の探索を可能にします。例えば後の章では、性質を証明する L の最も早い有限段階を選ぶために使われます。排中律が入るのは探索の各降下段階で問われる判定のところだけです。束の定義、その法則、そして自然数の順序は構成的なままです。