2004 Fiscal Year Annual Research Report
限量子付き等式仕様からのプログラム生成に関する研究
| Project/Area Number |
16650005
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
草刈 圭一朗 名古屋大学, 大学院・情報科学研究科, 講師 (90323112)
|
|---|
| Keywords | 限量子付き等式仕様 / 項書換え系 / 被覆集合 / 論理式変換系 |
|---|
| Research Abstract |
本研究の目的は,変換規則によりE_i ; R_iをE_<i+1> ; R_<i+1>に変換することを繰り返えしてプログラムを自動生成する方法を開発することである.ここに,E_iは∀と∃を許した等式だけからなる論理式の集合であり,仕様という.R_iは項書換え系であり,実行可能であるのでプログラムとみなせる.R_0は既に開発済みのプログラムであり,E_0はR_0を基礎に新たに定義したい関数の定義である.あるnでE_nが空集合になれば変換プロセスは終了し,R_nが生成されたプログラムとなる.
今年度は以下の研究を行った。
1.等式仕様と項書換え系の対E ; Rを変換する規則集合(変換系)を与え,その規則の正当性を証明した.すなわち,変換によって得られる論理式集合の下では,その仕様である元の論理式が帰納的定理になることを証明した.さらに,この変換系の適用により実行可能な項書換え系が得られる変換系列を挙げて,プログラム生成への応用例を示した.
2.関数型プログラムの最適化変換としてよく知られているデフォレステーションを上述の変換系で模倣できることを証明した.この結果は,変換系の能力の高さを示すだけでなく,デフォレステーションの正当性の別証明になっている.つまり,我々の変換系はプログラム変換の正当性の証明にあらたな手法を与え,我々の変換系を基礎としたプログラム変換理論の新たな展開の可能性を示した.
|
