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

点击翻译按钮获取中文摘要

まず、昨年度の「今後の研究の推進方針」の「圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査」について述べる。圏MetCpoはプログラミングでの繰り返し処理を捉える数学的構造とプログラムが入力に対しどの程度の依存度を持っているかを測る「距離」と呼ばれる尺度を兼ね備えた数学的対象である。この圏上には繰り返し処理を捉えるための数学的構造から得られるトレース演算子という繰り返し処理に相当する数学的構造が入る。トレース演算子は直感的には繰り返し処理に相当しているが、技術的にはトレース演算子では直接forループのような繰り返し処理を捉えられない。そこで気になる点が昨年度の「今後の研究の推進方針」の中で述べた「(1)この『ガード付きの不動点演算子』は圏MetCpoのスケーリング関手に対する余クライスリ圏上の演算子としてガード付きの不動点演算子になっていないかを調べる。」である。つまり、圏MetCpoの上には、プログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」の目盛りを拡大・縮小する演算子があり、この演算子を経由して圏MetCpoのトレース演算子から繰り返し処理を捉える数学的構造（ガード付きの不動点演算子）が得られないかということである。研究結果として「距離」の目盛りがコンウェイ半環と呼ばれる数学的構造で与えられている場合には繰り返し処理を捉える数学的構造（コンウェイ半環を指標に持つガード付き不動点演算子と呼ぶべき構造）が得られることがわかった。次に、圏MetCpo上のトレース演算子の調査について述べる。Int構成と呼ばれる手法を経由して得られる線形ラムダ計算（ある種のプログラミング言語）のプログラムの間の距離の研究を行った。具体的には線形ラムダ計算上の距離として他に3種類を構成し、それらの距離の関係を明らかにした。