| 研究課題/領域番号 |
02680020
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829)
|
|---|
| 研究分担者 |
酒井 正彦 名古屋大学, 工学部, 助手 (50215597)
直井 徹 名古屋大学, 工学部, 助手 (10207699)
平田 富夫 名古屋大学, 工学部, 助教授 (10144205)
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
|
|---|
| キーワード | 論理型計算モデル / 関数型計算モデル / 並行計算 / CCS / ナロ-イング / 並行プロセス / 同期通信 |
|---|
| 研究概要 |
本研究では並行計算モデルとして動的に書換え規則が変化するナロ-イングシステム(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を用いることで、並行プロセスの制御のために基本的である通信の入出力のマッチングが自然に記述されることが示せた。
|
