| 研究課題/領域番号 |
21K11753
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
長谷川 真人 京都大学, 数理解析研究所, 教授 (50293973)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
2023年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2022年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2021年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | プログラミング言語 / 意味論 / 圏論 / 低次元トポロジー / モノイダル圏 / ラムダ計算 / コンビネータ代数 / 量子トポロジー / テンソル圏 / オペラッド / プログラム意味論 / 実装モデル |
|---|
| 研究開始時の研究の概要 |
プログラミング言語の意味論（プログラム意味論）は、プログラムの挙動を数学的に正確かつ抽象化して捉えることにより、プログラムの性質を議論するための数学的基盤と有効な道具を与えるものである。従来のプログラム意味論は、主として、高水準の、抽象度の高いモデルを与えることで多くの成果を挙げてきた。一方、プログラミング言語の実装モデル}に焦点をあてたプログラム意味論は未だ発展途上段階にある。
本研究では、プログラミング言語実装モデルと、結び目の理論等の低次元トポロジーの親和性に焦点を当て、低レベル・超低レベルの実装モデルに対応できるトポロジカルなプログラム意味論の構築を行う。
|
| 研究成果の概要 |
従来のプログラム意味論は高水準プログラミング言語について多くの成果を挙げてきたが、低水準言語実装については未だ発展途上段階にある。本研究は、低水準実装モデルと結び目理論等の低次元トポロジーの親和性に注目し、低水準実装モデルに対応できるトポロジカルなプログラム意味論の構築を目指した。特に、変数の順番の入れ替えを許さない平面ラムダ計算・平面コンビネータ代数の理論をもとに、変数の入れ替えを組み紐で表現するブレイド付きラムダ計算や、結び目の不変量を与えるリボン圏に対応するコンビネータ代数の理論を構築した。同時に、基礎となるモノイダル圏について、ホップモナドによるトレース構造の持ち上げを中心に調べた。
|
| 研究成果の学術的意義や社会的意義 |
本研究はプログラミング言語の理論の基礎付けに関するものであり、圏論や幾何学・トポロジーの知見や技法をプログラム意味論に取り入れること、および必要となる圏論の整備の両方を目指したものである。本研究によりプログラミング言語設計やプログラム検証に用いることのできる数学的手法が拡充され、短期的には、このような低次元トポロジー的なアプローチに基づく理論研究の活性化・深化、また、長期的には、実装レベルに踏み込んだソフトウェア開発・検証技術の発展に寄与することが期待される
|
