序数的类型论方法

在构造性设定中，序数的任何具体表述都无法同时具备人们可能感兴趣的所有性质；例如，能够计算序列的极限在构造性上与判定外延相等性不相容。我们以同伦类型论(homotopy type theory)为基础设定，发展了序数理论的抽象框架，并建立了一系列期望的性质与构造。随后我们研究并比较了同伦类型论中三种具体的序数实现：第一，基于康托尔范式(Cantor normal forms，即二叉树)的记号系统；第二，布劳威尔树(Brouwer trees，即无穷分支树)的精炼版本；第三，外延良基序(extensional well-founded orders)。我们的三种表述都具有序数所期望的核心性质，例如配备外延且良基的序关系以及允许基本算术运算，但它们在额外所能实现的功能上有所不同。例如，对于有限序数集合，康托尔范式具有可判定的性质，但无穷集合的上确界无法计算。相比之下，外延良基序能很好地处理无穷集合，但几乎所有性质都不可判定。布劳威尔树取二者之中道，将受限的可判定性与处理无穷递增序列的能力结合起来。我们的三种方法通过从“更可判定”到“较不可判定”概念的标准保序函数相连。我们已在cubical Agda中形式化了关于康托尔范式和布劳威尔树的结果，而外延良基序已由Escardo及其合作者深入研究和形式化。最后，我们将自身实现的计算效率与Berger所报告的结果进行了比较。