完全分离的类型
Compact totally separated types
浏览论文内容
中文总结 AI 辅助
本文利用拓扑学构造可有限时间穷尽搜索的无限类型（紧致类型），通过两种序数记号系统（Brouwer编码及其推广）衡量其逻辑复杂性，并证明相关性质在构造性设置中的限制，扩展至Martin-Löf类型论并形式化于Agda。
中文摘要 AI 辅助
也许令人惊讶的是，存在可以在有限时间内机械地穷尽搜索的无限类型。我们使用拓扑学的思想来构造大量这样的类型，将可搜索的类型称为紧致类型，并使用序数来衡量其逻辑复杂性。我们考虑两种序数记号系统，在这两种系统下，一个记号同时表示一个离散序数和一个紧致序数，并且前者到后者的嵌入的像具有空补集。一个布尔值函数决定嵌入的像中的哪些点是孤立的，哪些点是拓扑极限点。第一个系统由传统的Brouwer编码组成，第二个是推广它们的归纳-递归宇宙。如此获得的离散序数是三分法的，而紧致序数对于补集子集具有最小元性质，但这两个理想性质在构造性设置中不能同时满足。从Brouwer编码获得的序数进一步享有布尔莱布尼茨原理，其拓扑对应物是完全分离性的概念。这扩展了先前从Gödel的system T到具有单值宇宙的内涵Martin-Löf类型论的工作，并在TypeTopology仓库中以Agda形式化。
英文摘要
Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel's system T to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.
