|
最終年度は前年度の「圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査」の成果を拡張することを目指し研究を行った。前年度までの研究においては、プログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」をコンウェイ半環で捉えることを考え、コンウェイ半環で指標が与えられる様相演算子とトレース演算子から繰り返し処理を捉える数学的構造（コンウェイ半環を指標に持つガード付き不動点演算子と呼ぶべき構造）が得られることがわかっていた。本年度はこのコンウェイ半環の構造を双モノイダル圏とその上のある条件をみたす関手として一般化しても依然この構成が可能であることを明らかにした。さらにこの構成の具体例としてガード付き不動点演算子が得られることを明らかにした。研究期間全体を通じては、本研究ではまず、圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査を行った。ここでは圏MetCpo上の実数を指標に持つ様相演算子とMetCpo上のトレース演算子から、既存研究で知られている不動点演算子が得られることが明らかになった。この具体的な状況の研究を通じ、得られた研究成果を一般化することを行った。指標を与える実数はコンウェイ半環、そしてより一般に双モノイダル圏とその上のある条件をみたす関手として一般化した。この枠組みにおいて不動点演算子の構成を与え、その特殊例としてガード付き不動点演算子が得られることを明らかにした。
|
