氏名: 伊園基宏 (m953402)
論文題目: 動的項書き換え計算を用いた項書き換え系の
等価性判定の自動化に関する研究
論文概要
プログラムの等価性は、プログラムの信頼性向上のために最も基本的な問題
の一つである。例えば、同一目的のプログラムを複数作成し、それらが等価で
あることを示すことができれば、そのプログラムの信頼性は高い。また、仕様
とプログラムが同一の言語で記述される場合には、両者の等価性を示すことで
プログラムが仕様を満たすことの検証ができる。
プログラムの等価性証明について議論を行なう場合、項書換え系（TRS）な
どの形式的な計算モデルを用いると都合がよく、実際、これまでにさまざまな
研究が行なわれている。TRS は方向付けられた等式の有限集合で、その等式に
従って与えられた項を書き換えていくことが TRS によって表される計算であ
る。馮 [94] では動的項書換え計算（DTRC）という TRS を拡張した計算モデ
ルを用いた TRS の等価性判定法が提案されている。その方法は概略次の通り
である。2つの TRS と被覆集合帰納法で使われる被覆集合が与えられたとき、
[< 等価性証明の環境 >](and([;: Hyp1](t1),...,[;: Hypm](tm)))
という形の DTRC 項を構成する。そして、この項を評価した結果が
[...](true) の形の DTRC 項になれば 2つの TRS が等価であるとする。この
方法では、2つの TRS の他に被覆集合を与えなければならないため、完全な等
価性証明の自動化にはなっていない。
本研究では、与えられた 2つの TRS がある条件を満たすとき、その TRS か
ら等価性証明に使える被覆集合を合成し、その被覆集合を用いて上述の DTRC
項を生成するアルゴリズムを示すとともに、その健全性、すなわち、生成され
た DTRC 項の評価が [...](true) になれば 2つのTRSは等価であることの証明
を与えた。このアルゴリズムにより、TRS の等価性判定の自動化が可能となる。
本論文の等価性判定法を、Toyama [91] で取り上げられている等価な TRS
の例に対して適用したところ、13例のうち 11例については自動証明に成功し
た。残りの 2例については自動証明に成功する被覆集合を合成できなかった。
これらの例に対してはユーザが被覆集合を与えなければ自動証明に成功しない。
今後はこのような例に対しても自動証明に成功するように、被覆集合の合成法
を改良するのが課題である。
目次に戻る