单叶类型论中的部分函数与递归
Partial Functions and Recursion in Univalent Type Theory
摘要：
我们调查部分功能和可计算性理论从一个建设性的，单叶类型论。重点是将可计算性置于更大的数学背景下，而不是可计算性理论的完整发展。我们开始处理部分功能，使用的概念，这是用于合成域理论讨论类部分地图的优势。我们将这个和其他想法从合成域理论的其他方法，以消除类型论。我们表明，优势的概念是很难适用于我们的设置：一套$Σ_0^1$命题Rosolini调查形成一个优势，如果一个弱的，但仍然无法证明，选择原则持有。为了解决这个问题，我们提出了另一种部分函数的概念，我们称之为纪律映射。在可数选择存在的情况下，这个概念与罗索利尼的一致。使用部分函数的一般概念，我们在构造性可计算性理论中迈出了第一步。我们既把可计算性作为结构来做这件事，在这里我们可以直接存取程序;又把可计算性作为属性来做这件事，在这里我们必须以程序不变的方式工作。我们展示了这两种方法之间的差异，通过展示这些方法如何与拓扑理论和类型理论的关注所产生的可计算性理论的事实。最后，我们把这两条线索联系在一起：假设可数选择和所有全函数$\mathbb{N}\to\mathbb{N}$都是可计算的（这两个都在有效拓扑中成立），那么Rosolini部分函数、有纪律的映射和可计算的部分函数都是重合的。然而，我们观察到，所有部分函数的类包括不可计算的部分函数。
英文摘要：
We investigate partial functions and computability theory from within a constructive, univalent type theory. The focus is on placing computability into a larger mathematical context, rather than on a complete development of computability theory. We begin with a treatment of partial functions, using the notion of dominance, which is used in synthetic domain theory to discuss classes of partial maps. We relate this and other ideas from synthetic domain theory to other approaches to partiality in type theory. We show that the notion of dominance is difficult to apply in our setting: the set of $Σ_0^1$ propositions investigated by Rosolini form a dominance precisely if a weak, but nevertheless unprovable, choice principle holds. To get around this problem, we suggest an alternative notion of partial function we call disciplined maps. In the presence of countable choice, this notion coincides with Rosolini's. Using a general notion of partial function, we take the first steps in constructive computability theory. We do this both with computability as structure, where we have direct access to programs; and with computability as property, where we must work in a program-invariant way. We demonstrate the difference between these two approaches by showing how these approaches relate to facts about computability theory arising from topos-theoretic and type-theoretic concerns. Finally, we tie the two threads together: assuming countable choice and that all total functions $\mathbb{N}\to\mathbb{N}$ are computable (both of which hold in the effective topos), the Rosolini partial functions, the disciplined maps, and the computable partial functions all coincide. We observe, however, that the class of all partial functions includes non-computable partial functions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
