Subrecursive Realizability Interpretation for Intuitionistic Arithmetic

研究数学的可计算性和复杂性已经形成了一个涉及计算机科学和数学的跨学科研究领域，并将在世纪内成为一个重要的研究领域，因为数学为科学和工程提供了基础，而我们社会中信息技术的快速发展将迫使计算机科学使基础成为可计算的。特别是构造性数学将在这一领域发挥重要作用，因为Curry-Howard对应，即“证明作为程序”，在构造性逻辑中成立。该项目的目的是通过构造性数学的可实现性解释来澄清分析提取程序的计算复杂性的问题。（直觉）算术;描述算术系统，我们可以从中提取某些复杂性类的程序，例如多时间可计算函数类，然后找到解决问题的方法。虽然在项目期间，我们可以在这个问题上有一些重要的结果，包括一个很好的多时间函数的特征，我们留下了一个困难的问题，如何整合这些结果分布在各个领域，如建设性数学，数理逻辑，可计算性理论，计算复杂性等，成为一个系统的理论。

Investigating computability and complexity in mathematics has been forming an interdisciplinary research area involving computer science and mathematics, and will be an important research area within a century since mathematics provides science and engineering with basics and rapid progress of information technology in our society will force computer science to make the basics computable. Especially constructive mathematics will play an important role in the area, as the Curry-Howard correspondence, that is "Proofs as Programs", holds in constructive logic.The project started with the aim of clarifying problems onanalyzing computational complexity of extracted programs by realizability interpretation for constructive (intuitionistic) arithmetic ;characterizing arithmetical systems from which we can extract programs in certain complexity class, for example the class of polytime computable functions,and then finding solutions for the problems. Although during the period of the project, we could have some important results on the subject, including a nice characterization of polytime functions, we have left a difficult problems of how to integrate these results spreading over varieties of fields, for examples constructive mathematics, mathematical logic, computability theory, computational complexity and so on, into a systematic theory.