非停止プロセスの抽象化と代数的仕様記述に関する基礎的研究

1988 年度 実績報告書

• 研究課題/領域番号: 63580025
• 研究機関: 名古屋大学
• 研究代表者: 坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829)
• 研究分担者: 平田 富夫 名古屋大学, 工学部, 助教授 (10144205) ; 稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
• キーワード: 非停止プロセス / 等式論理 / 代数的仕様 / 並行プロセス / CCS

研究概要

本研究では昭和63年度に
1.無限計算過程が陽に表現できる有理等式論理の定式化。
2.有理等式論理を基礎にした代数的仕様記述の意味論の検討
3.有理等式論理と項書換え系との関係の解明
の研究を計画した。
まず、計画の1.および2.については次のような研究成果を得ることができた。
当初の有理等式論理における有理項は、関数の再帰的定義が項の中で記述できるように従来の項を拡張したものであったが、非停止プロセスの記述を容易にするため、さらに拡張して、関数の一般再帰的定義が項の中で記述できるようにした拡張有理等式論理を考案した。構文論についてはほぼ確定しているが、意味論、推論規則については現在検討中である。また、これと並行して、拡張有理等式論理の評価を行うプログラムのプロトタイプを作成中である。
計画3.については有理項の書き換えに必要な木パターンマッチングの高速化に関する成果を得た。
当初の計画にはなかったが、CCSと有理等式論理の間の関係を解明することを計画に加えることにしたので、CCSについての研究も進め、とくに通信ポートの動的な名前づけを許すCCS(拡張CCS)について検討を加え、拡張CCSの意味論に関する結果を得ている。
設備としては、計画通り、代数的仕様記述言語の処理系、検証支援系の開発のためにUNIXワークステーション(サンマイクロ社製SUN3160HM)を購入した。本ワークステーションの導入により、有理項のインタプリータや代数的仕様の直接実行システムなどの開発のために必要なプログラミング作業の能率が向上した。

研究成果

• [文献書誌] 結縁祥治,坂部俊樹,稲垣康善: 情報処理学会研究報告. 88ーSFー26. 26.6.1-26.6.10 (1988)
• [文献書誌] 平田富夫,稲垣康善: 情報処理学会研究報告. 88ーALー4. 4.1.1-4.1.7 (1988)
• [文献書誌] 酒井正彦,坂部俊樹,稲垣康善: 電子情報通信学会技術研究報告. COMP88ー86. 83-92 (1989)
• [文献書誌] 酒井正彦,坂部俊樹,稲垣康善: 電子情報通信学会技術研究報告. COMP88ー93. 37-40 (1989)
• [文献書誌] 山本晋一郎,酒井正彦,坂部俊樹,稲垣康善: 電子情報通信学会技術研究報告. COMP88ー94. 41-50 (1989)
• [文献書誌] 山中英樹,坂部俊樹,稲垣康善: 電子情報通信学会技術研究報告. COMP88ー96. 61-70 (1989)