氏名: 早川　　香奈子 (089531442)

論文題目: メタ項書き換え計算による項書き換え系の等価性判定の自動化

論文概要

 プログラムの等価性判定の研究は、プログラム検証や等価変換において
さまざまな応用ができる。このような議論には項書き換え系(ＴＲＳ)の
ような形式的な言語が用いられることが多い。ＴＲＳは方向づけられた
等式の有限集合で、その等式にしたがって与えられた項を書き換えてい
くことがＴＲＳにおける計算である。
 このＴＲＳの等価性判定の自動化について、
 
     １.２つのＴＲＳが等価であることを構造帰納法や被覆集合帰納法
         などの帰納法で証明するための命題の自動生成
     ２．生成された命題の自動証明
     
などの研究が動的項書き換え計算(ＤＴＲＣ)やメタ項書き換え計算(ＭＲＣ)
というＴＲＳを拡張した計算モデルなどを用いて行われている。
 ＭＲＣは、ＤＴＲＣの構文の制約を少なくしてより単純にすることでそ
の表現能力を改善したもので、

     ・ＴＲＳの組み合わせの記述
     ・ＴＲＳの自動検証やルールの書き換えなどのＴＲＳの処理の記述
     ・ＴＲＳの処理を扱う処理プログラム自体の自動検証
     
などの実現を目的とした計算モデルである。
 本研究では、上記１,２をＭＲＣで実現すること、つまり、帰納法で証明
するときの基底段階や帰納段階を表すメタ項生成アルゴリズム自体をＭＲ
Ｃで記述し、さらにそのメタ項で表現される命題の証明もＭＲＣで自動的
に行うことをめざし、その第一段階として、２つのＴＲＳから被覆集合帰
納法で用いる被覆集合を自動生成するプログラムをＭＲＣで記述する。

目次に戻る