论文标题
在Baire类别定理的计算属性上
On the computational properties of the Baire Category Theorem
论文作者
论文摘要
计算性理论是计算机科学与数学逻辑交集的学科，其中基本问题是： 给定两个数学对象x和y，x原理计算y吗？ 如果X和Y是实数，Turing的著名“机器”模型为此问题提供了“计算”的标准解释。为了使涉及（总）抽象对象的计算形式化，克莱恩介绍了他的S1-S9计算方案。反过来，DAG NORMANN和作者引入了lambda微积分的版本，涉及固定点运算符，该固定点运算符准确捕获S1-S9并容纳部分对象。在本文中，我们使用这种新模型来开发由于Baire和Volterra和相关结果而引起的各种知名定理的可计算理论。这些定理仅需要基本的数学概念，例如连续性，开放集和密度。我们表明，从我们的新模型的角度来看，由于Baire和Volterra引起的这些定理在计算上是相当于的，有时在Goedel的T的相当驯服的片段中起作用。
Computability theory is a discipline in the intersection of computer science and mathematical logic where the fundamental question is: given two mathematical objects X and Y, does X compute Y in principle? In case X and Y are real numbers, Turing's famous 'machine' model provides the standard interpretation of 'computation' for this question. To formalise computation involving (total) abstract objects, Kleene introduced his S1-S9 computation schemes. In turn, Dag Normann and the author have introduced a version of the lambda calculus involving fixed point operators that exactly captures S1-S9 and accommodates partial objects. In this paper, we use this new model to develop the computability theory of various well-known theorems due to Baire and Volterra and related results; these theorems only require basic mathematical notions like continuity, open sets, and density. We show that these theorems due to Baire and Volterra are computationally equivalent from the point of view of our new model, sometimes working in rather tame fragments of Goedel's T.
