关于Baire范畴定理的一致计算内容

我们研究了Weihrauch格中Baire范畴定理不同版本的一致计算内容。Baire范畴定理可看作一种鸽巢原理，其陈述为一个完备（即“大”）度量空间不能被分解为可数个无处稠密的（即“小”）子集。Baire范畴定理是一个说明性的例子，表明一个经典定理可以有若干不同的计算解释。首先，我们区分了该定理的两个不同逻辑版本，其中一个可视为另一个的逆否形式。第一个版本旨在给定一列无处稠密的闭集时，在空间中发现一个未被覆盖的点。第二个版本旨在给定覆盖空间的一列闭集时，找出某个在某处稠密的闭集的索引。尽管这些版本背后的两个陈述在经典逻辑中彼此等价，它们在直觉逻辑中并不等价，同样在Weihrauch格中表现出不同的计算行为。除了这一逻辑区分，我们还考虑了闭集序列被“给出”的不同方式。本质上，我们可以区分关于闭集的肯定信息与否定信息。我们讨论了由此产生的Baire范畴定理的全部四个版本。有些令人惊讶的是，提供输入信息的差异也可以用跳跃操作来表达。最后，我们还将Baire范畴定理与泛性和可计算余贫集的概念联系起来。