| 研究概要 |
本研究では,文脈依存書換え系を標準的な項書換え系に変換する手法について考察を行なった.文脈依存書換えとは,Lucasにより提案された,項書き換えの拡張である.文脈依存書換えでは,関数記号のどの引数を評価すべきかを指定することができ,これにより,一種の簡約戦略を記述することが可能になる.本研究で主に取り組んだのは,停止性に関する変換手法に関する理論的考察である.特に,健全性をもつような変換,つまり,変換後の項書換え系の性質から,変換前の文脈依存書換え系の性質を保証できるような変換について,理論的性質を明らかにした.健全な変換を用いる利点は,既存の項書換え系の性質の証明手法が,そのまま,文脈依存書換えの性質の証明に利用できる点にある.
本研究では,停止性証明のための2つの新しい変換法を開発した.第1の変換法は,これまでに知られていた変換法よりも強力であり,しかも簡潔な変換法である.第1の変換法は,健全性をもつが,完全性がない.つまり,停止性をもつ文脈依存書換え系を変換しても,変換により得られる項書換え系が停止性をもたない場合がある.これを改良して得られた第2の変換法は,健全性に加え,完全性をも満たす.この,完全性を満たす変換法の発見により,文脈依存書換えの停止性証明法を新たに開発する必要性がないことが,理論的に明らかになった.以上の2つの変換法の研究は,主に,Darmstadt工科大学のJurgen Gieslとの共同研究により得られ,書換え理論とその応用に関する国際会議RTA'99において,成果を公表済みである(論文一覧を参照).さらに,書換え系の変換法の比較に関する研究を行なうことにより,依存対を用いる停止性のための変換手法が,ダミー除去と呼ばれる停止性のための変換手法よりも強力であることを証明した.この研究により,依存対による変換の前処理としてダミー除去をする必要がないことが理論的に明らかになった.ダミー除去を中心とした変換法の比較に関する研究は,学術誌Acta Informaticaへの掲載が決定している(論文一覧を参照).
|
