2019 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 |
プログラミング言語実装モデルの幾何的な側面に着目し、低レベル・超低レベルの実装モデルに対応できる幾何的なプログラム意味論の構築を目指した。本年度は以下の成果をあげた。
（１）プログラム実装の意味論および位相量子計算の意味論の両方に共通する基礎となる、ブレイド（組み紐）を持つラムダ計算の構文論と意味論を研究した。ブレイドはデータの順序の入れ替えの３次元空間における実装を表現しているとみなせる。ブレイドを持つ計算系・証明体系の研究は先例があるが、ラムダ計算としての定式化はこれがはじめてである。ブレイド付きラムダ計算に対応するコンビナトリ―論理もあわせて定式化した。このブレイド付きラムダ計算は型を持たないため、その意味論を与えることは量子トポロジーや位相的量子場の理論で用いられる圏（たとえば量子群の有限次元表現の圏）では困難ないしほぼ不可能である。この問題を、長谷川が以前の研究で構成した交差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 |
２０２０年３月に本研究に関連する高次元圏論とそのための証明支援系を研究している研究者をフランスより招聘する予定であったが、コロナ禍のために直前に招聘を中止せざるを得なくなった。可能であれば次年度中に改めて招聘を行いたいと考えている。ただし、コロナ禍の状況によってはさらなる計画変更が必要となる可能性がある。
|
