形式化大数数学（1.2-Veblen函数）一

目录

形式化大数数学（1.2-Veblen函数） ▹

综述 ▹

二元Veblen函数 ▹

三元Veblen函数 ▹

四元Veblen函数 ▹

形式化大数数学 (1.2 - Veblen函数)

本文源码: Multinary.lagda.md

高亮渲染: Multinary.html

module Veblen.Multinary where

open import Veblen.Basic public

综述

前篇讲了Veblen层级的构造需要的三个高阶函数

1. 无穷迭代 λF，Fω

2. 跳出运算 jump

3. 不动点的枚举 fixpt

以及ε，ζ，η函数的定义

观察这些定义的形式, 不难发现, 很自然地, 构造更大序数的下一步操作是迭代高阶函数fixpt 本身. 这要求一个更高阶的函数 Φ₂， 然后我们会想要再次迭代这个更高阶的函数, 这又要求一个更更高阶的函数 Φ₃， 乃至 Φ₄， 以此类推.

• Φ₂：(Ord → Ord) → Ord → Ord → Ord

• Φ₃：(Ord → Ord → Ord) → Ord → Ord → Ord → Ord

• Φ₄：(Ord → Ord → Ord → Ord) → Ord → Ord → Ord → Ord → Ord

• …

回想梦的开始λα，ωα：Ord → Ord，把它记作 φ₁.

• 从 φ₁ 开始, 用 Φ₂ 迭代 fixpt， 得到的函数叫做二元Veblen函数 φ₂：Ord → Ord → Ord

• 从 φ₂ 开始, 用 Φ₃ 迭代 Φ₂， 得到的函数叫做三元Veblen函数 φ₃：Ord → Ord → Ord → Ord

• 从 φ₃ 开始, 用 Φ₄ 迭代 Φ₃， 得到的函数叫做四元Veblen函数 φ₄：Ord → Ord → Ord → Ord → Ord

• ...

φ₁，φ₂，. . . 分别具有定义

• φ₁：＝λα，ωα

• φ₂：＝Φ₂ φ₁

• φ₃：＝Φ₃ φ₂

• φ₄：＝Φ₄ φ₃

• …

剩下的只需要处理Φ₂，Φ₃，. . . 的细节.

下标位是稀缺资源. 后文中, 在没有歧义的情况下, 我们会省去表示元数的下标. 如有歧义, 我们用Bin. Φ，Tri. Φ，Qua. Φ，. . . 以及 Bin. φ，Tri. φ，Qua. φ，. . . 来区分元数. 下文中的下标将另作他用, 注意区分.

二元Veblen函数

module BinaryVeblen where

由上面的讨论, 二元版本的Φ 需要迭代 fixpt, 这也是由强大的 rec 函数完成的. 注意 rec 可以处理任意类型 A, 一个序数函数类型不管再高阶, 它也是一个类型, 所以适用 rec. 这是类型论语言的方便之处.

定义 二元版本的 Φ 为, 对给定的序数函数 F：Ord → Ord， 使用 rec， 其三个参数分别如下.

• 初始值：F

• 后继步骤：迭代 fixpt

• 极限步骤：对步骤的基本列取极限, 再做一次跳出操作

即

Φ F：＝rec F fixpt (λφ，jump λβ，lim λn，φ[n]β)

Φ : (Ord → Ord) → Ord → Ord → Ord

Φ F = rec F fixpt (λ φ[_] → jump λ β → lim λ n → φ[ n ] β)

注意 极限步的跳出操作是反直觉的一步. 从通常的定义式反推不难发现这里需要跳出. 仔细分析二元Veblen函数的序性质才能更好的理解这里跳出的动机, 具体可以参看 Agda大序数(9) 二元Veblen函数. 这里只需简单的理解为是为了更好的性质和更高的增长率就行了.

定义 二元Veblen函数

φ：＝Φ λα，ωα

φ : Ord → Ord → Ord

φ = Φ (ω ^_)

我们习惯将最后一个参数之前的所有参数都写成下标.

例 由定义, 以下等式成立.

φ₀＝λα，ωα

φ₁＝ε

φ₂＝ζ

φ₃＝η

φ-0 : φ 0 ≡ ω ^_

φ-0 = refl

φ-1 : φ 1 ≡ ε

φ-1 = refl

φ-2 : φ 2 ≡ ζ

φ-2 = refl

φ-3 : φ 3 ≡ η

φ-3 = refl

定理 对于第一个参数为后继和极限的情况, 由定义, 有以下等式成立.

φα⁺＝fixpt φα

φₗᵢₘ f＝jump λα，lim λn，φ f ₙ α

φ-suc : φ (suc α) ≡ fixpt (φ α)

φ-suc = refl

φ-lim : φ (lim f) ≡ jump λ α → lim λ n → φ (f n) α

φ-lim = refl

为了对jump 的行为有更加直观的感受, 对第一个参数为极限的情况, 我们对第二个参数再次分成零, 后继和极限的情况进行讨论, 有如下等式成立.

φₗᵢₘ f0＝lim λn，φ f ₙ 0

φₗᵢₘ f(β⁺)＝lim λn，φ f ₙ (φlim f β)⁺

φₗᵢₘ f(lim g)＝lim λn，φₗᵢₘ f (g n)

φ-lim-0 : φ (lim f) 0 ≡ lim λ n → φ (f n) 0

φ-lim-0 = refl

φ-lim-suc : φ (lim f) (suc β) ≡ lim λ n → φ (f n) (suc (φ (lim f) β))

φ-lim-suc = refl

φ-lim-lim : φ (lim f) (lim g) ≡ lim λ n → φ (lim f) (g n)

φ-lim-lim = refl

很快, 我们来到了二元Veblen函数的能力极限.

定义 对函数 λα，φα 0 取不动点枚举, 得到的函数称为 Γ.

Γ：＝fixpt λα，φα 0

Γ : Ord → Ord

Γ = fixpt λ α → φ α 0

例 最小的 Γ 数是

Γ₀＝φφφφ…0 0 0 0

Γ-0 : Γ 0 ≡ iterω (λ α → φ α 0) 0

Γ-0 = refl

没有什么能阻止我们继续取不动点枚举. 将Γ 看作新的 λα，ωα， 我们可以得到所谓第二代 ε，ζ，η 函数, 分别记作 ·ε，·ζ，·η.

·ε＝fixpt Γ

·ζ＝fixpt ·ε

·η＝fixpt ·ζ

ε̇ ζ̇ η̇ : Ord → Ord

ε̇ = fixpt Γ

ζ̇ = fixpt ε̇

η̇ = fixpt ζ̇

然后有第二代φ 和第二代 Γ 函数.

·φ：Φ Γ

·Γ：＝fixpt λα，·φα 0

φ̇ : Ord → Ord → Ord

φ̇ = Φ Γ

Γ̇ : Ord → Ord

Γ̇ = fixpt λ α → φ̇ α 0

乃至第三代ε，ζ，η 函数

··ε：＝fixpt ·Γ

··ζ：＝fixpt ··ε

··η：＝fixpt ··ζ

ε̈ ζ̈ η̈ : Ord → Ord

ε̈ = fixpt Γ̇

ζ̈ = fixpt ε̈

η̈ = fixpt ζ̈

和第三代φ 和第三代 Γ 函数.

··φ：＝Φ ·Γ

··Γ：＝fixpt λα，··φα 0

φ̈ : Ord → Ord → Ord

φ̈ = Φ Γ̇

Γ̈ : Ord → Ord

Γ̈ = fixpt λ α → φ̈ α 0

以此类推, 直至超限代. 三元Veblen函数将把这些后代函数囊括其中.

三元Veblen函数

module TrinaryVeblen where

本小节我们将上一小节的谈论过事物x 记作 Bin. x， 以让出命名空间, 但没有歧义时会省略.

private module Bin = BinaryVeblen

open Bin using (Γ; ε̇; ζ̇; η̇; φ̇; Γ̇; ε̈; ζ̈; η̈; φ̈; Γ̈)

定义 三元版本的 Φ 为, 对给定的序数函数 F：Ord → Ord → Ord， 使用 rec， 其三个参数分别如下.

• 初始值：F

• 后继步骤: 迭代 λφα，Bin. Φ (fixpt λβ，φα，ᵦ 0)

一些解释

此处迭代的是二元函数 Ord → Ord → Ord， 以得到一个三元函数.参数 φα 是上一步的结果, 它是一个二元函数, 看作是对三元函数 φ 输入了上一步的编号 α 所得到的结果.这一步我们先对 λβ，φα，ᵦ 0 取不动点枚举, 再交给二元 Φ 处理

回想上一小节我们是怎么从一代 φ 得到二代 φ 的, 这里的处理方式就是对该操作的反映.注意: 对任意元 φ， 我们都是取第二个参数的不动点枚举, 而对右边剩下的参数全部填零. 二元 Φ 的时候这个规律还看不出来, 现在才显现出来.

• 极限步骤: 对步骤的基本列取极限, 再做一次跳出操作, 再交给二元 Φ 处理

注意: 与后继步骤类似地, 这里是对第二个参数跳出, 右边其余参数全部填零.

Φ F：＝rec F (λφα，Bin. Φ (fixpt λβ，φα，ᵦ 0))

(λφ，Bin. Φ (jump λβ，lim λn，φ[n]ᵦ 0))

Φ : (Ord → Ord → Ord) → Ord → Ord → Ord → Ord

Φ F = rec F

(λ φ-α → Bin.Φ $ fixpt λ β → φ-α β 0)

(λ φ[_] → Bin.Φ $ jump λ β → lim λ n → φ[ n ] β 0)

定义 三元Veblen函数

φ：＝Φ Bin. φ

φ : Ord → Ord → Ord → Ord

φ = Φ Bin.φ

例 由定义, 以下等式成立.

φ₀＝Bin. φ

φ₁，₀＝Γ

φ₁，₁＝·ε

φ₁，₂＝·ζ

φ₁，₃＝·η

φ₁＝·φ

φ₂，₀＝·Γ

φ₂，₁＝··ε

φ₂，₂＝··ζ

φ₂，₃＝··η

φ₂＝··φ

φ₃，₀＝··Γ

φ-0 : φ 0 ≡ Bin.φ

φ-0 = refl

φ-1-0 : φ 1 0 ≡ Γ

φ-1-0 = refl

φ-1-1 : φ 1 1 ≡ ε̇

φ-1-1 = refl

φ-1-2 : φ 1 2 ≡ ζ̇

φ-1-2 = refl

φ-1-3 : φ 1 3 ≡ η̇

φ-1-3 = refl

φ-1 : φ 1 ≡ φ̇

φ-1 = refl

φ-2-0 : φ 2 0 ≡ Γ̇

φ-2-0 = refl

φ-2-1 : φ 2 1 ≡ ε̈

φ-2-1 = refl

φ-2-2 : φ 2 2 ≡ ζ̈

φ-2-2 = refl

φ-2-3 : φ 2 3 ≡ η̈

φ-2-3 = refl

φ-2 : φ 2 ≡ φ̈

φ-2 = refl

φ-3-0 : φ 3 0 ≡ Γ̈

φ-3-0 = refl

定理 对于第一个参数为后继的情况, 我们对第二个参数分情况讨论, 由定义, 有以下等式成立.

φα⁺，₀＝fixpt λβ，φα，ᵦ 0

φα⁺，ᵦ⁺＝fixpt φα⁺，ᵦ

φα⁺，ₗᵢₘ g＝jump λγ，lim λn，φα⁺，g n γ

φ-suc-0 : φ (suc α) 0 ≡ fixpt λ β → φ α β 0

φ-suc-0 = refl

φ-suc-suc : φ (suc α) (suc β) ≡ fixpt (φ (suc α) β)

φ-suc-suc = refl

φ-suc-lim : φ (suc α) (lim g) ≡ jump λ γ → lim λ n → φ (suc α) (g n) γ

φ-suc-lim = refl

定理 对于第一个参数为极限的情况, 我们对第二个参数分情况讨论, 由定义, 有以下等式成立.

φα⁺，₀＝fixpt λβ，φα，ᵦ 0

φα⁺，ᵦ⁺＝fixpt φα⁺，ᵦ

φα⁺，ₗᵢₘ g＝jump λγ，lim λn，φα⁺，g ₙ γ

φ-suc-0 : φ (suc α) 0 ≡ fixpt λ β → φ α β 0

φ-suc-0 = refl

φ-suc-suc : φ (suc α) (suc β) ≡ fixpt (φ (suc α) β)

φ-suc-suc = refl

φ-suc-lim : φ (suc α) (lim g) ≡ jump λ γ → lim λ n → φ (suc α) (g n) γ

φ-suc-lim = refl

定理 对于第一个参数为极限的情况, 我们对第二个参数分情况讨论, 由定义, 有以下等式成立.

φₗᵢₘ f，₀＝jump λβ，lim λn，φ f ₙ，ᵦ 0

φₗᵢₘ f，ᵦ⁺＝fixpt φlim f，ᵦ

φₗᵢₘ f，lim g＝jump λᵧ，lim λn，φₗᵢₘ f，g ₙ γ

φ-lim-0 : φ (lim f) 0 ≡ jump λ β → lim λ n → φ (f n) β 0

φ-lim-0 = refl

φ-lim-suc : φ (lim f) (suc β) ≡ fixpt (φ (lim f) β)

φ-lim-suc = refl

φ-lim-lim : φ (lim f) (lim g) ≡ jump λ γ → lim λ n → φ (lim f) (g n) γ

φ-lim-lim = refl

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。