| 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 |
|
|---|
| 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 Final Research Achievements |
In this research, we studied relationship between the category MetCpo of metric cpos and non-expansive and continuous maps with guarded fixed point operator. We showed that the trace operator and the linear exponential comonad on MetCpo graded by the semiring of real numbers give rise to a "graded fixed point operator" given in an existing work. We then generalized this this result. We first give a generalization of this construction by replacing the semiring of real numbers with a Conway semiring, and we give a further generalization based on bimonoidal categories with a functor corresponding to Conway star-operator. We observed that the guarded fixed point operator on the topos of trees appears as a concrete example of this construction.
|
| Academic Significance and Societal Importance of the Research Achievements |
ガード付き不動点演算子は論理関係を利用して再帰的な構造を持つプログラミング言語の性質を調べる手法の一つとして研究されていたが、近年では指標付きコモナド(graded comonad)に基づいた型システムの研究においても類似の構造が現れている。また、別のガード付き不動点演算子と類似の構造として、部分的に定義される不動点演算子の定式化として指標付きコモナド(graded comonad)に基づいた不動点演算子を考える研究が行われている。本研究の一般的な枠組みからはこの多様な「ガード付き不動点演算子」に対する包括的な枠組みを与えることが期待できる。
|
