|
平成２6年度は、移動型並行計算モデルとしてπ-計算および高階ストリーム型通信を行う系に対して、コンテクストをラベルとする遷移システムによる操作的意味論を定義し、その妥当性の検証と双模倣等価性の定式化を行った。
π-計算の操作的意味論としては、動作をラベルとする通常の遷移系と同様な推論規則の集合を与え、それが定義する遷移関係が、従来の簡約系による意味論と整合していることを示した。また、本研究であたえたコンテクストラベルに基づく遷移系をもとに、強双模倣によるプロセスの等価関係を定義し、このように定義された等価関係が合同性を満足することを示した。
また高階ストリーム型通信を行う並行計算系のモデルとして、バイグラフをもとにした有効非巡回グラフ（DAG）を用いたグラフ書換え系を採用した。このモデルに対しては、先の年度に簡約系に基づく操作的意味論を提案していたが、平成２６年度においては新たにコンテクストラベルを用いた遷移系に基づく操作的意味論を定義した。このためにDAG上でのコンテクストの概念を新たに定義し、それに基づく代入の操作を定式化した。その上で、ここで定義した遷移系に基づく操作的意味論が簡約系に基づく意味論と整合することを示した。さらに意味論が簡約系に加えて遷移系で与えられたことにより、高階ストリーム型通信を行うモデルに対して双模倣によるプロセスの等価性が定義でき、またその等価関係が合同性を満足することを示した。
|
