| 研究概要 |
前年度に得られた,単純型付き項書き換え系の停止性証明技法の実験システムの実装を行い,実験を進めた.他方,理論的な解析を更に進めた結果,単純型付き項書き換え系の簡約関係について次のような新たな考察が得られた.(1)単純型付き項書き換え系の簡約関係は,特殊なソート付き項書き換え系の簡約関係と対応する.(2)意味ラベリング法を用いることにより,頭部記号を根記号のラベルとして取り入れても簡約関係が保存される.これらの考察を応用することにより,前年度に報告を行なった停止性証明技法の高度化が可能となる.この結果は,項書き換え分野の代表印な国際会議の1つであるRTA(書き換え技法と応用)'03に採録され,国際的な報告を行なった.
次に,AC記号を明示的にではなく,暗黙的に組み込む手法について考察を進めるため,高階項書き換え系における帰納的定理証明について解析を,進めた.具体的には単純型付き項書き換え系を用いて,関数の等価性を可能にする帰納的定理の枠組みについて考察を進めた.その結果,従来の帰納的定理の枠組みを拡張することにより,高階記号がある場合でも自然となる枠組みが構築できることが判明し,これを高階帰納的定理として形式化した.次に,高階帰納的定理の自動証明法について考察を進め,潜在帰納法の原理に基づく手法を構築した、これらの結果に基づいて,高階関数型プログラムにおける帰納的定理証明の,枠組みと自動証明技法についてFIT2003情報科学技術フォーラムにおいて報告を行った.
|
