2018 Fiscal Year Research-status Report
Quantization, Categorification and Geometrization of Program Semantics
| Project/Area Number |
18K11165
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
長谷川 真人 京都大学, 数理解析研究所, 教授 (50293973)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | プログラミング言語 / 意味論 / 圏論 / 量子トポロジー / 線形論理 / ラムダ計算 |
|---|
| Outline of Annual Research Achievements |
プログラミング言語実装モデルの幾何的な側面に着目し、低レベル・超低レベルの実装モデルに対応できる幾何的なプログラム意味論の構築を目指した。本年度は以下の成果をあげた。
（１）プログラム実装の意味論および位相量子計算の意味論の両方の基礎となる、トレー
ス演算子を持つテンソル圏の基礎理論の研究を行った。特に、トレース付きテンソル圏からコンパクト閉圏への埋め込みを与えるInt 構成について、その埋め込み関手と別の関手の合成が右随伴を持つための必要十分条件を発見した。この結果を、トレース付きテンソル圏を用いた巡回共有構造を持つラムダ計算のモデルに適用することにより、古典線形論理のモデルを構成することができる。さらに、このモデル構成から、古典線形論理に対応する線形ラムダ計算から巡回ラムダ計算への健全な翻訳が導かれる．この翻訳を定式化し，その非線形な部分の翻訳が、関数型プログラミング言語の実装に用いられる継続渡し方式（CPS）変換に一致することを示した。この成果を論文にまとめ、査読付き国際研究集会およびその論文集で発表した。
（２）プログラム意味論の量子化の技術的基礎となる非可換（非対称）なテンソル圏およ
びそれに基づく意味論の研究を行った。具体的には、古典線形論理の圏論的モデルとなる＊-自律圏に関して、＊-自律圏の構造がモナドの代数の圏に持ち上げられるための必要十分を、位相的量子場の理論・量子トポロジーと深く関連するHopfモナドの概念を用いて与えた。この成果をまとめた論文は査読付き国際学術誌に掲載された。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
トレース付きテンソル圏に関する結果から具体的なプログラム変換を導くことができることは研究の構想段階から予想していたが、そのとおりに順調に論文にまとめ発表することができた。CPS変換との関係づけは想定を上回る成果である。
＊-自律圏の構造を持ち上げるモナドの特徴づけについては、ある程度予想はできていたものの、技術的詳細については研究開始段階ではまだ明らかではなかった。幸いこの問題に関心を持つ共同研究者を得ることができ、当初の計画以上の速さで技術的問題を解決し、論文発表までこぎつけることができた。
|
| Strategy for Future Research Activity |
今年度に引き続き、プログラム意味論の非可換化およびトレース付きモノイダル圏の基礎理論の研究を行う。具体的な課題としては、（１）非可換なトレース付き＊-自律圏の構造決定問題の解決、（２）トレース付きテンソル圏の構造を持ち上げるモナドの特徴づけ、（３）平面コンビナトリ代数に基づく非可換実現可能性解釈モデルの構築、などに取り組む。
一方、低水準実装の幾何的構造の研究の出発点として、ダイアレクティカ解釈に基づくモデル構成およびその相互作用の幾何との関連について研究を行う。順調に進めば、線形ラムダ計算から値呼び関数型プログラミング言語への変換、およびそのCPS変換との関係などが得られると期待している。
|
| Causes of Carryover |
研究に使用するノートパソコン（３０万円程度）を１台購入する予定であったが、以前別予算で購入したパソコンがまだ使用に耐えたため、購入を次年度にまわすことにした。
|
