2007 Fiscal Year Annual Research Report
関数型プログラムの限界を越える安全なポインタを持つ再帰データ型の理論
| Project/Area Number |
19700006
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 Gunma University, 大学院・工学研究科, 助教 (90334135)
|
|---|
| Keywords | 関数プログラム / 項書替え / 情報基礎 |
|---|
| Research Abstract |
高階書換え系の停止性技術を発展させたものを用いて、ポインタを持つ再帰データ型を用いるアルゴリズムの停止性を理論的に保証する技術を確立した。これは与えられた高階項書換え系の停止性判定問題を考察することに他ならなく、既存の高階項書換え系の停止性判定技法のみでは、不十分であることが分かっていた。そこで先に得られたポインタを持つ再帰データの代数構造を最大限に活用した。すなわち、申請者の先行研究の高階構文の代数的意味論の構造を用い、一階項書換え系の意味ラベル技術を高階に拡張した。代数的意味論を用いると、高階書換えの対象の高階項にラベル付けする操作をラベル付き項の代数的構造を考察することによって、自然に準同型写像として定式化できるという利点があるため、円滑に拡張が行えた。さらにGeneral Schemaと呼ばれる停止性判定技法とこの意味ラベルを組み合わせることにより、停止性を証明する技法を確立した。
さらにこれに加えて高階書換え系についての新たな結果も得た。高階書換え系にソリッド性という性質を導入し、これに関する停止性のモジュラ性を意味ラベリング手法を用いて証明することに成功した。それと共に高階書換え系と高階プログラムスキームの合成に関する停止性のモジュラ性も証明することができた。この結果は国際会議ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programmingで論文と共に発表した。
|
