| 研究課題/領域番号 |
23700034
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
千葉 勇輝 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
|
|---|
| キーワード | プログラム変換 / パターンマッチング / 単純型付き項書き換えシステム |
|---|
| 研究概要 |
パターンによるプログラム自動変換において，変換の正当性は入出力システムの等価性によって定義される．本研究では研究代表者による1階項書き換えに基づくパターンによるプログラム変換の枠組みを拡張し，高階プログラムを取り扱うことができる枠組みの提案を目指している．従来の1階項書き換えでは高階プログラムを直接取り扱うことは難しいので，Yamada (2001)によって提案された単純型付き項書き換えシステム(Simply Typed Term Rewriting Syste, 以下STTRS)を用いて枠組みを構築する．
前年度までの研究実績で，1階項書き換えの枠組みでは自明に成立する下記の命題(1)がSTTRSでは一般に成立しないことが確認された．
(1) 任意の基底項tが導入規則によって導入された関数記号を含んでいる場合，tは正規形ではない．
上記の命題(1)は等価変換手続きによって等価性を保証するために欠かせない命題である．
平成25年度は，相対停止性の概念を用いることによって命題(1)を解決することができることを明らかにした．相対停止性とは，他のシステムによる書き換えをを法とした書き換えが無限に起こらないことである．導入規則によって導入された書き換え規則が，入力STTRSに対して相対停止性を持つ場合，命題(1)が成立する．STTRSの停止性，相対停止性は一般的に決定不能な問題である．Geserによって示された停止性チェックを組み合わせた判定基準を応用することで，STTRSの相対停止性を示すことが可能である．また，STTRSの停止性はToyamaが提案した再起経路関係により判定できる．これらの技術を応用することで，STTRSの等価性の判定が可能となる．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究の目標であるSTTRSに基づくパターンによるプログラム自動変換では，STTRSの等価変換手続きが変換の正当性を保証するための基礎となる．相対停止性の概念を導入することにより，等価変換手続きによってSTTRSの等価性を示すことが可能となった．また，本研究の枠組みにおける変換パターンのシンタックスや，パターンマッチングアルゴリズムはすでに完成している．従って，本研究における理論的枠組みの構築ははほぼ完了した．
等価変換手続きによってSTTRSの等価性を自動検証するためには，STTRSの合流性，高階十分完全性，停止性，相対停止性，および仮定した帰納的性質の自動証明が必要となる．これらはすでに自動検証方法がいくつか知られている．その自動検証手法を組み合わせることにより，STTRSの等価性の自動検証が可能となる．本研究の目的のうち，
1. 変換の正当性を示すために, STTRS の等価性を検証するアルゴリズムの提案，
2. 変換パターンの概念を構築，および
3. 1 に基づき,変換の正当性を検証する手法の提案，
が完了したこととなる．
|
| 今後の研究の推進方策 |
本研究では，今後は25年度までに得られた理論的枠組みを計算機上に実装し，パターンによる高階プログラムの自動変換システムを構築することを目指す．STTRSの合流性，停止性，相対停止，および，高階十分完全性の判定手法を実装し，変換の正当性自動検証を実現する．また，STTRSの高階パターンマッチングアルゴリズムST-Matchを実装し，パターンによるプログラム自動変換手続きを実装する．
本研究で実装したシステムを適用してプログラム変換を実現するためには，変換パターンをあらかじめ準備する必要がある．SML/NJやHaskellといった関数型プログラミング言語におけるプログラム自動変換を調査し，本研究における理論的枠組みの基礎であるSTTRSを用いて変換パターンを作成する．作成した変換パターンを利用して実験をすることにより，本研究で実装したシステムの有用性を確認する．
|
| 次年度の研究費の使用計画 |
平成23年度はセルビアで開催された国際会RTAに参加する予定であった．しかし，震災の影響で研究費交付の決定が遅れたため参加できなかった．そのため未使用額が生じ，その未使用額が現在まで続いている．
次年度は7月にオーストリアで開催される書き換え分野ではトップの国際会議RTAに参加し,項書き換えに関する情報収集に努める．また，プログラム変換に関するRTAの併設ワークショップであるWPTEに参加，研究発表を行い議論を通して具体的な問題を理解する．また，毎年2回国内で開催されているTRS meetingで発表を行い議論を通して本研究の理論を更に深める．
|
