A study of proof theory and theory of computation in a type-theoretical approach

首先，为了研究二叉树上可计算函数的结构，我们通过两种不同的方式扩展了自然数上递归函数的概念，定义了两类递归函数，并定义了二叉树上While-程序中可计算的函数类。然后，通过二叉树和自然数之间的标准编码函数，证明了这些类与自然数上递归函数的共轭类重合。我们还研究了当改变编码函数时会发生什么，并给出了编码函数满足上述性质的充要条件。大体上说，这意味着在研究树函数的可计算性时，是否依靠经典的方法通过编码函数(从二叉树到自然数)将问题归结为数值函数的可计算性，或者是否应用递归树函数的新概念是无关紧要的，只要选择的编码函数是正确的。在研究上述可计算函数时，我们注意到在研究可计算性的早期，人们之所以关注自然数作为一种独特的数据结构，是因为在1930年的S时代，还没有计算机，也不需要被复杂的数据结构所困扰，因为没有人用编程语言编写程序来处理各种数据结构。但现在，人们对计算机有很多经验，他们用各种语言编写程序，为处理各种数据结构提供了工具。在这方面，我们一直致力于计算理论的适当“现代化”。

First, in order to investigate the structure of computable functions over binary trees, we define two classes of recursive funftions by extending the notion of recursive functions over natural numbers in two different ways, and also define the class of functions computable in while-programs over binary trees. Then we show that those classes coincide with the class of conjugates of recursive functions over natural numbers via a standard coding function between binary trees and natural numbers. We also study what happens when we change the coding function, and present a necessary and sufficient condition for a coding function to satisfy the property above mentioned.Roughly speaking, this means that in studying computability of tree functions, whether one relies on the classical way to reduce the problem to the computability of numeric functions via a coding function (from binary trees to natural numbers) or whether one applies the new notion of recursive tree functions is immaterial, as long as the coding function one chooses is a right one.While working on computable functions as mentioned above, we noticed the fact that in the early days of investigation of computability, people were concerned with natural numbers as the unique data structure, because in 1930's there was no computers, and no need to be bothered by complex data structures, since there was no one who wrote programs in programming languages which provide facilities to handle various data structures. But nowadays people have a lot of experiences with computers, and write programs in various languages which provide tools for handling various data structures. In this respect, we have been working on what would be a suitable "modernization" of theory of computation.