Bedrock後者段階の要素の正準な名前
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ後続段階の要素は、一つの論理式と直前の段階から取った有限個のパラメータによって定まる。本章ではそのデータを名前としてまとめ、すべての要素が名前をもつことを示し、最小の代表を選べるよう名前全体を整列する。
後続段階の要素とは、その下の段階の定義可能部分集合のことであり、前の章たちはこのことを二通りに述べてきた。一つは L.Definability で、その段階から取ったパラメータ付きの論理式としてであり、もう一つは FOL.Manipulation.ParameterAbstraction で、パラメータを構文から取り除いた後の「パラメータなし論理式とパラメータ列の組」としてである。比較できるのは後者の形である。その論理式は有限な構文片なので、そのコードは遺伝的有限集合であり、極限段階 Lset ω に既に現れている。L.Choice.FiniteStageOrders はまさにそこを整列する。パラメータは下の段階の要素であり、この章が呼ばれる時点で、外側の構成によって既に整列されている。名前とは、その間にアリティを挟んだこの組であり、本章はそれを構成し、後続段階の各要素が名前をもつことを示し、名前全体を整列する。
この順序は、三つの鍵による辞書式比較をそのまま書き下したものである。ここに「依存和上の一般的な順序」のインスタンスは何もなく、それは意図的なことである。そのような一般論は、第一の鍵で索引された順序の族を運び、四つの法則をその一般性のもとで証明せねばならず、一度しか使わない用途には大きすぎる定理になる。三つの鍵にはそれぞれ名前がついており、各鍵は既に存在する順序によって比較される。
明示的な古典的入力は lem : LEM (ℓ-suc ℓ) です。これは論理式コードに用いる有限段階の極限順序と、最後の最小要素探索の双方を支えます。モジュール引数として保つことで、二つの構成が共通して必要とする強さを記録できます。その間の符号化、抽象化、辞書式順序の法則、到達可能性の議論は追加の公理を用いません。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Choice.CanonicalNames {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
名前を書き表す語彙は、集合論の一階述語論理の言語から来る。ここでの論理式は、定数記号の領域と固定個数の自由変数スロットをともに持ち、構成子は所属、等号、論理結合子、偽、そして両種の量化子を覆う。有界形式も並べて挙げられている。この構文は既に存在しており、本章が要するのは、定数領域が空であるという特別な形の論理式に名前を付け、比較することだけである。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; con; var ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Semantics
定数付きの定義を名前へ変える実質的な作業は、論理式に対する既存のいくつかの操作が担う。項と論理式を集合へ符号化する操作は、第一の鍵となるコードを供給する。定数の改名の補題は、定数領域の埋め込みを通して論理式を読んでも充足関係が保たれることを述べる。出現の数え上げとパラメータの抽象は、定数を新しい変数とパラメータ列に置き換える。宇宙の側では、構造 𝒮ᵥ が V の中でこの言語を解釈し、対の構成 pr がコードの断片を集合として包む。
open import FOL.Manipulation.ConstantMapping using ( mapTm; embed ) open import FOL.Manipulation.Relabelling using ( embed-⊨ ) open import FOL.Manipulation.ConstantOccurrences using ( countFo; constantsFo ) open import FOL.Manipulation.ParameterAbstraction using ( absFo; ⊨-abs₁ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
構成可能な側は、名前を付けられる対象を供給する。Lset は V の中の構成可能階層の一つの段階であり、𝒟ₒ は定義可能冪集合の演算子である。これは集合を一つ取り、その部分集合のうち、それを定数域とする一変数の論理式で定義できるもの全体を返す。決定的なのは、𝒟ₒ が手渡すのはそのような論理式が存在することの截断された証拠だけだという点で、したがって名前付けの完全性は、選ばれた論理式ではなくこの截断を引き継ぐことになる。モジュール DefOf は内側の充足関係とその小ささの事実を運び、指示対象はこれらから組み立てられる。
open import V.Coding {ℓ} using ( pr; module VCode ) open import V.Model {ℓ} using ( self∈sucV ) open import L.Constructible {ℓ} using ( Lset; Lset-mono; 𝒟ₒ; 𝒟ₒ-inv ) open import L.Definability {ℓ} using ( module DefOf )
第一の鍵には、既に順序が届く居場所が必要である。この言語の数項、すなわち von Neumann 自然数は L の中の順序数であり、各数項はその一段上の段階に属する。段階の要素どうしの対は、さらに二段先に現れる。極限段階 Lset ω は、何らかの有限段階までに現れたものを集め、Limit はその要素に所属の証明書を添えたものである。この段階の上で limitOrder がすべてを整列し、Tri-map は同値に沿って三分の判定を輸送する。この道具は第三の鍵の三分で再利用される。
open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω ) open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc ) open import L.Axioms.Basic {ℓ} using ( pr∈Lset-suc ) open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; inSome; limitOrder; Tri-map ) open import L.WellOrder.Base {ℓ-suc ℓ}
順序の抽象概念は、レコードとしてまとめられた狭義整列順序である。狭義の比較、三分性、非反射性、推移性、整礎性に加え、そのようなレコードを用いる最小要素探索 leastOf をともなう。名前が満たすと示されるのは、まさにこの四つの法則である。型理論の側で読み込まれる道具は、名前の論理式とパラメータ列がアリティを指数にもつことから生じる依存型における等式の処理を扱う。依存対へのパスの構成、パスに沿った置換と定数関数の交換、同値の両方向、そして埋め込みから取り出す単射性である。
using ( Tri; lt; eq; gt; SWO; IsLeast; leastOf ) open import Cubical.Foundations.Prelude using ( toPathP ) open import Cubical.Foundations.Transport using ( constSubstCommSlice ) open import Cubical.Foundations.Equiv using ( equivFun; invEq ) open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
自然数はアリティを供給し、自然数上の順序は中間の鍵を供給する。ここでのその三分は決定可能なので、名前の比較は arity a ≟ arity b の上で直接分岐できる。_<_ の推移性と整礎性は対応する法則に入る。⇔toPath は命題的な同値条件の証明をパスへ変えるもので、これにより指示対象の所属の特徴づけは、二つの含意ではなく命題の等式として述べられる。toℕ は有界な添字を通常の数項として読む。
open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Data.Nat using ( _+_; +-comm ) open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ ) import Cubical.Data.Nat.Order as NatOrder open import Cubical.Data.FinData using ( toℕ )
辞書式比較は和型として書かれる。各鍵の判定は「狭義に前」か「等しい」かのいずれかであり、等しい場合は次の鍵が決める。したがって本章には、構成子つきの二項和、map をもつパラメータ列、そして整礎帰納の道具一式が要る。Acc は要素からの任意の狭義降下が終わることを表し、acc がその証明を包み、WFI がそれを帰納原理に変える。ここでの列は長さを指数にもつ。まさにそれが、後で扱うアリティの輸送の問題を強いるのである。
open import Cubical.Data.Sigma using ( ΣPathP ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Data.Vec using ( map ) open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded; module WFI )
二つの消去の帰結となる型は、数学そのものによって固定されている。空型の消去子は、定数を含むパラメータなし論理式といった不可能な場合を片付ける。命題的截断は、選ばれた証拠を単なる存在主張へ変える。A が居住者をもてば ∥ A ∥₁ ももつが、その消去は命題値の帰結に限られる。累積的集合の階層は、小さな指数型から組み立てられる集合 sett と、小さな型の要素を宇宙の要素とみなす埋め込み ⟪_⟫ を供給する。
import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett ) open import Cubical.HITs.CumulativeHierarchy.Properties
最後のグループは、名前が読まれる具体的な解釈を固定する。# は自然数を宇宙の中の対応する数項へ変え、ω は無限集合である。したがって極限段階で用いた種類の数項の所属証明書が作れる。ここで使う真理値と結合子は、hProp (ℓ-suc ℓ) 上の論理演算から直接得られ、構造 𝒮ᵥ のもとで ZFStructure の意味論を開けば、論理式が V の中で何を意味するかが定まる。以下のすべての充足判断はこの内側の判断であり、名前の指示対象を定義可能冪集合自身の定義可能性の概念に結びつけるのはこれである。
using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; ω )
最後の宣言群は章全体で用いる解釈を固定する。論理式は V 上の集合論的構造で読み、真理値は命題とする。
open hPropStructure 𝒮ᵥ
パラメータなしコードは遺伝的有限である
名前の第一の鍵は、パラメータなし論理式のコードである。この有限な構文コードは遺伝的有限なので、既に極限段階に属し、そこで構成済みの整列順序によって比較できる。
第一の鍵は、論理式を Lset ω の要素として扱う。そこでまず示すべきは、そのコードがそうであるということだ。V.Coding の符号化の節々を読めば、使われているのはこれだけである。タグのための数項、de Bruijn 番号のための数項、そして各部分を包む Kuratowski 対。有穷の世界から出てしまうおそれのある構成は定数の節だけだが、それは任意の集合をコードに入れるものであり、パラメータなし論理式には定数がそもそもない。
そこで必要なのは二つの閉包性の事実だけで、どちらも再証明せず既存の結果を引き上げて使う。L.Choice.FiniteStageOrders の inSome は、Lset ω の要素が有限段階の中には現れていることを言い、L.Axioms.Basic の pr∈Lset-suc は、一つの段階の二つの要素の Kuratowski 対が二段階後に現れることを言う。ある有限段階から後の段階へ進むのは、数項の後者に沿って単調性を適用することであり、これがこの節で唯一の再帰である。
極限段階への所属の証明書は、要素が有限段階のどこかにあるとしか言わないので、直接使うには扱いにくい。補助の述語 AtStage は、どの有限段階かを記録する。自然数 k と、その要素が Lset (# k) に属する証明の組である。要素を一つの段階に固定してしまえば、raiseTo はその証明書を前へ進められる。段階 # k から段階 # (d + k) へ、d についての再帰で進む。各後者の段階で、self∈sucV によりその段階がそれを限定する数項を含むことが観察され、Lset-mono がそれを段階の単調性に変える。
private AtStage : S → Type (ℓ-suc ℓ) AtStage x = Σ[ k ∈ ℕ ] ⟨ x ∈ˢ Lset (# k) ⟩ raiseTo : (x : S) (d k : ℕ) → ⟨ x ∈ˢ Lset (# k) ⟩ → ⟨ x ∈ˢ Lset (# (d + k)) ⟩ raiseTo x zero k h = h
数項はこの議論の原子なので、その配置から始めます。numeral-ord により # k は L の順序数であり、ord∈Lset-suc はそれを自身の段階の後者に置きます。#∈ω は境界となる数項が ω に属することを述べるので、単調性によってその数項を極限段階へ持ち上げられます。対に関する閉性は、x と y がともに極限段階にあれば pr x y もそこにあると述べ、複合構文の符号化に必要な事実を与えます。
raiseTo x (suc d) k h = Lset-mono (self∈sucV (# (d + k))) (raiseTo x d k h) numeral∈limit : (k : ℕ) → ⟨ (# k) ∈ˢ Lset ω ⟩ numeral∈limit k = Lset-mono (#∈ω (suc k)) (ord∈Lset-suc (# k) (numeral-ord k)) pr∈limit : (x y : S) → ⟨ x ∈ˢ Lset ω ⟩ → ⟨ y ∈ˢ Lset ω ⟩ → ⟨ pr x y ∈ˢ Lset ω ⟩
対の主張の証明には一つ折り返し点がある。inSome が渡す段階の証人は命題的截断の中にあるため、その段階の番号をデータとして取り出すことはできない。しかし帰結は所属の命題であり、截断された証人は命題値の帰結へは消去できる。外側の PT.rec が x の証人をほどき、内側のものが y の証人をほどき、両方を実際の作業をする補題 both に渡す。
pr∈limit x y hx hy = PT.rec (snd (pr x y ∈ˢ Lset ω)) (λ atX → PT.rec (snd (pr x y ∈ˢ Lset ω)) (both atX) (inSome y hy)) (inSome x hx) where both : AtStage x → AtStage y → ⟨ pr x y ∈ˢ Lset ω ⟩
x の段階の番号を j、y のそれを k とすると、まず二つの要素を共通の段階 # (k + j) へ持ち上げて pr∈Lset-suc が適用できるようにし、その対を二段階後、ω において # (suc (suc (k + j))) の下に置く。共通段階の被加数は逆順に現れるので、+-comm に沿った一回の置換がこれを正す。数項と対が極限段階で閉じている以上、タグ付きコードも、それは数項と中身の対にすぎないが、tag∈limit により閉じている。この三つの事実が、これから行う構文の帰納の負担のすべてである。
both (j , hj) (k , hk) = Lset-mono (#∈ω (suc (suc (k + j)))) (pr∈Lset-suc (# (k + j)) x y (raiseTo x k j hj) (subst (λ n → ⟨ y ∈ˢ Lset (# n) ⟩) (+-comm j k) (raiseTo y j k hk))) tag∈limit : (k : ℕ) (x : S) → ⟨ x ∈ˢ Lset ω ⟩ → ⟨ VCode.mkTag k x ∈ˢ Lset ω ⟩ tag∈limit k x h = pr∈limit (# k) x (numeral∈limit k) h
数項、対、タグが揃えば、すべてのパラメータなしコードの配置は構文上の構造的帰納で従う。この帰納が短いのは、先の三つの閉包性の事実がすべての仕事を担うからである。各構成子の場合はそれらを組み立て直すだけであり、有穷の世界から逃げ出しうる唯一の場合である定数の場合は、定数領域が空型であるため空である。タグの数字は全体を通してリテラルとして現れるが、その値について使われるのは、数項であるという以上のことではない。
まず項を扱う。その帰納は二つの節からなる。変数は定数の内容をもたないので、そのコードは de Bruijn 番号の数項をタグ 1 で包んだものであり、tag∈limit が直ちに適用される。パラメータなし項の定数の節は矛盾である。定数領域 ⊥* には要素がないので、不可能な場合は空型の消去子で片付く。述語の中の mapTm は、パラメータなし項を作業用の構文へ埋め込む操作で、定数をホストの値に置き換える。⊥* の上では置き換えるものは何もない。
codeTm∈limit : ∀ {n} (t : Term (⊥* {ℓ}) n) → ⟨ VCode.⌜ mapTm Empty.rec* t ⌝ᵗ ∈ˢ Lset ω ⟩ codeTm∈limit (con c) = Empty.rec* c codeTm∈limit (var i) = tag∈limit 1 (# (toℕ i)) (numeral∈limit (toℕ i)) code∈limit : ∀ {n} (χ : Formula (⊥* {ℓ}) n) → ⟨ VCode.⌜ embed χ ⌝ ∈ˢ Lset ω ⟩
論理式は同じ形をたどり、構成子ごとに一つのタグをもつ。二項の各節は、直下の二つの部分論理式または部分項のコードを一つのタグのもとで対にし、結合子と量化子の節は単一の部分コードを包み、偽は零の裸の数項である。いずれの場合も帰結は、帰納の仮定に対する tag∈limit か pr∈limit の一回の適用であり、だから各節の本体は一行である。
code∈limit (t ∈̇ u) = tag∈limit 0 _ (pr∈limit _ _ (codeTm∈limit t) (codeTm∈limit u)) code∈limit (t ≐ u) = tag∈limit 1 _ (pr∈limit _ _ (codeTm∈limit t) (codeTm∈limit u)) code∈limit (φ ∧̇ ψ) = tag∈limit 2 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ)) code∈limit (φ ∨̇ ψ) = tag∈limit 3 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ)) code∈limit (φ ⇒̇ ψ) = tag∈limit 4 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ))
最後の四つの節は量化子とその有界形式を覆い、タグは 6 から 9 までである。有界形式はさらに、範囲を定める項のコードを対に加える。この章にとって重要なのは帰結だけである。すべてのパラメータなし論理式は極限段階に居座るコードをもち、その段階が既にもつ順序で比較できる。タグの番号付けは任意の簿記であり、数学的主張の一部ではない。
code∈limit ⊥̇ = tag∈limit 5 _ (numeral∈limit 0) code∈limit (∃̇ φ) = tag∈limit 6 _ (code∈limit φ) code∈limit (∀̇ φ) = tag∈limit 7 _ (code∈limit φ) code∈limit (∀̇∈ t φ) = tag∈limit 8 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ)) code∈limit (∃̇∈ t φ) = tag∈limit 9 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ))
極限段階の要素は所属の証明書をともなう。それゆえ第一の鍵は裸のコードではなく、コードとその証明書を合わせたものである。この小節は両者をまとめ、比較に必要となる、アリティの等式に沿う輸送についての補助事実を一つ記録する。
limitCode は、パラメータなし論理式を、そのコードと今作った所属証明の対へ送る。この対はまさに Limit の要素であり、極限段階の順序が作用する対象である。二番目の主張は依存的な構文の微妙さに関わる。論理式の型はそのアリティに言及するので、二つの名前のアリティが等しいと判明した後、一方の論理式はその等式に沿って置換しなければ、他方と比較することさえできない。code-shift は、この置換がコードには見えないことを言う。アリティ suc i の論理式をパス i ≡ j に沿って輸送しても、同じコードをもつ論理式が得られる。
limitCode : ∀ {n} → Formula (⊥* {ℓ}) n → Limit limitCode χ = VCode.⌜ embed χ ⌝ , code∈limit χ code-shift : {i j : ℕ} (e : i ≡ j) (χ : Formula (⊥* {ℓ}) (suc i)) → VCode.⌜ embed (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e χ) ⌝ ≡ VCode.⌜ embed χ ⌝
証明は、帰結の型が指数に依存しない関数はその指数に沿う置換と可換だという一般事実を用いる。論理式の符号化は、論理式がどのアリティに居ようと、固定された型 S に落ちる。それゆえ constSubstCommSlice により、輸送された論理式のコードは元のものと等しい。主張は sym で、置換された論理式から元の論理式へと読める方向に並べてある。
code-shift e χ = sym (constSubstCommSlice (λ k → Formula (⊥* {ℓ}) (suc k)) S (λ _ ψ → VCode.⌜ embed ψ ⌝) e χ)
パラメータなし論理式はその像から復元できる
同じアリティでは、符号化は異なる二つのパラメータなし論理式を同一視しない。遺伝的有限な像を復号し、構文の符号化の単射性を使えば、この単射性が得られる。
コードとアリティがともに等しい二つの名前は、同じ論理式から作られていなければならない。さもなければ比較は、互いに小さくもなく何とも等しくもないと、異なる二つの名前を判定してしまう。V.Coding はそれ自身の単射性を証明しているが、それは作業用の構文、すなわち定数域が台である構文の上でのことだった。ここで必要なのは、embed を通してその構文に届くパラメータなし論理式についての単射性である。
この隙間は逆向きに走る抹消で埋められる。パラメータなし論理式の上での左逆であれば足りるのだから、抹消は粗雑で構わない。定数は番号零の変数へ送られる。そのスロットは常にあり、扱う論理式はどれも少なくとも一つの自由変数スロットをもつからである。他の各節は構成子の上での恒等写像である。もともと定数を含まない論理式には、抹消は節ごとに何も変えない。すると単射性は、三つのパスの合成になる。
項の抹消が、唯一の創造的な仕事をする。作業用の構文では任意の集合を値にもつ定数は、番号零の変数に置き換えられる。変数はそのまま残る。これが正当なのは、帰結がアリティ suc n の論理式に制限されているからで、だからこそ零番のスロットが常に存在する。論理式の抹消はその後、同型的に宣言される。各構成子を自身へ写し、部分には抹消を施す。
private eraseTm : ∀ {n} → Term S (suc n) → Term (⊥* {ℓ}) (suc n) eraseTm (con x) = var zero eraseTm (var i) = var i eraseFo : ∀ {n} → Formula S (suc n) → Formula (⊥* {ℓ}) (suc n)
最初の五つの節は、原子論理式と命題結合子を覆う。二つの原子関係は項の実引数に抹消を施し、三つの二項結合子は両方の部分論理式に再帰する。ここで起きるのは、抹消を構成子を通して分配することだけで、定数の情報はすでに項の水準で捨てられている。
eraseFo (t ∈̇ u) = eraseTm t ∈̇ eraseTm u eraseFo (t ≐ u) = eraseTm t ≐ eraseTm u eraseFo (φ ∧̇ ψ) = eraseFo φ ∧̇ eraseFo ψ eraseFo (φ ∨̇ ψ) = eraseFo φ ∨̇ eraseFo ψ eraseFo (φ ⇒̇ ψ) = eraseFo φ ⇒̇ eraseFo ψ
残りの五つの節は文字どおりの恒等である。偽は部分をもたず、各量化子は抹消された本体を包んで自身を組み立て直す。どの節も強制されており、論理式の抹消のされ方に選択の余地はない。これが、このあとの左逆の計算を予測可能にしている。
eraseFo ⊥̇ = ⊥̇ eraseFo (∃̇ φ) = ∃̇ eraseFo φ eraseFo (∀̇ φ) = ∀̇ eraseFo φ eraseFo (∀̇∈ t φ) = ∀̇∈ (eraseTm t) (eraseFo φ) eraseFo (∃̇∈ t φ) = ∃̇∈ (eraseTm t) (eraseFo φ)
左逆の性質は、一段ずつ述べられ、一段ずつ証明される。項については、mapTm Empty.rec* の後で eraseTm を施すと元の項が返る。定数の場合は、パラメータなし項には定数がないので空であり、変数の場合は、どちらの合成も同じ変数を組み立て直すので refl である。論理式の水準の主張はその次に、パラメータなし論理式の埋め込みを抹消すれば、パスをひとつ添えて元の論理式が返る、と述べる。
eraseTm-embed : ∀ {n} (t : Term (⊥* {ℓ}) (suc n)) → eraseTm (mapTm Empty.rec* t) ≡ t eraseTm-embed (con c) = Empty.rec* c eraseTm-embed (var i) = refl eraseFo-embed : ∀ {n} (χ : Formula (⊥* {ℓ}) (suc n)) → eraseFo (embed χ) ≡ χ
証明は論理式についての帰納で進み、項が現れるところでは項の水準の事実を再利用する。原子と二項結合子の節は、二つの再帰結果に二項の同余 cong₂ を適用し、部分のパスから合成物のパスを組み立てる。
eraseFo-embed (t ∈̇ u) = cong₂ _∈̇_ (eraseTm-embed t) (eraseTm-embed u) eraseFo-embed (t ≐ u) = cong₂ _≐_ (eraseTm-embed t) (eraseTm-embed u) eraseFo-embed (φ ∧̇ ψ) = cong₂ _∧̇_ (eraseFo-embed φ) (eraseFo-embed ψ) eraseFo-embed (φ ∨̇ ψ) = cong₂ _∨̇_ (eraseFo-embed φ) (eraseFo-embed ψ) eraseFo-embed (φ ⇒̇ ψ) = cong₂ _⇒̇_ (eraseFo-embed φ) (eraseFo-embed ψ)
偽には refl が要るだけである。そこには何も埋め込まれていないからである。四つの量化子の節は一項の同余を適用し、有界形式は項も運ぶので cong₂ を使う。これで、すべてのパラメータなし論理式に、抹消された像から自身へ戻る明示的なパスが備わった。
eraseFo-embed ⊥̇ = refl eraseFo-embed (∃̇ φ) = cong ∃̇_ (eraseFo-embed φ) eraseFo-embed (∀̇ φ) = cong ∀̇_ (eraseFo-embed φ) eraseFo-embed (∀̇∈ t φ) = cong₂ ∀̇∈ (eraseTm-embed t) (eraseFo-embed φ) eraseFo-embed (∃̇∈ t φ) = cong₂ ∃̇∈ (eraseTm-embed t) (eraseFo-embed φ)
単射性は今や一つの文である。同じアリティの二つのパラメータなし論理式について、埋め込まれたコードが一致すると仮定する。符号化自身の単射性がそれを、埋め込まれた論理式どうしの等式に変える。両辺に抹消を施しても等式は保たれる。抹消は関数だからである。そして左逆のパスが、両辺を元の論理式へと帰着させる。合成されたパスが求める χ ≡ ψ であり、したがって、固定したアリティでは、異なる二つのパラメータなし論理式のコードは等しくならない。
code-inj : ∀ {n} (χ ψ : Formula (⊥* {ℓ}) (suc n)) → VCode.⌜ embed χ ⌝ ≡ VCode.⌜ embed ψ ⌝ → χ ≡ ψ code-inj χ ψ e = sym (eraseFo-embed χ) ∙ cong eraseFo (VCode.⌜⌝-inj (embed χ) (embed ψ) e) ∙ eraseFo-embed ψ
名前を構成するデータ
名前は、アリティ、一つの出力変数を余分にもつパラメータなし論理式、そのアリティのパラメータ列を記録する。その指示対象は、この環境で論理式が段階から切り出す部分集合である。
本章の残りの部分はすべて、一つの集合 A、すなわち名前が書かれる段階と、その段階の要素の上の一つの狭義整列順序とに相対的である。そこで作業はモジュール Naming A w の中で進む。名前とは、アリティ、それより一つ多い自由変数スロットをもつパラメータなし論理式、そして A の小さな要素型から取った、その個数のパラメータの列である。余分なスロットが部分集合を切り出すためのものであり、残りのスロットがパラメータを受け取る。第一の鍵は論理式から直ちに読み取れる。
モジュールは、段階 A と、決定的に重要なことにその要素の上の狭義整列順序とをパラメータとして取る。第三の鍵がパラメータをその順序で比較するのであり、任意の段階の上に順序を作るのはこの章の仕事ではないからである。型 Name は依存的な三つ組である。自然数 k、suc k 個の自由変数スロットをもつパラメータなし論理式、そして A の台の k 個の要素の列。列の長さはアリティに強制されるので、名前が公式と誤った個数のパラメータを組にすることはない。
module Naming (A : S) (w : SWO ⟪ A ⟫) where module DA = DefOf A open DA using ( _⊨ᵐ_ ) Name : Type ℓ Name = Σ[ k ∈ ℕ ] (Formula (⊥* {ℓ}) (suc k) × Vec ⟪ A ⟫ k)
射たちは三つの鍵の出所に名前を与える。arity はその数を返し、formula はちょうど一つ多い変数スロットをもつパラメータなし論理式を、params は列を返す。それらの型は名前そのものに依存する。だから formula a はアリティ suc (arity a) に、params a は arity a に住む。この依存性こそ、のちの比較における輸送の問題すべての出所である。
arity : Name → ℕ arity a = a .fst formula : (a : Name) → Formula (⊥* {ℓ}) (suc (arity a)) formula a = a .snd .fst params : (a : Name) → Vec ⟪ A ⟫ (arity a)
第一の鍵もまた射である。codeOf は論理式に limitCode を適用し、そのコードを極限段階での所属証明書とともに届ける。limitOrder が比較できるように。
params a = a .snd .snd codeOf : Name → Limit codeOf a = limitCode (formula a)
名前の指示対象とは、パラメータが環境として与えられたとき、その論理式が選び出す A の部分集合です。その並びはパラメータ抽象化定理が要求する順序です。環境は一つの要素とそれに続くパラメータ列からなり、すべて定義可能冪集合自身の定数解釈によって制限された台へ読み込まれ、充足は内側のものを取ります。したがって指示対象は、Def A を定義したのと同じ概念によって A から切り出された部分集合です。小ささはそのまま引き継がれます。任意の論理式と任意の環境における内側の充足は小さいので、この部分集合は小さな索引型の上の sett となり、レベルの引き下げの費用は一切かかりません。
述語によって A から切り出される部分集合は直接提示できます。subsetOf は A の小さな要素型の上の命題族を受け取り、索引型を「要素 m と、その m で述語が成り立つ証明」の依存対とし、その対を集合 ⟪ A ⟫↪ m へ送る sett を組み立てます。したがって索引とは証人とその証明書の対であり、結果の集合への所属はそのような対が「だけ」存在することを要求します。これは defSet と同じ形なので、どちらの形で書いた述語も同じ種類の対象を提示します。
private module SemM = FOL.Semantics DA.𝒮M open SemM using ( _^_ ) subsetOf : (⟪ A ⟫ → hProp ℓ) → S subsetOf P = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ P m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))
指示対象そのものの前に、提示上の二つの細部を確かめます。補題 ⟪⟫↪-inj は、写像 ⟪ A ⟫↪ が埋め込みであること、つまりその値の間の経路が根底の添字の間の経路から来ることを記録します。これにより m' ≡ m が復元され、所属の仕様の順方向を閉じるのに使われます。環境はその後組み立てられます。自由変数を担う要素 m に対し、環境は DA.ι m に DA.ι で復号したパラメータ列を続けたものです。先頭の項が部分集合を切り出す一つの余分なスロットを埋め、残りの項がパラメータのスロットを埋めます。環境の長さは定義上 suc (arity a) であり、名前の論理式のアリティとちょうど一致します。
⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m
environment : (a : Name) → ⟪ A ⟫ → DA.SM ^ (suc (arity a))
environment a m = DA.ι m ∷ map DA.ι (params a)
satAt : (a : Name) → ⟪ A ⟫ → hProp ℓ
名前の指示対象を定める述語は satAt a m です。これは、埋め込まれた論理式が組み立てた環境で内側の充足を受けるという命題と同値な小さな命題です。これを subsetOf に通すと、denote a は階層の集合となり、内側の意味論が A から選んだ部分集合になります。ここで新たなサイズの決定は一切行われません。小ささは ⊨ᵐ-small を通じて一度だけ入り、sett の索引型に費やされるのです。
satAt a m = DA.⊨ᵐ-small (embed (formula a)) (environment a m) .fst denote : Name → S denote a = subsetOf (satAt a)
この仕様は「指示する」という語を文字どおりに述べます。A の要素がその指示対象に属するのは、内側の世界が名前の定める環境でその論理式を充足するとき、そしてそのときに限ります。小さな命題への圧縮は符号化にすぎず、同値がそれを元に戻します。
この定理は命題としての経路であり、defSet-mem が述べられたのと同じ形をしています。二つの含意から ⇔toPath によって証明されます。補助定義 decode は satAt a m を ⊨ᵐ-small が返す完全な対へ展開し直し、両方向がその第二成分の同値、つまり小さな命題と内側の充足の命題を結ぶ同値を使えるようにします。
denote-mem : (a : Name) (m : ⟪ A ⟫) → (⟪ A ⟫↪ m ∈ˢ denote a) ≡ (environment a m ⊨ᵐ embed (formula a)) denote-mem a m = ⇔toPath fwd bwd where decode = DA.⊨ᵐ-small (embed (formula a)) (environment a m)
sett への所属は添字の存在を切り捨てた形で与えるので、順方向は切断を命題へ消去し、索引 (m' , h) と ⟪ A ⟫↪ m' から ⟪ A ⟫↪ m への経路 q を得ます。埋め込みの単射性が q を m' ≡ m に変え、それに沿って h を輸送すれば satAt a m の証明が得られ、decode の同値がその証明を充足の命題へ変換します。各段階は命題しか要らない場所で証明を費やすだけで、証人が選ばれることはありません。
fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩ → ⟨ environment a m ⊨ᵐ embed (formula a) ⟩ fwd = PT.rec (snd (environment a m ⊨ᵐ embed (formula a))) (λ { ((m' , h) , q) → invEq (decode .snd) (subst (λ v → ⟨ satAt a v ⟩) (⟪⟫↪-inj q) h) }) bwd : ⟨ environment a m ⊨ᵐ embed (formula a) ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩
逆方向は同じ同値を逆向きに走らせます。充足の証明が satAt a m の証明に変わり、それを自明な経路とともに索引 (m , 証明) として ∣_∣₁ で切断します。両方向を合わせると、所属と内側の充足は余りなく同一視され、これが「指示する」という語に求められた意味です。
bwd h = ∣ (m , equivFun (decode .snd) h) , refl ∣₁
後者段階の各要素は名前をもつ
定義可能冪集合の仕様は、後続段階の各要素に定数付き論理式を与える。その定数を抽象すると、名前を構成するパラメータなし論理式とパラメータ列が得られる。
𝒟ₒ A の要素は、その演算子自身の仕様によれば、A の定数を用いた一自由変数の論理式で定義される部分集合にすぎません。パラメータ抽象化は、その論理式をより高いアリティのパラメータなし論理式へ変換し、そこに現れる定数の列を与えます。後者を前者から読み出すこと、それが名付けのすべてであり、しかもそれは関数です。
関数 nameOf は三つの鍵を一度に組み立てます。countFo φ は定数の出現を一つずつ数えてアリティを与え、したがって抽象 absFo φ は 1 + countFo φ 個の自由スロット、つまりアリティの後続数のところに住みます。constantsFo φ は同じ順序で定数を並べ、⟪ A ⟫ の中のちょうどその長さの列です。nameOf が受け取るのは定数付きの論理式であって、名前のパラメータなし成分ではないことに注意してください。抽象化は定義の内部で、構成子ごとに一つの節として行われます。
nameOf : Formula ⟪ A ⟫ 1 → Name nameOf φ = countFo φ , (absFo φ , constantsFo φ)
その妥当性はパラメータ抽象化定理 ⊨-abs₁ から従い、その前に空の定数領域に対する二つの解釈を同一視します。パラメータなし論理式には二つの読み方が現れるので、まず両者を同一視しなければなりません。名前の指示対象は embed を通して定数域 ⟪ A ⟫ の中で式を読み、一方抽象化の定理は空の定数域で読みます。二つの解釈は空型から出る関数なので一致し、この一致を述べることが同一視に必要な検証のすべてです。
抽象化の定理 ⊨-abs₁ は空の定数域の上での充足を語り、一方名前の意味論は ⟪ A ⟫ の上の充足を読みます。二つの命題を項ごとに比べるため、emptySat は任意の定数解釈 f : ⊥* → DA.SM における充足の命題の形を固定し、f の変更を関数の関数への適用の問題にします。論理式そのものは定数を一切言及しないので、この一様性が使えるのです。
private emptySat : (f : ⊥* {ℓ} → DA.SM) {n : ℕ} → DA.SM ^ n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ) emptySat f γ χ = γ ⊨ᶠ χ where open SemM.At (⊥* {ℓ}) f using () renaming ( _⊨_ to _⊨ᶠ_ )
パラメータなし論理式の二つの定数解釈は、どちらも型 ⊥* → DA.SM をもちます。作業用の意味論が使う方、すべての定数を DA.ι (Empty.rec* b) へ送るものと、消去子 Empty.rec* 自身です。⊥* には要素がないので、funExt と消去子だけで二つの関数の相等 sameReading が証明され、何も検査する必要がありません。そして absSat は、指示対象が embed を通して使う環境の読み方と、抽象化の定理が使う空定数域の読み方が、同じ要素 m と同じ抽象化された論理式において一致することを述べます。
sameReading : (λ (b : ⊥* {ℓ}) → DA.ι (Empty.rec* b)) ≡ Empty.rec*
sameReading = funExt (λ b → Empty.rec* b)
absSat : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
→ (environment (nameOf φ) m ⊨ᵐ embed (formula (nameOf φ)))
≡ ((DA.ι m ∷ []) ⊨ᵐ φ)
証明は三段の経路です。改名の補題 embed-⊨ は、パラメータなし論理式をより豊かな定数域へ埋め込んでもその意味は変わらないと言い、これが左辺を Empty.rec* の標識の読み方へ移します。次に sameReading が指示対象自身の読み方をそこへ代入します。最後に ⊨-abs₁ を逆向きに読むと、抽象化された論理式の単一パラメータにおける充足と元の論理式の充足とを同一視する抽象化の定理そのものです。各段階は前の章の定理をつなぐだけで、再証明はしません。
absSat φ m = embed-⊨ DA.𝒮M DA.ι (absFo φ) (environment (nameOf φ) m) ∙ cong (λ f → emptySat f (environment (nameOf φ) m) (absFo φ)) sameReading ∙ sym (⊨-abs₁ DA.𝒮M DA.ι φ (DA.ι m))
二つの読み方を命題の面で同一視したうえで、satAt-abs はこの同一視を充足の命題から、集合が構成される小さな命題へ引き上げます。比較するのは、名前の指示対象の根底にある小さな命題 satAt (nameOf φ) m と、defSet φ の根底にある小さな命題 DA.smallSat φ m です。補助名 big と small がそれぞれの ⊨ᵐ-small の対を展開し、どちらの方向も二つの同値を使えるようにします。
satAt-abs : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
→ satAt (nameOf φ) m ≡ DA.smallSat φ m
satAt-abs φ m = ⇔toPath fwd bwd
where
big = DA.⊨ᵐ-small (embed (formula (nameOf φ))) (environment (nameOf φ) m)
順方向は三つの変換を証明に施して合成します。まず大きい方の同値を逆向きに走らせて埋め込まれた充足の命題に達し、経路 absSat φ m に沿って証明を空定数域の命題へ輸送し、それから小さい方の同値を順方向に走らせて DA.smallSat φ m に達します。経路 absSat φ m が二つの充足型を同一視するので、通常の輸送によって証明を必要な向きへ移せます。命題性は充足型を hProp としてまとめるために使われ、輸送そのものが必要とするのはこの経路です。
small = DA.⊨ᵐ-small φ (DA.ι m ∷ []) fwd : ⟨ satAt (nameOf φ) m ⟩ → ⟨ DA.smallSat φ m ⟩ fwd h = equivFun (small .snd) (subst ⟨_⟩ (absSat φ m) (invEq (big .snd) h)) bwd : ⟨ DA.smallSat φ m ⟩ → ⟨ satAt (nameOf φ) m ⟩ bwd h = equivFun (big .snd)
逆方向は同じ合成で経路を逆向きにしたものです。sym (absSat φ m) が証明を逆方向へ動かし、二つの同値も逆の順序で適用されます。ここで新たに証明されるものはありません。要点は、すべての m に対して satAt (nameOf φ) m と DA.smallSat φ m が同じ小さな命題であることであり、これが次の段階で二つの集合を等しくするのです。
(subst ⟨_⟩ (sym (absSat φ m)) (invEq (small .snd) h))
どちらの部分集合も、その要素の上の小さな述語によって A から切り出されています。したがって二つの述語が等しければ、二つの集合は合同によって等しく、外延性を持ち出す必要はありません。完全性はその等式に沿って輸送すれば得られ、命題的に切り詰めた形で述べられます。定義可能冪集合が論理式を与える仕方がもともとそうだからです。
等式 denote-defSet は、述語の一致 satAt-abs を集合の等式に変えたものです。funExt が点ごとの等しさを述語族の等しさにまとめ、cong subsetOf がそれを提示された集合へ運びます。完全性は証明書 h : ⟨ x ∈ˢ 𝒟ₒ A ⟩ を 𝒟ₒ-inv で反転することから始まります。これは defSet φ ≡ x を満たす論理式 φ を「だけ」与えるものであり、したがって結論も名前と等式の存在を切り詰めた形であり、選ばれた名前ではありません。
denote-defSet : (φ : Formula ⟪ A ⟫ 1) → denote (nameOf φ) ≡ DA.defSet φ denote-defSet φ = cong subsetOf (funExt (satAt-abs φ)) names-complete : (x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩ → ∥ Σ[ a ∈ Name ] (denote a ≡ x) ∥₁ names-complete x h = PT.map named (𝒟ₒ-inv A x h)
切断の内側では、反転されたデータから求める対への段階は普通のものです。論理式 φ は nameOf φ によって名付けられ、必要な等式は denote-defSet φ ∙ q、つまり名前の指示対象から defSet φ への経路に、与えられた x への経路を続けたものです。目標の ∥ Σ[ a ∈ Name ] (denote a ≡ x) ∥₁ は命題なので、PT.map は切断の下で働き、ただ与えられた論理式をただ与えられた名前へ写します。それがどの論理式かを検査することは一切ありません。
where named : Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DA.defSet φ ≡ x) → Σ[ a ∈ Name ] (denote a ≡ x) named (φ , q) = nameOf φ , (denote-defSet φ ∙ q)
パラメータ列上の順序
パラメータ列は A の要素に与えられた整列順序によって辞書式に比較します。この関係は異なる二つの長さを受け取り、一方が先に尽きる場合には先行元を持たず、両方が空でなければ先頭を比較し、先頭が等しいときだけ尾へ進みます。この形により、三つの列の実際の長さのまま推移性を使えます。三分性は後で、アリティの経路に沿って一方を他方の長さへ輸送してから適用します。
ここでは二つの整列順序が働いており、どちらも短い名前で一度に固定されます。極限段階の順序 limitOrder は論理式コードを比較し、_≺_ と改名されます。モジュールパラメータ w、つまり A の要素の上の整列順序はパラメータを比較し、_≺ₚ_ と改名されます。各 open は三分性・非反射性・推移性・整礎性の法則も改名するので、これからの証明はどちらの順序の法則も長い修飾名なしに呼び出せます。
open SWO limitOrder using () renaming ( _<∙_ to _≺_ ; tri∙ to ≺-tri ; irr∙ to ≺-irr ; trans∙ to ≺-trans ; wf∙ to ≺-wf ) open SWO w using () renaming ( _<∙_ to _≺ₚ_ ; tri∙ to ≺ₚ-tri ; irr∙ to ≺ₚ-irr
比較そのものは両ベクトルのパターン照合で定義され、長さ j と k で添字づけられます。どちらかの列が空なら、それ以上の降下は不可能で、結果の型は空型になります。使い尽くされた列の下にはどの位置にも何もないのです。これらの場合は費用がゼロで、反証できるという事実こそ、推移性と非反射性の証明で使われるものです。
; trans∙ to ≺ₚ-trans ; wf∙ to ≺ₚ-wf ) infix 20 _≺ᵥ_ _≺ᵥ_ : ∀ {j k} → Vec ⟪ A ⟫ j → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ) [] ≺ᵥ [] = ⊥* [] ≺ᵥ (y ∷ q) = ⊥*
二つの空でない列は先頭で比較されます。先頭 x がパラメータ順序で y より下に落ちるか、先頭同士が経路として等しく、降下が尾へ続くかのどちらかです。狭義の場合が和の左の支、等しい先頭の場合が右の支なので、後の証明はどの位置が先に判定したかで場合分けできます。先頭の相等は経路 x ≡ y であり、推移性の混在する場合はこれを比較の中へ代入することになります。
(x ∷ p) ≺ᵥ [] = ⊥* (x ∷ p) ≺ᵥ (y ∷ q) = (x ≺ₚ y) ⊎ ((x ≡ y) × (p ≺ᵥ q))
四つの法則のうち三つはそのままの帰納法で得られます。非反射性と三分性は長さが等しいことを要求します。列がある列と等しくなりうるのはそこでだけだからです。推移性はそれを要求せず、三つの異なる長さの列を受け取り、すべての列が空でない場合を除くすべての場合が空型によって反証されます。
非反射性はベクトルに関する帰納法で証明されます。ベクトルが自分自身より下になることは決してありません。p ≺ᵥ p は二つの出現が同じ長さをもつことを要求するので、この命題は単一の長さでのみ意味をもち、帰納法は一段短い長さでの命題を尾に対して消費します。続いて推移性の命題が続きます。こちらは三つの長さに対して一度に述べられます。
≺ᵥ-irr : ∀ {k} (p : Vec ⟪ A ⟫ k) → p ≺ᵥ p → Empty.⊥ ≺ᵥ-irr [] h = Empty.rec* h ≺ᵥ-irr (x ∷ p) (inl h) = ≺ₚ-irr x h ≺ᵥ-irr (x ∷ p) (inr (_ , h)) = ≺ᵥ-irr p h ≺ᵥ-trans : ∀ {i j k} (p : Vec ⟪ A ⟫ i) (q : Vec ⟪ A ⟫ j) (r : Vec ⟪ A ⟫ k)
推移性は三つのベクトルに対する同時の場合分けで証明されます。最初の降下が使い尽くされた列から始まるなら、その比較の型はすでに空型であり、中間の列が使い尽くされた場合も同様です。三番目の列が使い尽くされた場合は、二番目の比較が反証可能です。そのようなすべての場合において証明は空型の消去子であり、それ自体の数学的内容はありません。
→ p ≺ᵥ q → q ≺ᵥ r → p ≺ᵥ r ≺ᵥ-trans [] [] r h k = Empty.rec* h ≺ᵥ-trans [] (y ∷ q) r h k = Empty.rec* h ≺ᵥ-trans (x ∷ p) [] r h k = Empty.rec* h ≺ᵥ-trans (x ∷ p) (y ∷ q) [] h k = Empty.rec* k
三つの列がすべて空でないとき、比較は先頭から読み取れ、最初の二つの混在する場合が興味の対象です。x が y より下で y が z と等しいなら、その経路を最初の比較に代入して x が z より下であることが得られます。対称的に、x ≡ y の後に y が z より下が続くなら、二番目の比較を経路に沿って逆向きに輸送します。どちらも同じ動きの実例です。要素の経路は輸送によって比較に作用するのです。
≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inl k) = inl (≺ₚ-trans x y z h k) ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inr (e , k)) = inl (subst (λ v → x ≺ₚ v) e h) ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inl k) = inl (subst (λ v → v ≺ₚ z) (sym e) k)
推移性の最後の場合は両方の先頭をそのままにします。二つの経路は x ≡ z に連結され、再帰は尾へ降ります。長さはそれぞれの列がもつものそのままです。推移性が済むと、三分性は一つの長さをもつ二つの列に対して述べられます。二つの列が一致しうるのはそこでだけだからです。空の列どうしは refl によって等しくなります。
≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inr (e' , k)) = inr (e ∙ e' , ≺ᵥ-trans p q r h k) ≺ᵥ-tri : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Tri (p ≺ᵥ q) (p ≡ q) (q ≺ᵥ p) ≺ᵥ-tri [] [] = eq refl ≺ᵥ-tri (x ∷ p) (y ∷ q) = decide (≺ₚ-tri x y)
空でない列では、先頭がパラメータ順序の三分性によって比較され、補助 decide が判定を先頭から列全体へ運びます。どちら向きの狭義の判定も左の支になります。先頭で決着がつき、尾は一切登場しないからです。等しい場合だけが尾を調べる必要があり、それは次で扱われます。
where decide : Tri (x ≺ₚ y) (x ≡ y) (y ≺ₚ x) → Tri ((x ∷ p) ≺ᵥ (y ∷ q)) ((x ∷ p) ≡ (y ∷ q)) ((y ∷ q) ≺ᵥ (x ∷ p)) decide (lt h) = lt (inl h) decide (gt h) = gt (inl h)
先頭が経路 e によって等しいとき、ベクトルの比較は尾の比較に帰着し、Tri-map が三つの結果に付け替えます。尾が狭義に下なら右の支 e , h となり、尾が等しいことは cong₂ _∷_ のもとで列全体の相等となり、鏡像の判定には sym e が付きます。再帰は尾について構造的で、帰納はここで閉じます。
decide (eq e) = Tri-map (λ h → inr (e , h)) (cong₂ _∷_ e) (λ h → inr (sym e , h)) (≺ᵥ-tri p q)
整礎性は計画を要するものです。ベクトルから降りていくと、先頭が与えられた順序で落ちて尾が同じ長さの任意のものに置き換わるか、先頭はそのままで尾が落ちるかのどちらかです。したがって降下は二重の帰納です。先頭には与えられた順序の整礎性を、尾には尾の到達可能性を使い、任意の尾は一段短い長さでの命題が供給します。この第三の材料があるからこそ、全体も長さについて再帰します。また、先頭の帰納を再帰引数ではなく帰納原理として取るのはこのためです。三つの要求を一つの再帰で同時に満たそうとすると、降下が単一の減少尺度を提示できなくなるからです。
補助 consAcc は到達可能性を長さ k から suc k へ持ち上げます。長さ k のすべての列が到達可能であるという仮定のもとで、y ∷ q の到達可能性を組み立てます。入力 prev は一段前の長さでの命題そのものであり、狭義の場合に尾を同じ長さの任意の r に置き換えられるのはこのためです。証明は先頭について与えられた順序の整礎帰納を実行し、先頭の降下が駆動装置となり、尾の到達可能性はその内部で使われます。
private consAcc : (k : ℕ) → ((r : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) r) → (y : ⟪ A ⟫) (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q → Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q) consAcc k prev = WFI.induction ≺ₚ-wf onHead
帰納仮説 ih の述べ方は慎重です。y より狭義に下のすべての z に対し、尾自身の到達可能性を与えれば、z ∷ q の到達可能性が長さ k のすべての尾 q について成り立つというものです。q についての全称量化があるから、狭義の場合は調べているベクトルへの再帰なしに機能します。そしてこれが可能なのは、≺ₚ-wf を再帰的に呼び出すのではなく帰納原理として適用したからです。
where onHead : (y : ⟪ A ⟫) → ((z : ⟪ A ⟫) → z ≺ₚ y → (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q → Acc (_≺ᵥ_ {suc k} {suc k}) (z ∷ q)) → (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q
到達可能性は構成されたデータです。acc は要素と、狭義に下のすべての要素をその要素自身の到達可能性へ送る関数とを対にします。したがって y ∷ q に対する目標は acc によって与えられ、それに適用されるのは、y ∷ q からの狭義の降下が取りうる二つの形を処理するステップ関数です。証明の残りはこのステップ関数の本体です。
→ Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q) onHead y ih q (acc rq) = acc step where step : (r : Vec ⟪ A ⟫ (suc k)) → r ≺ᵥ (y ∷ q) → Acc (_≺ᵥ_ {suc k} {suc k}) r
狭義の場合は先頭 z が y より下で、尾 r は任意です。ここでは帰納仮説がすべての仕事をします。z ≺ₚ y と、長さ k における r の到達可能性 prev r とから、z ∷ r の Acc が供給されます。等しい場合は先頭を保ちます。経路が z と y を同一視するので、y ∷ r の到達可能性を sym e に沿って逆向きに輸送すれば z ∷ r の到達可能性が得られます。先頭の経路に沿ったこの輸送が、長さを越えた比較の代価であり、ここで一度だけ支払われます。
step (z ∷ r) (inl h) = ih z h r (prev r) step (z ∷ r) (inr (e , h)) = subst (λ v → Acc (_≺ᵥ_ {suc k} {suc k}) (v ∷ r)) (sym e) (onHead y ih r (rq r h)) ≺ᵥ-wf : (k : ℕ) (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p
主定理は長さに関する帰納法です。空の列の到達可能性は直ちに得られます。唯一の候補となる先行要素は空の列自身であり、その比較は空型だからです。x ∷ p に対しては consAcc を適用し、≺ᵥ-wf k が一段前の長さでの任意の尾についての命題を、≺ᵥ-wf k p がこの列自身の尾の到達可能性を供給します。両方とも k に関する一つの構造的再帰から来ます。
≺ᵥ-wf zero [] = acc (λ { [] h → Empty.rec* h }) ≺ᵥ-wf (suc k) (x ∷ p) = consAcc k (≺ᵥ-wf k) x p (≺ᵥ-wf k p)
この比較に伴って一つの派生的な事実が使われ、経路の帰納法で証明されます。列を長さの等式に沿って移しても、それが何の下にあるか、何がその下にあるかは変わりません。これが必要なのは三分性と降下の二箇所で、どちらも長さが等しいが同一ではない二つの列に出会います。
左側の補題は、比較 subst (Vec ⟪ A ⟫) e p ≺ᵥ q が p ≺ᵥ q への経路であること、つまり比較される列を長さの等式 e に沿って輸送しても比較の命題は変わらないことを述べます。証明はベクトルの場合分けをまったく展開しません。一般の補題 constSubstCommSlice は、e に沿う輸送が添字を使わない型族と可換であることを言い、固定された q との比較はまさにそのような型族です。sym は等式を後の証明が必要とする向きに整えます。
private ≺ᵥ-subst-left : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ i) (q : Vec ⟪ A ⟫ k) → (subst (Vec ⟪ A ⟫) e p ≺ᵥ q) ≡ (p ≺ᵥ q) ≺ᵥ-subst-left e p q = sym (constSubstCommSlice (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → v ≺ᵥ q) e p)
右側の補題は鏡像です。もう一方の列をそれ自身の長さの等式に沿って移しても、その下にあるものは変わりません。両方向が必要なのは、名前の比較が lt の場合は最初の名前のパラメータを二番目の長さへ輸送し、gt の場合は逆向きだからであり、後の整礎性の証明ではどちら側も動きます。両方の向きを一度に述べておけば、これ以降の証明は列の上の subst について推論する必要がなくなります。
≺ᵥ-subst-right : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ k) (q : Vec ⟪ A ⟫ i)
→ (p ≺ᵥ subst (Vec ⟪ A ⟫) e q) ≡ (p ≺ᵥ q)
≺ᵥ-subst-right e p q = sym (constSubstCommSlice
(Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → p ≺ᵥ v) e q)
三つの鍵を順に比較する
名前は論理式コード、アリティ、パラメータ列の順に辞書式で比較します。比較を三つの場合として明示することで、三分性と推移性を鍵ごとに示せます。
この比較は定義からそのまま読み取れる型の族です。外側の支は、極限順序の下での論理式コードの狭義の比較です。一方の名前のコードが他方より下なら、コードが判定し、他は一切問われません。右の支は経路 codeOf b ≡ codeOf a、つまり次の鍵へ進むことを許すコードの相等を携え、それを第二の鍵の比較、自然数のアリティの狭義の不等号と組みにします。
infix 20 _≺ₙ_ _≺ₙ_ : Name → Name → Type (ℓ-suc ℓ) a ≺ₙ b = (codeOf a ≺ codeOf b) ⊎ ( (codeOf b ≡ codeOf a) × ( (arity a < arity b)
最も内側の支が降下を完成させます。コードが等しくアリティも等しい場合、後者はやはり経路 arity b ≡ arity a として携えられ、その上でパラメータ列が _≺ᵥ_ によって比較されます。したがって入れ子の各層は「前の鍵の相等」と「次の鍵の狭義の比較」の対であり、四つの法則の場合分けはまさにこの形に沿って鍵ごとに進みます。
⊎ ((arity b ≡ arity a) × (params a ≺ᵥ params b)) ) )
非反射性と推移性は、三つの鍵それぞれの法則を場合分けで並べたものです。推移性の混在する場合は、一方の鍵の等式を他方の鍵の比較に代入するだけで、必要な検証はそれですみます。パラメータの場合は三つの長さでの列の比較を援用します。あの比較を長さを越えて証明したのはこのためです。
名前が自分自身より狭義に下になることは決してなく、三つの節がそれぞれ理由を言います。a ≺ₙ a を証明する和の支はどれも、三つの鍵のどれかが自分自身への狭義の降下を与えることになるからです。コードの場合は極限順序の非反射性と矛盾し、アリティの場合は自分自身より小さい自然数となり ¬m<m で反証され、パラメータの場合は params a 自身の長さでの列の非反射性と矛盾します。
≺ₙ-irr : (a : Name) → a ≺ₙ a → Empty.⊥ ≺ₙ-irr a (inl h) = ≺-irr (codeOf a) h ≺ₙ-irr a (inr (_ , inl h)) = ¬m<m h ≺ₙ-irr a (inr (_ , inr (_ , h))) = ≺ᵥ-irr (params a) h ≺ₙ-trans : (a b c : Name) → a ≺ₙ b → b ≺ₙ c → a ≺ₙ c
推移性は三つの名前に対して述べられ、二つの比較がそれぞれどこで決着したかによる場合分けで証明されます。両方がコードで決着したときは、極限順序の推移性を直接適用します。最初の混在した場合は、a がコードで b より狭義に下であり、二番目の比較が知っているのは codeOf c ≡ codeOf b だけです。その等式を逆向きに代入すれば codeOf a が codeOf c より下であることが得られ、対称の場合は同じ代入を順方向に読んだものです。混在した各場合は輸送が一回あるだけで、それ以上ではありません。
≺ₙ-trans a b c (inl h) (inl k) = inl (≺-trans (codeOf a) (codeOf b) (codeOf c) h k) ≺ₙ-trans a b c (inl h) (inr (q , _)) = inl (subst (λ v → codeOf a ≺ v) (sym q) h) ≺ₙ-trans a b c (inr (q , _)) (inl k) =
アリティの鍵で決着した場合は、自然数で同じ型を繰り返します。二つの狭義のアリティの不等号は <-trans で合成され、狭義の不等号とアリティの等式が並ぶときは、適切な端点を代入する輸送で狭義の不等号に変わります。携えられる経路の向きに注意してください。比較が記録するのは codeOf b ≡ codeOf a と arity b ≡ arity a、つまりより大きな名前の側で述べた相等なので、連結と代入はその向きに逆らって走ります。
inl (subst (λ v → v ≺ codeOf c) q k) ≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inl k)) = inr (q' ∙ q , inl (<-trans h k)) ≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inr (e , _))) = inr (q' ∙ q , inl (subst (λ j → arity a < j) (sym e) h))
最後の場合は、三つの鍵がパラメータに至るまで一致しているところであり、ここでまさに必要なのが第三の鍵の三つの長さでの推移性です。≺ᵥ-trans はそれぞれの列のもつ長さで params a ≺ᵥ params b と params b ≺ᵥ params c を受け取り、params a ≺ᵥ params c を返します。二つのアリティの経路は arity a ≡ arity c に連結され、右の支の三つの成分がそろいます。
≺ₙ-trans a b c (inr (q , inr (e , _))) (inr (q' , inl k)) = inr (q' ∙ q , inl (subst (λ j → j < arity c) e k)) ≺ₙ-trans a b c (inr (q , inr (e , h))) (inr (q' , inr (e' , k))) = inr (q' ∙ q , inr (e' ∙ e , ≺ᵥ-trans (params a) (params b) (params c) h k))
三歧性は三番目の法則であり、他の法則を組み合わせるのではなく比較そのものを読み取るものです。証明は鍵の順に降りていきます。コードがすでに判定を与えれば直ちに結論が出て、コードが等しければアリティが判定し、アリティも等しければパラメータ列が判定します。最後の段階だけが注意を要します。等しいアリティは同一化ではなく経路で結ばれているため、params a と params b は異なる長さに住んでいます。まず前者を後者の長さへ輸送しなければベクトル比較は実行できず、比較が返す狭義の判定も元の型へ輸送し戻して初めて、元の二つの名前の間の比較になります。等しい場合はさらに多くが要ります。二つの名前を等しい依存三つ組として提示しなければならないので、論理式そのものも一致する必要があり、それを与えるのがまさにコードの単射性です。code-shift はアリティの経路に沿う輸送がコードを変えないことを述べ、コード上の判定はコードがすでに一致していると言っているからです。
主張の型は Tri、つまり三択の判定であり、a ≺ₙ b の証明、経路 a ≡ b、あるいは b ≺ₙ a の証明のいずれかを運びます。証明は問題全体をコード上の順序に委ねます。≺-tri はすでに二つのコードに対しこうした判定を返すので、局所的な補助関数 byCodes がコード上の判定を名前上の判定へ変換します。補助関数はまず型で導入されるため、変換の形が各節の前に見えています。
≺ₙ-tri : (a b : Name) → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a) ≺ₙ-tri a b = byCodes (≺-tri (codeOf a) (codeOf b)) where byCodes : Tri (codeOf a ≺ codeOf b) (codeOf a ≡ codeOf b) (codeOf b ≺ codeOf a) → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
狭義の場合は直接です。どちら向きであれ、コードの狭義比較は名前の順序の和の左成分そのものです。等しい場合は第二の鍵が開かれ、byArities に委ねられます。これはアリティに対して、byCodes がコードに対してしたのと同じことをします。
byCodes (lt h) = lt (inl h) byCodes (gt h) = gt (inl h) byCodes (eq ec) = byArities (arity a ≟ arity b) where byArities : NatOrder.Trichotomy (arity a) (arity b)
ここでの判定は和の右成分を取り、コードの等式そのものを運びます。向きに注意してください。比較は大きな名前の側で述べた codeOf b ≡ codeOf a を記録するので、こちらの狭義の場合には sym ec が、双対の場合には書かれたままの ec が要ります。アリティも等しいときは ≺ᵥ-tri がベクトルを比較しますが、params a は長さ arity a、params b は arity b に住むので、最初のベクトルはアリティの経路 e に沿って輸送されてから比較されます。
→ Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a) byArities (NatOrder.lt h) = lt (inr (sym ec , inl h)) byArities (NatOrder.gt h) = gt (inr (ec , inl h)) byArities (NatOrder.eq e) = byParams (≺ᵥ-tri (subst (Vec ⟪ A ⟫) e (params a)) (params b))
輸送されたベクトルには shifted という名前が与えられ、以下の記述が各自の実際の長さで読みやすく保たれます。等しい場合に必要なのはベクトルだけではありません。a ≡ b を直接得るには論理式も一致しなければならず、sameFormula は輸送された論理式のところでこれを述べます。その型は、アリティ arity b の名前の論理式の型です。この等式がなければ、二つの名前は判定済みの二つの鍵でもパラメータでも一致しながら、構文の上ではなお異なり得ます。
where shifted : Vec ⟪ A ⟫ (arity b) shifted = subst (Vec ⟪ A ⟫) e (params a) sameFormula : subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a) ≡ formula b
なぜ論理式が一致するのか。code-shift により、formula a を e に沿って輸送してもそのコードは変わらず、ec の第一成分は formula a のコードが formula b のコードと等しいことを述べます。これらを連結すれば等しいコードが得られ、code-inj が等しいコードを等しいパラメータなし論理式へと戻します。これは本章の前半で証した単射性そのものであり、ここでその主張が予期していた仕事を果たします。shifted と sameFormula がそろえば、byParams がベクトル上の判定を名前上の判定へ変換します。
sameFormula = code-inj (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a)) (formula b) (code-shift e (formula a) ∙ cong fst ec) byParams : Tri (shifted ≺ᵥ params b) (shifted ≡ params b)
狭義の判定は輸送後の長さで得られたので、その述べ方を元へ戻す必要があります。≺ᵥ-subst-left は、subst (Vec ⟪ A ⟫) e p を q と比べることは命題として p を q と比べることと同じだと言うので、h をこの等式に沿って輸送すれば shifted についての比較が params a についての比較に変わります。どちらの判定も、和が要求する向きに揃えたコードとアリティの等式を運びます。双対の場合は対称で、比較の反対側の ≺ᵥ-subst-right を使います。
(params b ≺ᵥ shifted) → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a) byParams (lt h) = lt (inr (sym ec , inr (sym e , transport (≺ᵥ-subst-left e (params a) (params b)) h))) byParams (gt h) = gt (inr (ec , inr (e ,
等しいという判定は Name の二つの元の間の経路であり、Name はそれ自身三つ組です。ΣPathP はアリティの経路 e を残りの成分どうしの経路と組み合わせます。toPathP sameFormula が論理式の等式を型族 Formula (⊥*) (suc k) に沿って持ち上げ、toPathP ep がベクトルの等式に同じことをします。ここが sameFormula の出番です。判定済みの二つの鍵が等しくパラメータも等しい後、欠けているのは論理式の等式だけであり、それが補われれば二つの名前はデータとして同一になります。
transport (≺ᵥ-subst-right e (params b) (params a)) h))) byParams (eq ep) = eq (ΣPathP (e , ΣPathP (toPathP sameFormula , toPathP ep)))
三つの鍵に沿って降下する
整礎性は入れ子になった降下に従い、鍵ごとに一層をなします。最内層ではコードとアリティを固定してパラメータ列を降り、減少する引数はベクトルの到達可能性です。中層ではコードを固定してアリティを降り、最外層ではコードを降ります。各層は外側の層の帰納仮定を引数として受け取る別個の関数なので、それぞれがちょうど一つの到達可能性の証明について再帰し、再帰は至る所構造的です。すべての主張は名前そのものの上で、各鍵の位置を言う等式とともになされます。これは三歧性で見たのと同じ規律であり、名前の射影の上で述べた内容は名前の上で述べた内容と一致させなければなりません。
最内層は、降下の全体像を一つの引数列に記録する関数です。与えられるのは、固定されたコード c、コードが c より下のすべての名前を覆う外側の帰納仮定 ihC、境界 k、コードが c でアリティが k より下の名前を覆う中層の帰納仮定 ihK、それ自身のベクトル到達可能性をもつパラメータ列 p、そして研究対象の名前 a と、三つの等式です。qc はコードを c に、ek はアリティを k に固定し、qp は輸送されたパラメータ列を p と同一視しますです。結論は単に a が到達可能だということです。
private accAtParam : (c : Limit) → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b) → (k : ℕ) → ((b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b)
ベクトル到達可能性のパラメータの型は単一の長さ k で述べられ、p と一致しています。これが、パラメータをその場で比較するのではなく等式 qp によって p の長さへ輸送する理由です。a の到達可能性は構成子 acc とステップ関数によって与えられます。すべての名前が到達可能だと示すには、各 a に対し、a より下の任意の b を受け取って b の到達可能性を返す関数を示せば十分です。
→ (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p → (a : Name) → codeOf a ≡ c → (ek : arity a ≡ k) → subst (Vec ⟪ A ⟫) ek (params a) ≡ p → Acc _≺ₙ_ a accAtParam c ihC k ihK p (acc rp) a qc ek qp = acc step
ステップ関数は、どの鍵が b ≺ₙ a を判定したかで場合分けします。コードが落ちた場合、qc は codeOf b ≺ codeOf a を codeOf b ≺ c へ移し、外側の帰納仮定で終わります。アリティが判定した場合、この先行元の判定は q : codeOf a ≡ codeOf b を運ぶので、sym q ∙ qc : codeOf b ≡ c が得られます。さらに ek : arity a ≡ k に沿って arity b < arity a を arity b < k へ輸送すれば、中層の帰納仮定を適用できます。
where step : (b : Name) → b ≺ₙ a → Acc _≺ₙ_ b step b (inl h) = ihC b (subst (λ v → codeOf b ≺ v) qc h) step b (inr (q , inl h)) = ihK b (sym q ∙ qc) (subst (λ j → arity b < j) ek h) step b (inr (q , inr (e , h))) =
残るのはパラメータの鍵であり、最内層で再帰する唯一の場合です。先行元の判定 b ≺ₙ a では、この枝は e : arity a ≡ arity b を与え、ek : arity a ≡ k は現在の名前を固定アリティに結びます。したがって eb = sym e ∙ ek は arity b ≡ k をもち、これに沿って params b を輸送すると固定長の先行ベクトル pb が得られます。コードの等式は独立に sym q ∙ qc で揃えます。
accAtParam c ihC k ihK pb (rp pb hb) b (sym q ∙ qc) eb refl where eb : arity b ≡ k eb = sym e ∙ ek pb : Vec ⟪ A ⟫ k
狭義の比較 h は params b と params a の間で各自の長さでなされたもので、用いられる到達可能性は p のものです。この隔たりは二つの操作で埋まります。≺ᵥ-subst-left と ≺ᵥ-subst-right は、長さの等式に沿う輸送がベクトルの下辺を変えないと言うので、まず h を境界の長さでの比較へ書き換えます。次に qp が右端点を params a から p へ輸送し、hb : pb ≺ᵥ p が得られます。再帰呼び出しは hb を p の到達可能性である rp に渡し、b の到達可能性を返します。
pb = subst (Vec ⟪ A ⟫) eb (params b) hb : pb ≺ᵥ p hb = subst (λ v → pb ≺ᵥ v) qp (transport (sym (≺ᵥ-subst-right ek pb (params a))) (transport (sym (≺ᵥ-subst-left eb (params b) (params a))) h))
中層は一つのコードを固定し、アリティに沿って降ります。引数列は短くなります。コードの帰納仮定 ihC、自然数順序での到達可能性をもつ境界 k、そしてコードを c に、アリティを k に固定された名前です。ベクトルの到達可能性の代わりになったのは自然数の到達可能性 rk で、アリティの鍵は ℕ の中で降りるからです。
accAtArity : (c : Limit)
→ ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b)
→ (k : ℕ) → Acc _<_ k
→ (a : Name) → codeOf a ≡ c → arity a ≡ k → Acc _≺ₙ_ a
accAtArity c ihC k (acc rk) a qc ek =
本体はすべてを最内層に委ねます。パラメータ列は k へ輸送され、そのベクトル到達可能性は ≺ᵥ-wf がすべての長さのすべてのベクトルに対して成り立つので、ここでは再帰を要求せずそのまま供給されます。真の帰納はアリティについてだけです。局所的な ihK が自然数の到達可能性 rk をほどき、コードが c でアリティが真に小さい名前はその小さい境界での再帰呼び出しで処理されます。この層が、任意の名前の真に小さいアリティを小さい境界へ変換する場所です。
accAtParam c ihC k ihK (subst (Vec ⟪ A ⟫) ek (params a)) (≺ᵥ-wf k (subst (Vec ⟪ A ⟫) ek (params a))) a qc ek refl where ihK : (b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b ihK b q h = accAtArity c ihC (arity b) (rk (arity b) h) b q refl
最外層はコードに沿って降り、アリティについての等式をまったく必要としません。コード c の到達可能性と、コードが c である名前が与えられると、境界 arity a で中層を呼び出し、無条件に成り立つ自然数の到達可能性を供給します。局所的な ihC がコードの到達可能性をほどき、コードが真に小さい名前はその名前自身のコードでの再帰呼び出しを得ます。これは中層の正確な写しであり、一段だけ外側です。
accAtCode : (c : Limit) → Acc _≺_ c → (a : Name) → codeOf a ≡ c → Acc _≺ₙ_ a
accAtCode c (acc rc) a qc =
accAtArity c ihC (arity a) (<-wellfounded (arity a)) a qc refl
where
ihC : (b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b
最後の定理は三層の一行の合成です。名前 a が与えられると、コード順序自身の整礎性が codeOf a の到達可能性を与え、最外層がそれを a の到達可能性へ変換します。コードの等式は反射性により成立します。こうしてすべての名前は三つの鍵による比較のもとで到達可能となり、これが狭義整列順序の整礎性の法則です。
ihC b h = accAtCode (codeOf b) (rc (codeOf b) h) b refl ≺ₙ-wf : WellFounded _≺ₙ_ ≺ₙ-wf a = accAtCode (codeOf a) (≺-wf (codeOf a)) a refl
整列順序と最小の名前
四つの法則は、名前全体が狭義整列順序を運ぶことを示します。それをその構造のレコードへまとめることで、一般の最小要素探索に渡せるようになります。この順序に探索を適用すると、単に非空な名前の族が確定した最小元へ変わります。名前を構成した目的はまさにここにあります。一つの段階の上の集合の族は名前の族になり、名前の族には最小元があるからです。
レコード nameOrder は、すでに証明済みの四つの法則をフィールドごとに集めます。比較そのもの、三歧性、非反射性、推移性、そして整礎性です。ここで新たに証明されるものは何もありません。束の意味は、下流の構成がこの順序の組立方を知らずに狭義整列順序を消費できるようにすることにあります。
nameOrder : SWO (Name) nameOrder = record { _<∙_ = _≺ₙ_ ; tri∙ = ≺ₙ-tri ; irr∙ = ≺ₙ-irr
最小要素探索はこの束をその言葉どおりに使います。族の引数は hProp への関数なので、性質は各名前の上で述べられます。仮定は截断 ∥ Σ ... ∥₁、つまり単に非空であることで、選ばれた証人を運びません。結論は名前とその最小性の明示的な対であり、結局は選ばれた証人で、leastOf がこのモジュールの古典的仮定 lem とともにこれを取り出します。切り捨てを除去できるのは、最小証人全体の型 Σ[ a ∈ Name ] IsLeast nameOrder P a が命題だからです。任意の二つの最小証人は三分性により一致します。したがって古典的降下が単なる非空性を確定した最小の名前へ変換します。
; trans∙ = ≺ₙ-trans ; wf∙ = ≺ₙ-wf } leastName : (P : Name → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ Name ] ⟨ P a ⟩ ∥₁ → Σ[ a ∈ Name ] IsLeast nameOrder P a leastName = leastOf nameOrder lem
まとめ
これで後続段階の各要素は名前をもち、名前全体には狭義整列順序が入ったので、最小の代表を選べます。Name は、アリティ、変数を一つ多くもつパラメータなし論理式、段階から取ったパラメータ列の三つ組です。denote はそれが切り出す部分集合であり、denote-mem は定義可能冪集合の基礎となる内側の意味論でこれを述べます。names-complete は後続段階の各要素が何らかの名前によって指示されることを言い、その存在主張は截断された形です。定義可能冪集合がそもそもそのように論理式を与えるからです。
code∈limit は第一の鍵を、極限段階の順序が比較できる場所へ置き、code-inj はアリティを揃えた後の符号化が単射であることを示します。そのとき、等しいコードから等しいパラメータなし論理式が復元されます。_≺ᵥ_ は第三の鍵を長さを越えて順序づけ、_≺ₙ_ は三つの鍵による比較そのものであり、狭義整列順序の四つの法則すべてと、非空族の最小の名前を返す leastName を伴います。この組み合わせこそ、後の選択構成が用いるものです。一つの段階の上の部分集合の族は名前の族となり、leastName が正準な代表を選びます。その間、截断された完全性の主張から論理式を選び出すことは一度もありません。