2009 Fiscal Year Annual Research Report
関数型プログラムの限界を越える安全なポインタを持つ再帰データ型の理論
| Project/Area Number |
19700006
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 Gunma University, 大学院・工学研究科, 助教 (90334135)
|
|---|
| Keywords | 関数プログラム / 項書換え / 情報基礎 / データ構造 |
|---|
| Research Abstract |
本年は、ポインタを持つ再帰データ型のための始代数理論を完成きせ、プログラミングや推論に有用な様々な原理を導出した。関数型言語において、始代数は特にパターンマッチと構造再帰、そして推論における構造帰納法と密接に関係している。ポインタを持つ再帰データ型に対して、この関係を詳細に調べ、具体的にそれらの原理がどのような形になるかを明らかにした。さらにポインタを持つ再帰データ型の依存型表現を依存型プログラミング言語Agdaを用いて明らかにした。この結果はNinth International Conference on Typed Lambda Calculi and Applications(TLCA 2009)で発表し、論文ははSpringer-Verlagから出版された。さらにこれを拡張したジャーナル版論文も学術論文誌Logical Methods in Computer Scienceに採録決定している。
また、高階書換え系の停止性技術を発展させたものを用いて、ポインタを持つ再帰データ型を用いるアルゴリズムの停止性を理論的に保証する技術を確立した。先に得られたポインタを持つ再帰データの代数構造を最大限に活用し、一階項書換え系の意味ラベル技術を高階に拡張した。さらに高階の再帰経路順序の技法とこの意味ラベルを組み合わせることにより、停止性を証明する技法を確立することができた。この結果は18th International Workshop on Functional and(Constraint)Logic Programmingで発表し、論文はSpringer-Verlagから出版された。
|
