2017 Fiscal Year Annual Research Report
Semantics for Implementations of Programming Languages
| Project/Area Number |
15K00013
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
長谷川 真人 京都大学, 数理解析研究所, 教授 (50293973)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | プログラミング言語 / 意味論 / 位相的量子計算 / 遅延評価 / 圏論 / 線型論理 |
|---|
| Outline of Annual Research Achievements |
プログラミング言語の実装モデルに焦点をあてたプログラム意味論の構築を目指し、そのために必要な数学構造の研究を行った。特に、トレース付きモノイダル圏を中心とする、モノイダル圏及びその意味論への応用の研究に取り組んだ。
効率的なプログラム実装の意味論の基礎となる線形論理の圏論モデルについては、巡回共有構造を持つラムダ計算の圏論的なモデルから線型論理のモデルを構築する一般的な方法を見出した。また、このモデル構成技法から、線型論理に対応するラムダ計算から巡回共有構造を持つラムダ計算への翻訳を与えた。これは、従来のトレース付きモノイダル圏に基づく「相互作用の幾何」の流れに属するものであるが、線型冪コモナドの構成がこれまで知られていなかったものであり、非線形な項の翻訳が名前呼び継続渡し方式（CPS）変換と完全に一致していることが特徴である。純粋に圏論的な考察から応用上よく知られているCPS変換が得られることは、このアプローチの妥当性・有用性を示していると考えられる。この成果を論文にまとめた（投稿中）。
また、前年度に引き続き、対称モノイダル圏がトレース付きモノイダル圏に埋め込み可能かを問う未解決問題について研究を進めた（論文準備中）。
さらに、双対性を持つモノイダル圏とトレース付きモノイダル圏との間に位置する、弱い双対性を持つモノイダル圏の概念に着目し、その基礎的な結果をまとめた（論文準備中）。
|
