Lower.lagda.md

title	zhihu-tags	zhihu-url
Agda大序数(1-7*) 低阶不动点	Agda, 序数, 大数数学	https://zhuanlan.zhihu.com/p/582065361

Agda大序数(1-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 (π≈ _)

幂运算不动点

同样地, 由于 ^_ 是序数嵌入, 因此存在 ^_ 的不动点, 它就是著名的 ε 数, 我们将在下一章介绍. 与 σ 和 π 不同的是 ε 不存在自下而上的算术表示, 因此它更具意义.