| 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 |
星野 直彦 崇城大学, 情報学部, 助教 (20611883)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | ガード付き不動点演算子 / トレース演算子 / プログラミング言語 / 意味論 / 圏論 |
|---|
| Outline of Research at the Start |
プログラミング言語の構造を解析する数学的手法の研究を推し進めることで、プログラムの検証手法の発展に寄与することが本研究課題の目的である。本研究課題が対象とするのはプログラミング言語の基本的な構成要素のひとつであるループ構造である。ループ構造を捉える数学的概念には複数のものがある。代表的なものとしてトレース演算子およびそれに類似した演算子であるガード付きトレース演算子や部分トレース演算子が挙げられる。本研究課題の具体的な目標はこれらの演算子の関係を明らかにし、既存のループ構造の解析手法をより強力なものとすることである。
|
| Outline of Annual Research Achievements |
まず、昨年度の「今後の研究の推進方針」の「圏MetCpo上のトレース演算子およびガード付き不動点演算子の関係の調査」について述べる。圏MetCpoはプログラミングでの繰り返し処理を捉える数学的構造とプログラムが入力に対しどの程度の依存度を持っているかを測る「距離」と呼ばれる尺度を兼ね備えた数学的対象である。この圏上には繰り返し処理を捉えるための数学的構造から得られるトレース演算子という繰り返し処理に相当する数学的構造が入る。トレース演算子は直感的には繰り返し処理に相当しているが、技術的にはトレース演算子では直接forループのような繰り返し処理を捉えられない。そこで気になる点が昨年度の「今後の研究の推進方針」の中で述べた「(1)この『ガード付きの不動点演算子』は圏MetCpoのスケーリング関手に対する余クライスリ圏上の演算子としてガード付きの不動点演算子になっていないかを調べる。」である。つまり、圏MetCpoの上には、プログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」の目盛りを拡大・縮小する演算子があり、この演算子を経由して圏MetCpoのトレース演算子から繰り返し処理を捉える数学的構造（ガード付きの不動点演算子）が得られないかということである。研究結果として「距離」の目盛りがコンウェイ半環と呼ばれる数学的構造で与えられている場合には繰り返し処理を捉える数学的構造（コンウェイ半環を指標に持つガード付き不動点演算子と呼ぶべき構造）が得られることがわかった。次に、圏MetCpo上のトレース演算子の調査について述べる。Int構成と呼ばれる手法を経由して得られる線形ラムダ計算（ある種のプログラミング言語）のプログラムの間の距離の研究を行った。具体的には線形ラムダ計算上の距離として他に3種類を構成し、それらの距離の関係を明らかにした。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
圏MetCpo上のトレース演算子と不動点演算子の研究は進んでいる。一方で、圏MetCpo上のトレース演算子という具体的な対象についての研究によって、トレース演算子とガード付きトレース演算子の関係についての理解を深めるという点に関しては十分な進捗が得られていない。ひとつには圏MetCpoのトレース演算子という具体的な対象の既存研究が少なく手探りの状態であることが考えられる。また、圏MetCpoの上のプログラムが入力に対しどの程度の依存度を持っているのかを測る「距離」の目盛りを拡大・縮小する演算子は指数付き線形冪余単子と呼ばれる数学的構造を持っていることは知られているが、この数学的構造とトレース演算子との関係についてはほとんど知られておらず、この点についても研究で明らかにしていかなければならないことも理由として考えられる。
|
| Strategy for Future Research Activity |
引き続き、圏MetCpo上のトレース演算子とガード付き不動点演算子の関係についての研究を進めていく。まず、これまでの研究で得られている繰り返し処理を捉える数学的構造はコンウェイ半環を指標に持つガード付きコンウェイ演算子と呼ぶべき構造であるが、現状では、「コンウェイ半環を指標に持つガード付きコンウェイ演算子」がどのように定義すべき概念かは不明である。そこで、まずは、この点を明らかにしていく。また、すでにガード付き型システムにおけるガード付き不動点演算子が「コンウェイ半環を指標に持つガード付きコンウェイ演算子」の具体例であることを明らかにしている。そこでこれまでの成果をまとめることで、コンウェイ半環による指標を軸にトレース演算子とガード付き不動点演算子の関係を明らかにしていく計画である。
|
Report
(2 results)
Research Products
(1 results)
