| Project/Area Number |
21K11762
|
|---|
| 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 | Sojo University |
|---|
Principal Investigator |
星野 直彦 崇城大学, 情報学部, 助教 (20611883)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | ガード付き不動点演算子 / トレース演算子 / プログラミング言語 / 意味論 / 圏論 |
|---|
| Outline of Research at the Start |
プログラミング言語の構造を解析する数学的手法の研究を推し進めることで、プログラムの検証手法の発展に寄与することが本研究課題の目的である。本研究課題が対象とするのはプログラミング言語の基本的な構成要素のひとつであるループ構造である。ループ構造を捉える数学的概念には複数のものがある。代表的なものとしてトレース演算子およびそれに類似した演算子であるガード付きトレース演算子や部分トレース演算子が挙げられる。本研究課題の具体的な目標はこれらの演算子の関係を明らかにし、既存のループ構造の解析手法をより強力なものとすることである。
|
| Outline of Annual Research Achievements |
最終年度は前年度の「圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査」の成果を拡張することを目指し研究を行った。前年度までの研究においては、プログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」をコンウェイ半環で捉えることを考え、コンウェイ半環で指標が与えられる様相演算子とトレース演算子から繰り返し処理を捉える数学的構造（コンウェイ半環を指標に持つガード付き不動点演算子と呼ぶべき構造）が得られることがわかっていた。本年度はこのコンウェイ半環の構造を双モノイダル圏とその上のある条件をみたす関手として一般化しても依然この構成が可能であることを明らかにした。さらにこの構成の具体例としてガード付き不動点演算子が得られることを明らかにした。研究期間全体を通じては、本研究ではまず、圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査を行った。ここでは圏MetCpo上の実数を指標に持つ様相演算子とMetCpo上のトレース演算子から、既存研究で知られている不動点演算子が得られることが明らかになった。この具体的な状況の研究を通じ、得られた研究成果を一般化することを行った。指標を与える実数はコンウェイ半環、そしてより一般に双モノイダル圏とその上のある条件をみたす関手として一般化した。この枠組みにおいて不動点演算子の構成を与え、その特殊例としてガード付き不動点演算子が得られることを明らかにした。
|
Report
(3 results)
Research Products
(1 results)
