1
日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

公平な並列実行のためのゲーム意味論
西村 進

Algol 風の並列プログラミング言語に対して，その公平な並列実行のゲーム意味論を提案する．従来のゲーム意
味論では，可能なゲームの進行を規定する安全性 (safety) のみ表現することが可能であり，公平性のような活性(liveness) を規定する術を持ち合わせていなかった．本稿では，先行研究で提案した wait-notify ゲームを発展させ，
非決定性を誘導する可能性のある計算資源一般へのアクセスをゲーム列の中に明示する．これによって，プログラ
ムは非決定性の度合いが特定のゲーム手の出現数によって有界に制限される WN 有界戦略となることが示される．
WN 有界戦略と公平なスケジュールに相当する戦略の合成により，外延的ゲーム意味論を導出し，これが公平な並列実行の操作的意味論に関して完全抽象であることを示す．

本稿では，Algol 風の共有変数並列プログラミング

1 はじめに言語に対して，公平な並列実行のためのゲーム意味論

並列プログラムの実行は，複数の逐次スレッドの[11] [3] を提案する．ここで提案するのは，Harmer に実行を細切れにしこれらを適当に並べ換えて順番による有界非決定性のためのゲーム意味論 [9] [10] を基

実行 (インターリーブ実行) しているものとして理解にしたものである．公平な並列実行をモデル化する際できる．並列実行は，各システム固有のスケジューラに問題となるのは以下の２点である．

の実装および偶然性に依存して決まる複雑度の高い

ゲームモデルの逐次性 Harmer のゲーム意味論は計算現象であるが，いわゆる公平性 — すべての並列

Hyland-Ong 流のゲームの定式化 [11] を踏襲してスレッドは等しく実行の機会を与えられるという性

おり，オセロや将棋のようにふたりのゲーム参加

質— は多くの並列システムに共通する一般的な性質

者 (Opponent および Player と呼ばれる) が自分と仮定して議論することができる．

のゲーム手を交互にひとつずつ打つことでゲー

しかしながら，公平性は並列プログラムの振舞いにムを進行する形を取る．このゲームモデルの逐次重大な違いをもたらすことがある．次のようなプログ性 (sequentiality) のため，複数の並行する計算

ラム (文献 [18] より引用．newvar は局所変数のスコーをゲーム列 (ゲーム手の交互列) としてモデル化

プ，∥ は並列実行を表す) を考えよう．

することが困難になる．
活性の欠如 ゲーム意味論では，プログラムの実行

newvar u = 0 in newvar v = 0 in
(u:=1 ∥ while ! u = 0 do v:=! v + 1)

(1)

をゲーム戦略で表現するが，ゲーム戦略はゲーム

公平なスケジューラの下ではコマンド u:=1 はいつか

列 (の有限偶数長プレフィックス) の集合で表す

必ず実行されプログラムは停止する．一方，公平でなため，どのような実行が可能かのような安全性

いスケジューラの下では，コマンド u:=1 のスレッド(safety) は表現できても，公平性のように無限長が永遠にスケジュールされないかもしれないのでこののゲーム列を考慮する必要がある活性 (liveness)

プログラムは停止しない可能性がある．

を記述することはできない．

Susumu Nishimura, 京都大学大学院理学研究科, Graduate School of Science, Kyoto University.

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

2

1. 1 Wait-notify ゲームと非決定性計算資源

定的にどちらかを選択する非決定的計算．

逐次性の問題に関しては，渡辺と西村が wait-notify

再帰不動点 不動点演算子 fix M による再帰呼び

ゲーム [20] [17] による解決方法を提案している．例え出し．非決定性とは無関係のように見えるが，発ば次のような並列プログラムを考えよう．

散 (停止しない計算) もひとつの非決定的選択肢

v:=0 ∥ v:=! v + 1のひとつと考えると，プログラム例 (1) で見たよ

ゲーム意味論では，第 1 のスレッドが変数 v に 0 をうに不動点演算子が導く潜在的な発散と公平性

書き込む動作をゲーム列 run·wr0 ·ok·done で，第 2 のは密接に関連しており，再帰呼び出しを非決定性スレッドが変数 v から値を読み込んだ後 v に値を書に関連する計算資源とみなすのがふさわしい．

き込む動作をゲーム列 run·rd·n·wrn+1 ·ok·done でそれぞれ表現する．並列実行において，第 2 のスレッド

1. 2 公平な無限ゲーム列とスケジューラ戦略

が変数から値を読み込んだ直後 (変数に書き込む前)公平性の問題に関しては Harmer のゲームモデルに，第 1 のスレッドが変数に書き込むという振舞い

における発散の扱いを洗練することによって解決すは例えばる．Harmer のモデルでは，ふたつのゲーム戦略の合

run·rd·n·run·wr0 ·ok·done·wrn+1 ·ok·done

成によって無限に続くゲーム列が生成されたときこれのようなゲーム列 (可読性のため第 1 スレッド由来

をゲームモデルにおける発散と定義していたが，このゲーム手に下線を施した) で表現したいところ

れを改め，無限に続く「公平な」ゲーム列が生成さだが，第 2 スレッドによる Opponent のゲーム手 n

れたときのみが発散と定義し直す．ただし，これだけのあとに第 1 スレッドによる Opponent のゲームでは不十分である．なぜなら，非決定的な計算シス

手 run が続いており，逐次性の要件に反している．

テムにおいては公平性が非有界非決定性 (unbounded

Wait-notify ゲームでは，共有変数にアクセスする

nondeterminism) すなわち可算無限個の非決定的選度に対応するゲーム手の直前にふたつの特別なゲー

択を誘導する [18] [6] からである．(例えば，上記プロ

ム手 W と N を挿入することによってこの問題を解決

グラム (1) ではプログラムが停止したときの変数 v

する．例えば上の例の場合，第 1 スレッドのゲーム
列は run·W·N·wr0 ·ok·done，第 2 のスレッドのゲームの値は任意の自然数を持ち得る．) Harmer のモデル
では無限可算個の非決定的選択は発散を意味する†1 の列は run·W·N·rd·n·W·N·wrn+1 ·ok·done でのように表さで，公平性から意図しない発散が導かれてしまう可能れ，これらの並列実行を性がある．

run·W·N·rd·n·W·run·W·N·wr0 ·ok·done·N·wrn+1 ·ok·done

以上の公平性に関連する問題を解決したゲーム意のように逐次性を保ったゲーム列として表現すること

味論を与えるため，本稿で考察する並列言語は以下のが可能となる．

ふたつの活性条件を満たすものとする．

新たに導入されたゲーム手 W, N は通常外部からは

弱公平性 (weak fairness) ある逐次スレッドが観測できないイベントであり，W はスケジューラが変ある時点以降はいつでも次の計算を進めること

数アクセスを許可するまでの実行待機を，N はスケができる状態ならばそのスレッドはいつか必ず実

ジューラによるアクセスの許可を表していると考える

行の機会を与えられる．

ことができる．本稿では，この解釈をより一般化し，持続性 (vitality) [4] 計算を終了していないどの非決定性を誘導する可能性のあるすべての計算資源スレッドもいつかは観測可能なイベントを生成へのアクセスの直後にゲーム手 W, N を挿入する．本する．

稿で考察すべき非決定性に関連する計算資源には，変数アクセスに加えて次のふたつがある．
有界非決定性選択 Harmer の非決定性ゲームモデ
ルで考察された，ふたつの自然数のうちから非決

これらふたつの活性条件に対応してゲーム戦略と†1 もし必ずしも発散しなくても良いとするとゲーム戦略のなす領域が cpo であることが示せなくなるので不適切である．

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

3

それらの合成を定義する．戦略の合成が弱公平なゲー

問題を解決するため，先行研究 [17] と同様に並列ス

ム列を生成する時のみ発散すると定義することによっレッドのスケジューリングに対応するスケジューラ戦て弱公平性のゲームモデルが与えられる．また上述の略を導入し，これとの公平な合成に関する同値類をとように，不動点演算子による再帰呼び出しの度に W,ることで外延的モデルを得る．

N が観測されるようにすることによって持続性をみたすゲーム列が必ず生成されるようになる．これらの定

1. 3 関連研究

義によって，発散するプログラムのゲーム戦略は，非ゲーム意味論は，PCF や Idealized Algol 言語の決定的実行の選択肢の数の上限が W と N の出現回数

ための完全抽象モデル [11] [2] として最初与えられた．

に支配されるような WN 有界戦略 (4. 2 節参照) で以降，様々な言語機能の拡張がゲーム意味論で定式表される．

化されてきたが，非決定性や並列・並行性に関連すゲーム戦略の WN 有界性によって，非有界非決定

る拡張も多数試みられている．Laird [14] はメッセー性に関する問題を排除できる．例えば，任意の自然

ジ・パッシングに基づく並行言語について，Harmer

数を出力する非決定的プログラムは Harmer のゲーと McCusker [9] [10] はプログラム実行の収束・発散

ム意味論ではゲーム列として {q·n|n ≥ 0} を含むよに無関係に選択を行う erratic な非決定的選択についうな非有界非決定性ゲーム戦略で表されるが，これて，それぞれゲーム意味論を提案している．Ghica

は WN 有界ではない．しかし，持続性を仮定したと Murawski [8] は，プログラムが収束と発散両方の

wait-notify ゲームにおいては同様のプログラムは例

可能性があるならば前者が選択される angelic な並列

えば {q·(W·N)·n|n ≥ 0} のようなゲーム列を含むよ

拡張について，ゲーム意味論を提案しているがそこうなゲーム戦略で表される．この戦略においては，実では Hyland-Ong ゲームの逐次性を無視してゲーム

2n手を並べることを許している．これに対して，渡辺に続く手は W もしくは n の２通りのみ) だが，どんなと西村 [20] [17] は erratic な並列拡張について，上述

大きな自然数も十分多くの W と N の組を生成した後の wait-notify ゲームによるゲーム意味論を構築してには出力することが可能となる．

いる．

2n

行途中の非決定的選択肢の数は常に有界 (q·(W·N)

以上のようにして公正な並列実行を記述するためのしかしながら，これらのいずれも並列実行の公平

内延的ゲームモデルが得られる．なお，内延的ゲーム性については取り扱っていない．上で述べたように，モデルでは２種類の異なる発散の形態が区別される

そもそもゲーム意味論は無限長のゲーム列についてことに注意されたい．ひとつは無限個の W, N を含むの言及が必要な公平性 (より一般的には活性) を規定

ゲーム列で表されるものであり，無限に続く計算に対する術を持たないからである．本稿の提案は，ゲーム応している．もう一つは完成されることなく途切れて意味論において公平性を議論するための手法の初めしまうゲーム列で表されるものであり，プログラムのての提案であるといえる．

実行途中で計算が不完全に終了してしまう場合に相なお，本稿で考察するのはあくまでも並列スレッド

当する．本稿で考察する並列プログラミング言語は，の公平な実行に関するものに限定されていることに後者の場合に対応して abort コマンドを提供する．

注意されたい．ここで提案するゲームモデルでいうとしかしながら，この内延的モデルでは，通常は観測

ころの公平性とは，ある時点から継続的に評価可能な不可能なイベントに対応するゲーム手である W と N がプログラムの部分式があった場合その部分式はいつか明示されているため，プログラムの観測同値性を論じ必ず評価される，という性質のことである．例としてるには細かすぎる．例えば，何もしないコマンド skip

次に示す非決定的関数 f (or は非決定的選択を表す)とこれと観測同値なコマンド newvar v = 0 in v:=0の再帰的定義では，後者のゲーム列に局所変数 v へのアクセスに

f x = if (0 or 1)=0 then x else f (x + 1)

対応するため余分な W と N が含まれてしまう．このを考えよう．広い意味での公平性を認めると，このプ日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

4

λxT .MMM′

ラムダ項と再帰不動点x

自然数

n (n ≥ 0)

非決定的選択N or N

Idle コマンド

skip

逐次合成

seq C M条件分岐

if0 N then M else M ′変数アクセス

V :=N

局所変数

newvar v = n in M

並列実行

C1 ∥ · · · ∥Cζ

擬似変数

mkvar L N M

実行放棄

abortT

図1

fixT MN ⋆N

cas V N N ′!V

P ≫j C (1 ≤ j ≤ ζ)

プログラミング言語の文法

ログラムはいつか 0, 1 のうち 0 が選択されて停止す

列コマンドの型 par のいずれかである．

ることになるが，本稿ではこのプログラムは停止しな

T ::= B | T → T

い可能性があると解釈する．なぜなら，本稿で言うと

B ::= nat | com | var | par

ころの公平性は，再帰呼び出しの度に生成される部

プログラミング言語の文法は図 1 のとおりである．

分項 0 or 1 のコピーについて 0, 1 のどちらを非決定(ほぼ [17] と同じものだが，プログラムの実行放棄を的に選択するかについては何の制約も要求しないの表す abort が新たに加わっている．) Γ を型環境 (識で，ずっと 1 だけを選択し続けることも可能だから

別子とその型を対応付ける有限写像) とするとき，そである．

の型環境 Γ の下でプログラム項 M が型 T を持つこと

本稿の構成を型判定 Γ ⊢ M : T で表す．型判定を導く導出規則

以降，2 節では，Algol 風並列プログラミング言語を図 2 に示す．なお便宜的に，N , C, V , P でそれぞの文法と公平な並列実行の操作的意味論を与える．3

れ型 nat, com, var, par を持つプログラム項を表す

節では，ゲームの基本的定義および wait-notify ゲー

こととする．

ムとそれから導かれる計算構造について概説する．4

以下，プログラミング言語の各要素について順を

節では， 各プログラム項に対してそれらのゲーム戦

追って簡単に解説する．ラムダ項と再帰不動点は通常

略による解釈を与え，それらが WN 有界戦略である

通りで，単純型付きで名前呼びで評価する．自然数のことを示す．これとスケジューラ戦略との合成により項としては定数と適当な二項演算子 ⋆ がある．また，外延的ゲーム意味論を与え，その健全性を示す．5 節

N or N ′ は２つの自然数項からひとつを非決定的に選は，ゲームモデルの完全抽象性を示す．最後に，6 節

択する．skip は何もしない逐次実行コマンドである．

でまとめと将来課題について述べる．

seq C M は逐次コマンド C を実行してから M の計算を開始する．(ただし，M の型は nat, com, par の2 公平な並列プログラミング言語

いずれか) 条件分岐 if0 N then M else M ′ は自然数

本稿では Idealized Algol [19] を並列拡張したプロ

項 N の値が 0 ならば then 節を，0 以外ならば else 節

グラミング言語を考察する．プログラムの型は以下のを評価する．(ただし，M1 , M2 の型は nat, com, parように定義される．B は基礎型で，自然数の型 nat,のいずれか) V :=N は変数 V への自然数項 N の値の

逐次コマンドの型 com, プログラム変数の型 var, 並

代入，! V は変数 V の値の読み出し，cas V N N ′ は日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

Γ, x : T ⊢ M : T′
Γ ⊢ λxT .M : T → T′

Γ, x : T ⊢ x : TΓ ⊢ n : nat

Γ ⊢ M : T′ → TΓ ⊢ M ′ : T′
Γ ⊢ MM′ : TΓ ⊢ N : nat
Γ ⊢ N ′ : nat
Γ ⊢ N ⋆ N ′ : nat
Γ ⊢ C : com

Γ⊢M :TΓ⊢M :T→TΓ ⊢ fixT M : TΓ ⊢ N : nat
Γ ⊢ N ′ : nat
Γ ⊢ N or N ′ : natΓ⊢M :TT ∈ {nat, com, par}Γ ⊢ seq C M : TΓ ⊢ skip : com
Γ ⊢ N : nat

5Γ ⊢ M′ : T

T ∈ {nat, com, par}Γ ⊢ if0 N then M else M ′ : TΓ ⊢ V : varΓ ⊢ N : natΓ ⊢ V N :=:com

Γ ⊢ V : var
Γ ⊢ ! V : natΓ ⊢ V : varΓ ⊢ N : nat
Γ ⊢ N ′ : natΓ ⊢ cas V N N ′ : nat

Γ, v : var ⊢ M : T
T ∈ {com, par}Γ ⊢ newvar v = n in M : TΓ ⊢ C1 : com···
Γ ⊢ Cζ : com
Γ ⊢ C1 ∥ · · · ∥Cζ : parΓ ⊢ M : nat → com

Γ ⊢ P : parΓ ⊢ C : com
Γ ⊢ P ≫j C : parΓ ⊢ N : nat
Γ ⊢ L : nat → nat → nat
Γ ⊢ mkvar M N L : var
図2Γ ⊢ abortT : T

型付け規則

共有メモリアーキテクチャの命令セットによく見らためのものである．†2 実行放棄 abortT は，Felleisen

れる compare-and-swap (CAS) 操作で，排他的に変の A [5] と同様に現在の評価文脈を (並行して実行中数の値を更新する．cas v n m は，変数 v の現在のの他のスレッドのものも含めて) すべて放棄して計算値が n と等しいときのみ変数 v の値を m に更新するを終了させる．

条件付き変数更新操作である．CAS の一連の操作はこのプログラミング言語における変数の扱いはアトミックに行われ，他の並列スレッドの実行によっ

Algol と同様である．すなわち，局所変数として宣て途中で割り込まれることはない．なお，CAS はア
トミックな操作を終了した直後に v に格納されてい言された変数はその有効範囲の外で使用することはできない．†3 また，言語拡張で提供される非決定性

る値を返す．newvar v = n in M はその有効範囲がは有限的 (２つの選択肢からひとつ選ぶ) であるこ

項 M であるような初期値 n の局所変数 v を導入すとに注意せよ．また，選択肢の型としては自然数項

る．C1 ∥ · · · ∥Cζ は複数の逐次コマンドを並列実行すしか認められていないが，条件分岐と組み合わせてる．本稿を通して，並列度 (並列実行における逐次コ

if0 0 or 1 then C else C ′ のように書けばコマンドのマンドの数) は ζ (ζ ≥ 2) で固定されているものとす

実行を非決定的に選択することもできる．

る．P ≫j C は並列コマンド P の j 番目のスレッドのプログラ ムの逐次結合 seq C M を行うときは実行をコマンド C で延長する．すなわち，j 番目のス

C は コ マ ン ド で な け れ ば な ら な い ．し た がって ，レッドが実行を終了したらそのスレッドは引き続きコマンド C を実行する．擬似変数 mkvar L N M は標
準的でない振る舞いをするプログラム変数を作り出す†2 擬似変数は完全抽象の証明のときに必要となるが，通常のプログラミングにはあまり関係しない．
†3 一般的な書き換え可能レファレンスを扱うにはゲーム
意味論を本稿よりもっと一般的 (より構造の少ない)
ゲームモデルで考える必要がある． [1]日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集6

seq (C1 ∥C2 ) (C1′ ∥C2′ ) のようには書けないが，代わりのスレッドの部分項を簡約する (すなわち適当なに並列コマンドの延長を使って (C1 ∥C2 ) ≫1 C1′ ≫2 C2′

k > K について，⟨Mk , sk ⟩ −→j ⟨Mk+1 , sk+1 ⟩)．

と書くことはできる．(ただし，並列実行 C1 ∥C2 となお，無限長の実行列は無限回の再帰呼び出しもしC1′ ∥C2′ が順番に起こるのではなく，２つの逐次実行

くは abort の簡約を必ず含む．(一度 abort が簡約さ

seq C1 C1′ と seq C2 C2′ が並列に実行されることにれると以降は abort を自分自身に簡約する列が無限に気をつけよ．)

続く．)

図 3 に操作的意味論を与える．状態 s とは，有限個初期状態 s の下で項 M の評価が may 収束するとの変数に自然数を対応させる写像である．プログラム

は，⟨M, s⟩ から始まる収束実行列が存在することを

項 M が状態 s の下で 1 段階評価され項 M ′ に変化しいう．また，初期状態 s の下で項 M の評価が must′

その副作用で状態も s に更新されるとき，これを 1′′

ステップ簡約関係 ⟨M, s⟩ −→ ⟨M , s ⟩ で表す．なお，′′⟨s | v 7→ m⟩ で，s (v) = m かつ s (u) = s(u) (ただ′収束するとは，⟨M, s⟩ から始まる公平な発散実行列が存在しないことをいう．とくに M が自由変数を含まない閉項であるとき，M が may 収束することし u ̸= v) のように更新された状態 s を表す．また，を M ⇓may と，must 収束することを M ⇓must と表記

M [N/x] で代入，すなわち M 中の変数 x の自由な出する．

現をすべて N で置き換えて得られる項を表す．通常穴の型が par であるような任意の文脈 C[−] に通り，代入の際変数の衝突が起こる場合は適宜束縛変

ついて，C[M ]⇓may ならば C[N ]⇓may であるとき，数の名前替えを行うものとする．

M ≲may N と定義する．また，M ≲may N かつ各簡約規則において，書き換えられる部分項は (値M ≲must N であるとき M ≲m&m N と書き，M よ

呼びの) 評価文脈 (evaluation context) E[ ](穴がひとり N の方がより止まりやすいプログラムであること

つだけ開いた項) によって特定される．E[M ] と書いを表す．

て文脈 E[ ] に M を埋めて得られる項を表す．
非決定的選択と並列実行の評価文脈の取り方は一意

3 有界非決定性ゲームモデルと公平合成に定まらないことに気をつけよ．特に，簡約項 M が評

Harmer による有界非決定性のためのゲームモデル

価文脈 E ′ [C1 ∥ · · · ∥Cj−1 ∥E ′′ [M ]∥ Cj+1 ∥ · · · ∥Cζ ] に[9] [10] を基に公平な並列実行のためのゲームモデル

よって特定される項に対して行われるとき (簡約が並を構成する．ただし，ここでは拡張部分の解説に重き

列実行の j 番目のスレッドの部分項について行われるをおき，その他の部分に関しては概要のみ紹介しそのとき)，その簡約関係を −→j で表す．

背景や詳細については他の文献 (ゲーム意味論一般に

有 限 も し く は 無 限 長 の 1 ス テップ 簡 約 の 列⟨M0 , s0 ⟩ −→ ⟨M1 , s1 ⟩ −→ · · · を，項 M0 の初期状

ついては [3] 等，Harmer のゲームモデルについては[10]) に譲ることとする。

態 s0 の下での実行列という．収束実行列とは，有限長の実行列 ⟨M0 , s0 ⟩ −→ ⟨M1 , s1 ⟩ −→ · · · ⟨Mm , sm ⟩で ⟨Mm , sm ⟩ をさらに簡約する規則がないものをい3. 1 有界非決定性ゲームモデル

う．発散実行列とは，無限長の実行列 ⟨M0 , s0 ⟩ −→ゲームが展開されるゲームの場 (arena) A を，３つ組 (M , λ , ⊢ ) で表す．†4 ただし，M は可能⟨M1 , s1 ⟩ −→ · · · のうち次の公平性条件を満たすもの

なゲーム手 (game move) の可算集合，λA : MA →をいう．

{O, P} × {Q, A} はラベル付関数 (labeling function)，

簡約の公平性条件 任意の K, j (K > 0, 1 ≤ j ≤

A

A

A

A

二項関係 ⊢A ⊆ MA × MA は活化関係 (enabling re-ζ) について，どの i > K についても Mi の j 番目

lation) であり，次の条件を満たすものとする．

のスレッドが簡約可能な部分項を持つ (すなわち(i) a ⊢A b ならば π1 (λA (a)) ̸= π1 (λA (b)).

′′⟨Mi , si ⟩ −→j ⟨Mi+1, s′i+1 ⟩ なる Mi+1と s′i+1 が存在する) ならば，その実行列はいつか必ず j 番目

†4 本当はこれに加えて MA 上の全順序関係が必要 [17]だが，ここでは本筋とあまり関連しないので省略する．

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

7

E ::= [] | E ⋆ N | n ⋆ E | EM | seq E M | if0 E then M else M | V :=E | E:=n | ! E| cas V E N | cas V m E | cas E m n | C1 ∥ · · · ∥Cj−1 ∥E∥Cj+1 ∥ · · · ∥Cζ()⟨E[ λxT .M N ], s⟩ −→ ⟨E[M [N/x]], s⟩⟨E[fix M ], s⟩ −→ ⟨E[M (fix M )], s⟩⟨E[m ⋆ n], s⟩ −→ ⟨E[n′ ], s⟩, ただし n′ = m ⋆ n⟨E[N or N ′ ], s⟩ −→ ⟨E[N ], s⟩⟨E[N or N ′ ], s⟩ −→ ⟨E[N ′ ], s⟩⟨E[if0 0 then M else M ′ ], s⟩ −→ ⟨E[M ], s⟩⟨E[if0 n+1 then M else M ′ ], s⟩ −→ ⟨E[M ′ ], s⟩⟨E[v:=n], s⟩] −→ ⟨E[skip], ⟨s | v 7→ n⟩⟩⟨E[seq skip M ], s⟩ −→ ⟨E[M ], s⟩⟨E[! v], s⟩ −→ ⟨E[s(v)], s⟩⟨E[cas v m n], s⟩ −→ ⟨E[n], ⟨s | v 7→ n⟩⟩, ただし s(v) = m⟨E[cas v m n], s⟩ −→ ⟨E[s(v)], s⟩, ただし s(v) ̸= m
⟨E[newvar v = n in skip], s⟩ −→ ⟨E[skip], s⟩⟨E[newvar v = n in (skip∥ · · · ∥skip)], s⟩ −→ ⟨E[skip∥ · · · ∥skip], s⟩⟨M, ⟨s | v 7→ n⟩⟩ −→ ⟨M ′ , ⟨s′ | v 7→ n′ ⟩⟩M ′ ̸= abort′⟨E[newvar v = n in M ], s⟩ −→ ⟨E[newvar v = n in M ′ ], ⟨s′ | v 7→ s(v)⟩⟩⟨E[(· · · ∥Cj ∥ · · · ) ≫j C], s⟩ −→ ⟨E[(· · · ∥seq Cj C∥ · · · )], s⟩⟨E[(newvar v = n in P ) ≫j C], s⟩ −→ ⟨E[newvar v = n in (P ≫j C)], s⟩⟨P, s⟩ −→ ⟨P ′ , s′ ⟩P ′ ̸= abort

P は C1 ∥ · · · ∥Cζ または newvar コマンドの形でない⟨E[P ≫j C, s]⟩ −→ ⟨E[P ′ ≫j C], s′ ⟩⟨E[(mkvar M N L):=n], s⟩ −→ ⟨E[M n], s⟩⟨E[!(mkvar M N L)], s⟩ −→ ⟨E[N ], s⟩⟨E[cas (mkvar M N L) m n], s⟩ −→ ⟨E[Lmn], s⟩⟨E[abort], s⟩ −→ ⟨abort, s⟩⟨M, ⟨s | v 7→ n⟩⟩ −→ ⟨abort, s′ ⟩⟨P, s⟩ −→ ⟨abort, s′ ⟩⟨E[newvar v = n in M ], s⟩ −→ ⟨abort, s′ ⟩⟨E[P ≫j C, s]⟩ −→ ⟨abort, s′ ⟩図3

評価文脈と簡約規則(ii) a ⊢A b となるような a ∈ MA が存在しないとき，λA (b) = (O, Q).

(iii) a ⊢A b かつ π2 (λA (b)) = A ならば π2 (λA (a)) =Q.

すこととする．

a ⊢A b のとき，a は b を活化するという．条件 (i)はあるゲーム手が別のゲーム手を活化するとき，一方が Opponent で他方が Player でなければならない

以下，記号 a, b, p, q 等でゲーム手を表すこととすことを意味する．条件 (ii) は他のゲーム手に活化さる．ラベル付関数は，各ゲーム手 a の属性を定める．

れないゲーム手の属性は Opponent かつ Question で

π1 (λA (a)) = O のとき a は Opponent のゲーム手であることを示している．このようなゲーム手のことあるといい，π1 (λA (a)) = P のとき Player のゲームを初期手 (initial move) という．条件 (iii) は Answer

手であるという．また，π2 (λA (a)) = Q のときゲー属性を持つゲーム手は Question 属性を持つゲーム手ム手 a は Question であるといい，π2 (λA (a)) = A ののみによって活化されることを示している．

とき Answer であるという．OA で Opponent のゲー

ゲーム意味論では型 T をゲーム場と解釈し，これをム手の集合を，PA で Player のゲーム手の集合を表[[T]] のように表示する．基本型 nat, com, var に対応

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

8

するゲーム場 [[nat]], [[com]], [[var]] をそれぞれ N, C,

可読性のため s · t) のように書き，sn で文字列 s の n

and Var と表記することにする．これらのゲーム場

個分の結合を表す．また，|s| で文字列 s の長さを表および後で使うゲーム場 WN は次の表で示すようにし，s ⊑ t で s が t のプレフィックス (s の連続する部定義される．(ただし，n, m, l は任意の自然数．)

分文字列で先頭文字を含むもの) であることを表す．
ゲーム手の文字列 s において，s に含まれるゲーム

ゲーム場

初期手 (O, Q)

活性化手 (P, A)

N

q

n

C

run

done

Var

wrn

ok

s′ q t p · · ·rdnを持つとき，p は q によって正当化されるという．

手 p がそれより前に出現するゲーム手 q で p を活性化するものに向かう以下に示すような正当化ポイン
タ (justification pointer)

casm,nl

文字列 s 中に含まれる初期手を除くすべてのゲー

WN

ム手が正当化されている場合，その文字列を正当化さWNれた文字列 (justified string) という．本稿では紙面
これら基本型に対応するゲーム場においては，すべの節約のため正当化ポインタは表示しない．その代わての Question 属性を持つゲーム手は初期手であり，り上記のような正当化の情報が必要な場合，「ゲーム

すべての Answer 属性を持つゲーム手は表と同じ行

手 p が q により正当化される」のように言及するか，にある初期手によって活化される Player のゲーム手

もしくはもっと厳密に「sqtp が sq により正当化されとなることに注意せよ．例えば，ゲーム場 N においる」のようにプレフィックス込みでゲーム手の出現位ては Opponent による初期手の Question q に対して置を曖昧性なく指定することとする．

Player が Answer として任意の自然数 n で応答することができる．
合成型と型環境のため，ゲーム場を組み合わせて次のように構成する．

正当化されたゲーム手の列において，o1 p1 o2 p2 · · ·のように Opponent のゲーム手 o1 , o2 , · · · と Playerのゲーム手 p1 , p2 , · · · が交互に現れるとき，このゲー
ム手の列を適正ゲーム列 (legal play) という．ゲーム• 積ゲーム場 (product arena) を A × B = (MA +場 A における適正ゲーム列の集合を LA と書く．まMB , λA + λB , ⊢A ∪ ⊢B ) で定義する．ただし，た，Levenで偶数長の適正ゲーム列の集合を， Lodd
A
A

MA + MB はゲーム手の直和集合，λA + λB はで奇数長の列の集合を表す．

直和集合上のラベル付関数である．

適正ゲーム列 s に対して，その Player view V(s)• 巾ゲーム場 (arrow arena) を A ⇒ B = (MA +を s の長さに関する帰納法で次のように定義する．

MB , λA + λB , ⊢A ∪ ⊢B ∪{(a, b) | a ∈ MA , b ∈(i) q が初期手のとき，V(sq) = q. (ii) Opponent p

MB , a と b は初期手 }), で定義する．ただし，が q によって正当化されるとき，V(sqtp) = V(s)qp.

λA は元のラベル付関数 λA において属性 O と P(iii) q が Player のとき，V(sq) = V(s)q.

を入れ替えたものを表す．

• 持 ち 上 げ ゲ ー ム 場 (lifting arena) を A⊥ =√√({?, }∪MA , λA ∪{(?, (O, Q)), ( , (P, A))}, ⊢A√√∪{( , ?)} ∪ {( , a) | a ∈ MA , a は初期手 }) で定義する．
以下，ゲーム手を要素とする有限長の文字列を記号

ゲーム場 A における (well-defined な) 戦略 (strat-egy) σ = (Tσ , Dσ ) とはトレース列の集合 Tσ と発散列の集合 Dσ の組であり，次の条件を満たすものを言う．

• トレース列の集合 Tσ は Levenの部分集合で次Aの条件を満たす．

s, t, u 等で表すこととする．特に，空文字列を ε で，(t1) ε ∈ Tσ .

また一文字のみからなる文字列をその文字そのもの(t2) sab ∈ Tσ ならば s ∈ Tσ .

で表す．ふたつの文字列 s と t の結合を st (もしくは戦略 σ の定義域 (domain) を dom(σ) = {sa |日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集9sab ∈ Tσ なる b が存在する } で定める．また，任互作用列から有限個のプレフィックスを除いた残りは意の sa ∈ Loddについて，sa における σ の値
A

MB の要素のみからなることが導かれる．)

域 (range) を rng σ (sa) = {sab | sab ∈ Tσ } で定２つの戦略 σ : A ⇒ B と τ : B ⇒ C を合成して得める．

られるゲーム場 A ⇒ C の戦略を σ; τ と書く．また，T発散列の集合 Dσ は Loddの部分集合で次の条Aおよび T ′ をそれぞれゲーム場 A ⇒ B および B ⇒ C

件を満たす．
(d1) s ∈ Tσ かつ sa ∈ LA かつ sa ̸∈ dom(σ) なにおける適正ゲーム列の集合としたとき T ∥ T ′ =•らば d ⊑ sa となるような d ∈ Dσ が存在する．

{u ∈ int(A, B, C) | u ↾ A, B ∈ T ∧ u ↾ B, C ∈ T ′ } を
これらの並行合成 (parallel composition) という．
合 成 戦 略 σ; τ の ト レ ー ス 列 の 集 合 は Tσ;τ =(d2) sa ∈ Dσ ならば s ∈ Tσ .

{u ↾ A, C | u ∈ Tσ ∥ Tτ }, すなわちふたつの戦略(d3) rng σ (sa) が無限集合ならば d ⊑ sa となるの並行合成からゲーム場 B に属するゲーム手を除去d ∈ Dσ が存在する．

することによって得られるゲーム列の集合として与え

発散列 sa ∈ Dσ は Opponent のゲーム手 a によっられる．一方，発散列の集合 Dσ;τ は，２種類の異なて引き起こされるプログラムの実行の発散を表してる方法で生成されたものの和として定義される．ひいる．(d2) は，そのような Opponent のゲーム手にとつは，一方の戦略のトレース列ともう一方の発散

トレース列で到達できなければならないことを意味

列を組合せて生成される適正相互作用列 Dσ Dτ =し，(d1) および (d3) は，ある Opponent のゲーム手{u ∈ int(A, B, C) | (u ↾ A, B ∈ Tσ ∧ u ↾ B, C ∈ Dτ )に応答できる Player のゲーム手がトレース列中に０∨ (u ↾ A, B ∈ Dσ ∧ u ↾ B, C ∈ Tτ )} から導かれるも個 (すなわち Player が応答できない) かもしくは無限のであり，あとひとつは以下のように２つの戦略のト個存在する (すなわち非有界な非決定性がある) 場合，レース列によって生成される無限相互作用列から導か

その Opponent のゲーム手もしくはそこに到達するれるものである．

までのどこかでプログラムの実行が発散する可能性があることを意味する．
発散列 d ∈ Dσ について，d ∈ dom(σ) のとき d をTσ Tτ = {u∞ ∈ int ∞ (A, B, C) |す べ て の v ⊑ u∞ な る v に つ い てv↾A, B ∈ cc(σ) かつ v↾B, C ∈ cc(τ )}.

本質的 (interesting) な発散列，そうでないとき非本

ただし，cc(σ) = Tσ ∪ dom(σ) である．合成戦略の発質的 (uninteresting) な発散列という．戦略 σ は，任散列集合は上記２つの相互作用列からゲーム場 B に属意の sa ∈ dom(σ) について rng σ (sa) が 1 点集合のするゲーム手を除去することによって得られる．すな

とき決定的 (deterministic) であるという．また，σが決定的かつ任意の発散列 sa ∈ Dσ が本質的なとき，reliable であるという．
３ つ の ゲ ー ム 場 A, B, C に お け る 適 正 相 互
作用列 (legal interaction) u ∈ int(A, B, C) とは，

u ↾ A, B ∈ LA⇒B か つ u ↾ B, C ∈ LB⇒C か つu ↾ A, C ∈ LA⇒C であるような正当化されたゲー
ム列のことをいう．ただし，u ↾ A, B はゲーム手

わち Dσ;τ = {u ↾ A, C | u ∈ Dσ Dτ } ∪ {u∞ ↾ A, C |u∞ ∈ Tσ Tτ } と定義される．
ふたつの戦略 σ, τ : A について次の条件が満たされるとき，τ の方が σ より止まりやすいと定義し，σ ≤♮ τ で表す．
Tσ ⊆ Tτ ∧ ∀d′ ∈ Dτ .∃d ∈ Dσ .d ⊑ d′ ∧∀sab.(sab ∈ Tτ ∧ sab ∈/ Tσ =⇒ ∃d ∈ Dσ .d ⊑ sab).
この半順序関係 ≤♮ から導かれる同値関係を =♮MA ∪ MB の要素のみからなる文字列 u の部分文と書く．すなわち =♮ =≤♮ ∩(=♮ )−1 である．なお，字列を表す．無限相互作用列 (infinite interaction)

戦 略 σ の 極 小 発 散 集 合 (minimal divergences) を

u∞ ∈ int ∞ (A, B, C) と は ，そ の 任 意 の 有 限 プ レ

div (σ) = {d ∈ Dσ | ∀d′ ∈ Dσ .(d′ ⊑ d =⇒ d′ = d)}フィックスが int(A, B, C) に属するような無限列ので定めると，σ =♮ τ であることと Tσ = Tτ かつことをいう．(なお，ゲーム列の適正性より，無限相

div (σ) = div (τ ) とは同値である． [10]

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

10

ゲーム列 s が高々１個の初期手しか含まないとき単分に長い) 有限長プレフィックス tb ⊑ u∞ が存在して，初期手列 (well-opened game play) であるという．戦tb より長い任意の有限長プレフィックス t′ b′ ⊑ u∞

略 σ が単初期手戦略 (well-opened strategy) であるについて，t′ b′ は sa によって正当化されず，しかもとは，Tσ の空でないトレース列および Dσ の本質的b′ ∈ PB ならば sa によって正当化される t′ b′′ ∈ U がな発散列がすべて単初期手列であることを言う．また，存在することをいう．

戦略 σ が単スレッド戦略 (single-threaded strategy)

無限相互作用列 u∞ がいずれかの有限長プレフィッ

であるとは，そのトレース列集合 Tσ が，Tσ のいく

クス sa に関して U -不公平なとき，u∞ は U -不公平でつかの単初期手列を任意に偶数長でインターリーブあるという．U -不公平でない無限相互作用列 u∞ をすることによって得られることをいう．(正式な定義

U -公平 (U -fair) であるという．

は [10] を参照．) 単初期手戦略と単スレッド戦略 (の♮戦略 σ : A ⇒ B と τ : B ⇒ C の公平な合成を= に関する同値類) は全単射で結び付けられる．すσ ;fair τ と書く．公平な合成の定義は σ; τ とほぼ同じ

なわち，単スレッド戦略から単初期手戦略への全単射

だが，２つの戦略のトレース列によって生成される無WO (−) とその逆写像 ST (−) が存在する．

限相互作用列は，Tσ Tτ に代えて，次のように公平

これ以降本稿では，戦略といえば単スレッド戦略

なものだけに限定したものとする．

♮(の = に関する同値類) を指すものとする．なお，

Tσ∞∈ int ∞ (A, B, C) |fair Tτ = {ureliable な戦略については，これを単初期手のトレー

u∞ は (cc(σ) ∥ cc(τ ))-公平かつすべてス列の集合で (曖昧性なく) 定義することができる．

の v ⊑ u∞ なる v について v ↾ A, B ∈ゲームの圏 C を，ゲーム場を対象，A ⇒ B の戦
略を射 A → B とする圏とする．この圏において，恒等射 id : A → A は Opponent のゲーム手に対して Player がすぐ同じ手で対応する模倣戦略 (copycat

strategy) である．また，終対象 1 はゲーム手の集合が空であるようなゲーム場であり，任意の対象 A について射 !A : A → 1 を持つ．圏 G を，C の射を次の３つの性質 (i) player visibile かつ (ii) player bracketing
かつ (iii) subquestion-aﬃne な戦略に限定した (lluf)
部分圏とする．(i) と (ii) は PCF や idealized Algolのゲーム意味論の計算構造を特徴付ける条件 [2] である．また，(iii) の条件は，並列計算のコピーを aﬃne
なものに限定するもの [17] である．
なお C と G はどちらもカルテシアン閉圏である．
[10] [17]cc(σ) かつ v ↾ B, C ∈ cc(τ )}.
公平な合成について次の性質が成り立つ．
補題 3.1. ふたつの戦略 σ : A ⇒ B および τ : B ⇒ C
が以下の条件を満たすとする．

• 任意の sa ∈ dom(σ) について a ∈ OB ならば
sab ∈ rng sa (σ) なる b ∈ OA は存在しない．
• 定 数 m が 存 在 し て ，任 意 の sa ∈ dom(τ )に つ い て ，#{t ∈ Tτ | sa ⊑ t かつ sa は tを正当化する } ≤ m.
こ の と き ，任 意 の u∞ ∈ cc(σ) ∥ cc(τ ) に つ いて ，u′ ⊑ u∞ な る u′ ∈ Dσ Dτ が 存 在 す る か ，

u∞ ↾ A, C ⊑ u′′ ↾ A, C なる u′′ ∈ Tσ ∥ Tτ が存在するか，もしくは v ∞ ↾ A, C = u∞ ↾ A, C なるv ∞ ∈ Tσfair Tτ が存在する．

Proof. u′ ⊑ u∞ なる u′ ∈ Dσ Dτ も，u∞ ↾ A, C ⊑3. 2 公平な合成

u′′ ↾ A, C なる u′′ ∈ Tσ ∥ Tτ も存在しないと仮定す上で定義した戦略の合成は公平性を考慮していなる．無限相互作用列 u∞ が公平でないとき，補題の条い．公平な戦略の合成を (すでに定義したものとは別件をみたす公平な無限相互作用列 v ∞ を以下のように) 与えよう．

にして得ることができる．

U ⊆ int(A, B, C) を適正相互作用列の集合とする．
無限相互作用列 u∞ がその有限長プレフィックス sa に関して U -不公平 (U -unfair) であるとは，(sa より十不公平性より，次のようなプレフィックス sa ⊑ u∞が存在する．

sa より長くかつ sa には正当化されていない

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集
プレフィックス tb′ ⊑ u∞ と b′′ ∈ PB が存在

11

GF の 射 f : 1 → WN⇒N = {q·W·N·0} と g :して，tb ∈ cc(σ) ∥ cc(τ ) は sa に正当化さ

N → WN′ ⇒C = {run·q·0·W′ ·N′ ·done} を 考 え よれるう．Kleisli 拡張 g ∗ : WN⇒N → WN′ ⇒C は上の′′

このようなプレフィックス sa のうち最も短いものを

ゲーム列の q と 0 の間にゲーム場 WN と WN′ か考える．すると，上の仮定と補題の条件および (d1) よらゲーム手をいくつか加えることによって得られる．

∞

り，十分に長いプレフィックス ub0 ⊑ uと b′0 ∈ PB

ただし，新しく加えられたゲーム手は例えばが存在して，sa は ub′0 を正当化しかつこれに続く新run·q·W·W′ ·N′ ·N·0·W′ ·N′ ·done

たな無限相互作用列 tb′0 b1 b2 · · · を得ることができる．

のように，f のゲーム手 W を g のゲーム手 W′ で，g のこの操作を，プレフィックス ub′0 の取り方をどんど

ゲーム手 N′ を f のゲーム手 N で模倣していなければん長くなるように繰り返すと，無限相互作用列は公平ならない．戦略合成 f ; g = f ; g ∗ によって，ゲーム場

な無限列に収束する．

WN のゲーム手はすべて WN′ のゲーム手にコピーされて生き残り，ゲーム列 run·W′ ·N′ ·W′ ·N′ ·done を生

3. 3 Wait-notify ゲームの Kleisli 圏

成する．

第 1 節 で 紹 介 し た wait-notify ゲ ー ム の 持 つ 計

Kleisli 圏 GF は カ ル テ シ ア ン 閉 圏 で あ り，そ の

算 構 造 は ，F : G → G を 関 手 WN⇒(−) と し

評 価 写 像 を evA,B : (A ⇒ B) × A → B で ，た と き ，canonical な 可 換 強 モ ナ ド (F, η, µ, t) と

射 f : C × A → B に対応するカリー化同型をし て 定 式 化 で き る ． [17] 具 体 的 に は ，自 然 変 換ΛA (f ) : C → (A ⇒ B) で 表 す．ま た ，射 影 を

ηA : A → WN⇒A は ふ た つの ゲ ー ム 場 A の 間

πBi : B1 × · · · × Bk → Bi (1 ≤ i ≤ k) で，射の模倣戦略，µA : WN1 ⇒(WN2 ⇒A) → WN0 ⇒A

f1 : A → B1 , . . . , fk : A → Bk に対する仲介射をはゲーム場 WN1 および WN2 のゲーム手とゲーム
場 WN のゲーム手との間の模倣戦略†5 ，ストレン⟨ f1 , . . . , fk⟩ : A → B1 × · · · × Bk で表す．

0

グス tA,B : A × (WN⇒B) → WN⇒(A × B) はふ

3. 4 戦略のなす cpo

たつのゲーム場 A × (WN⇒B) と WN⇒(A × B)

3. 1 節で定義した二項関係 ≤♮ に関して，以下の性質がゲームの圏 C で満たされることが示されていの間の模倣戦略で表される．
上記モナドから導かれる Kleisli 圏を GF とする．

(すなわち，GF の対象は G の対象であり，homset
GF (A, B) は G(A, F B) である．) Kleisli 圏 GF におる． [10] (圏 G および GF に関しても同様の性質が示される．)• ゲーム場 A の戦略は最小元として，トレース列

いては (G より太い記号を使って) 射 f ∈ GF (A, B)の集合が一点集合 {ε} であるようなを持つ．こを f : A → B で，射 f : A → B および g : B → C

れを ⊥A と書く．

の 合 成 を f ; g で あ ら わ す．(合 成 は Kleisli 拡 張 を∗

g : F B → F C = F g; µC としたとき，f ; g = f ; g∗で定義される．)
この Kleisli 圏で特徴的なのは，ふたつの射 (戦略) の 合 成 に よって そ れ ら の 射 に 含 ま れ る す べて の ゲ ー ム 手 W お よ び N が 保 存 さ れ ，合 成 結
果 に 引 き 継 が れ る こ と で あ る ．例 え ば ふ た つ の†5 同一のゲーム場のコピーが複数現れる場合，便宜的にこれらに添字等をつけて区別することにする．また，これに対応して各ゲーム場のゲーム手にも添字等を付けることとする．

• ゲーム場 A の戦略からなる集合は dcpo を構成する．ただし，任意の有向集合 ∆ についてその⊔最小上界 ∆ は，そのトレース列と発散列が∪T⊔ ∆ =Tσσ∈∆

D⊔ ∆ ={sa ∈ LA | s ∈ T⊔ ∆ ∧∀σ ∈ ∆.∃d ∈ Dσ .d ⊑ sa}で定義される戦略として与えれる．

• 戦略の合成操作は ≤♮ に関して単調かつ連続であり，C は ≤♮ に関して cpo 豊穣圏となる．

• 戦略 σ は，その WO (σ) のトレース列集合が有日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

12

限集合であるときおよびそのときに限りコンパ

W·N·cas1,2 ·k·k (n, k は任意の自然数) を持つ戦クトである．

略として解釈されるが，このトレース列は例え• 戦略の cpo は代数的 (algebraic) である．

ば n = 2, k = 3 の場合アクセス履歴と整合しない．ゲーム意味論においては，変数のゲーム手は4 並列言語のゲーム意味論と健全性

局所変数のスコープ内で使用されて初めて，戦ゲーム意味論は，型をゲームの圏の対象 (すなわち略 cell n (n は局所変数の初期値) との合成によっ

ゲーム場) に，型付き項を射 (すなわちゲーム戦略) にて，アクセス履歴と整合性のあるトレース列のみ対応させることによって与えられる．

が有効となり，他は無効となる．上記の項を例えば局所変数のスコープ newvar v = 0 in · · · 内に

4. 1 内延的ゲーム意味論

埋め込んだ場合，cell 0 が定める整合性のある変2 節で導入した並列言語の (内延的) ゲーム意味論

数アクセスのトレース列 rd·0·wr1 ·ok·cas1,2 ·2 との合成により，その解釈はトレース列 q·(W·N)3 ·2

は，具体的には以下のように与えられる．
まず，型に対応するゲーム場を以下のように帰納的となる．

• 並 列 実 行 を 表 す 項 Γ ⊢ P : par は ゲ ー ムに与える．

場 [[Γ]] → (C1 × · · · × Cζ )⊥ に お い て 解 釈 さ[[nat]] = N, [[com]] = C, [[var]] = Var,′′[[par]] = (C1 × · · · × Cζ )⊥ , [[T → T ]] = [[T]] ⇒ [[T ]]また型環境は [[x1 : T1 , · · · , xk : Tk ]] = [[T1 ]]×· · ·×[[Tk ]]のように対応するゲーム場の積に対応させる．

れ ，そ の ゲ ー ム 列 は 初 期 手 ? で 始 ま り，An√swer
が 初 期 手 に 応 答 し た 後 ，各 ス レッドの ゲ ー ム 列 が 任 意 に ( 偶 数 長 で) 区 切 ら れ イ

型付き項 Γ ⊢ M : T は Kleisli 圏 GF の射 (つまりンターリブされたものが続く形で表される．

ゲーム戦略) [[Γ]] → [[T]] で解釈され，[[Γ ⊢ M : T]] (ま例 え ば ，⊢ skip1 ∥ · · · ∥skipζ : par の 戦 略 は ト√
レース列 ?· ·runj1 ··donej1 · · · runjζ ··donejζ でたは前後の文脈から明らかな部分を省略して [[Γ ⊢ M ]]図中，戦略 σ : A → B に対して，そのゲーム列に現

j1 , · · · , jζ は 1, · · · , ζ の任意の順列であるよう√なもので解釈される．また，ゲーム手 ? とれる各初期手の直後に W·N を挿入して得られる戦略の間に他のゲーム手が挟まれているときは，そあるいは [[M ]]) と表す．項の解釈の定義を図 4 に示す．

′

を yld (σ) : A → B で表す．すなわち，σ をトレース

れらは並列実行に先立つ逐次実行を表す．例え

列集合 Tσ′ = {ε} ∪ {q·W, q·W·N·a·s | q·a·s ∈ TWO(σ) }ば，v : var ⊢ seq (v:=1) (C1 ∥ · · · ∥Cζ ) : par は√?·wr1 ·ok· · · · のようなトレース列を持つ戦略でと発散列集合 Dσ′ = {q | q ∈ DWO(σ) } ∪ {q·W·N·s |q·s ∈ DWO(σ) , s ̸= ε}. からなる単初期手戦略とした
とき，yld (σ) = ST (σ ′ ) と定義する．

解釈される．

• 並列実行の延長コマンド P ≫j C の戦略は，任ゲームによる項の解釈は先行研究 [17] の定義とほぼ意の並列インターリーブ実行で j 番目のスレッ同様であるが，いくつか重要な点について解説する．

ドの実行終了後にコマンド C のゲーム列を任意• [17] では変数アクセスの度にゲーム手 W と N のに (偶数長で) インターリーブしながら編み込む組をひとつゲーム列に挿入していたが，これに加ことによって得られる．この編み込みは，戦略

えて非決定的選択や不動点演算子による再帰呼び

cont j との合成によって行われる．

出しが行われるときにも W と N の組を挿入する．

• 項 Γ ⊢ abortT : T はゲーム場 [[Γ]] ⇒ (WN⇒[[T]])• 局 所 変 数 の ス コ ー プ に 入って い な い 変 数 アの最小戦略で解釈される．通常の発散する項

クセスについては，そのトレース列は必ずし[[fix (λx.x) : T]] はトレース列として q·W·N·W · · ·も ア ク セ ス 履 歴 と 整 合 し な い ． [2] 例 え ば 項(q は初期手) を持つ戦略で解釈され，最小戦略とv : var ⊢ seq (v:=! v + 1) (cas v 1 2) : nat
は ト レ ー ス 列 と し て q·W·N·rd·n·W·N·wrn+1 ·ok·は異なる．
本 稿 冒 頭 の 並 列 プ ロ グ ラ ム (1) を 例 に ，ゲ ー

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集• [[Γ, x : T ⊢ x : T]] = π[[T]]•13[[Γ ⊢ λxT .M : T′ ]] = Λ[[T]] ([[Γ, x : T ⊢ M : T′ ]])• [[Γ ⊢ M M ′ : T]] = ⟨ [[Γ ⊢ M : T′ → T]], [[Γ ⊢ M ′ : T′ ]]⟩⟩; ev[[T′ ]],[[T]]⊔• [[Γ ⊢ fixT M : T]] =i σi , た だ し σ0 , σ1 , · · · : [[Γ]] → [[T]] は σ0 = ⊥ お よ び σi+1 =⟨ id[[Γ]] , σi⟩ ; yld (Λ−1[[T]] ([[Γ ⊢ M : T → T]])) によって帰納的に定義．
• [[Γ ⊢ n : nat]] = {q·n | n ≥ 0}
• [[Γ ⊢ N1 ⋆N2 : nat]] = ⟨ [[Γ ⊢ N1 ]], [[Γ ⊢ N2 ]]⟩⟩; binop ⋆ , ただし binop ⋆ : N1 ×N2 → N = {q·q1 ·n1 ·q2 ·n2 ·n |n1 , n2 ≥ 0, n = n1 ⋆ n2 }.
• [[Γ ⊢ skip : com]] = {run·done}• [[Γ ⊢ seq C M : T]] = ⟨ [[Γ ⊢ C : com]], [[Γ ⊢ M : T]]⟩⟩; seq [[T]] , ただし seq A : C × A → A = {q·run·done·t |q·t ∈ TWO(id:A⇒A) }.
• [[Γ ⊢ if0 N then M1 else M2 : T]] = ⟨ [[Γ ⊢ N : nat]], [[Γ ⊢ M1 : T]], [[Γ ⊢ M2 : T]]⟩⟩; cond [[T]] , ただし
cond A : N × A1 × A2 → A = {q·q·n·t | (n = 0 ∧ q·t ∈ TWO(id:A1 ⇒A) ) ∨ (n ≥ 1 ∧ q·t ∈ TWO(id:A2 ⇒A) )}.
• [[Γ ⊢ V :=N : com]] = ⟨ [[Γ ⊢ V ]], [[Γ ⊢ N ]]⟩⟩; yld (asgn), ただし asgn : Var × N → C = {run·q·n·
wrn ·ok·done | n ≥ 0}.
• [[Γ ⊢ ! V : nat]] = [[Γ ⊢ V ]]; yld (deref ), ただし deref : Var → N = {q·rd·n·done | n ≥ 0}.
• [[Γ ⊢ cas V N1 N2 : nat]] = ⟨ [[Γ ⊢ V ]], [[Γ ⊢ N ]], [[Γ ⊢ N ′ ]]⟩⟩; yld (cas), ただし cas : Var × N1 × N2 →N = {q·q1 ·m·q2 ·n·W·N·casm,n ·k·k | m, n, k ≥ 0}.
()• [[Γ ⊢ newvar v = n in M : T]] = ST ⟨id [[Γ]] , ![[Γ]] ; cell n ⟩; WO ([[Γ, v : var ⊢ M : T]]) .

ただし

cell n : 1 → Var は，初期値 n を持つ変数の戦略．(詳しくは本文参照．)• [[Γ ⊢ N1 or N2 : nat]] = ⟨[[Γ ⊢ N1 ]], [[Γ ⊢ N2 ]]⟩⟩; yld (choice), ただし choice : N1 × N2 → N = {q·qi ·n·n |i ∈ {1, 2}, n ≥ 0}.
• [[Γ ⊢ P ≫j M : par]] = ⟨ [[Γ ⊢ P : par]], [[Γ ⊢ M : com]]⟩⟩; cont j , た だ し σi : C1 × · · · ×
C′ζ × C → Ci = {runi ·run′i ·done′i ·t·donei | (i ̸= j ∧ t = run·done) ∨ (i = j ∧ t = ε)} と し て√√cont j : (C′1 × · · · × C′ζ )⊥ × C → (C1 × · · · × Cζ )⊥ = {??′ ′ s | s ∈ T⟨σ1 ,··· ,σζ ⟩ } と定義．
• [[Γ ⊢ C1 ∥ · · · ∥Cζ : par]] = σζ , た だ し σ0 , · · · , σζ : [[Γ]] → (C1 × · · · × Cζ )⊥ は σ0 =√{? ·runρ(1) ·doneρ(1) · · · runρ(ζ) · doneρ(ζ) | ρ : {1, . . . , ζ} 7→ {1, . . . , ζ} は全単射 } および σi+1 =⟨ σi , [[Γ ⊢ Ci+1 : com]]⟩⟩; cont i+1 によって帰納的に定義．
• [[Γ ⊢ mkvar M N L : var]] = ⟨ [[Γ ⊢ M ]], [[Γ ⊢ N ]], [[Γ ⊢ L]]⟩⟩; acpt, ただし acpt : (N ⇒ C) × N × (N1 ⇒N2 ⇒ N) → Var = {wrn ·run·(q·n)k ·done·ok | n, k ≥ 0} ∪ {rd·q·n·n | n ≥ 0} ∪ {casn1 ,n2 ·q·t·n·n |n1 , n2 ≥ 0, t = a1 ·b1 · · · ak ·bk (k ≥ 0), ただし aj ·bj は q1 ·n1 または q2 ·n2 }.
• [[Γ ⊢ abortT : T]] = ⊥図4

ゲーム戦略による項の解釈√?· ·run·W·run·(W·N)2 ·rd·0·W·N·wr1 ·ok·done·N·rd′ ·m1 ·W·N·wr′m1 +1 ·ok′ ·(W·N)2 ·rd·(n + 1)·done√?· ·run·W·run·(W·N)2 ·rd·0·W·N·rd′ ·m1 ·W·N·wr1 ·ok·done·N·wr′m1 +1 ·ok′ ·(W·N)2 ·rd·(n + 1)·done√?· ·run·W·run·(W·N)2 ·rd·0·W·N·rd′ ·m1 ·W·N·wr′m1 +1 ·ok′ ·W·N·W·N·wr1 ·ok·done·N·rd·(n + 1)·done
図5

並列実行のゲーム列の例

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集14

ム 戦 略 に よ る 解 釈 を 見 て み よ う．局 所 変 数 の スと数える) を表す．σ が WN 有界 (WN-bounded)

コ ー プ の 中 の 型 環 境 Γ = u : var, v : var に 対であるとは，任意の sa ∈ dom(WO (σ)) に対して，

応 す る ゲ ー ム 場 を [[Γ]] = Var × Var′ と し た とs′ ⊑ s なる s′ ∈ LevenA⇒F B が存在して次の条件が成り

き ，第 1 の ス レッド の コ マ ン ド u:=1 は ト レ ー ス

立つことをいう．

列 run·W·N·wr1 ·ok·done を持つ戦略で，第 2 のスレッ
ドのコマンドの while ループ (適当な不動点演算子で表される) は k (k ≥ 0) 回目のループで止まるト
レース列として run·t1 ·t2 · · · tk ·(W·N)2 ·rd·(n+1)·done,て ∥sa∥σ = 1.

• sa = s′ t なるゲーム列 t について，t はゲーム手
N の出現を m 個含み，∥sa∥σ ≤ 2m .

(W·N) ·rd·0·W·N·rd ·mk ·W·N·wr′mk +1 ·ok′

補題 4.1. σ : A → B と τ : B → C がそれぞれ(n, mk は任意の自然数) となるような戦略で解釈

WN 有界戦略ならば，これらの合成戦略 σ; τ もまたされる．これら２つのスレッドの並列実行は，例えWN 有界戦略である．

ば図 5 のようなトレース列で表される．(簡単のたProof. u を，u ↾ A, F B ∈ Tσ かつ u ↾ F B, F C ∈ Tτ ∗ただし tk =2′• 任意の s′ t′ a′ ⊑ s なる s′ t′ a′ ∈ Lodd
A⇒F B についめ k = 1 の場合の一部だけを示した．可読性のため第 1 スレッド由来のゲーム手に下線を施してある．) いま，これらスレッドの並列実行は局所変数のスコープ newvar u = 0 in newvar v = 0 in · · ·内であることから，図 5 のトレース列のうち３番を満たす適正ゲーム列とする．3. 3 節で見たように，
合成 σ; τ は，σ と τ 両方の戦略のゲーム列に含まれる部分列 W と N を保存する．したがって，合成戦略の sa ∈ dom(σ; τ ) における分岐数は，高々σ と τ におけるそれぞれの分岐数の積で抑えられる．

目だけが変数のアクセス履歴と整合的であり，この列からゲーム場 [[Γ]] = Var × Var′ のゲーム手を削除して，プログラム (1) を解釈する戦略の (計算が停止する場合の) トレース列のひとつとして√?· ·run·W· run·(W·N)6 ·done·N·done を得る．k = 1 以
外の場合も同様に考えて，この戦略は他にもトレース√
列 ?· ·run·W·run·(W·N)4k+2 ·done·N·done (k ≥ 0) を含むことがわかる．

一般に，任意の型付き項は Kleisli 圏 GF において

WN 有界戦略となる．
命題 4.2. 任意の項 Γ ⊢ M : T について, [[Γ ⊢ M : T]]
は WN 有界戦略である．

Proof. 項 M の構造に関する帰納法による．再帰不動点以外の項については補題 4.1 より従う．再帰不動⊔
点 fix M については，最小上界 [[fix M ]] = i σi (ただし各 σi は図 4 で定義したもの) で与えられ，WN

4. 2 WN 有界性

有界となる．なぜなら，各 σi は WN 有界であり，そ上で定義した内延的ゲームモデルは必ず有限分岐のの構成は σi から σi+1 を得る際，再帰呼び出し１回戦略を与える．すなわち，各 Opponent のゲーム手に分に相当する W, N が 1 組挿入されるため，σi+1 は各

対して Player は高々有限個の応答しかできない．しsa ∈ dom(WO (σi )) について分岐数を増加させるよかも，以下で見るように，Player が可能な応答の数

うなことはないからである．

はゲーム列に現れるゲーム手 W, N の数に支配される．

σ : A → B をゲームの Kleisli 圏 GF の射とする．任意の sa ∈ dom(WO (σ)) について，sa における σ の分岐数 (branching width) を，δσ (sa) をd ⊑ sa を満たすような d ∈ DWO(σ) が存在するとWN 有界戦略はまた次の性質を満たす．
補題 4.3. 任意の WN 有界戦略 σ : A → B につい⊔て，σ = i σi となるようなコンパクトで WN 有界
な戦略の有向集合 {σi | i ≥ 0} が存在する．

き 1 を返しそうでなければ 0 を返す関数としたとき，

Proof. 単初期手戦略 σi′ をトレース列の集合 Tσi′ =∥sa∥σ = #rng σ (sa) + δσ (sa) で定義する．すなわ{s ∈ TWO(σ) | |s| ≤ 2i} および発散列の集合 Dσi′ =ち ∥sa∥σ は，戦略 σ においてゲーム列 sa に対して{d ∈ DWO(σ) | |d| < 2i} ∪ {sa ∈ dom(WO (σ)) |Player が応答できるゲーム手の種類 (発散も１種類|sa| = 2i + 1} で定め，σi = ST (σi′ ) とすればよ日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

15

GF /≃ の射 E[[M ]] = [[[M ]]]≃ と定義する．以下のようい．

に，この外延的モデルに関する健全性が示される．

4. 3 スケジューラ戦略と外延的ゲーム意味論

命題 4.4 (consistency). M ⇓may ならば run·done ∈4. 1 節で定義した内延的ゲーム意味論では，非決T[[M ]] ;fair sched である．また，M ⇓must ならば run ̸∈

定的選択や変数アクセス，あるいは再帰呼び出しをD[[M ]] ;fair sched である．

ゲーム列中にゲーム手 W と N で記録してしまう．こ命 題のため，プログラムの観測同値性を論じるには細か

T[[M ]] ;fair sched ならば M ⇓すぎる．例えば，何もしないコマンド skip と (外部D[[M ]] ;fair sched ならば M ⇓must である．

から観測できない) 局所変数にアクセスするコマンド

定理 4.6 (soundness). 任意の閉じた項 ⊢ M : T

newvar v=0 in v:=1 は観測同値であるべきだが，後および ⊢ N : T について，E[[M ]] ≼ E[[N ]] ならば者のゲーム戦略には変数アクセスに伴う余計なゲー

M ≲m&m N である．

4.5

(adequacy). も し run· donemay∈

である．また，run ̸∈

ム手 W と N が含まれてしまう．
先 行 研 究 [17] で は こ の 問 題 を 解 決 す る た め ，ス ケ ジュー ラ 戦 略 (scheduler strategy) sched

5 完全抽象定理:

先行研究 [9] [17] と同様に，本稿で考察する Algol

F (C1 × · · · × Cζ )⊥ → C を 導 入 し ，こ れ と の 合

風並列プログラミング言語に関する完全抽象 (full

成 に よって ゲ ー ム 戦 略 中 の 余 計 な ゲ ー ム 手 W とabstraction) 定理は基本的に，reliable factorization,

N を無視した外延的ゲーム意味論を定義した．

innocent factorization, definability を段階的に示す

ス ケ ジュー ラ 戦 略 は ト レ ー ス 列 の 集 合 Tsched =√{run·?·(W·N)k · ·s·done | k ≥ 0, s ∈ CPP }, ただしことによって示すことができる．

CPP は ζ 個のトレース列 run1 j·(W·N) ·done1 , ...,

非決定的な神託戦略 (oracle strategy) と非決定性を

runζ ·(W·N) ·doneζ (k1 , . . . , kζ ≥ 0) を任意に偶数長排除した reliable な戦略との合成に分解する．ただしでインターリービングして得られるゲーム列の集合

WN 有界性により，神託戦略は先行研究のものより

k1

kζ

まず reliable factorization は，与えられた戦略をを表す．なお，スケジューラ戦略は player visible で

単純な oracle = {q·W·N·0, q·W·N·1} (つまり非決定的も player bracketing でもない C の射であり，高階リプログラム 0 or 1 の戦略) で十分である．

ファレンスや汎用の実行継続制御の仕組みを持たない

命題 5.1 (Reliable factorization). σ : 1 → A が

本稿のようなプログラミング言語では定義不可能でGF のコンパクトな WN-bounded 戦略のとき，コある [1] [12] [13] ことがわかる．

ンパクトかつ reliable な戦略 det(σ) : N → A で√スケジューラ戦略は例えば，?· ·run1 ·W·run2 ·W·N·W·

N·W·N · · · のような無限に延長可能なゲーム列との合成が可能だが，これとの合成は不公平な相互作用列を生み出すので，これをもってプログラムが発散するとしてはいけない．公平性を考慮に入れたゲームモデル
を，intrinsic quotient [2] [15] [10] を用いて次のように定義する．GF の射 f, g : A → B について f ≼ gを，任意の WN 有界戦略 h : (A ⇒ B) → Cζ ⊥ について (‘f ’; h) ;fair sched ≤♮ (‘g’; h) ;fair sched が成り立つことと定義する．ただしここで ‘f ’ : 1 → A ⇒B = ΛA (πA ; f ) である．
f ≃ g と書いて f ≼ g かつ g ≼ f であることを意味する．項 M に対してその外延的モデルを商圏

σ =♮ oracle; det(σ) を満たすものがある．
Proof. 各 sa ∈ dom(WO (σ)) に対して次のような変更を加えることで reliable な戦略 det(σ) を得ることができる．

WN 有界性より，sa は t·b·W·t1 ·N · · · W·tn−1 ·N·W·tm ·N·tm+1 ·a (n ≥ 0, t0 , t1 , ..., tm+1 は W, N を含まない)のような形の列でありしかも ∥sa∥σ ≤ 2m を満たす．
また，rng σ (sa) = {sac0 , ..., sacn } だとする．

d ⊑ sa なる d ∈ DWO(σ) が存在しないとき，次のようにゲーム列を変更する．sa ̸∈ DWO(σ) のとき，
次のようにゲーム列を変更する．

t·b·q·t1 ·b1 ·q·t2 ·b2 · · · q·tm ·bm ·tm ·a·cp

日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集16

ただし，bi ∈ {0, 1} であり，p は n と m-bit ２進数

fix (λx.x) の代わりに，abort でこれを定義する必要

b1 b2 · · · bm のうち大きくない方の値とする．

がある．

d ⊑ sa なる d ∈ DWO(σ) が存在するときもほぼ同

スケジューラ戦略との公平な合成についての次の性様だが，m-bit ２進数 b1 b2 · · · bm の値 p が n 以下の質より完全抽象が導かれる．

場合のみ Player は cp で応答し，それ以外の場合につ補題 5.4. 任意の GF の WN 有界戦略 σ, σ ′ : 1 →いては発散列Cζ ⊥ について以下が成り立つ．

t·b·q·t1 ·b1 ·q·t2 ·b2 · · · q·tm ·bm ·tm ·aをもつ戦略に変更する．
前段階で得られた reliable な戦略をさらに，局所変数の戦略と innocent な戦略の合成に分解する．ある決• σ ;fair sched は C の well-defined な戦略である．
• σ ≤♮ σ ′ ならば σ ;fair sched ≤♮ σ ′ ;fair sched .
また，任意の GF の戦略 1 → Cζ ⊥ の有向集合 ∆⊔⊔について，( ∆) ;fair sched =♮ σ∈∆ (σ ;fair sched )定的戦略 σ が innocent とは，任意の sab, s′ a′ b′ ∈ Tσが成り立つ．

に対して V(sa) = V(sa′ ) ならば b と b′ は等しい

Proof. 通常の戦略の合成の場合 [10] とほぼ同様に示′(b = b かつ Player view の中の同じゲーム手に正すことができるが，well-definedness に関しては補題当化される) ことをいう．以下で definability を示す

3.1 を用いて性質 (d1) を示す必要がある．

ときの都合のため，ここでは d-delayed innocent な定理 5.5 (完全抽象). 任意の閉じた項 ⊢ M : T およ

戦略との合成に分解する．ある戦略 σ が d-delayed

innocent とは，任意の sab ∈ Tσ に対して，sa に続
く Player のゲーム手が V(sa) によって一意に決まるび ⊢ N : T について，E[[M ]] ≲ E[[N ]] のときおよびそのときに限り M ≲m&m N が成り立つ．

場合を除いては，b = W であるかさもなくば適当なProof. 一方は健全性によって示されているので，逆向ゲーム列 t に対して V(sab) = t·(W·N)d ·b が成り立つ

きだけ示す．E[[M ]] ̸≲ E[[N ]] と仮定する．補題 4.3，5.4

ことをいう．

により，適当なコンパクトかつ WN 有界戦略 h が存在

命 題 5.2 (d-delayed innocent factorization [17]).

して ([[M ]]; h) ;fair sched ̸≤♮ ([[N ]]; h) ;fair sched が成f : 1 → A を GF のコンパクトで reliable な戦略とり立つ．定理 5.3 により，h は適当な文脈 C[] によってする．また，code をゲーム列から自然数へのコーディ定義され，[[C[M ]]] ≃ [[M ]]; h かつ [[C[N ]]] ≃ [[N ]]; hング関数とする．このとき任意の d ≥ 1 について，とできる．命題 4.4 と 4.5 より M ̸≲m&m N が従

d-delayed innocent な戦略 innd (f ) : Var → A でう．

(cell code(ε) ; ηVar ); innd (f ) ≃ f を満たすものがある．
Innocent factorization は [2] と同様に，Opponent

6 まとめと将来課題と Player のゲーム手の履歴を戦略 cell code(ε) で表さ

Algol 風並列プログラミング言語について，その公れる局所変数に記憶・参照することで達成できる．た平な実行に対するゲーム意味論を与えた．従来のゲー

だし，並列実行による共有変数のアクセスに際してスム意味論では公平性を含む活性条件を表現することがレッド間の競合が起こるのを CAS を用いて回避する困難だったが，本稿では先行研究である wait-notify必要がある．(詳しくは [17] を参照．)

ゲーム [20] [17] におけるゲーム手 W, N を，非決定性を

上記２つの factorization より次の結果が導かれる．

誘導する可能性のある計算資源一般へのアクセスを

定理 5.3 (Definability [17]). σ : [[Γ]] → [[T]] を GF表すために利用し，これによって非決定性がゲーム手のコンパクトで WN 有界な戦略とする．このとき，W, N の数によって支配される WN 有界戦略で表され

σ ≃ [[M ]] となるような閉じた項 M が存在する．

ることを示し，公平なスケジューラの下でのプログラ

これの証明は [17] と基本的に同じであるが，戦略中に発散が含まれる場合，停止しない再帰呼び出し

ムの観測同値性に関して完全抽象なゲーム意味論を日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集与えた．
本稿で提案したゲーム意味論は，公平な並列プログ
ラムの等価性の機械判定に応用できると考えている．
逐次プログラムに関して行われた手法 [7] [16] と類似の方法で，並列プログラムの適当なクラスに対してそのような等価性の判定方法を開発するのが次の課題である．

謝辞
本研究は JSPS 科研費 24500014 の助成を受けたものである．

参 考 文 献[ 1 ] Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for generalreferences. In 13th Annual IEEE Symposium on
Logic in Computer Science, pages 334–344, 1998.
[ 2 ] Samson Abramsky and Guy McCusker. Linearity, sharing and state: A fully abstract game semantics for idealized Algol with active expressions. In
P. W. O’Hearn and R. D. Tennent, editors, Algollike Languages, volume 2 of Progress in Theoretical Computer Science, pages 297–329. Birkhäuser,
1997.
[ 3 ] Samson Abramsky and Guy McCusker. Game
semantics. In H. Schwichtenberg and U. Berger,
editors, Computational Logic: Proceedings of the1997 Marktoberdorf Summer School, pages 1–56.
Springer-Verlag, 1999.
[ 4 ] Pierpaolo Degano and Ugo Montanari. Livenessproperties as convergence in metric spaces. In Proceedings of the 16th Annual ACM Symposium on
Theory of Computing, pages 31–38, 1984.
[ 5 ] Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential
control and state. Theoretical Computer Science,
103(2):235–271, 1992.
[ 6 ] Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986.
[ 7 ] Dan R. Ghica and Guy McCusker. The regularlanguage semantics of second-order idealized ALGOL. Theoretical Computer Science, 309(1–3):469–
502, 2003.

17[ 8 ] Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Annalsof Pure and Applied Logic, 151(2-3):89–114, 2008.
[ 9 ] Russel Harmer and Guy McCusker. A fully abstract game semantics for finite nondeterminism. In
Proceedings of the 14th Annual IEEE Symposiumon Logic in Computer Science, pages 422–430, 1999.
[10] Russell Harmer. Games and Full Abstraction
for Nondeterministic Languages. PhD thesis, University of London, 1999.
[11] J. M. E. Hyland and C.-H. Luke Ong. On full
abstraction for PCF: I, II, and III. Information andComputation, 163(2):285–408, 2000.
[12] James Laird. Full abstraction for functional languages with control. In 12th Annual IEEE Symposium on Logic in Computer Science, pages 58–67,
1997.
[13] James Laird. A fully abstract game semantics
of local exceptions. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 105–114,
2001.
[14] James Laird. Game semantics for higher-orderconcurrency. In FSTTCS 2006: Foundations ofSoftware Technology and Theoretical Computer Science, 26th International Conference, LNCS, pages
417–428. Springer, 2006.
[15] Guy McCusker. Games and Full Abstraction fora Functional Metalanguage with Recursive Types.
Distinguished Dissertations. Springer, 1998.
[16] Andrzej S. Murawski and Igor Walukiewicz.
Third-order idealized algol with iteration is decidable. Theoretical Computer Science, 390(2–3):214–
229, 2008.
[17] Susumu Nishimura. A fully abstract game semantics for parallelism with non-blocking synchronization on shared variables. In Computer Science
Logic 2013 (CSL 2013), pages 578–596, 2013.
[18] David Park. On the semantics of fair parallelism.
In Abstract Software Specifications, volume 86 of
LNCS, pages 504–526. Springer, 1980.
[19] John C. Reynolds. The essence of Algol. In
Proceedings of the 1981 International Symposium
on Algorithmic Languages, pages 345–372. NorthHolland, 1981.
[20] Keisuke Watanabe and Susumu Nishimura.
May&must-equivalence of shared variable parallel
programs in game semantics. Information Processing Society of Japan Transactions on Programming(PRO), 5(4):17–26, 2012.