Categorical study of guarded type systems

2023 Fiscal Year Final Research Report

• 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: Hoshino Naohiko 崇城大学, 情報学部, 助教 (20611883)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Keywords: ガード付き不動点演算子 / トレース演算子

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.

Free Research Field

プログラミング言語

Academic Significance and Societal Importance of the Research Achievements

ガード付き不動点演算子は論理関係を利用して再帰的な構造を持つプログラミング言語の性質を調べる手法の一つとして研究されていたが、近年では指標付きコモナド(graded comonad)に基づいた型システムの研究においても類似の構造が現れている。また、別のガード付き不動点演算子と類似の構造として、部分的に定義される不動点演算子の定式化として指標付きコモナド(graded comonad)に基づいた不動点演算子を考える研究が行われている。本研究の一般的な枠組みからはこの多様な「ガード付き不動点演算子」に対する包括的な枠組みを与えることが期待できる。