研究課題
本年は、依存型が帰納的に定義される帰納族とよばれる依存データ型の理論の解明を行った。依存性がない場合の帰納型は、集合上の関手として特徴付けできることが知られているが、帰納族については、個別の場合ごとにアドホックに対処されてきた。これに対し、GambinoとHylandによる依存多項式を用いることにより、すべての帰納族が一般的に依存多項式で表すことができることを初めて明らかにした。加えてHaskellの一般化代数データ型も同様に依存多項式で表すことができることも初めて明らかにした。そしてこの一般理論をデータ上のディペンダビリティを保証したプログラミングへ応用した。これは帰納族に対するジェネリックなZipperデータ構造を導出することに成功したものである。この結果は、依存型によるプログラミング技術と理論についての最新結果を議論する国際ワークショップであるShonan Workshop on Dependently Typed Programming及びShonan Workshop on Agda Meetingの共通開催日にて発表し、結果を多くの専門家に周知させることができた。本研究成果の洗練された定式化には関連研究者から好評価を得た。そして論文発表として7th ACM SIGPLAN Workshop on Generic Programmingで発表し、論文はACM Pressより出版された。これにより、依存型によるデータ構造の表現の基礎理論として、依存多項式が有効であることを明らかにすることができた。
24年度が最終年度であるため、記入しない。
すべて 2012 2011 その他
すべて 雑誌論文 (2件) (うち査読あり 2件) 学会発表 (5件) (うち招待講演 2件) 図書 (1件)
Functional and Logic Programming
巻: LNCS 7294 ページ: 136-150
0.1007/978-3-642-29822-6_13
Generic Programming
巻: WGP'11 ページ: 59-70
10.1145/2036918.2036927
