2001 Fiscal Year Annual Research Report
定理証明システムによる型システムとプログラム変換の検証
| Project/Area Number |
13780193
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
南出 靖彦 筑波大学, 電子・情報工学系, 講師 (50252531)
|
|---|
| Keywords | 定理証明システム / 型システム / プログラム変換 / 操作的意味論 |
|---|
| Research Abstract |
3種類のCPS変換の検証を定理証明システムIsabelle/HOLで行った.最初に検証したPlotkinによる基本的なCPS変換の検証では,変換によって新しく導入される変数の扱いが問題になった.変数の型に関してパラメータ化した抽象構文を用いて,導入される変数が新しい変数であることを暗黙の制約として表現することで検証を簡略化できることがわかった.次に,DanvyとFilinskiによって提案されたある種の最適化を変換と同時に行うCPS変換の正当性の検証を行った.PlotkinによるCPS変換の検証を参考にして検証を行ったが,アルファ同値の扱いが新たに問題になった.通常のアルファ同値の定義は,定理証明システムで自動的に推論するには適していない.そこで構文に沿って定義される演繹体系としてアルファ同値を定義して検証を行った.DanvyとNielsenは,最近,DanvyとFilinskiのCPS変換を簡略化した変換を提案した.この変換については,PlotkinのCPS変換及びDanvyとFilinskiのCPS変換に対する証明スクリプトを参考にすることで,約3日程度で検証することができた.
今後,定理証明システムを用いてプログラム変換が性能に関して安全であることを示すことを考えている.そのために,性能に関する安全性を証明する手法を研究した.プログラム変換として,部分型を持つプログラミング言語のプログラムに対して,部分型の型規則が使われている部分に型変換を挿入する変換を考えた.この変換に関して,部分型の型規則がある条件を満たすときは,実行時間及びスタック空間に関して安全であることを示した.この研究でプログラム変換の正当性の証明に用いられる論理関係による証明法が,実行時間及びスタック空間に関するプログラム変換の安全性の証明に利用できることが示せた.
|
