1990 Fiscal Year Annual Research Report
| Project/Area Number |
02680020
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
酒井 正彦 名古屋大学, 工学部, 助手 (50215597)
直井 徹 名古屋大学, 工学部, 助手 (10207699)
平田 富夫 名古屋大学, 工学部, 助教授 (10144205)
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
|
|---|
| Keywords | 論理型計算モデル / 関数型計算モデル / 並行計算 / CCS / ナロ-イング / 並行プロセス / 同期通信 |
|---|
| Research Abstract |
本研究では並行計算モデルとして動的に書換え規則が変化するナロ-イングシステム(Dynamic Narrowing System,DNS)を検討して、高信頼性並行プロセス型ソフトウェアの開発技術の基礎を確立することを目的とし、平成2年度では、(1)DNSの定式化(2)DNSのシミュレ-タの開発、(3)DNSからCCSへの変換に関する研究を進めることを計画し、以下のような成果を得た。
まず、DNSの定式化の準備段階として、ナロ-イングの特別の場合である通常のパタ-ンマッチングによる書換え計算モデル(Dynamic Term Rewriting Calculus,DTRC)を定式化し,その表現能力を検討した。その結果、DTRCによって、単一化、拡張単一化、項書換え系の等価変換、等式理論の帰納的定理の構造帰納法による証明などが自然に表現出来ることが示せた。
次に、DNSのシミュレ-タとDNSにへの変換については、CCSに関連した研究を推進した。すなわち、CCSのシミュレ-タを開発すると共に、通信される値を等式で定義できるCCS(CCS/cond)の定式化を行い、その意味論、表現能力を検討した。CCS/condにおいては、等式の解釈は、等式を書換え規則と見なして、動作式の振舞いの中に含められる。このことにより、値の意味を含む動作式の意味がその振舞いだけから定義できるようになる。振舞いのみによる定義は、値の意味記述を含むCCSの動作式の実行に対応する。CCS/condを用いることで、並行プロセスの制御のために基本的である通信の入出力のマッチングが自然に記述されることが示せた。
|
-
[Publications] 結縁 祥治: "CCSによるモニタの動作の形式的記述" 電子情報通信学会論文誌. J73ーDーI. 683-692 (1990)
-
[Publications] 酒井 正彦: "代数的仕様記述法に基づく言語処理系の自動生成システム" 電子情報通信学会論文誌. J73ーDーI. 829-838 (1990)
-
[Publications] 酒井 正彦: "代数的仕様の検証のための被服集合帰納法" 電子情報通信学会技術研究報告. COMP90ー5. 37-46 (1990)
-
[Publications] 結縁 祥治: "CCSlcond:等式によって値の意味と導入したCCS" 電子情報通信学会技術研究報告. COMP90ー10. 11-19 (1990)
-
[Publications] 山本 晋一郎: "並列分散TRSシミュレ-タの実現方法について" 情報処理学会研究報告. 91ーSFー38. 1-9 (1991)
-
[Publications] 島谷 隆司: "グラフの推移的閉包をオンラインで計算するアルゴリズム" 電子情報通信学会論文誌. J73ーDーI. 705-706 (1990)
