氏名: 冨田 泰弘 (289934184)

論文題目: 代入が制約されたR単一化判定アルゴリズムに基づく

R単一化子の発見法とその実現


論文概要

単一化問題とは、二つの目標項 s,t と項書き換え系Rが与えられたとき、R によって sσ と tσ から共に到達可能な項 u と代入 σ が存在するか否かを判定する問題である。 このとき解を与える代入σ を単一化子という。 Kaji(1997)らは、ある線形条件の下で、木オートマトンを用いた単一化問題の 解法の手続きを提案した。しかし、Kajiらの手続きは二つの目標項が単一化可能かどうか を判定するだけのアル ゴリズムである。 例えば、暗号通信規約の安全検証において、Kajiらの手続きでも盗聴の可能性を知ること はできるが、 代入が求まらないために盗聴の方法が判らない。

そこで本研究では、この手続きを拡張して、単一化子を 計算し表示する機能を追加する。 Kajiらの手続きを変更し代入をも求めるためには、木オートマトンの空判定問題を解く際 に、 同時に受理系列の一つを求めておく。 また、受理系列と代入の間には密接な関係があるため、 M'(s)およびM'(t)の状態と遷移規則を変更する際にそれと関係する代入を テーブルに記憶しておき、随時テーブルを参照したい。そのために代入付木オートマトン を導入した。代入付木オートマトンとは、 項を状態として、状態と、代入と、新しく加えてよい変数の集合が、組になって遷移して いく木オートマトンである。 項と、代入と新しく加えてよい変数の集合の組は、オートマトンの一動作毎に変化してい く。 各動作で求められた代入を合成することにより単一化子を求めることが可能になった。


目次に戻る


提出時刻:2001/02/06 14:13:36