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

点击翻译按钮获取中文摘要

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.