形式化大数数学（1.2-Veblen函数）一 (5-3)

·η＝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)

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。