external choice(外部選択)

代数演算子

external choice P[]Q はプロセスの選択を意味する。プロセスP,Q のどちらのイベントが先に起こるかによって実行するプロセスが決定される。
例えば、コインを入れた後、いくつかの種類が選べる自動販売機は次のようになる。

channel coin, coke, lemonade
VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS )

プロセスVMSはイベント coin の後、coke->VMS, lemonade->VMS のexternal choice'[]'となっている。イベントcoke,lemonade のどちらが起きるかで次に実行されるプロセスが選択される。今回はどちらイベントが起きても再びVMSに戻る。external（外部）の意味は、この選択がVMS自身だけでなく外部の要因(今回は購入者？)が関与するということである。*1

括弧()をなくして記述してしまうと次のように coin と lemonade で選択が行われてしまうので注意。

channel coin, coke, lemonade
VMS = coin -> coke -> VMS
      []
      lemonade -> VMS   --lemonade は無料！？


external choiceは自然に拡張できる。イベントciderを加えた場合は次のようになる。

channel cider
VMS = coin -> ( coke -> VMS
                []
                lemonade -> VMS
                []
                cider -> VMS )
boolean gard

external choiceの選択はboolean gard によりその選択をガードすることができる。

例えば、コインを何枚でも自由に入れることができ、その分だけジュースが買える自動販売機VMGを考えてみる。まず、変数nで自販機に入れられたコインの枚数をカウントすることにする。

VMG(n) = coin -> VMG(n+1)

VMGはコインを入れるかジュースを出すかを選択でき、ジュースを出せば保持しているコインの枚数が１枚減るはずなので上記のVMGを拡張し、

VMG(n) = coin -> VMG(n+1)
         []
         juice -> VMG(n-1)

となりそうだが、juiceのイベントが選べるのは n>0 の場合であるはず。このような場合は次のように書けば n>0 でないと juiceイベントが起きないようにできる。

 VMG(n) = coin -> VMG(n+1)
          []
          (n>0)&juice -> VMG(n-1)

 -- つまり、n=0 のときは VMG(0) = coin -> VMG(1) と同じ。

また次のように、コインの枚数をn、ジュースの在庫をmとし、その両方を保持することもできる。juiceのイベントを起こせるのはコインを入れており(n>0) かつジュースの在庫がある(m>0) ときであり、イベント後は両方とも１つ減る。

VMG2(m,n) = coin -> VMG2(m,n+1)
            []
            (m>0)and(n>0)&juice -> VMG2(m-1,n-1)
補足

boolean gard は conditional choiceの特別な場合の省略形であり、external choice との組み合わせでなくても使ってよい。

(condition)&PROC ≡ if (condition) then PROC else STOP

つまり、上記 VMG(n)の元の記述は次のようなる。

 VMG(n) = coin -> VMG(n+1)
          []
          if (n>0) then juice -> VMG(n-1)
          else          STOP

 -- n=0 のときは
 VMG(0) = (coin -> VMG(1)) [] STOP
 -- これは、VMG(0) = coin -> VMG(1) と同じ。
 -- CSPの代数法則 P[]STOP ≡ P による。

*1:詳しくは internal choice（内部選択）の説明時に