2011 Fiscal Year Annual Research Report
ディペンデント型によるディペンダビリティ保証付きデータ構造の理論
| Project/Area Number |
22700004
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 工学(系)研究科(研究院), 助教 (90334135)
|
|---|
| Keywords | 関数プログラム / 依存型 / 情報学基礎 / 自動定理証明 / データ構造 |
|---|
| Research Abstract |
本年は、依存型が帰納的に定義される帰納族とよばれる依存データ型の理論の解明を行った。依存性がない場合の帰納型は、集合上の関手として特徴付けできることが知られているが、帰納族については、個別の場合ごとにアドホックに対処されてきた。これに対し、GambinoとHylandによる依存多項式を用いることにより、すべての帰納族が一般的に依存多項式で表すことができることを初めて明らかにした。加えてHaskellの一般化代数データ型も同様に依存多項式で表すことができることも初めて明らかにした。そしてこの一般理論をデータ上のディペンダビリティを保証したプログラミングへ応用した。これは帰納族に対するジェネリックなZipperデータ構造を導出することに成功したものである。
この結果は、依存型によるプログラミング技術と理論についての最新結果を議論する国際ワークショップであるShonan Workshop on Dependently Typed Programming及びShonan Workshop on Agda Meetingの共通開催日にて発表し、結果を多くの専門家に周知させることができた。本研究成果の洗練された定式化には関連研究者から好評価を得た。そして論文発表として7th ACM SIGPLAN Workshop on Generic Programmingで発表し、論文はACM Pressより出版された。
これにより、依存型によるデータ構造の表現の基礎理論として、依存多項式が有効であることを明らかにすることができた。
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
-
-
-
-
-
-
-
-
[Book] チューリングを読む2012
Author(s)
チャールズ・ペゾルド (著), 井田哲雄, 鈴木大郎, 奥居哲, 浜名誠, 山田俊行(訳)
Total Pages
612ページ
Publisher
日経BP
