---
title: "狭義整列順序と最小要素の探索"
module: L.WellOrder.Base
lang: ja
site: "Bedrock"
description: "狭義整列順序と最小要素の探索"
stage: "正準整列順序と選択公理"
reading_order: 73
canonical: https://bedrock.institute/ja/L.WellOrder.Base.html
html: L.WellOrder.Base.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/WellOrder/Base.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Semantics]
routes: [canonical-order]
translations: [https://bedrock.institute/en/L.WellOrder.Base.md, https://bedrock.institute/zh/L.WellOrder.Base.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

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

```agda
open import Base.Prelude
```

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

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

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

```agda
open import Base.Classical using ( LEM )
open import FOL.ZFStructure using ( ZFStructure; ZFStructureₕ )
import FOL.Semantics as Semantics
```

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

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

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

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

```agda
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` に対する三路判定を構成子ごとに翻訳して埋められる。

```agda
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` のいずれかである。三分性は後で最小要素の一意性を支えるもので、二人の候補が互いに真に小さいことはあり得ない。

```agda
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` はより小さい各要素に対して到達可能性のデータを生み出す。段階ごとに受け渡されるこの供給こそが、探索の降下を停止させるものである。

```agda
    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` の反証へ送る関数との対である。最小性の条件が要求されるのは実際に述語を満たす要素についてだけであり、部分集合の外の要素はどこにあってもよいことに注意してほしい。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

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

</summary>
<div class="submodule-fold-content">

```agda
  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` である。

```agda
  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'))
```

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

```agda
    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)
```

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

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

```agda
  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₀ })
```

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

```agda
    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` より下の要素の上で定義されている。これが降下の一段であり、これが無限に続かないことを保証するのは到達可能性のデータである。

```agda
      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) ∣₁)
```

定理 `hostLeastOf` は制限のないホスト層の道具である。その述語は `hProp` への任意の関数でよく、降下中に問われる古典的命題が集合論の言語から来る必要はない。呼び出し側には `HostLeast.leastOf` として公開され、この境界が各呼び出しで見える。モデルに面する構成には通常、より狭い境界が要る。`P` を `FormulaPredicate` を通して与えれば、その論理式、環境、読み取り定理も一緒に運ばれる。`leastOfFormula` は同じ降下を行うが、この定義可能性の証拠を定理の入力の一部にする。

```agda
  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
```

</div>
</details>

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

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

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

</summary>
<div class="submodule-fold-content">

```agda
  leastOf = hostLeastOf w
```

</div>
</details>

## 自然数の整列順序

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

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

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

```agda
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)` を与える。ここで自然数の順序について新しい数学が証明されるわけではなく、行われるのはレベルの調整と束のフィールド名への名前の付け替えだけである。

```agda
  ; 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` は構成子ごとに写す。どちらの方向の真に小さいことの証明も持ち上げられ、等式はそのまま通る。自然数の等しさにはレベルの調整が要らないからである。

```agda
  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` は完全に組み立てられた束となり、前節までの結果が適用される。排中律が与えられれば、`ℕ` 上の証人をもつ命題値述語には一意な最小の証人が存在する。

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

## まとめ

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