2014 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 |
ラムダ計算の操作的意味論や抽象機械など多くの関数型プログラミング言語の計算モデルの代数構造をbasic combinatorial object (BCO)を用いて記述することでその後の論理関係の研究の基盤を構築することを目指した。本研究の目的を遂げる上での問題点の一つは既存のBCOからなる２－圏の2-cellが半順序で与えられていることである。BCOの具体例について考えると、本研究の目的を達するためにはこのことは既存のBCOの定義が荒いものであるということができる。そこで既存のBCOからなる2-圏の定義を精密化することが本研究における第一ステップである。ところで本研究課題とは直接の関係がないが東京大学の蓮尾一郎氏らとの共同研究でGeometry of Interaction (GoI)を用いた副作用を持つラムダ計算の圏論的モデルの構成に関する研究を行ったが、その研究において「副作用をもつBCO」から論理関係の手法によって副作用を持つラムダ計算の圏論的モデルを構成した。副作用に対する圏論的モデルの構成にはmonadを考えることが基本的であるが、この共同研究では２つのBCOを考え一方から他方への射（ここでは既存のBCOの定義の意味で）がある状況から論理関係によって構成されるラムダ計算の圏論的モデル上のモナドを構成した。本研究計画の立案段階では既存のBCOからなる２－圏の定義から得られるmonadはidempotentなつまらないものだけであると考えており、そのため既存のBCOからなる２－圏の定義の精密化が必要であると考えていたが、この共同研究の結果実際にはそうではなく既存のBCOの定義であっても十分多くの関数型プログラミング言語の計算モデルに対応できそうであるということがわかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
計画ではbasic combinatorial object（BCO）からなる２－圏の精密化された定義とその2-圏を含むコンパクト閉圏をあたえる予定であったが後半は未達成である。BCOからなる２－圏を含むコンパクト閉圏を用いて、例えばラムダ計算のラムダ抽象に関する構造（デカルト閉圏における冪）を捉えようとすることが予想以上に困難であったためである。
|
| Strategy for Future Research Activity |
BCOからなる２－圏を含むコンパクト閉圏を定義しそれによってプログラミング言語の計算モデルの代数構造を捉えようとすることと並行してBCOからなる２－圏の言葉だけでも捉えられる代数構造、主に副作用に焦点をしぼり研究計画の遂行に当たる。コンパクト閉圏の言葉を使って捉えようとしていた代数構造である冪や不動点演算子は副作用を記述するための代数構造（monadとLawvere理論）とは独立した概念でありこれらの研究を分離することは可能である。
|
| Causes of Carryover |
書籍などの購入の必要が発生しなかったため。
|
| Expenditure Plan for Carryover Budget |
物品費して使用予定。
|
Research Products
(1 results)
