2003 Fiscal Year Annual Research Report
| Project/Area Number |
13480084
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
高橋 大輔 早稲田大学, 理工学部, 助教授 (50188025)
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046)
山本 章博 京都大学, 情報学研究科, 教授 (30230535)
|
|---|
| Keywords | 形式的証明 / 形式的技法 / 学習理論 / 極限計算 / 非構成的論理 |
|---|
| Research Abstract |
本年も数々の新知見を得たが、特筆すべきは、LCM階層の完全な決定と、LCMゲームの発見である。
LCM階層の構造は、すでに分かっていたが、その詳細な理論の整備、特にprenex normal formへの変換アルゴリズム、階層性の証明の詳細などは未完成のままであった。これを林、Kohlenbach, Berardi(2名とも海外共同研究者),赤間のチームで完成した。この成果は、IEEELICS'04に投稿中である。この研究の途中、分配法則が階層において重要な役割を果たすことが発見された。これはE.Martinが指摘していた、LCMとconstant domainのKrike意味論との関係の糸口となる可能性がある。
もう一方のLCMゲームとは、LCM意味論の親の親とでも言うべき、Coquandのゲーム意味論のバックトラッキングを、浅いバックトラックのみに制限することによって得られるゲーム意味論が、丁度、LCM意味論に対応するという発見である。ゲーム意味論は、prenex normal formに制限されているので、一般的な問題にこれを適用することはできないが、多くの現実的命題は、prenex normal formに変換可能であるため、これをつかって、懸案であるproof animationをよりよく実現できる可能性も開けてきた。
この他に、Berardiによる、Dickson lemmaの研究、Degree2のcalibration、本研究の一貫としてドイツより招いたBrattkaによるΔ1計算可能解析学、および、Kohlenbachの学生Toftdalによる解析学のcalibrationなど、calibration関係が着実に進化を始めたのも大きな成果である。
|
