| 研究概要 |
並列計算システムの形式性, 記述性, 理解性, 簡潔性に優れた仕様記述ならびに検証のための体系の基礎を確立することを目的に, 本年度は, (1)MilnerのCCSの拡張とそれに基づくHoareのモニタの動作記述, 並びに, (2)項書き換え系の代数的意味論に関する研究を行い, 所期の目的を達成した.
(1)については, 動作体と呼ばれる計算単位が, 互いに同期して通信しながら計算を進める並列計算のモデルであるMilnerのCCSモデルに拡張を施し, それを用いてHoareのモニタの動作の記述を行い, (a)排他制御と同期メカニズムの明示的記述のできることを示すと共に(b)並列計算システムにおけるデータの概念を明確にすることができた. これらの成果は, 並行プログラムにおけるデータ型の仕様記述言語の設計に応用できる.
(2)については, 無あいまい線形項書き換え系を抽象計算機械として捉え, Scott的な枠組みでその代数的意味論を与え, その諸性質を明らかにして, 抽象データ型の代数的仕様記述法へのその寄与を明らかにした. すなわち, 無限大に対する項書き換えを考え, 無限木に対する近似正規形を与え, これを用いて必ずしも停止するとは限らない書き換えの極限を定式化することによって, 項書き換え系の意味は, 無限木の集合の上の巾等な連続写像として与えた. 更に, この意味論を代数的な観点から検討し, 次のような結果を示した. まず, この写像から導かれる無限木の集合上の同値関係が, 代入と両立するような合同関係であることを示し, この結果を用いて, この合同関係から定まる商代数はADJの提案した連続代数になっていること, および, この同値関係が妥当であるようなすべての連続代数からなるクラスに対する自由代数になっていることを明らかにした. これらの諸結果は, 代数的仕様記述法の基礎を与えるものである.
|
