Agda大序数(7) 序数嵌入的不动点
交流Q群: 893531731
目录: NonWellFormed.html
本文源码: Fixpoint.lagda.md
高亮渲染: Fixpoint.html
{-# OPTIONS --without-K --safe --experimental-lossy-unification #-}
{-# OPTIONS --no-qualified-instances #-}
module NonWellFormed.Fixpoint where
前置
本章考察序数嵌入的不动点, 需要开头四章作为前置.
open import NonWellFormed.Ordinal open NonWellFormed.Ordinal.≤-Reasoning open import NonWellFormed.WellFormed hiding (wf⇒wf) open import NonWellFormed.Function open import NonWellFormed.Recursion
以下是标准库依赖.
open import Data.Nat as ℕ using (ℕ; zero; suc) open import Data.Nat.Properties as ℕ using (m≤n⇒m<n∨m≡n) open import Data.Unit using (tt) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂) open import Function using (_∘_; λ-) open import Relation.Binary.PropositionalEquality as Eq using (refl)
定义
我们说序数 α 是序数函数 F 的不动点, 当且仅当 F α ≈ α.
_isFixpointOf_ : Ord → (Ord → Ord) → Set α isFixpointOf F = F α ≈ α
我们说 rec F from α by ω 是 F 从 α 开始的无穷迭代, 记作 F ⋱ α.
_⋱_ : (Ord → Ord) → (Ord → Ord) F ⋱ α = rec F from α by ω
由超限递归的相关引理立即可知无穷迭代保持函数的弱增长性和 ≤-单调性.
module _ {F : Ord → Ord} where
⋱-incr-≤ : ≤-increasing F → ≤-increasing (F ⋱_)
⋱-incr-≤ ≤-incr = rec-from-incr-≤ ω ≤-incr
⋱-mono-≤ : ≤-monotonic F → ≤-monotonic (F ⋱_)
⋱-mono-≤ ≤-mono = rec-from-mono-≤ ω ≤-mono
我们说 F ∘ suc 的从 F zero 开始的递归是 F 的后继迭代, 记作 F ⁺
_⁺ : (Ord → Ord) → (Ord → Ord) F ⁺ = rec F ∘ suc from (F zero) by_
后继迭代具有良好的性质, 只要 F ≤-单调且弱增长, F ⁺ 就是序数嵌入.
⁺-normal : ∀ F → ≤-monotonic F → ≤-increasing F → normal (F ⁺)
⁺-normal F F-mono-≤ F-incr-≤ =
rec-by-mono-≤ Fs-mono-≤ (<⇒≤-incr Fs-incr-<)
, rec-by-mono-< Fs-mono-≤ Fs-incr-<
, λ- ≈-refl where
Fs-mono-≤ : ≤-monotonic (F ∘ suc)
Fs-mono-≤ ≤ = F-mono-≤ (s≤s ≤)
Fs-incr-< : <-increasing (F ∘ suc)
Fs-incr-< α = s≤⇒< (F-incr-≤ (suc α))
我们说 F ⋱_ ∘ suc 的从 F ⋱ zero 开始的递归是 F 的不动点枚举函数, 记作 F ′.
_′ : (Ord → Ord) → Ord → Ord F ′ = F ⋱_ ⁺
我们接下来解释该定义的合理性.
不动点
给定一个序数嵌入 F.
module _ {F : Ord → Ord} (nml@(≤-mono , <-mono , ct) : normal F) where
private ≤-incr = normal⇒≤-incr nml
引理 F 的从任意初始值开始的无穷递归都是 F 的不动点.
⋱-fp : ∀ α₀ → (F ⋱ α₀) isFixpointOf F
⋱-fp α₀ = begin-equality
F (F ⋱ α₀) ≈⟨ ct _ ⟩
lim (λ n → F (rec F from α₀ by ⌜ n ⌝)) ≈˘⟨ l≈ls (≤-incr α₀) ⟩
F ⋱ α₀ ∎
注意 存在 F 的任意大的不动点.
_ : ≤-increasing (F ⋱_) _ = ⋱-incr-≤ ≤-incr
最小不动点
引理 F 的从零开始的无穷递归 F ⋱ zero 是 F 的最小不动点.
⋱₀-fp : (F ⋱ zero) isFixpointOf F
⋱₀-fp = ⋱-fp zero
⋱₀-min : ∀ {α} → α isFixpointOf F → F ⋱ zero ≤ α
⋱₀-min {α} fp = l≤ helper where
helper : ∀ n → (rec F from zero by ⌜ n ⌝) ≤ α
helper zero = z≤
helper (suc n) = begin
rec F from zero by ⌜ suc n ⌝ ≤⟨ ≤-mono (helper n) ⟩
F α ≈⟨ fp ⟩
α ∎
现在, 假设 F 在零处增长.
module _ (z-incr : zero-increasing F) where
引理 F 的从零开始的有穷递归是递归次数的单调序列.
⋱₀-monoSeq : MonoSequence (rec F from zero by_ ∘ ⌜_⌝)
⋱₀-monoSeq = wrap mono where
mono : monoSequence _
mono {m} {suc n} (ℕ.s≤s m≤n) with m≤n⇒m<n∨m≡n m≤n
... | inj₁ m<n = begin-strict
rec F from zero by ⌜ m ⌝ <⟨ mono m<n ⟩
rec F from zero by ⌜ n ⌝ ≤⟨ ≤-incr _ ⟩
rec F from zero by ⌜ suc n ⌝ ∎
... | inj₂ refl = helper m where
helper : ∀ m → rec F from zero by ⌜ m ⌝ < rec F from zero by ⌜ suc m ⌝
helper zero = z-incr
helper (suc m) = <-mono (helper m)
引理 如果 F 保良构, 那么 F ⋱ zero 良构.
⋱₀-wf : wf-preserving F → WellFormed (F ⋱ zero)
⋱₀-wf wfp = helper , ⋱₀-monoSeq where
helper : ∀ {n} → WellFormed (rec F from zero by ⌜ n ⌝)
helper {zero} = tt
helper {suc n} = wfp helper
事实 如果 F 还在良构后继处增长, 那么 F 的最小不动点严格大于 F 在有限序数处的值.
Fn<F⋱₀ : suc-increasing F → ∀ n → F ⌜ n ⌝ < F ⋱ zero
Fn<F⋱₀ s-incr n = begin-strict
F ⌜ n ⌝ <⟨ <-mono <s ⟩
F ⌜ suc n ⌝ ≤⟨ ≤-mono (helper n) ⟩
rec F from zero by ⌜ suc (suc n) ⌝ ≤⟨ f≤l ⟩
F ⋱ zero ∎ where
helper : ∀ n → suc ⌜ n ⌝ ≤ F (rec F from zero by ⌜ n ⌝)
helper zero = <⇒s≤ z-incr
helper (suc n) = begin
⌜ suc (suc n) ⌝ ≤⟨ <⇒s≤ (s-incr ⌜ n ⌝ ⦃ ⌜ n ⌝-wellFormed ⦄) ⟩
F ⌜ suc n ⌝ ≤⟨ ≤-mono (helper n) ⟩
F (F (rec F from zero by ⌜ n ⌝)) ∎
后继不动点
引理 F 的从 suc α 开始的无穷递归是 F 的大于 α 的最小不动点, 叫做 F 于 α 的后继不动点.
⋱ₛ-fp : ∀ α → (F ⋱ suc α) isFixpointOf F
⋱ₛ-fp α = ⋱-fp (suc α)
⋱ₛ-incr-< : <-increasing (F ⋱_ ∘ suc)
⋱ₛ-incr-< α = s≤⇒< (⋱-incr-≤ ≤-incr (suc α))
⋱ₛ-suc : ∀ α β → α < β → β isFixpointOf F → F ⋱ suc α ≤ β
⋱ₛ-suc α β α<β fp = l≤ helper where
helper : ∀ n → rec F from suc α by ⌜ n ⌝ ≤ β
helper zero = <⇒s≤ α<β
helper (suc n) = begin
F (rec F from suc α by ⌜ n ⌝) ≤⟨ ≤-mono (helper n) ⟩
F β ≈⟨ fp ⟩
β ∎
引理 F ⋱_ ∘ suc ≤-单调.
⋱ₛ-mono-≤ : ≤-monotonic (F ⋱_ ∘ suc) ⋱ₛ-mono-≤ α≤β = ⋱-mono-≤ ≤-mono (s≤s α≤β)
现在, 假设 F 在良构后继处增长.
module _ (s-incr : suc-increasing F) where
引理 F 的从 suc α 开始的有穷递归是递归次数的单调序列.
⋱ₛ-monoSeq : ∀ α → ⦃ WellFormed α ⦄ → MonoSequence (rec F from suc α by_ ∘ ⌜_⌝)
⋱ₛ-monoSeq α = wrap mono where
mono : monoSequence _
mono {m} {suc n} (ℕ.s≤s m≤n) with m≤n⇒m<n∨m≡n m≤n
... | inj₁ m<n = begin-strict
rec F from suc α by ⌜ m ⌝ <⟨ mono m<n ⟩
rec F from suc α by ⌜ n ⌝ ≤⟨ ≤-incr _ ⟩
rec F from suc α by ⌜ suc n ⌝ ∎
... | inj₂ refl = helper m where
helper : ∀ m → rec F from suc α by ⌜ m ⌝ < rec F from suc α by ⌜ suc m ⌝
helper zero = s-incr α
helper (suc m) = <-mono (helper m)
引理 如果 F 保良构, 那么 F ⋱_ ∘ suc 也保良构.
⋱ₛ-wfp : wf-preserving F → wf-preserving (F ⋱_ ∘ suc)
⋱ₛ-wfp wfp {α} wfα = helper , ⋱ₛ-monoSeq α ⦃ wfα ⦄ where
helper : ∀ {n} → WellFormed (rec F from suc α by ⌜ n ⌝)
helper {zero} = wfα
helper {suc n} = wfp helper
不动点的枚举
引理 F ⋱_ ∘ suc 的从 F ⋱ zero 开始的递归是 F 的不动点枚举函数.
′-fp : ∀ α → (F ′) α isFixpointOf F
′-fp zero = ⋱₀-fp
′-fp (suc α) = ⋱ₛ-fp _
′-fp (lim f) = begin-equality
F ((F ′) (lim f)) ≈⟨ ct _ ⟩
lim (λ n → F ((F ′) (f n))) ≈⟨ l≈l (′-fp (f _)) ⟩
(F ′) (lim f) ∎
我们接下来证明高阶函数 _′ 保持序数函数的一系列性质.
定理 _′ 保持序数嵌入.
′-normal : normal (F ′) ′-normal = ⁺-normal (F ⋱_) (⋱-mono-≤ ≤-mono) (⋱-incr-≤ ≤-incr)
注意 这意味着 _′ 也可以一直迭代下去, 得到高阶不动点.
定理 _′ 保持保良构性.
′-wfp : zero-increasing F → suc-increasing F → wf-preserving F → wf-preserving (F ′) ′-wfp z-incr s-incr wfp = rec-wfp (⋱₀-wf z-incr wfp) ⋱ₛ-mono-≤ ⋱ₛ-incr-< (⋱ₛ-wfp s-incr wfp)
定理 _′ 保持零处增长性.
module _ {F} where
′-zero-incr : zero-increasing F → zero-increasing (F ′)
′-zero-incr z-incr = <f⇒<l {n = 1} z-incr
定理 _′ 保持良构后继处增长性.
′-suc-incr : normal F → suc-increasing F → suc-increasing (F ′)
′-suc-incr nml s-incr α = begin-strict
suc α <⟨ s-incr α ⟩
rec F from suc α by ⌜ 1 ⌝ ≤⟨ f≤l ⟩
F ⋱ suc α ≤⟨ ⋱ₛ-mono-≤ nml (rec-by-incr-≤ (⋱ₛ-mono-≤ nml) (⋱ₛ-incr-< nml) α) ⟩
(F ′) (suc α) ∎
高阶性质
_⁺ 和 _′ 也具有与增长性, 单调性, 合同性类似的性质, 只不过是高阶的.
定理 _′ 满足高阶增长性.
module _ {F} (nml@(≤-mono , _ , _) : normal F) where
′-incrʰ-≤ : ∀ α → F α ≤ (F ′) α
′-incrʰ-≤ α = begin
F α ≤⟨ ≤-mono (normal⇒≤-incr (′-normal nml) α) ⟩
F ((F ′) α) ≈⟨ ′-fp nml α ⟩
(F ′) α ∎
引理 _⁺ 满足高阶单调性.
module _ {F G} (≤-mono : ≤-monotonic F) where
⁺-monoʰ-≤ : (∀ {α} → F α ≤ G α) → (∀ {α} → (F ⁺) α ≤ (G ⁺) α)
⁺-monoʰ-≤ F≤G {zero} = F≤G {zero}
⁺-monoʰ-≤ F≤G {suc α} = begin
F (suc ((F ⁺) α)) ≤⟨ ≤-mono (s≤s (⁺-monoʰ-≤ F≤G)) ⟩
F (suc ((G ⁺) α)) ≤⟨ F≤G ⟩
G (suc ((G ⁺) α)) ∎
⁺-monoʰ-≤ F≤G {lim f} = begin
lim (λ n → (F ⁺) (f n)) ≤⟨ l≤l (λ n → ⁺-monoʰ-≤ F≤G) ⟩
lim (λ n → (G ⁺) (f n)) ∎
引理 _′ 满足高阶单调性.
module _ {F G} (≤-mono : ≤-monotonic F) where
′-monoʰ-≤ : (∀ {α} → F α ≤ G α) → (∀ {α} → (F ′) α ≤ (G ′) α)
′-monoʰ-≤ F≤G = ⁺-monoʰ-≤ (⋱-mono-≤ ≤-mono) (l≤l ≤) where
≤ : ∀ {α} n → rec F from α by ⌜ n ⌝ ≤ rec G from α by ⌜ n ⌝
≤ zero = ≤-refl
≤ {α} (suc n) = begin
F (rec F from α by ⌜ n ⌝) ≤⟨ ≤-mono (≤ n) ⟩
F (rec G from α by ⌜ n ⌝) ≤⟨ F≤G ⟩
G (rec G from α by ⌜ n ⌝) ∎
定理 _⁺ 和 _′ 满足高阶合同性, 即保持函数外延 ≈ᶠ.
module _ {F G} (F-mono : ≤-monotonic F) (G-mono : ≤-monotonic G) where
⁺-congʰ : F ≈ᶠ G → (F ⁺) ≈ᶠ (G ⁺)
⁺-congʰ F≈ᶠG = ⁺-monoʰ-≤ F-mono (proj₁ F≈ᶠG)
, ⁺-monoʰ-≤ G-mono (proj₂ F≈ᶠG)
′-congʰ : F ≈ᶠ G → (F ′) ≈ᶠ (G ′)
′-congʰ F≈ᶠG = ′-monoʰ-≤ F-mono (proj₁ F≈ᶠG)
, ′-monoʰ-≤ G-mono (proj₂ F≈ᶠG)