| Project/Area Number |
21K11753
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2023: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | プログラミング言語 / 意味論 / 圏論 / 低次元トポロジー / モノイダル圏 / ラムダ計算 / コンビネータ代数 / 量子トポロジー / テンソル圏 / オペラッド / プログラム意味論 / 実装モデル |
|---|
| Outline of Research at the Start |
プログラミング言語の意味論（プログラム意味論）は、プログラムの挙動を数学的に正確かつ抽象化して捉えることにより、プログラムの性質を議論するための数学的基盤と有効な道具を与えるものである。従来のプログラム意味論は、主として、高水準の、抽象度の高いモデルを与えることで多くの成果を挙げてきた。一方、プログラミング言語の実装モデル}に焦点をあてたプログラム意味論は未だ発展途上段階にある。
本研究では、プログラミング言語実装モデルと、結び目の理論等の低次元トポロジーの親和性に焦点を当て、低レベル・超低レベルの実装モデルに対応できるトポロジカルなプログラム意味論の構築を行う。
|
| Outline of Final Research Achievements |
Traditional program semantics has achieved many results on high-level programming languages. On the other hand, semantics on the low-level implementation model of programming languages is still in the developing stage. This research focuses on the affinity between low-level implementation models and low-dimensional topology such as knot theory, and aims to construct topological program semantics that can support low-level implementation models. As first steps towards this direction, we introduced a theory of planar combinatory algebras in terms of operads and monoidal categories, and studied a braided lambda calculus in which swapping of variables are realized by braids. Furthermore, we introduced ribbon combinatory algebras, which correspond to ribbon categories used in the study of invariants of knots and tangles. At the same time, we studied traced monoidal categories and their lifting problem via Hopf monads.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究はプログラミング言語の理論の基礎付けに関するものであり、圏論や幾何学・トポロジーの知見や技法をプログラム意味論に取り入れること、および必要となる圏論の整備の両方を目指したものである。本研究によりプログラミング言語設計やプログラム検証に用いることのできる数学的手法が拡充され、短期的には、このような低次元トポロジー的なアプローチに基づく理論研究の活性化・深化、また、長期的には、実装レベルに踏み込んだソフトウェア開発・検証技術の発展に寄与することが期待される
|
