|
共有メモリ型並列プログラムのゲーム意味論を、wait-notifyゲームを用いることによって構築した。wait-notifyゲームが構成する圏において、可換強モナドの計算構造が誘導されることを示し、これによって関数型言語に書き換え可能変数を加えたAlgol言語の並列拡張の意味論がゲームのKleisli圏における射として与えられることと、full absraction定理を示した。公平性を考慮した並列実行に関しても、wait-notifyゲームにおいて非決定的選択も計算資源の一種であるとみなすことによって、WN有界戦略を構成することによって意味論を与えることができた。
|
