Agda大序数(8*) ε的另一种表示

交流Q群: 893531731
目录: NonWellFormed.html
本文源码: Epsilon/Alternative.lagda.md
高亮渲染: Epsilon.Alternative.html

{-# OPTIONS --without-K --safe --experimental-lossy-unification #-}

module NonWellFormed.Epsilon.Alternative where

前置

open import NonWellFormed.Ordinal
open NonWellFormed.Ordinal.≤-Reasoning
open import NonWellFormed.WellFormed
open import NonWellFormed.Arithmetic
open import NonWellFormed.Tetration using (_^^[_]_; _^^ω; _^^ω[_]; ^^≈^^[]ω)
open import NonWellFormed.Fixpoint.Lower using (π; π-fp; π≈)
open import NonWellFormed.Epsilon using (ε; ε-normal; ε-fp; ε-wfp)

open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)

准备工作

我们一般化 ε 的下标, 并建立 εα>1 实例.

private variable
  α : Ord

εα≥ω : ε α ≥ ω
εα≥ω {α} =  begin
  ω         ≈˘⟨ ^-identityʳ _ ⟩
  ω ^ ⌜  ⌝ ≤⟨ ≤f⇒≤l {n = } ≤-refl ⟩
  ε zero    ≤⟨ proj₁ ε-normal z≤ ⟩
  ε α       ∎

instance
  εα>1 : ε α > ⌜  ⌝
  εα>1 {α} =  begin-strict
    ⌜  ⌝     <⟨ n<ω ⟩
    ω         ≤⟨ εα≥ω ⟩
    ε α       ∎

ε的另一种表示

观察序列 ω ^^[ suc (ε α) ] ⌜_⌝ 的前几项有

$${ε_α}+1 = {ε_α}+1$$

_ : ω ^^[ suc (ε α) ] zero ≡ suc (ε α)
_ = refl

$$ω^{{ε_α}+1} = ε_α × ω$$

ω^^[sε]1 : ω ^^[ suc (ε α) ] ⌜  ⌝ ≈ ε α * ω
ω^^[sε]1 {α} =  begin-equality
  ω ^ ε α * ω   ≈⟨ *-congʳ {ω} (ε-fp α) ⟩
  ε α * ω       ∎

$$ω^{ω^{{ε_α}+1}} = {ε_α}^ω$$

ω^^[sε]2 : ω ^^[ suc (ε α) ] ⌜  ⌝ ≈ ε α ^ ω
ω^^[sε]2 {α} =                begin-equality
  ω ^ ω ^^[ suc (ε α) ] ⌜  ⌝ ≈⟨ ^-congˡ ⦃ n≤ω ⦄ ω^^[sε]1 ⟩
  ω ^ (ε α * ω)               ≈˘⟨ ^-*-assoc _ _ _ ⟩
  (ω ^ ε α) ^ ω               ≈⟨ ^-congʳ {ω} (ε-fp α) ⟩
  ε α ^ ω                     ∎

$$ω^{ω^{ω^{{ε_α}+1}}} = {ε_α}^{{ε_α}^ω}$$

ω^^[sε]3 : ω ^^[ suc (ε α) ] ⌜  ⌝ ≈ ε α ^ (ε α ^ ω)
ω^^[sε]3 {α} =                begin-equality
  ω ^ ω ^^[ suc (ε α) ] ⌜  ⌝ ≈⟨ ^-congˡ ⦃ n≤ω ⦄ (begin-equality
      ω ^^[ suc (ε α) ] ⌜  ⌝ ≈⟨ ω^^[sε]2 ⟩
      ε α ^ ω                 ≈˘⟨ π₁ ⟩
      π ⌜  ⌝                 ≈˘⟨ π-fp _ ⟩
      ε α * π ⌜  ⌝           ∎) ⟩
  ω ^ (ε α * π ⌜  ⌝)         ≈˘⟨ ^-*-assoc _ _ _ ⟩
  (ω ^ ε α) ^ π ⌜  ⌝         ≈⟨ ^-congʳ {π ⌜  ⌝} (ε-fp α) ⟩
  ε α ^ π ⌜  ⌝               ≈⟨ ^-congˡ π₁ ⟩
  ε α ^ (ε α ^ ω)             ∎ where
    π₁ =                      begin-equality
      π ⌜  ⌝                 ≈⟨ π≈ _ ⟩
      ε α ^ ω * ⌜  ⌝         ≈⟨ *-identityʳ _ ⟩
      ε α ^ ω                 ∎

归纳到任意 n 项.

module _ (wfα : WellFormed α) where

  ω^^[sε]n : ∀ n → ω ^^[ suc (ε α) ] ⌜ suc (suc n) ⌝ ≈ ε α ^^[ ω ] ⌜ suc n ⌝
  ω^^[sε]n zero    = ω^^[sε]2
  ω^^[sε]n (suc n) =
    let ssn = ω ^^[ suc (ε α) ] ⌜ suc (suc n) ⌝ in
    let sn  = ω ^^[ suc (ε α) ] ⌜ suc n ⌝ in
                                    begin-equality
    ω ^ ssn                         ≈⟨ ^-congˡ ⦃ n≤ω ⦄ (begin-equality
      ssn                           ≡⟨⟩
      ω ^ sn                        ≈⟨ ^-congˡ ⦃ n≤ω ⦄ (begin-equality
        sn                          ≈˘⟨ ω^-absorb-+ ⦃ wf n ⦄ (< n) ⟩
        ω ^ ε α + sn                ≈⟨ +-congʳ (ε-fp _) ⟩
        ε α + sn                    ∎) ⟩
      ω ^ (ε α + sn)                ≈⟨ ^-distribˡ-+-* _ _ _ ⟩
      ω ^ ε α * ω ^ sn              ≡⟨⟩
      ω ^ ε α * ssn                 ≈⟨ *-congʳ (ε-fp _) ⟩
      ε α * ssn                     ∎) ⟩
    ω ^ (ε α * ssn)                 ≈˘⟨ ^-*-assoc _ _ _ ⟩
    (ω ^ ε α) ^ ssn                 ≈⟨ ^-congʳ (ε-fp _) ⟩
    ε α ^ ssn                       ≈⟨ ^-congˡ (ω^^[sε]n _) ⟩
    ε α ^ (ε α ^^[ ω ] suc ⌜ n ⌝) ∎ where
      wf : ∀ n → WellFormed (ω ^^[ suc (ε α) ] ⌜ n ⌝)
      wf zero    = ε-wfp wfα
      wf (suc n) = ^-wfp ω-wellFormed ⦃ n<ω ⦄ (wf n)
      <  : ∀ n → ε α < ω ^^[ suc (ε α) ] ⌜ n ⌝
      < zero     = <s
      < (suc n)  =                  begin-strict
        ε α                         <⟨ < n ⟩
        ω ^^[ suc (ε α) ] ⌜ n ⌝     ≤⟨ ^-incrˡ-≤ _ _ ⦃ n<ω ⦄ ⟩
        ω ^ ω ^^[ suc (ε α) ] ⌜ n ⌝ ∎

推广到 ω 项.

$$ω^{ω^{ω^{.^{.^{{ε_α}+1}}}}} = {ε_α}^{{ε_α}^{.^{.^ω}}}$$

  ω^^ω[sε] : ω ^^ω[ suc (ε α) ] ≈ ε α ^^ω[ ω ]
  ω^^ω[sε] = begin-equality
    lim (λ n → ω ^^[ suc (ε α) ] ⌜ n ⌝)           ≈⟨ l≈ls incr ⟩
    lim (λ n → ω ^^[ suc (ε α) ] ⌜ suc n ⌝)       ≈⟨ l≈ls (^-monoʳ-≤ ω ⦃ n≤ω ⦄ incr) ⟩
    lim (λ n → ω ^^[ suc (ε α) ] ⌜ suc (suc n) ⌝) ≈⟨ l≈l (ω^^[sε]n _) ⟩
    lim (λ n → ε α ^^[ ω ] ⌜ suc n ⌝)             ≈˘⟨ l≈ls (^-incrˡ-≤ ω (ε α)) ⟩
    lim (λ n → (ε α ^^[ ω ] ⌜ n ⌝))               ∎ where
      incr : suc (ε α) ≤ ω ^ suc (ε α)
      incr = ^-incrˡ-≤ (suc (ε α)) ω ⦃ n<ω ⦄

于是我们得到了 ε 后继项的另一种表示.

$$ε_{α+1}={ε_α}^{{ε_α}^{{ε_α}^{.^{.^.}}}}$$

  εₛ : ε (suc α) ≈ ε α ^^ω
  εₛ =                    begin-equality
    ε (suc α)             ≡⟨⟩
    ω ^^[ suc (ε α) ] ω   ≈⟨ ω^^ω[sε] ⟩
    ε α ^^[ ω ] ω         ≈˘⟨ ^^≈^^[]ω _ _ εα≥ω ⦃ n≤ω ⦄ ⟩
    ε α ^^ω               ∎

注意 这种表示只对 ε 成立而对 ζ, η, … 不存在.