| 研究課題/領域番号 |
13480084
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| 研究分担者 |
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
高橋 大輔 早稲田大学, 理工学部, 教授 (50188025)
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 助教授 (10211046)
山本 章博 北海道大学, 大学院・工学研究科, 助教授 (30230535)
|
|---|
| キーワード | 形式的証明 / 形式的技法 / 学習理論 / 極限計算 / 非構成的原理 |
|---|
| 研究概要 |
秋になっての追加採択であったものの、十分な準備があったため、短期間の間に科研費を活用して多くの成果を上げることができた。特筆すべきは、次の点である。
1.北大における1月のワークショップを皮きりとして、学習理論のグループとの交流が始まり、新知見が多く得られた。一例として、E.Martin (New South Wales大学,研究組織外)と山本、および林の共同研究により、RichPrologによるLCM実装の可能性が明らかになり、山本とMartinが、Diksonのlemmaを実装した。これらの交流を通して、学習理論とLCMの相違点も明らかになった。例えば、現在までに発見されているLCMの極限計算は「単調」であり、学習としては特殊であることが、Martinにより指摘された。また、相違点の一つを計算複雑度論的証明論で埋めるという計画が提案された。
2.Berardiと赤間の共同研究により、両者の極限構成の違いと同一点が明らかにされた。
3.赤間と林の共同研究により、赤間のCombinatory algebraの極限構成を利用してCCCの極限構成法が完成された。これは、型理論へのLCMの拡張の最初の例である。
4.石原、Kohlenbach、八杉、林、および、山崎(大阪府立大学,研究組織外)の共同研究により、非構成的原理のcalibration理論(非構成的原理の逆数学と呼んでいたもの)の基礎がほぼ固まってきた。特にcalibrationを行うための、基礎形式系と、非構成的原理の第2階の定式化が得られ、また、非構成的原理と等価な数学定理の候補が数多く発見された。
|
