| 研究課題/領域番号 |
15K00015
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
立木 秀樹 京都大学, 人間・環境学研究科, 教授 (10211377)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2020-03-31
|
| キーワード | プログラム抽出 / 並列計算 / グレイコード / 表現空間 / コンパクト集合 |
|---|
| 研究実績の概要 |
並列な計算に対応する論理体系である 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 と関係した概念の計算可能性についても成果を得ることができた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
二つの国際的な共同研究において，多くの発見を行い，理論の構築がすすんだ。両方とも，論文にまとめる作業を進行している。
|
| 今後の研究の推進方策 |
それぞれの研究において，これまでの成果を論文にまとめたい。また，CFP の計算機での実現などについて考えたい。
|
| 次年度使用額が生じた理由 |
海外出張を予定していた先の共同研究者が，先方の研究費で来日してくれた。新しい年度の旅費として使用したい。
|
