2005 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.与えられた項書換え系が計算する関数の逆関数を計算する項書換え系を求める問題(逆計算問題という)は,既存プログラムと仕様からのプログラム生成の典型例である.この問題の解決法を詳細に検討することにより,本研究の目的であるプログラム自動生成のための変換規則の開発に向けて,多くの知見が得られると考えられる.この観点から逆計算問題について研究を進め,先に与えた逆計算問題解決法を改善することで構成子項書換え系に対しても有効であることを明らかにした.
2.プログラム自動生成のための変換規則の正しさは帰納的定理の概念によって定式化される.帰納的定理についての考察は,本研究の変換規則に深い洞察を与えると考えられる.このことから,帰納的定理に関する研究を行い,関数型プログラムの計算モデルである単純型項書換え系における帰納的定理自動証明法である暗黙帰納法に関する基礎的な結果を与えた.暗黙帰納法と本研究のプログラム生成法には共通する規則があり,両者の関連が興味深い.
|
