2018 Fiscal Year Research-status Report
| Project/Area Number |
15K00015
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| Project Period (FY) |
2015-04-01 – 2020-03-31
|
| Keywords | IFP / コンパクト集合 / T^omega / 計算可能解析学 / プログラム抽出 |
|---|
| Outline of Annual Research Achievements |
コンパクト集合の T^omega 表現についての研究をより精密化した。コンパクト集合の T^omega 表現の hereditary, faithful, matching representation などの性質を整理し，Proper Dyadic subbase との関係性を明確にした。最終的に，computably compact computable metric space のコンパクト集合全体は，faithful な T^omega 表現を持つという形の主定理が得られた。それ以外にも，証明や論文の手直しを行い，論文誌への投稿を行なった。
IFP について研究を進めた。IFP は，一階述語論理に最小不動点，最大不動点として述語を定義する機能を付け加えた論理体系であり，抽象的な数学の証明からプログラムを抽出することができる。IFP は，これまでのプログラム抽出のための論理体系とは異なり，計算的な対象とはならない数学的対象の上で量化子を行なうことができる。このことを用いて，部分関数を意味するプログラムを抽出することが可能となり，その応用としてグレイコードを出力するプログラムを数学的証明から抽出することができる。IFP において抽出されたプログラムが正しく動くことの証明は，Adequacy theorem を経由して証明される。IFP の無限的部分計算の機能に合致した adequacy theorem を，induction, coinduction という IFP の枠組みに沿った形で行なった。また，この意味論を CFP のプログラムの実行の正しさとつなげるための研究も行なった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
一つの研究で得られた結果を投稿し，研究に区切りをつけることができた。
もう一つの研究も，CFP のベースとなる IFP に関して研究する中で，IFP と非決定的な計算との関係が明確になり，意味論の展開ができるなどいい結果が出た。これは，論文として投稿間近な状態になっている。
|
| Strategy for Future Research Activity |
IFP に関する論文を完成させること，CFP に関する研究を深めること，IFP を応用した研究の可能性を探ることを，共同研究者とともに行なっていきたい。
|
| Causes of Carryover |
共同研究者との間で予定してた形で出張ができなかった。次年度にその分の出張を行いたい。
|
