| 研究課題/領域番号 |
21K11762
|
|---|
| 研究機関 | 崇城大学 |
|---|
研究代表者 |
星野 直彦 崇城大学, 情報学部, 助教 (20611883)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| キーワード | ガード付き不動点演算子 / トレース演算子 |
|---|
| 研究実績の概要 |
まず、昨年度の「今後の研究の推進方針」の「圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査」について述べる。圏MetCpoはプログラミングでの繰り返し処理を捉える数学的構造とプログラムが入力に対しどの程度の依存度を持っているかを測る「距離」と呼ばれる尺度を兼ね備えた数学的対象である。この圏上には繰り返し処理を捉えるための数学的構造から得られるトレース演算子という繰り返し処理に相当する数学的構造が入る。トレース演算子は直感的には繰り返し処理に相当しているが、技術的にはトレース演算子では直接forループのような繰り返し処理を捉えられない。そこで気になる点が昨年度の「今後の研究の推進方針」の中で述べた「(1)この『ガード付きの不動点演算子』は圏MetCpoのスケーリング関手に対する余クライスリ圏上の演算子としてガード付きの不動点演算子になっていないかを調べる。」である。つまり、圏MetCpoの上には、プログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」の目盛りを拡大・縮小する演算子があり、この演算子を経由して圏MetCpoのトレース演算子から繰り返し処理を捉える数学的構造（ガード付きの不動点演算子）が得られないかということである。研究結果として「距離」の目盛りがコンウェイ半環と呼ばれる数学的構造で与えられている場合には繰り返し処理を捉える数学的構造（コンウェイ半環を指標に持つガード付き不動点演算子と呼ぶべき構造）が得られることがわかった。次に、圏MetCpo上のトレース演算子の調査について述べる。Int構成と呼ばれる手法を経由して得られる線形ラムダ計算（ある種のプログラミング言語）のプログラムの間の距離の研究を行った。具体的には線形ラムダ計算上の距離として他に3種類を構成し、それらの距離の関係を明らかにした。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
圏MetCpo上のトレース演算子と不動点演算子の研究は進んでいる。一方で、圏MetCpo上のトレース演算子という具体的な対象についての研究によって、トレース演算子とガード付きトレース演算子の関係についての理解を深めるという点に関しては十分な進捗が得られていない。ひとつには圏MetCpoのトレース演算子という具体的な対象の既存研究が少なく手探りの状態であることが考えられる。また、圏MetCpoの上のプログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」の目盛りを拡大・縮小する演算子は指数付き線形冪余単子と呼ばれる数学的構造を持っていることは知られているが、この数学的構造とトレース演算子との関係についてはほとんど知られておらず、この点についても研究で明らかにしていかなければならないことも理由として考えられる。
|
| 今後の研究の推進方策 |
引き続き、圏MetCpo上のトレース演算子とガード付き不動点演算子の関係についての研究を進めていく。まず、これまでの研究で得られている繰り返し処理を捉える数学的構造はコンウェイ半環を指標に持つガード付きコンウェイ演算子と呼ぶべき構造であるが、現状では、「コンウェイ半環を指標に持つガード付きコンウェイ演算子」がどのように定義すべき概念かは不明である。そこで、まずは、この点を明らかにしていく。また、すでにガード付き型システムにおけるガード付き不動点演算子が「コンウェイ半環を指標に持つガード付きコンウェイ演算子」の具体例であることを明らかにしている。そこでこれまでの成果をまとめることで、コンウェイ半環による指標を軸にトレース演算子とガード付き不動点演算子の関係を明らかにしていく計画である。
|
| 次年度使用額が生じた理由 |
コロナ対応として出張時期と出張先を慎重に決定したため。次年度は感染者数などの状況を見つつ、学会等への出張を行う。
|
