|
本年度は、昨年度から引き続き、shift/resetと言うコントロールオペレータをもつ計算体系に対する公理化の研究、および、プログラム言語に対するメタレベル推論の形式化の研究を行った。
前者としては、shift/resetの公理系に関するこれまでの成果を雑誌論文の形にまとめ、"Higher-Order and Symbolic Computation"誌に投稿し、採録された(掲載は2006年の予定)。この過程で、従来得られていた公理系の完全性の証明を再構成した。すなわち、コントロールオペレータをもつ体系に意味を与えるCPS変換において、ターゲット言語の型システムに基づく証明方法と、ターゲット言語における継続パラメータの線形性に基づく証明方法の2つの組み合わせであることを発見した。
後者としては、変数の束縛(ラムダ抽象)を含むプログラム言語に対する性質の推論を形式化する研究を行った。昨年度の検討により、高階抽象構文に基づいたメタレベル推論を行うtwelfシステムを利用するのが適切であることがわかったので、今年度は、twelfシステムの上で、CPS変換の正しさの証明の形式化を行った。CPS変換の正しさは、健全性と完全性から構成される。我々の目的は、単に既存の(人手による)証明を形式化することではなく、束縛構造を含むプログラムに関するメタレベル推論に関する知見を得ることである。このため、種々のCPS変換の形式化にたいして、正しさの証明の形式化を試みた。その結果、単純な形式化における健全性の証明では特に問題は生じないが、効率的なCPS変換の定義において必要とされる形式では、健全性の証明で人間が見落としていた問題が存在することを発見した。これは変数の出現条件に関するものであり、twelfシステムが自動的に問題点を指摘した。また、完全性の証明においては、高階抽象構文による形式化の条件である「表現と代入の可換性」が成立しないことを発見した。さらに、この問題を解決するためには、コントロールオペレータのある体系を採用すればよいことを発見した。
以上のように本年度の研究の重点はメタレベル推論の形式化にあり、人手による証明では見過ごされてきた問題点の発見等に形式化が有用であることを実証した。次年度は、メタレベルの証明からのプログラム抽出や、メタプログラムそのものの形式化などにこれらの成果を適用し、信頼性の高いメタ・プログラム構成法の確立を目指す。
|
