Computability and Complexity in Constructive Mathematics

从2003年到2006年，我们对建构性数学中的可计算性和复杂性进行了为期4年的研究。在研究过程中，我们对这一课题有了一些重要的、更好的认识。其中最重要的理解之一是，在更一般的建构性逆向数学框架内，可以更好地处理建构性数学中的可计算性和复杂性。此外，构造性数学的发展，如构造性数学中的构造性集合论和拓扑学，也在构造性数学的可计算性和复杂性以及构造性逆数学中产生了新的问题。我们用Josef Berger博士研究了Brouwer的Fan定理和弱Koenig引理之间的关系，以及这些定理中的可计算性。与Peter Aczel教授、Laura Crosilla博士、Erik Palmgren教授和Peter Schuster副教授一起，我们处理了建设性Zermelo-Fraenkel集合论中的建设性逆数学问题。关于构造性数学中的拓扑学，我们与Erik Palmgren教授一起研究了构造性集合论和类型论中的商拓扑构造，并与Ray Mines教授、Peter Schuster副教授和Lumita Vita博士一起研究了拟分离性和邻域空间。此外，我们还讨论了实数构造论中的计算复杂性和构造性中间值定理，以及F-空间中Banach逆映射定理的构造性形式作为Baire定理的应用。进一步的研究项目是随着构造性数学如构造性集合论和构造性拓扑学的发展而推进构造性逆数学的研究。

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.