並行システムの実行時プログラム変換の形式化についての研究

点击翻译按钮获取中文摘要

本研究は,並行プロセスのソフトウェアの動的発展機能の形式的記述を確立することを目指すものである.その具体的手法として,与えられたプログラムの変換と実行を同時に進行させるプロセスの形式的記述を検討するものである.本研究で変換の対象とするプログラムのクラスは,応答型の並行プロセスである.まず本研究では、並行プロセスの機能の一部を起動中に外部からの要求に応じて変更する手法を提案した.ここで対象とする並行プロセスは線形論理の論理式の記法で記述されたものであり、非同期π計算と同等な記述能力をもつ.プロセスの起動及びメッセージの発信は○左導入の推論によって、またメッセージの受信は。左導入の推論規則によって表現される.その操作的意味論はシークエント計算LLの部分体系での証明によって記述される.本研究では、現在有効なプロセスの定義を機能の変更を求めるメッセージによって新しい機能のプロセス定義に置き換える機構を、線形論理の論理式の記法により記述する手法を提案した.このような機構の動作も、LLの推論規則によって構成される証明によって記述される.さらに本研究では逐次的に実行される部分を含も並行プロセスを並列実行する方法について考察する.ここで対象とする並行プロセスは線形論理で記述されたものであり、その操作的意味論はLK風のシークエント計算の推論規則によって記述される.本稿ではこの体系に並列実行のための規則として、プロセス定義の展開のための規則と値を将来実行される部分に伝搬して分岐を枝刈りのための規則を導入した.これらの規則を用いた推論がLLの体系で可能であることから、見込み計算によるプロセスの並列実行が線形論理におけるシークエント計算での証明の枠組みの中で記述できることを示した.またこれらの規則を用いた並列実行に対して、外部から観測した際に同等な計算とみなせる逐次実行が存在することを示した.