2017 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 | プログラム抽出 / 並列計算 / グレイコード / 表現空間 / コンパクト集合 |
|---|
| Outline of Annual Research Achievements |
並列な計算に対応する論理体系である CFP を構成し，CFPにおける形式的な証明からプログラムを抽出する研究を推し進めた。グレイコード上の計算は，ボトムを避けながら計算を行うために，並列処理が必要となる。CFPは，そのような並列処理を行うプログラムの入出力関係を表現し，推論できる論理である。それは，IFP という，演算子の最小不動点，最大不動点を基本演算とする論理に対し，停止性の条件を表現する演算子と並列実行を表現する演算子を追加した体系としてつくられる。これらの演算子に対応する realizer の規則を導き，その CFP の証明から，Amb オペレータで並列拡張された関数型言語のプログラムが得られることを示した。具体例として，グレイコードと純グレイコード，それに，符合付き二進表現の間の変換を行うプログラムを抽出した。
コンパクト集合のT-^omega表現について研究をすすめた。この表現を構成するために，Proper computable dyadic subbase を使用するが，Proper computable dyadic subbase が Computable metric space 一般において存在することが示せた。これにより，Computable metric space において，有限集合の濃度とボトムの個数が対応する matching representation を構成できることが分かった。また，Proper computable dyadic subbase を用いた matching representation の構成において，今まで研究してきた，Proper dyadic subbase が導出するドメイン表現の理論を応用することができた。proper computable dyadic subbase と関係した概念の計算可能性についても成果を得ることができた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
二つの国際的な共同研究において，多くの発見を行い，理論の構築がすすんだ。両方とも，論文にまとめる作業を進行している。
|
| Strategy for Future Research Activity |
それぞれの研究において，これまでの成果を論文にまとめたい。また，CFP の計算機での実現などについて考えたい。
|
| Causes of Carryover |
海外出張を予定していた先の共同研究者が，先方の研究費で来日してくれた。新しい年度の旅費として使用したい。
|
