| 研究課題/領域番号 |
23700034
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
千葉 勇輝 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
|
|---|
| 研究期間 (年度) |
2011-04-28 – 2014-03-31
|
| キーワード | プログラム変換 / 単純型付き項書き換えシステム / パターンマッチング |
|---|
| 研究概要 |
パターンによる高階プログラム変換において変換の正当性はプログラムの等価性によって定義される．本研究ではプログラムを単純型付き項書き換えシステム(Simply Typed Term Rewriting Syste, 以下STTRS)によって表現している．STTRSの等価性を自動検証するための枠組みを構築するための準備として，STTRSにおける自然帰納的定理の概念を導入した． STTRSに倚る枠組みに擱いて変換パターンを表現するために，パターン変数の概念を導入した．STTRSにおける項は単純型によって型付けられるため，項パターンも型付けされている必要がある．しかしながら，変換パターンを作成した時点では入力されるSTTRSの型は分からない．そこで，型変数を含む単純型パターンを導入し，単純型パターンによって型付けされるよう単純型付き項パターンを定義した．単純型パターンと単純型のパターンマッチングによって型変数と具体的な単純型の対応関係が決定される．型同士のパターンマッチングの解を表現するために単純型代入の概念を導入した．また，型パターンマッチングを解決するため，型パターンマッチングアルゴリズムを提案した． 変換パターンと入力STTRSのパターンマッチングでは，単純型付き項パターンと単純型付き項のパターンマッチングの自然な拡張で実現できる．そこで，単純型付き項パターンと単純型付き項のパターンマッチングの解を表現するため，STTRSにおける項準同型写像の概念を定義した．また，型パターンマッチングアルゴリズムを利用して単純型付き項のパターンマッチングアルゴリズムST-Matchを提案した．ST-Matchの有用性を確認するために，ST-Matchの停止性，健全性及び完全性を証明した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
本研究の基礎となる理論は外山によって提案された項書き換えシステムの等価変換である．外山による枠組みは抽象書き換えシステムによって議論されていたため，本研究が対象とするSTTRSにも容易に適用できると予想していた． しかしながら，調査の結果，STTRSの枠組みでは，既存の関数を利用して新たな関数を定義した場合，帰納的定理が保存されない，すなわち，帰納的定理の外延性が成立しないという問題が明らかとなった．新たな関数を導入することはプログラム変換において基本となる技術であるので，この問題は重大である． そこで，自然帰納的定理の概念を導入し，自然帰納的定理が外延性を満たすことを示した．自然帰納的定理を応用してSTTRSの等価性を検証する手法を提案することが今後の目標である． 単純型付き項パターンの概念を用いることによってSTTRSにおける変換パターンを実現できる．また，単純型付き項パターンマッチングアルゴリズムST-Matchを適用することで，変換パターンと入力されたプログラムのパターンマッチングを解決することが可能である．ST-Matchの停止性，健全性，完全性は証明済みであるので，ST-Matchの有用性も確認された．
|
| 今後の研究の推進方策 |
はじめに，自然帰納的定理の概念を利用してSTTRSの等価性判定手法を提案する．さらに，STTRSの等価性判定手法に基づき，パターンによるプログラム変換の正当性検証手法を構築する．正当性検証手法とST-Matchと組み合わせることによって変換の正当性自動検証機能を備えたパターンによる高階プログラム自動変換の枠組みを実現する． RAPT(Rewriting-based Automated Program Transformation system)は1階の項書き換えに基づいたパターンによるプログラム自動変換システムである．上記の結果を基にRAPTを拡張し，STTRSに基づいたパターンによるプログラム変換の枠組みを計算機上に実装する．RAPTはテキストを入出力とするプログラムであり，途中結果の可読性があまり高くない．そこで，ユーザインターフェースを改良しRAPTをより使いやすいシステムとする．また，改良したRAPTを広く公開し，ユーザーからの意見を参考にすることでシステムの改良を行う． 本研究の結果をより広く利用するためには，数多くの変換パターンが必要となる．そこで，変換パターンを用意に登録できるシステムを構築し，RAPTのユーザから広く変換パターンを募集する．
|
| 次年度の研究費の使用計画 |
23年度はセルビアで開催されたRTAに参加する予定で合ったが，震災の影響で研究費交付の決定が遅れたため参加できなかった．そのため未使用額が生じた次年度は名古屋で開催される項書き換え分野ではトップの国際会議RTAに参加し，項書き換えに関する情報収集に努める．また，高階書き換えシステムをターゲットとするRTAのサテライトワークショップHORでSTTRSに基づく変換パターン，およびパターンマッチングアルゴリズムの結果を発表し，議論を通して改善点，また今後の方向性を考える．さらに，STTRSの等価性判定手法，プログラム変換の正当性検証手法を構築し，論文としてまとめ発表する．研究発表ではスライドをプロジェクタに写すためのラップトップが必要となる．そこで，研究発表用のラップトップPCとしてPanasonicのLet's noteを購入する．
|
