| 研究課題/領域番号 |
24700012
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | モナド / 論理関係 / 計算効果 / TT-lifting |
|---|
| 研究概要 |
1. 一般的なエフェクトシステムの設計とその表示的意味論に関する研究を行った。プログラミング言語の表示的意味論を与えるには、言語と圏論の間の良く知られた対応関係(Curry-Howard-Lambek対応)に従い、言語の持つ構造に対応した圏論的構造を特定するのが自然である。本研究ではエフェクトシステムの特徴的な部分に対応する圏論的構造を「半順序モノイドから自己関手のなすモノイダル圏へのモノイダル関手」として特定し、その基本的な性質と構成方法を与えた。また、TT-liftingを拡張することでエフェクトシステムの健全性を示すことに成功した。本研究で得たエフェクトシステムのための圏論的構造は既知のものよりも一般的であり、しかも継続モナドに似た構成を許している点が新しく、広い応用が見込まれる。これらの研究成果は2012年12月、京都で開催された国際会議APLAS 2012にてポスター形式で発表した。
2. 京都大学数理解析研究所博士後期過程の佐藤哲也氏と共同で、モナド上の前順序に関する研究を行った。我々はTT-liftingがモナド上の前順序の構成に応用できること、そしてこの構成の普遍性を用いてモナド上の前順序全体が射影的極限となることを示した。モナド上の前順序は自然な概念であり、実例も豊富に存在するが、それらを系統的に構成し、定性的に調べる研究は皆無であった。従って本研究は圏論の基礎的な部分に対して新しい知見を与えたといえる。本研究の成果をまとめた論文は2013年3月、ローマで開催された国際会議FoSSaCS 2013に採択され、EATCS Best Paper Awardの候補となった他、佐藤哲也氏はBest Student Contribution Awardを受賞した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究成果1は平成24年度の研究計画に沿ったものである。今後、研究成果をまとめた論文を国際会議に投稿して発信する予定である。研究成果2は状態遷移系の間の模倣関係の定式化と密接な関係があり、「プログラム(=システム)の複雑な振る舞いを分析する」目的に応用できる。従って、本研究の進展に対して予定外の貢献を与えている。
|
| 今後の研究の推進方策 |
今後は研究プロジェクト(b)の「再帰型が存在する状況での計算効果の比較問題」について取り組む。まず準備として、計算効果の存在しない状況において、再帰型の論理関係を構成するのに十分な圏論的状況を特定する。これについては、最小不変性を満たす再帰型の存在する圏と、その上のファイブレーションが適切なものであると想定している。次に、この状況において意味論的TT-liftingが可能であることを調べ、計算効果の比較問題の理論を展開する。
このプロジェクトに加え、本研究の目的を達成する上でTT-liftingに関する基礎的な性質を明かにすることは重要であると考えている。この考えに従い、研究成果2を発展させ、モナド上の論理関係に対する新たな特徴付けを得ることを目指す。具体的には、モナド上の論理関係の集まりがある種の図式の射影的極限となっていることを示す予定である。さらに、この結果を、モナド上の論理関係の数え上げに応用する予定である。
|
| 次年度の研究費の使用計画 |
平成25年度には研究成果1と、研究成果2を発展させたものを海外において発表することを予定している他、エストニア国タリン大学のTarmo Uustalu氏との研究打ち合わせの予定がある。それらの旅費を確保するため、平成24年度の研究費の使用を少し抑え、平成25年度に用いるようにした。
|
