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

目录

形式化大数数学（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]β)

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