2021 Fiscal Year Research-status Report
| Project/Area Number |
21K11762
|
|---|
| Research Institution | Sojo University |
|---|
Principal Investigator |
星野 直彦 崇城大学, 情報学部, 助教 (20611883)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Keywords | ガード付き不動点演算子 / トレース演算子 |
|---|
| Outline of Annual Research Achievements |
差分プライバシーの研究で導入されたプログラミング言語Fuzzのための意味論の研究で現れるトレース演算子についての研究を行った。プログラミング言語Fuzzの意味論として距離付き完備版順序集合と非拡大連続写像からなる圏MetCpoによる意味論がある。この圏は対称モノイダル圏の構造を持ち、また、距離を非負実数倍するスケーリング関手が存在している。このスケーリング関手は圏MetCpoの対称モノイダル圏の構造に対して強モノイダル関手となっている。圏MetCpoはこのスケーリング関手をガードとして不動点演算子を持つことはすでに知られている。本年度明らかにしたことはこの圏MetCpoがトレース演算子を持つということである。さらに、このトレース演算子は完備半順序集合と連続写像の圏Cpoの上の最小不動点により与えられる不動点演算子から誘導されるトレース演算子を、圏MetCpoから圏Cpoへの忘却関手に沿って、圏MetCpoに制限したものになっている。不動点演算子とトレース演算子はカルテシアン圏上では本質的には全く同じ概念であり、常に一方から他方を構成することできることが知られており、強い関係性を持っている。本研究の目的はガード付き不動点演算子と通常の不動点演算子の関係性の理解であるが、圏MetCpo上のトレース演算子からすでに知られているガード付き不動点演算子の導出ができそうである。この具体例を今後研究することで本研究課題の目的に対してよい知見を得ることを目指したい。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
距離付き完備版順序集合と非拡大連続写像からなる圏MetCpoにおけるガード付き不動点演算子という具体例の研究は当初の計画にはなかった。これは具体的な圏MetCpoを調べていく中での、本研究課題のテーマである通常の不動点演算子とガード付き不動点演算子に関わる構造の発見という当初の計画では予想していなかった結果が得られたからである。に関連した構造を調べていく中でのこの圏での不動点演算子はガード付きのものである一方、トレース演算子は通常のものである。さらにこのふたつの概念はよく知られた不動点演算子とトレース演算子との関係と類似の結びつきを持っていると考えられる。また、ここでの圏MetCpo上のトレース演算子は完備半順序集合と連続写像の圏Cpoの上の最小不動点により与えられる不動点演算子から誘導されるトレース演算子を圏MetCpoへ制限したものになっている。さらに、圏MetCpoのガード付きの不動点演算子についても圏Cpo上の不動点演算子の制限となっている。このような状況はこれまでの研究では見たことがなく、研究計画での研究対象としてあがっていない。しかしながら、この状況を研究することはガード付き不動点演算子とガードのない通常の不動点演算子の関係を考える上で良い知見に結びつくと考えられる。
|
| Strategy for Future Research Activity |
圏MetCpo上のトレース演算子およびガード付きの不動点演算子の関係を調べることで、ガード付き不動点演算子とガードのない通常の不動点演算子との関係についての知見を得ることを目指す。圏MetCpo上のガード付きの不動点演算子は実際にはガード付きの不動点演算子と呼ぶべき形にはなっていない。これはこの「ガード付きの不動点演算子」が圏MetCpo上の対称モノイダル圏の構造とその上の対称強モノイダル関手であるスケーリング関手を利用して与えられているからである。今後の研究の推進方策としては（１）この「ガード付きの不動点演算子」は圏MetCpoのスケーリング関手に対する余クライスリ圏上の演算子としてガード付きの不動点演算子になっていないかを調べる。（２）圏MetCpo上の「ガード付きの不動点演算子」とトレース演算子が相互に導出できないかを調べる。（３）ガード付き不動点演算子とトレース演算子が関係づけられるような状況が他にも無いかをしらべる。ことを行っていく。
|
| Causes of Carryover |
コロナへの対応として出張を取りやめたため。次年度は感染者数などの状況をみつつ、学会等への出張を行う。
|
