2014 Fiscal Year Research-status Report
依存型理論による安全性保証付きデータ構造の創出・推論・進化
| Project/Area Number |
24300001
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 大学院理工学府, 助教 (90334135)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | プログラム理論 / 圏論 / 関数プログラム / 情報学基礎 / 構造再帰 / 半構造データ / 原始再帰 |
|---|
| Outline of Annual Research Achievements |
本年度は、安全性保証付きデータ構造の理論の適用範囲をさらに広げ、進化させるために半構造データおよび根付きグラフに対する帰納構造の計算原理の解明と代数化を行った。これまでそのような半構造データにサイクルがあるものの数学的モデルは不明だったが、トレース付きモノイダル圏によるサイクル構造の解釈が可能であることが分かった。圏論的構造から等式公理を定式化し、圏論的モデルを与えることで、根付きグラフの等式推論が可能となった。さらに特徴的な計算メカニズムの「グラフ上の構造再帰」は始モデルの普遍性から導けることがわかり、構造再帰の完全な特徴付けを得る事に成功した。より複雑な原始再帰の場合には、加えて代数モデルの考察が必要なことを明らかにし、これにはイテレーション代数により完全な特徴付けを得た。
これによりグラフ構成子を圏論的構成として理解することが可能となった。結果として根付きグラフの等価性に対する健全かつ完全な等式論理が得られた。これは半構造データについての新しい数理論理学な安全性保証の証明を与える枠組みとなった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
安全性保証の理論を半構造データおよび根付きグラフという複雑なデータ構造へ応用を広げることができた。成果については論文を執筆中である。
|
| Strategy for Future Research Activity |
研究内容については満足の行く成果が得られた。今後は国際会議や学術雑誌での論文発表を行う。
|
| Causes of Carryover |
研究成果を発表するための国際会議開催が次年度のため、そのための経費を持ち越すこととした。
|
| Expenditure Plan for Carryover Budget |
研究成果の国際会議での発表を国際会議で行うこととし、その経費に充てることとする。
|
