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

用类型论方法研究证明论和计算理论

• 批准号: 12640107
• 负责人: TAKAHASHI Masako
• 金额: $ 1.6万
• 依托单位: College of Liberal Arts, International Christian University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2000
• 资助国家: 日本
• 起止时间: 2000 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-12640107/
• 关键词: theory of computation; binary tree; recursive functions; primitive recursive functions; computable tree functions; 万能コンピュータ; コンピュータの歴史; 数理論理学の歴史; 型理論; 証明論; 項代数; 原始帰納法; 計算可能性; 二分木上の関数; 木構造を扱うアルゴリズム

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.

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.

项目成果

M.Takahashi: "Lambda-representable functions over term algebras"International J.of Foundations of Computer Science. Vol.12. 3-29 (2001)

M.Takahashi：“术语代数上的 Lambda 可表示函数”International J.of Foundations of Computer Science。

高橋 正子: "論理学の歴史とコンピュータ"数理解析研究所講究録. Vol.1286. 85-100 (2002)

Masako Takahashi：“逻辑和计算机的历史”数学分析研究所的 Kokyuroku Vol.1286（2002）。

Masako Takahashi: "Lambda-representable functions over term algebras"Int. Journal of Foundations of Computer Science. Vol.12. 3-29 (2001)

Masako Takahashi：“代数上的 Lambda 可表示函数”Int。

M.Takahashi: "History of logic and computers (in Japanese)"lecture Notes in RIMS. Vol.1286. 85-100 (2002)

M.Takahashi：RIMS 中的“逻辑和计算机史（日语）”讲义。

G.Pogosyan: "Classes of Boolean Functions defined by functional terms"Multiple valued Logic. Vol.7. 417-448 (2003)

G.Pogosyan：“由功能术语定义的布尔函数类”多值逻辑。