Computability and Complexity in Constructive Mathematics

从2003年到2006年，我们对构造数学的可计算性和复杂性进行了四年的研究。在研究过程中，我们对这一课题有了一些重要的认识。最重要的理解之一是，构造性数学中的可计算性和复杂性可以在构造性逆向数学的更一般框架内更好地处理。此外，随着构造性数学的发展，如构造性数学中的构造集合论和拓扑学，在构造性数学的可计算性和复杂性以及构造性逆数学中产生了新的问题，在本研究项目中，我们提出了一个新的构造性逆数学框架。本文研究了Brouwer扇定理与弱Koenig引理之间的关系，以及这些定理的可计算性。与Peter Aczel教授、Laura Crosilla博士、Erik Palmgren教授和Peter Schuster副教授一起，我们处理了构造性Zermelo-Fraenkel集合论中的构造性逆向数学问题。关于拓扑结构在建设性数学，我们曾在建设性的集理论和类型理论的商拓扑结构，与埃里克Palmgren教授，并在准apartness和邻域空间，与雷矿山教授，副教授彼得舒斯特和博士Luminita维塔。在此基础上，我们讨论了真实的数的构造性理论和构造性中值定理的计算复杂性，以及作为Baire定理应用的F-空间中的Banach逆映射定理的构造性版本，进一步的研究计划是随着构造性数学如构造性集合论和构造性拓扑学的进展，推进构造性逆数学的研究。

From 2003 to 2006, for 4 years, we have done a research on computability and complexity in constructive mathematics. During the research, we have got some important and better understandings on the subject. One of the most important understanding is that computability and complexity in constructive mathematics can be dealt with better within a more general framework of constructive reverse mathematics. Moreover, progress in constructive mathematics, such as constructive set theory and topology in constructive mathematics, has produced new problems in computability and complexity in constructive mathematics, and in constructive reverse mathematics.In this research project, we have proposed a new framework of constructive reverse mathematics. We have investigated relationship between Brouwer's fan theorem and weak Koenig's lemma, with Dr. Josef Berger, and computability in these theorems. With Professor Peter Aczel, Dr. Laura Crosilla, Professor Erik Palmgren, and Associate Professor Peter Schuster, we have dealt with a problem of constructive reverse mathematics in the constructive Zermelo-Fraenkel set theory. Concerning topology in constructive mathematics, we have worked on constructions of quotient topologies in constructive set theory and type theory, with Professor Erik Palmgren, and on quasi-apartness and neighbourhood spaces, with Professor Ray Mines, Associate Professor Peter Schuster and Dr. Luminita Vita. Furthermore, we have treated computational complexity in constructive theory of real numbers and the constructive intermediate value theorem, and a constructive version of Banach's inverse mapping theorem in F-spaces as an application of Baire's theorem.Further research project is putting research in constructive reverse mathematics forward with progress in constructive mathematics such as constructive set theory and constructive topology.