| 研究課題/領域番号 |
21K11762
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 崇城大学 |
|---|
研究代表者 |
星野 直彦 崇城大学, 情報学部, 助教 (20611883)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
2,600千円 (直接経費: 2,000千円、間接経費: 600千円)
2023年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2022年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2021年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | ガード付き不動点演算子 / トレース演算子 / プログラミング言語 / 意味論 / 圏論 |
|---|
| 研究開始時の研究の概要 |
プログラミング言語の構造を解析する数学的手法の研究を推し進めることで、プログラムの検証手法の発展に寄与することが本研究課題の目的である。本研究課題が対象とするのはプログラミング言語の基本的な構成要素のひとつであるループ構造である。ループ構造を捉える数学的概念には複数のものがある。代表的なものとしてトレース演算子およびそれに類似した演算子であるガード付きトレース演算子や部分トレース演算子が挙げられる。本研究課題の具体的な目標はこれらの演算子の関係を明らかにし、既存のループ構造の解析手法をより強力なものとすることである。
|
| 研究実績の概要 |
最終年度は前年度の「圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査」の成果を拡張することを目指し研究を行った。前年度までの研究においては、プログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」をコンウェイ半環で捉えることを考え、コンウェイ半環で指標が与えられる様相演算子とトレース演算子から繰り返し処理を捉える数学的構造（コンウェイ半環を指標に持つガード付き不動点演算子と呼ぶべき構造）が得られることがわかっていた。本年度はこのコンウェイ半環の構造を双モノイダル圏とその上のある条件をみたす関手として一般化しても依然この構成が可能であることを明らかにした。さらにこの構成の具体例としてガード付き不動点演算子が得られることを明らかにした。研究期間全体を通じては、本研究ではまず、圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査を行った。ここでは圏MetCpo上の実数を指標に持つ様相演算子とMetCpo上のトレース演算子から、既存研究で知られている不動点演算子が得られることが明らかになった。この具体的な状況の研究を通じ、得られた研究成果を一般化することを行った。指標を与える実数はコンウェイ半環、そしてより一般に双モノイダル圏とその上のある条件をみたす関手として一般化した。この枠組みにおいて不動点演算子の構成を与え、その特殊例としてガード付き不動点演算子が得られることを明らかにした。
|
