2023 年度研究成果報告書

ガード付き型システムの圏論的解明

研究課題

PDF

研究課題/領域番号	21K11762
研究種目	基盤研究(C)
配分区分	基金
応募区分	一般
審査区分	小区分60010:情報学基礎論関連
研究機関	崇城大学
研究代表者	星野直彦崇城大学, 情報学部, 助教 (20611883)
研究期間 (年度)	2021-04-01 – 2024-03-31
キーワード	ガード付き不動点演算子 / トレース演算子
研究成果の概要	本研究ではまず、圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査を行った。ここでは圏MetCpo上の実数を指標に持つ様相演算子とMetCpo上のトレース演算子から、既存研究で知られている不動点演算子が得られることが明らかになった。この具体的な状況の研究を通じ、得られた研究成果を一般化することを行った。指標を与える実数はコンウェイ半環、そしてより一般に双モノイダル圏とその上のある条件をみたす関手として一般化した。この枠組みにおいて不動点演算子の構成をあたえ、その特殊例としてガード付き不動点演算子が得られることを明らかにした。
自由記述の分野	プログラミング言語
研究成果の学術的意義や社会的意義	ガード付き不動点演算子は論理関係を利用して再帰的な構造を持つプログラミング言語の性質を調べる手法の一つとして研究されていたが、近年では指標付きコモナド(graded comonad)に基づいた型システムの研究においても類似の構造が現れている。また、別のガード付き不動点演算子と類似の構造として、部分的に定義される不動点演算子の定式化として指標付きコモナド(graded comonad)に基づいた不動点演算子を考える研究が行われている。本研究の一般的な枠組みからはこの多様な「ガード付き不動点演算子」に対する包括的な枠組みを与えることが期待できる。