2022 Fiscal Year Annual Research 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 – 2023-03-31
|
| Keywords | プログラミング言語 / 意味論 / 圏論 / 量子トポロジー / テンソル圏 / ラムダ計算 |
|---|
| Outline of Annual Research Achievements |
プログラミング言語実装モデルの幾何的な側面に着目し、低レベル・超低レベルの実装モデルに対応できる幾何的なプログラム意味論の構築を目指した。本年度は以下の成果をあげた。
（１）ブレイド付きラムダ計算に対応するコンビネータ代数の理論を、閉オペラッドの枠組みを用いて展開した。これにより、未解決だったブレイド付きコンビネータ代数の公理化と、ブレイド付きコンビネータ代数から閉ブレイド付きオペラッドを普遍的に構成する手法を与えることができた。これらの成果をまとめた論文を投稿し、国際会議にて発表・出版した。その後、結び目を表現できるよう拡張したトレース付きブレイド付きコンビネータ代数の概念を発見し、その特徴づけを研究した。
（２）プログラム意味論の量子化の技術的基礎となる非可換（非対称）なテンソル圏およびそれに基づく意味論の研究を行った。特に、トレース付きテンソル圏の構造を持ち上げるモナドの特徴づけについて、ホップモナドの概念を手掛かりに研究を進めた。これまでにホップモナドがトレース付きテンソル圏の構造を持ち上げる必要十分条件を特定し、様々な具体例・反例を構築した（JS Lemay氏との共同研究）。これらの成果を論文２編にまとめ、投稿中した。
|
