項書き換えシステムのモジュラ性

概要

論文の詳細を見る
項書き換えシステム(TRS)は等式にもとづく柔軟な計算法と効率的な証明法を提供できるため、定理自動証明、関数型あるいは論理型言語、代数的仕様記述、記号処理、プログラムの検証、合成、変換など、計算機科学のさまざまな分野で広くもちいられている。項書き換えシステムは方向付けられた等式(書き換え規則)の集合として定義される。項書き換えシステムの計算は、これらの書き換え規則を繰り返し適用することによって与えられた項がもっとも単純な形(正規形)に到達するまでリダクションすることで実現される。このようなリダクション過程でもっとも重要な性質は合流性(チャーチ・ロッサ性)と停止性である。これらの性質は一般に決定不可能であるため、さまざまな十分条件が提案されている。また、項書き換えシステムのモジュラ性を利用して、複雑なシステムを単純なシステムに分解して合流性や停止性を解析する手法も研究されている。このようなモジュラ性は、関数型プログラムや仕様記述の理論において重要な役割を果たすことが期待される。ここでは、合流性と停止性を中心に項書き換えシステムのモジュラ性について紹介する。
1996-09-18