1998 Fiscal Year Annual Research Report
| Project/Area Number |
10780180
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
|
|---|
| Keywords | 書換えシステム / 最適化 / 特殊化 / 弁別ネット / TRAM / CafeOBJ / モジュールシステム / データ構造 |
|---|
| Research Abstract |
本年度は,以下のとおり,書換えシステムの最適化技法としての特殊化を考案し,計算機実験を行なうとともに,中規模以上のソフトウェアを記述する際に必要不可欠である(書換えシステム用の)モジュールシステムを設計した.
1. 書換えシステムの最適化技法:Jim Christianの高速定理証明器HIPERで採用されている弁別ネットは,パタン照合を高速化できる点および書換え規則の追加・削除が低コストでできる点が優れており,HIPERのようなKunth-Bendix完備化を基礎とする定理証明器では真価を発揮する.ただし,必要以上に記憶領域を必要とする,という欠点も合わせ持つ.そこで,必要以上に記憶領域を必要としない弁別ネットのコンパクトな表現方法を考案した.このコンパクトな弁別ネットに関して,パタン照合器を特殊化する方法を提案し,計算機実験を行なった.さらに,項(式)を書換え規則で書換える(置換える)際に用いる,具現化手続きも各書換え規則ごとに特殊化することも行った.簡単なベンチマークプログラムによる計算機実験により,特殊化した照合器を用いた方が,汎用の照合器を用いる場合に比べ,5倍程度の高速化を実現できたことを確認した.
2. 書換えシステム用モジュールシステムの設計・検証:中規則以上のソフトウェアを記述するには,モジュールシステムは必要不可欠である.書換えシステム用モジュールシステムの仕様をCafeOBJで記述し,モジュールシステムのデータ構造をStandard MLの実装を参考に設計するとともに,その仕様をCafeOBJで記述した.前者の仕様を要求仕様,後者を設計仕様を呼ぶ.設計仕様が要求仕様の詳細化であることをCafeOBJを用いて検証した.
以上をもとに,次年度では,書換えシステムの最適化技法としての特殊化の有効性を,より規模の大きいベンチマークで確認するとともに,書換えシステムTRAMに適用する.また,設計したモジュールシステムを実装し,データ構造の妥当性を確認する.
|
-
[Publications] 五百蔵,緒方,二木: "モジュールシステムを備える書換え抽象機械の提案" 信学技報. 98・86. 1-8 (1998)
-
[Publications] Nagaya, Matsumoto, Ogata, Futatsugi: "How to give local ctiategias to function symbol for equality of two implomentations of the E-strategy with and without evaluation plags" Proc.of Asian Symposium on Computer Mathematics. 71-81 (1998)
-
[Publications] Ogata, Hirata, Ioroi, Futatsugi: "Experimantal implementation of Parallel TRAM on massively pallel computer" LNCSC Proc.of Euro-Par'98). 1470. 846-851 (1998)
-
[Publications] 五百蔵,緒方,二木: "モジュールシステムの要求仕様と設計仕様" 信学技報. 98・294. 7-14 (1998)
-
[Publications] 五百蔵,緒方,二木: "CafeOBJのモジュールシステムの設計およびCafeOBJによる検証" ソフトウェア工学の基礎V(レクチャーノート/ソフトウェア工学). 20. 209-218 (1998)
-
[Publications] Ogata, Ioroi, Futatsugi: "Optimizing tetra relating using discrimination nets with spacialization" Proc.of the 1999ACM Symposium on Applied Computing. (1999)
