2021 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 – 2023-03-31
|
| Keywords | プログラミング言語 / 意味論 / 圏論 / 量子トポロジー / テンソル圏 / ラムダ計算 |
|---|
| Outline of Annual Research Achievements |
プログラミング言語実装モデルの幾何的な側面に着目し、低レベル・超低レベルの実装モデルに対応できる幾何的なプログラム意味論の構築を目指した。本年度は以下の成果をあげた。
（１）前年度に引き続き、プログラム実装の意味論および位相量子計算の意味論の両方に共通する基礎となる、ブレイド（組み紐）を持つラムダ計算の理論を研究した。特に、ブレイド付きラムダ計算に対応するコンビネータ代数の理論を、閉オペラッドの枠組みを用いて展開した。これにより、未解決だったブレイド付きコンビネータ代数の公理化と、ブレイド付きコンビネータ代数から閉ブレイド付きオペラッドを普遍的に構成する手法を与えることができた。これらの成果をまとめた論文は、現在投稿準備中である。また、前年度に投稿したブレイド付きラムダ計算の最初の論文が、査読・修正のうえ受理され、出版された。
（２）プログラム意味論の量子化の技術的基礎となる非可換（非対称）なテンソル圏およびそれに基づく意味論の研究を行った。特に、トレース付きテンソル圏
の構造を持ち上げるモナドの特徴づけについて、ホップモナドの概念を手掛かりに研究を進めた。これまでにホップモナドがトレース付きテンソル圏の構造を持ち上げる必要十分条件を特定し、様々な具体例・反例を構築してきたが、新たに、冪等なモナドがトレース構造を持ち上げる必要十分条件等を見出した（JS Lemay氏との共同研究）。これらの成果について、現在論文の執筆を進めている。
|
| 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 |
引き続き、プログラム意味論の非可換化およびトレース付きモノイダル圏の基礎理論の研究を行う。具体的には、オペラッドによるコンビネータ代数の理論の整備、およびトレース付きテンソル圏の構造を持ち上げるモナドの特徴づけに取り組む。
|
| Causes of Carryover |
コロナ禍のため、国内外の学会に出席するための旅費を使うことができなかった。
次年度は主として学会参加費（オンライン含む）及びコロナ禍後の学会参加旅費、また論文執筆に必要な文献等の購入などに用いる予定である。
|
