2015 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 |
前年度に構成した副作用を持つBCO（basic combinatorial object）の研究を推し進めることを行った。前年度ではこの副作用をもつBCOから論理関係の手法を用いて副作用を持つラムダ計算の圏論的モデルを構成したが、その研究で考察したラムダ計算は不動点演算子を持たないものであった。そこですでに構成したこの副作用を持つBCOから不動点演算子と副作用を持つラムダ計算の圏論的モデルの構成を試みた。考察対象であるこのBCOには２つの不動点演算子に関連のある構造がある。一つは領域論的な構造である。つまりBCOの台集合がωCpoの構造を持ち、BCOの構造がこのωCpo構造を保っている。もうひとつの構造はコンパクト閉圏の構造である。このBCOの構成には圏論的なgeometry of interactionの手法が用いられている。圏論的なgeometry of interactionではトレース付き対称モノイダル圏からInt構成によりコンパクト閉圏を作り、そこでの反射的対象を用いてラムダ計算のモデルを構成する。そしてこのコンパクト閉圏の構造がほぼそのままBCOに反映されている。過去の研究で、圏論的なgeometry of interactionの手法を用いてBCOを構成し、そこから論理関係を用いて副作用のないラムダ計算の圏論的モデルを構成したが、その時にBCOの領域論的な構造とコンパクト閉圏の構造のいずれからも不動点演算子の解釈が得られ、更にそれらが一致することを観察していた。今回の状況でも同様の現象を期待し研究を行った結果、実際にそれぞれの構造から不動点演算子の解釈が得られ、それらが一致することが証明された。そして副作用と不動点演算子を持つラムダ計算に対する圏論的意味論をこのBCOから構成することに成功した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
副作用や不動点演算子などに対する具体例の考察が十分に集まってきた。具体的な状況に対する考察が研究の大きな部分を占め、論理関係についての抽象的な理解のための研究はあまり行えていないが、今後これらの具体例の背後にある構造を抽象化することで研究目的の達成が期待できる。
|
| Strategy for Future Research Activity |
これまでの研究で得られた具体的な状況をより詳しく考察し、そこからBCOからなる２－圏とそれを含むコンパクト閉圏の定義を与え、BCOの持つ構造がどのようにその２－圏の枠組みで捉えることができるかを調べる。副作用についてはモナドやLawvere theoryといった理論を通してBCOの構造が論理関係を介してどのように圏論的モデルに反映されているのかを研究する。また不動点演算子については今年度に観察した領域論的な構造から得られる解釈とBCO自体のコンパクト閉圏の構造から得られるものが一致する現象を手がかりにした研究を行う。
|
| Causes of Carryover |
出張が計画よりも少なかったため。
|
| Expenditure Plan for Carryover Budget |
出張旅費として使用予定。
|
