2013 Fiscal Year Research-status Report
| Project/Area Number |
24700012
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| Keywords | 計算効果 / モナド / 論理関係 / TT-lifting / エフェクトシステム / 国際研究者交流 |
|---|
| Research Abstract |
1. 2013年度の研究実績1において、エフェクトシステムの特徴的な部分に対応する圏論的構造を「半順序モノイドから自己関手のなすモノイダル圏へのモノイダル関手」として捉えた。以降この構造をパラメトリックエフェクトモナド(PEM)と呼ぶ。本年度は、エフェクトの観測と呼ばれる初等的なデータの組み合わせからPEMを構成する方法を与え，これを用いてPEMの具体例をいくつか構成した。この構成方法の特徴は、モナドとそれらの間の射というよく知られたデータから、エフェクトの定義とそれに付随するPEMの両方を同時に導くことができる点にある。PEMを手で構成するのはモナドよりも煩雑な作業になりがちだが、この構成方法を用いれば多くの具体例を簡単に構成することが可能となる。この研究成果と、2013年度の研究実績1を合わせたものをPrinciples of Programming Languages (POPL '14)にて発表した。
2. エストニア工科大学のUustalu氏と共同で、コモナドのためのTT-liftingの研究を行っている。Uustalu氏はタルトゥ大学のVene氏と共同でモナドの双対であるコモナドを用いた計算過程の表現を研究しており、Uustalu氏との議論の結果、コモナドのための論理関係の構成を検討することとなった。これに対し、TT-liftingのエッセンスを抽象化した後に圏論的な双対を取ることで、コモナドのための論理関係の構成方法を得られることが分かった。現在、この構成方法を用いてコモナドための論理関係を体系的に調べることを目指している。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
研究プロジェクト「一般的なエフェクトシステムの設計とその表示的意味論」は、基礎的な部分の研究が概ね完了した。このプロジェクトの成果はプログラミング言語理論に関するトップクラスの国際会議であるPOPLに採択され、良い評価を得ている。また、当初の研究計画には無かったものの、本研究の目的に合致することから昨年度は「モナド上の前順序」に関する研究プロジェクトに取り組み、これについても良い結果を得た。一方、研究計画に挙げた「再帰型が存在する状況での計算効果の比較問題」及び「モナドのためのパラメトリシティ原理の定式化とそのモデルの構成」についてはまだ研究が進んでいない。このため本研究の計画において掲げた三つの研究プロジェクトの遂行状況はやや遅れていると判断した。
|
| Strategy for Future Research Activity |
プログラムの実行時に起こる計算効果をより正確に捉えるため、様々なエフェクトシステムの拡張が提案されている。代表的な例として 1. エフェクトの表現力を高めるためにエフェクトに多相型を導入する拡張、2. 再帰のあるプログラムのエフェクトを見積もることができるよう、エフェクトに再帰を追加する拡張、の二つが挙げられる。次年度ではこれらの二つの拡張に対する表示的意味論を与えた後、TT-liftingを応用して一般的なエフェクト健全性を示す予定である。
また昨年度の推進方策に挙げられていた「再帰型が存在する状況での計算効果の比較問題」「論理関係の集まりの射影的極限による特徴づけ」に加えて、「コモナドの論理関係」に関する研究も推進する予定である。
|
| Expenditure Plans for the Next FY Research Funding |
研究費はおおむね予算通りに使用しているが、研究計画の遂行状況がやや遅れていることから、次年度の研究成果の発表に備えて使用額を残すこととした。
2014年4月にフランスのグルノーブルで開催されるワークショップMathematically Structured Functional ProgrammingにおいてTT-liftingに関する招待講演を行う予定であり、旅費として研究費を使用する。また、本年度の研究成果を発表するための旅費の他、コモナドの論理関係に関する共同研究のため、Uustalu氏の招聘に研究費を使用する予定である。
|
