A constructive manifestation of the Kleene-Kreisel continuous functionals
A constructive manifestation of the Kleene-Kreisel continuous functionals
复制标题
Kleene-Kreisel 连续泛函的建设性表现
DOI：
10.1016/j.apal.2016.04.011
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Chuangjie Xu
中科院分区：
文献类型：
--
作者：
M. Escardó;Chuangjie Xu
我们确定了另一个类别相当于Kleene-Kreisel连续泛函。通过构造性和谓词性的推理，从康托空间到自然数的所有函数在这一范畴内都是一致连续的。我们不需要假设Brouwerian连续性公理来证明这一点，但是，如果我们这样做，那么我们可以证明全类型层次等价于我们的连续泛函的表现。我们在一个具体层的范畴内构造这种表现，称为C-空间，它形成了一个局部的Carnival闭范畴，因此可以用来模拟系统T和依赖类型。我们证明了这一范畴具有一个泛函，并验证了这些理论中的一致连续性原理。我们的发展是在非正式的建设性数学，沿着主教数学的路线。然而，为了从我们的构造中提取具体的计算内容，我们在内涵的Martin-Löf类型理论中，在Agda符号中将其形式化，并在本文的最后讨论其主要技术方面。
We identify yet another category equivalent to that of Kleene–Kreisel continuous functionals. Reasoning constructively and predicatively, all functions from the Cantor space to the natural numbers are uniformly continuous in this category. We do not need to assume Brouwerian continuity axioms to prove this, but, if we do, then we can show that the full type hierarchy is equivalent to our manifestation of the continuous functionals. We construct this manifestation within a category of concrete sheaves, called C-spaces, which form a locally cartesian closed category, and hence can be used to model system T and dependent types. We show that this category has afan functionaland validates the uniform-continuity principle in these theories. Our development is within informal constructive mathematics, along the lines of Bishop mathematics. However, in order to extract concrete computational content from our constructions, we formalized it in intensional Martin-Löf type theory, in Agda notation, and we discuss the main technical aspects of this at the end of the paper.