2010 Fiscal Year Annual Research Report
ディペンデント型によるディペンダビリティ保証付きデータ構造の理論
| Project/Area Number |
22700004
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 大学院・工学研究科, 助教 (90334135)
|
|---|
| Keywords | 関数プログラム / 関数プログラム / 情報基礎 / 自動定理証明 / データ構造 |
|---|
| Research Abstract |
本年は、依存型による安全性の保証があるデータ構造の表現と理論の解明を行った。まず、循環共有ポインタを持つ木構造のデータに対して安全な依存型の表現方法を明かにした。ここでの安全性とは、未確定領域を指すポインタがデータ構造上にないことを保証したものである。これを依存型プログラミング言語Agdaを用いて実装し、その有効性を示した。さらにこれを前層の圏における始代数として特徴づけすることに成功した。この結果は、学術論文誌Logical Methods in Computer Scienceにて出版された。
次に、より複雑なデータ構造として、束縛を持つ抽象構文構造を考察した。多相型のシステムをモデル化するために、単純型付き抽象構文のための始代数の構成法を繰返し適用することを行った。この構成の中で、グロタンディーク構成を用いることで適切な多相型の文脈のための圏を構成できることを明らかにした。この始代数は、多項式関手によって与えられるが、これは依存型の表現ともみなせるため、実際にAgda上の依存型を導出し実装し、その有効性を確かめた。この結果は14th International Conference on Foundations of Software Science and Computation Structuresで発表し、論文はSpringer-Verlagから出版された。
この二つの結果により、依存型によるデータ構造の表現の基礎理論として、前層上の圏中の始代数が有効であることを明らかにすることができた。
|
