| 研究課題/領域番号 |
23700034
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
千葉 勇輝 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
|
|---|
| キーワード | プログラム変換 / 項書き換え / パターンマッチング |
|---|
| 研究概要 |
パターンによるプログラム自動変換において，変換の正当性は入出力システムの等価性によって定義される．本研究では申請者による1階項書き換えに基づくパターンによるプログラム変換の枠組みを拡張し，高階プログラムを取り扱うことができる枠組みの提案を目指している．従来の1階項書き換えでは高階プログラムを直接取り扱うことは難しいので，Yamada (2001)によって提案された単純型付き項書き換えシステム(Simply Typed Term Rewriting Syste, 以下STTRS)を用いて枠組みを構築する．
パターン変数の概念を導入し，STTRSに基づく枠組みにおける変換パターンを提案した．変換パターンを入力されたSTTRSの変換に適用するために，方パターンマッチングアルゴリズムと項パターンマッチングアルゴリズムからなるST-Matchアルゴリズムを提案した．ST-Matchの有用性を確認するために，ST-Matchの停止性，健全性及び完全性を証明した．
1階項書き換えシステムの等価性は，申請者が提案した項書き換えシステムの等価変換によって検証することが可能である．書き換えシステムの等価変換をSTTRSに拡張し，STTRSの等価変換手続きを提案した．現在，STTRSの等価変換手続きがSTTRSの等価性が保証することの証明を進めている．その過程において，1階項書き換えの枠組みでは自明に成立する下記の命題(1)がSTTRSでは一般に成立しないことが確認された．
(1) 任意の基底項tが導入規則によって導入された関数記号を含んでいる場合，tは正規形ではない．
上記の命題(1)は等価変換手続きは等価性を保証することを示すためには欠かせない命題である．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
現在，STTRSの等価変換手続きがSTTRSの等価性を保証することの証明を進めている．書き換えシステムにおける合流性の可換性と研究実績で示した導入された関数記号の除去が示されれば，等価性の保証に関する証明は校のデータ構造に依存しないことがわかっている．この結果は高階プログラムだけではなく，条件付き書き換えシステムや優先順序付き書き換えシステム，戦略を持つ書き換えシステムに本研究の結果を拡張する際にも有用な情報である．
具体例を用いて，STTRSの等価変換は関数型プログラムでは広く用いられるmapやfoldr関数を用いたプログラムを取り扱うことができることを確認している．したがって，STTRSの等価変換が実際に利用されている関数プログラムへ適用できることが期待される．
単純型付き項パターンの概念を用いることによってSTTRSにおける変換パターンを実現できる．また，単純型付き項パターンマッチングアルゴリズムST-Matchを適用することで，変換パターンと入力されたプログラムのパターンマッチングを解決することが可能である．ST-Matchの停止性，健全性，完全性は証明済みであるので，ST-Matchの有用性も確認された．
|
| 今後の研究の推進方策 |
導入された関数記号の除去はNipkow等による高階項書き換えシステム(Higher-order Rewriting System，以下HRS)では自明に成立することが調査により判明している．HRSはラムダ抽象を項書き換えシステムに導入することにより高階関数の表現を実現している．HRSはSTTRSと比べて記述力が高いことが知られているが，枠組みが複雑なためシステムの性質の検証や等価性判定は難しい．また，等価性を判定するために重要な帰納的定理を自動的に証明する手法はあまり知られていない．今後の研究ではSTTRSとHRSの特性を比較し，どちらが本研究の目的に合致するかを判定する．ここ決定した書き換えシステムを用いてパターンによるプログラム変換の枠組みを構築する．
RAPT(Rewriting-based Automated Program Transformation system)は1階の項書き換えに基づいたパターンによるプログラム自動変換システムである．上記の結果を基にRAPTを拡張し，高階プログラムを直接取り扱うことができるパターンによるプログラム変換の枠組みを計算機上に実装する．RAPTはテキストを入出力とするプログラムであり，途中結果の可読性があまり高くない．そこで，ユーザインターフェースを改良しRAPTをより使いやすいシステムとする．また，改良したRAPTを広く公開し，ユーザーからの意見を参考にすることでシステムの改良を行う．
本研究の結果をより広く利用するためには，数多くの変換パターンが必要となる．そこで，変換パターンを用意に登録できるシステムを構築し，RAPTのユーザから広く変換パターンを募集する．
|
| 次年度の研究費の使用計画 |
23年度はセルビアで開催されたRTAに参加する予定であったが,震災の影響で研究費交付の決定が遅れたため参加できなかった．そのため未使用額が生じ，その未使用額が現在まで続いている．
次年度は6月にオランダで開催される書き換え分野ではトップの国際会議RTAに参加し，項書き換えに関する情報収集に努める．また，毎年2回国内で開催されているTRS meetingで発表を行い議論を通して本研究の理論を更に深める．
システムの実装を行うためのマシンとして，DOS/VデスクトップPCを購入する．
|
