| 研究概要 |
本研究では,意味ラベリングと呼ばれる,項書換え系の停止性を証明する手法について考察を行なった.Zantemaは,意味ラベリングを等式付き書換えへ拡張しているが,この拡張は制限が強い.このため,(1)意味解釈を与える代数上の順序(半順序または擬順序)(2)代数と書換え系の関係(モデルまたは準モデル)(3)等式に現われる関数記号のラベル付け可能性(禁止または許可)の3つをパラメタ化することにより,強力な意味ラベリングの手法を導入した.Ohsaki,Gieslらとの共著論文では,この新しい停止性証明手法が健全性と完全性をもつことを証明し,応用の可能性を示した(論文一覧を参照).
また,遅延ナローイング計算系の完全性に関する考察も行なった.我々は,以前に発表した研究論文で,遅延ナローイング計算系LCNCが,条件部に外変数をもつ条件付き書換え系において,正規解に関して完全性をもつことを証明した.しかし,この論文中では,有用な選択関数を与えることができなかったため,計算系を実装する際,全ての解を列挙するために,ゴール中の等式を選択する場所へのバックトラックが必要となった.本研究では,この問題を解消するため,最左の等式を選択することにより,完全性が得られることを証明した.得られた研究成果は,Suzukiとの共著論文により公表する予定である(論文一覧を参照).
Durandとの共著論文(論文一覧を参照)では,必要呼び計算の研究に有用な理論を導入した.この理論をでは,木オートマトンと基底木変換系を用い,簡潔な決定可能性の証明を与えることができる.本研究では,停止性の成立する書換え系に関する所属問題のモジュラー性について考察を行なった.まず,関数記号を追加した場合の性質の保存について考察を行なった後,書換え系に対する制約を強めることにより,一般のモジュラー性や,構成子記号の共有を許す場合に,同様の結果が成立するかどうかも調べた.
|
