Logic of Limit Computing and its Applications
Project/Area Number 
13480084

Research Category 
GrantinAid for Scientific Research (B)

Allocation Type  Singleyear Grants 
Section  一般 
Research Field 
計算機科学

Research Institution  Kobe University 
Principal Investigator 
HAYASHI Susumu Kobe University, Computers and Systems Engineering, Professor, 工学部, 教授 (40156443)

CoInvestigator(Kenkyūbuntansha) 
YASUGI Mariko Kyoto Sangyo University, Computer Science, Professor, 理学部, 教授 (90022277)
TAMURA Naoyuki Kobe University, Information center, Professor, 学術情報基盤センター, 教授 (60207248)
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
高橋 大輔 早稲田大学, 理工学部, 助教授 (50188025)
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046)
山本 章博 京都大学, 情報学研究科, 教授 (30230535)

Project Period (FY) 
2001 – 2003

Project Status 
Completed (Fiscal Year 2003)

Budget Amount *help 
¥4,100,000 (Direct Cost: ¥4,100,000)
Fiscal Year 2003: ¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2002: ¥2,000,000 (Direct Cost: ¥2,000,000)

Keywords  Inductive inference / mathematical logic / classical proof execution / 形式的証明 / 形式的技法 / 学習理論 / 極限計算 / 非構成的論理 / 非構成的原理 
Research Abstract 
The fundamental theory of Limit Computable Mathematics (LCM) were founded and many new results have been obtained in the project. The followings are the main results among them : 1. Improved realizability interpretations for LCM 2. sublearning hierarchy 3. LCM game 4. the arithmetical hierarchy 5. LCM categories 6. Computability in analysis in the light of LCM. Computability theory of discontinuous functions 7. Models of Delta02 maps by means of concurrent computation Among them, the discovery of sublearning hierarchy is quite important. Below the hierarchy of LEM (the laws of excluded middle), principles corresponding to LLPO of constructive mathematics exist and they are related to WKL (Weak Koenig Lemma). This fact has been conceived by some researchers intuitively. By establishing computational and learning theoretic meanings of this fact, we finally explored the position of WKL in the hierarchy of LCM. We found that the principle represents the limit computational model of Popperian game of nondeterministic computation of refutability by finite numbers of processes. The full arithmetical hierarchy of LCM including this sublearning hierarchy was fully explored. This was done through various techniques of mathematical logic, and it is important also from mathematical point of view. The calibration theory according to this hierarchy has been started by a researcher out of our project. We also found that Coquand's game semantics could be restricted in a very natural way so that it coincides with LCM.

Report
(4 results)
Research Products
(11 results)