| 研究概要 |
本研究の目的は,「高階並行プロセス計算モデル」を構築し,その動作的意味論に関する基礎理論を確立すること,および,以上に基づいたプログラミング言語を開発し,実践を通して本モデルと基礎理論の妥当性を実証することである.本年度は,以下の項目に関して,以下の成果を得た.
(1)高階並行プロセス計算モデルの構築
高度な計算パラダイムを有する並行システムを記述・解析するための「高階プロセス計算モデル」を構築した.このモデルは,それぞれ研究項目(2),(3)で展開する数学的議論とプログラミング言語のベースモデルとなる.
(2)高階並行プロセス計算の動作的意味に関する数学的基礎理論の確立
(1)で提案した計算モデルに対して,以下の小項目に関する研究を実施し,その数学的基礎を確立させた.
(a)双模倣の概念による等価性:第2階のλ計算などに適用された適用双模倣性に基づいた等価性について検討し、高階プロセスの動作的意味を十分に反映した等価性の理論を与えた.
(b)高階様相論理体系とモデルチェッキング:高階論理を用いた高階プロセスの記述に適した証明システムを提案し,その健全性・完全性などの諸性質や,(a)で与えた等価性との関係に関する特性化定理を与えた.また,タブロ-法などのテクニックを用いたモデルチェッキング法の可能性を模索した。その場合計算可能性を考慮し,プロセスに妥当な制限を与え,ベース論理の1階論理への帰着可能性を示すことが重要となった.
(c)多相タイプシステム:高階システムに適したタイプ原理と具体的な多相タイプシステムを与えた.タイプシステムは,静的解析に用いられる他,高階プロセス計算の体系を与える際にも重要となった.
(d)等価性の公理化:より現実世界のモデルに制限した場合の公理化の可能性について検討した.
|
