|
合流性を満たす高階項書換えシステムのクラスの拡張・定式化を目標として、組合せ子が持つ書換え規則から成る項書換えシステムの理論的な解析を行った。これらは合流性を満たす代表的な項書換えシステムとして知られている。さらに、項書換えシステムを拡張した無限項書換えシステムの理論的な解析を行った。無限項書換えシステムは、ストリームといった仮想的に無限長として見做されるデータを扱う関数型プログラミシグ言語の計算モデルとして知られている。本年度の具体的な成果は以下のとおりである。1.組合せ子が持つ書換え規則から成る項書換えシステムの強頭部正規化可能性(強収束性)を調査し、組合せ子が持つ書換え規則から成る項書換えシステムの多くは強頭部正規化可能性を持たないことを反例を構成することによって示した。本研究は、第8回情報科学技術フォーラムで報告した。2.無限項書換えシステムに対する強頭部正規化可能性の反証手続きを提案し、その正当性を示した。提案した反証手続きの特徴は、より長い書換え列を可能とする代入から、変数の同一視により正則項(部分項が有限個の無限項)による反例を具体的に構築する点である。従来、このような正則項を利用した強頭部正規化可能性の反証法は知られておらず、提案手法を従来の強頭部正規化可能性の自動証明法と組合せることにより、より強力な強頭部正規化可能性の自動判定法が実現可能である。また、強頭部正規化可能性が成立しない多くの例に対して、提案手法が有効に適用できた。本研究は、第12回プログラミングおよびプログラミング言語ワークショップで報告した。
|
