Computability and Complexity in Constructive Mathematics

从2003年到2006年，我们用4年的时间对构造数学中的可计算性和复杂性进行了研究。在研究过程中，我们对这个问题有了一些重要的和更好的理解。最重要的理解之一是，构造数学中的可计算性和复杂性可以在构造逆数学的更一般的框架内得到更好的处理。此外，构造数学的进步，如构造集论和构造数学中的拓扑，在构造数学中的可计算性和复杂性以及构造逆数学中产生了新的问题。在这个研究项目中，我们提出了一个新的构造性逆数学框架。我们与Josef Berger博士一起研究了browwer扇形定理与弱Koenig引理之间的关系，以及这些定理的可计算性。我们与Peter Aczel教授、Laura Crosilla博士、Erik Palmgren教授和Peter Schuster副教授一起，讨论了建构性Zermelo-Fraenkel集合论中的一个建构性逆数学问题。在构造数学拓扑方面，我们与Erik Palmgren教授合作研究构造集论和类型论中商拓扑的构造，与Ray Mines教授、Peter Schuster副教授和Luminita 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.