2020 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 – 2022-03-31
|
| Keywords | プログラミング言語 / 意味論 / 圏論 / 量子トポロジー / 線形論理 / ラムダ計算 |
|---|
| Outline of Annual Research Achievements |
プログラミング言語実装モデルの幾何的な側面に着目し、低レベル・超低レベルの実装モデルに対応できる幾何的なプログラム意味論の構築を目指した。本年度は以下の成果をあげた。
（１）プログラム実装の意味論および位相量子計算の意味論の両方に共通する基礎となる、ブレイド（組み紐）を持つラムダ計算の構文論と意味論を研究した。
ブレイドはデータの順序の入れ替えの３次元空間における実装を表現しているとみなせる。ブレイドを持つ計算系・証明体系の研究は先例があるが、ラムダ計算としての定式化はこれがはじめてである。ブレイド付きラムダ計算に対応するコンビナトリ―論理もあわせて定式化した。このブレイド付きラムダ計算は型を持たないため、その意味論を与えることは量子トポロジーや位相的量子場の理論で用いられる圏（たとえば量子群の有限次元表現の圏）では困難である。この問題を、長谷川が以前の研究で構成した交差G集合と適切な二項関係のなすリボン圏を用いることで解決し、具体的なモデルの例を与えた。これらの成果を国際研究集会で発表した。また、成果をまとめた論文を投稿し、査読を経て改訂した。
（２）プログラム意味論の量子化の技術的基礎となる非可換（非対称）なテンソル圏およびそれに基づく意味論の研究を行った。特に、トレース付きテンソル圏の構造を持ち上げるモナドの特徴づけについて、ホップモナドの概念を手掛かりに研究を進めた。これまでにホップモナドがトレース付きテンソル圏の構造を持ち上げる必要十分条件を特定し、また、ホップモナドではないがトレースを持ち上げるようなモナドの具体例を与えていたが、新たに、トレースを持ち上げないホップモナドの実例の構築に成功した。
|
| 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 |
引き続き、プログラム意味論の非可換化およびトレース付きモノイダル圏の基礎理論の研究を行う。具体的な課題としては、（１）非可換なトレース付き＊-自律圏の構造決定問題の解決、（２）トレース付きテンソル圏の構造を持ち上げるモナドの特徴づけ、（３）ブレイド付きラムダ計算の研究などに取り組む。また、低水準実装の幾何的構造の研究として、ダイアレクティカ解釈に基づくモデル構成およびその相互作用の幾何との関連についても研究を行う。線形ラムダ計算から値呼び関数型プログラミング言語への変換、およびそのCPS変換との関係などが得られると期待している。
|
| Causes of Carryover |
コロナ禍のため、国内外の学会に出席するための旅費を使うことができなかった。
次年度は主として学会参加費（オンライン含む）及びコロナ禍後の学会参加旅費、また論文執筆に必要な文献等の購入に用いる予定である。
|
