氏名: 白井 基裕 (l0481636)
論文題目: メタ項書換え計算を用いた項書換え系の等価性判定アルゴリズムの実現
論文概要
項書換え系（TRS）の等価性証明の一つの方法として構造帰納法を用いる方法
があり、この方法を機械的に行なうために、動的項書換え計算（DTRC）を用い
る研究が伊園によって行なわれた。この方法の問題点の一つは、書換え戦略によっ
ては無限書換えに入ってしまって証明が成功しない場合があることである。本
研究では、この証明法を、DTRCを改良した計算モデルであるメタ項書換え計
算（MRC）を用いて実現する。このとき、MRCに導入されている書換え過程の
制御を行なうための同期演算を活用することで、より証明成功に導きやすい証
明法の実現とすることが目標である。この目標に向けての第一歩として、
TRS等価性判定の例が、同期演算による書換え制御で、自動
実行でも停止して証明成功に到達するようにできることを明らかにした。
目次に戻る