| 研究概要 |
本年度は,以下のとおり,書換えシステムの最適化技法としての特殊化を考案し,計算機実験を行なうとともに,中規模以上のソフトウェアを記述する際に必要不可欠である(書換えシステム用の)モジュールシステムを設計した.
1. 書換えシステムの最適化技法:Jim Christianの高速定理証明器HIPERで採用されている弁別ネットは,パタン照合を高速化できる点および書換え規則の追加・削除が低コストでできる点が優れており,HIPERのようなKunth-Bendix完備化を基礎とする定理証明器では真価を発揮する.ただし,必要以上に記憶領域を必要とする,という欠点も合わせ持つ.そこで,必要以上に記憶領域を必要としない弁別ネットのコンパクトな表現方法を考案した.このコンパクトな弁別ネットに関して,パタン照合器を特殊化する方法を提案し,計算機実験を行なった.さらに,項(式)を書換え規則で書換える(置換える)際に用いる,具現化手続きも各書換え規則ごとに特殊化することも行った.簡単なベンチマークプログラムによる計算機実験により,特殊化した照合器を用いた方が,汎用の照合器を用いる場合に比べ,5倍程度の高速化を実現できたことを確認した.
2. 書換えシステム用モジュールシステムの設計・検証:中規則以上のソフトウェアを記述するには,モジュールシステムは必要不可欠である.書換えシステム用モジュールシステムの仕様をCafeOBJで記述し,モジュールシステムのデータ構造をStandard MLの実装を参考に設計するとともに,その仕様をCafeOBJで記述した.前者の仕様を要求仕様,後者を設計仕様を呼ぶ.設計仕様が要求仕様の詳細化であることをCafeOBJを用いて検証した.
以上をもとに,次年度では,書換えシステムの最適化技法としての特殊化の有効性を,より規模の大きいベンチマークで確認するとともに,書換えシステムTRAMに適用する.また,設計したモジュールシステムを実装し,データ構造の妥当性を確認する.
|
