Agda大序数(7*) 低阶不动点
交流Q群: 893531731
目录: NonWellFormed.html
本文源码: Fixpoint/Lower.lagda.md
高亮渲染: Fixpoint.Lower.html
本章是关于不动点的一些平凡的例子, 与主线无关, 可以跳过.
{-# OPTIONS --without-K --safe --experimental-lossy-unification #-}
前置
open import NonWellFormed.Ordinal open NonWellFormed.Ordinal.≤-Reasoning open import NonWellFormed.WellFormed open import NonWellFormed.Function open import NonWellFormed.Recursion open import NonWellFormed.Arithmetic open import NonWellFormed.Fixpoint open import Data.Nat as ℕ using (ℕ; zero; suc) open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)
本章的所有内容都是参数化到某序数 ξ 上的.
module NonWellFormed.Fixpoint.Lower {ξ : Ord} where
加法不动点
我们知道 +_ 是序数嵌入, 因此存在 +_ 的不动点, 我们记作 σ.
σ : Ord → Ord σ = (ξ +_) ′ σ-fp : ∀ α → (σ α) isFixpointOf (ξ +_) σ-fp α = ′-fp (+-normal ξ) α
+_ 的最小不动点可以表示为序数乘法. 非形式地, σ zero ≈ ... + ξ + ξ ≈ ξ * ω.
σ₀ : σ zero ≈ ξ * ω
σ₀ = l≈l helper where
helper : ∀ {n} → rec _+_ ξ from zero by ⌜ n ⌝ ≈ ξ * ⌜ n ⌝
helper {zero} = ≈-refl
helper {suc n} = begin-equality
ξ + (rec (ξ +_) from zero by ⌜ n ⌝) ≈⟨ +-congˡ helper ⟩
ξ + ξ * ⌜ n ⌝ ≈⟨ +-assoc-n ξ n ⟩
ξ * ⌜ n ⌝ + ξ ≡⟨⟩
ξ * suc ⌜ n ⌝ ∎
σ α 的下一个不动点就是 σ α 的后继.
σ⋱ₛ : ∀ α → σ (suc α) ≈ suc (σ α)
σ⋱ₛ α = l≤ helper , <⇒s≤ (<-mono <s) where
helper : ∀ n → rec (ξ +_) from suc (σ α) by ⌜ n ⌝ ≤ suc (σ α)
helper zero = ≤-refl
helper (suc n) = begin
ξ + (rec (ξ +_) from suc (σ α) by ⌜ n ⌝) ≤⟨ +-monoʳ-≤ ξ (helper n) ⟩
ξ + suc (σ α) ≡⟨⟩
suc (ξ + σ α) ≤⟨ s≤s (proj₁ (σ-fp α)) ⟩
suc (σ α) ∎
<-mono = proj₁ (proj₂ (′-normal (+-normal ξ)))
于是 σ 可以完全用序数算术表示.
σ≈ : ∀ α → σ α ≈ ξ * ω + α σ≈ zero = σ₀ σ≈ (suc α) = begin-equality σ (suc α) ≈⟨ σ⋱ₛ α ⟩ suc (σ α) ≈⟨ s≈s (σ≈ α) ⟩ suc (ξ * ω + α) ≡⟨⟩ ξ * ω + suc α ∎ σ≈ (lim f) = l≈l (σ≈ _)
乘法不动点
与加法不动点不同的是乘法要求 ξ 大于 1, 不然每个序数都是平凡的不动点.
module _ ⦃ ξ>1 : ξ > ⌜ 1 ⌝ ⦄ where
instance
ξ>0 : ξ > zero
ξ>0 = <-trans <s ξ>1
ξ≥1 : ξ ≥ ⌜ 1 ⌝
ξ≥1 = <⇒≤ ξ>1
ξ*-normal : normal (ξ *_)
ξ*-normal = *-normal ξ
由于 *_ 是序数嵌入, 因此存在 *_ 的不动点, 我们记作 π.
π : Ord → Ord π = (ξ *_) ′ π-fp : ∀ α → (π α) isFixpointOf (ξ *_) π-fp α = ′-fp ξ*-normal α
此外, 由序数算术定律, 可以证明 ξ ^ ω 也是 ξ *_ 的不动点.
ξ^ω-fp : (ξ ^ ω) isFixpointOf (ξ *_)
ξ^ω-fp = begin-equality
lim (λ n → ξ * ξ ^ ⌜ n ⌝) ≈⟨ l≈l (*-assoc-n ξ _) ⟩
lim (λ n → ξ ^ ⌜ suc n ⌝) ≈˘⟨ l≈ls (^-monoʳ-≤ ξ ≤s) ⟩
lim (λ n → ξ ^ ⌜ n ⌝) ∎
我们接下来将建立 π 与 ξ ^ ω 的联系. 首先, 乘法的最小不动点是平凡的零.
π₀ : π zero ≈ zero
π₀ = l≤ helper , z≤ where
helper : ∀ n → rec _*_ ξ from zero by ⌜ n ⌝ ≤ zero
helper zero = ≤-refl
helper (suc n) = begin
ξ * (rec _*_ ξ from zero by ⌜ n ⌝) ≤⟨ *-monoʳ-≤ ξ (helper n) ⟩
ξ * zero ≡⟨⟩
zero ∎
因此我们还要额外考察 π ⌜ 1 ⌝.
π₁ : π ⌜ 1 ⌝ ≈ ξ ^ ω
π₁ = ⋱ₛ-suc ξ*-normal _ _ π₀<ξ^ω ξ^ω-fp , l≤ ξ^n≤π₁ where
π₀<ξ^ω = begin-strict
π zero ≈⟨ π₀ ⟩
zero <⟨ <s ⟩
ξ ^ zero ≤⟨ f≤l {n = 0} ⟩
ξ ^ ω ∎
ξ^n≤π₁ : ∀ n → ξ ^ ⌜ n ⌝ ≤ π ⌜ 1 ⌝
ξ^n≤π₁ zero = begin
⌜ 1 ⌝ ≤⟨ s≤s (proj₂ π₀) ⟩
suc ((ξ *_) ⋱ zero) ≤⟨ f≤l {n = 0} ⟩
π ⌜ 1 ⌝ ∎
ξ^n≤π₁ (suc n) = begin
ξ ^ suc ⌜ n ⌝ ≡⟨⟩
ξ ^ ⌜ n ⌝ * ξ ≈˘⟨ *-assoc-n ξ n ⟩
ξ * ξ ^ ⌜ n ⌝ ≤⟨ *-monoʳ-≤ ξ (ξ^n≤π₁ n) ⟩
ξ * π ⌜ 1 ⌝ ≈⟨ π-fp ⌜ 1 ⌝ ⟩
π ⌜ 1 ⌝ ∎
然后, π α 的下一个不动点是 π α 与 π ⌜ 1 ⌝ 的和.
π⋱ₛ : ∀ α → π (suc α) ≈ π α + ξ ^ ω
π⋱ₛ α = ⋱ₛ-suc ξ*-normal _ _ πα<πα+ξ^ω πα+ξ^ω-fp , l≤ helper where
πα<πα+ξ^ω = +-incrʳ-< _ ^>0 _
πα+ξ^ω-fp = begin-equality
ξ * (π α + ξ ^ ω) ≈⟨ *-distribˡ-+ ξ _ _ ⟩
ξ * π α + ξ * ξ ^ ω ≈⟨ +-congˡ ξ^ω-fp ⟩
ξ * π α + ξ ^ ω ≈⟨ +-congʳ {ξ ^ ω} (π-fp α) ⟩
π α + ξ ^ ω ∎
helper : ∀ n → π α + ξ ^ ⌜ n ⌝ ≤ π (suc α)
helper zero = begin
π α + ξ ^ zero ≈⟨ +-congˡ {π α} ≈-refl ⟩
suc (π α) ≤⟨ <⇒s≤ (<-mono <s) ⟩
π (suc α) ∎
where <-mono = proj₁ (proj₂ (′-normal ξ*-normal))
helper (suc n) = begin
π α + ξ ^ ⌜ suc n ⌝ ≈˘⟨ +-congˡ (*-assoc-n ξ n) ⟩
π α + ξ * ξ ^ ⌜ n ⌝ ≈˘⟨ +-congʳ (π-fp α) ⟩
ξ * π α + ξ * ξ ^ ⌜ n ⌝ ≈˘⟨ *-distribˡ-+ ξ _ _ ⟩
ξ * (π α + ξ ^ ⌜ n ⌝) ≤⟨ *-monoʳ-≤ ξ (helper n) ⟩
ξ * π (suc α) ≈⟨ π-fp (suc α) ⟩
π (suc α) ∎
于是 π 也可以用序数算术表示.
π≈ : ∀ α → π α ≈ ξ ^ ω * α
π≈ zero = π₀
π≈ (suc α) = begin-equality
π (suc α) ≈⟨ π⋱ₛ α ⟩
π α + ξ ^ ω ≈⟨ +-congʳ {ξ ^ ω} (π≈ α) ⟩
ξ ^ ω * α + ξ ^ ω ≡⟨⟩
ξ ^ ω * suc α ∎
π≈ (lim x) = l≈l (π≈ _)
幂运算不动点
同样地, 由于 ^_ 是序数嵌入, 因此存在 ^_ 的不动点, 它就是著名的 ε 数, 我们将在下一章介绍. 与 σ 和 π 不同的是 ε 不存在自下而上的算术表示, 因此它更具意义.