2006 Fiscal Year Annual Research Report
| Project/Area Number |
18500005
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Ochanomizu University |
|---|
Principal Investigator |
浅井 健一 お茶の水女子大学, 理学部, 助教授 (10262156)
|
|---|
| Keywords | 部分継続 / プログラム理論 / 情報基礎 |
|---|
| Research Abstract |
本年度は、主に部分継続の基礎理論の確立、型推論器の作成、そして部分継続の応用プログラムの作成を行い、以下のような成果を得た。
・多相性の入っていない部分継続の型システムを定義し、その健全性を定理証明系であるIsabelle/HOLを使って証明した。作成した型システムは、ほぼDanvy, Filinskiによる型システムと同じだが、不動点演算子を組み込んでおり、これにより再帰の入ったプログラムの型付けも行うことができる。また、部分継続の入った体系における不動点演算子の型については、これまで知られていなかったが、その(自明でない)型付けを示すとともに、その健全性も証明した。
・次に、多相性の入った部分継続の型システムを定義し、その健全性の証明を試みた。ほぼ証明できる見通しであるが、まだいくつか小さい補題の証明が終了しておらず、Isabelle/HOLによる証明は完成していない。来年度は、まず手による証明を完成させ、その上でIsabelle/HOLによる証明も完成させる予定である。研究計画で問題となると予想された名前の付け替えの問題については、de Bruijn levelを使っても問題の複雑さは変わらないことがわかった。代わりにIsabelle/HOL上で最近、開発されているNominalパッケージを使用すると、手による証明とほぼ同じ複雑度で証明ができそうなことがわかった。
・上の証明とは平行して、多相性の入った部分継続の型システムとインタプリタを実装した。この処理系の上でいくつかのプログラムを実行し、従来、多相性が入っていなくても型がつくと思われていたプログラムが、実は多相性がないと型がつかないことなどがわかった。
・応用プログラムとしてprintfの型付け問題について検討した。printfを部分継続を使って実装できることを示した上で、その型付けには継続の結果の型が異なることが本質的であることを示した。
|
