2016 Fiscal Year Research-status Report
関数型プログラミング言語の代数構造の解明：論理関係の数学的理論の構築に向けて
| Project/Area Number |
26730004
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
|
|---|
| Project Period (FY) |
2014-04-01 – 2018-03-31
|
| Keywords | 圏論的意味論 / 論理関係 |
|---|
| Outline of Annual Research Achievements |
ラムダ計算の研究において完全抽象性を満たす圏論的意味論を構成するという問題がある。この問題はすでにゲーム意味論を用いて解決されているが、ゲーム意味論以外の手法により完全抽象性を満たす圏論的意味論を構成することはより深いラムダ計算の理解につながり重要である。ラムダ計算に副作用を発生させるオペレーターを追加すると副作用を持たないラムダ計算にはない高階関数が得られることがあることは知られているのだが、完全抽象性を満たす圏論的意味論を構成するにはこのようなラムダ計算にはない高階関数をいかにして排除するかが問題である。前年度に構成した副作用を持つラムダ計算の圏論的意味論における副作用と論理関係の間の対応を観察しているなかで、論理関係を用いてラムダ計算の一種であるPCFに対する完全抽象性を満たす圏論的意味論を構成するための着想を得た。おおむねこの着想はうまく働いているように思われたが、実際に構成した圏論的意味論が完全抽象性を満たすことを証明しようとするとうまく議論が進まない点が幾つか現れてくる。現在、論理関係を用いた圏論的意味論の構成を含めた議論の修正を試みている。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
完全抽象性を満たす圏論的意味論の構成のための着想が当初の期待よりも機能していなかったため。
|
| Strategy for Future Research Activity |
引き続き、これまでの研究から得られた着想を基に論理関係を用いた完全抽象性を満たす圏論的意味論の構成を目指し議論の修正を行っていく。
|
| Causes of Carryover |
現在の研究が想定よりも進行せず、研究成果発表のための旅費を使用しなかったため。
|
| Expenditure Plan for Carryover Budget |
研究成果発表のための旅費として使用予定。
|
