wrap_abort の話 ()

OCaml Formal

OCaml (Concurrent ML?) の Event.wrap_abort という関数はちょっと面白い．

val wrap_abort : 'a event -> (unit -> unit) -> 'a event
wrap_abort ev fn returns the event that performs the same communications as ev, but if it is not selected the function fn is called after the synchronization.

selectで選ばれなかった場合の処理を型unit->unitで渡せる． MilnerのCCSにはこういう演算子はなかったと思うけど，まあ適当に定義してみる． (ちゃんと探せばあるんだろうけど頭の体操的な)

プロセス構文の修正

P\quad ::=\quad \alpha .P\quad |\quad \cdots
を
P\quad ::=\quad \alpha .P\quad \mbox{\bf abort}\quad Q\quad |\quad \cdots
と書き換える．
ここで \alpha .P\quad \mbox{\bf abort}\quad Q は 直観的には 動作\alpha後にPに遷移するが 選択されない場合のみ Qに遷移するプロセス．
従来の \alpha.P は， \alpha.P\quad \mbox{\bf abort}\quad 0 の略記とする (0 は終了したプロセス)．

操作的意味の修正

まず . 演算子の規則を次の2つの公理 ACT, ABT に置き換える:
\mbox{ACT : }\alpha .P\quad \mbox{\bf abort}\quad Q\quad \stackrel{\alpha}{\longrightarrow}\quad P
\mbox{ABT : }\alpha .P\quad \mbox{\bf abort}\quad Q\quad \stackrel{\mbox{\bf abort}}{\longrightarrow}\quad Q
ここで\stackrel{\mbox{\bf abort}}{\longrightarrow}はアボートの動作を表す関係で遷移関係とは別もの

あとは + 演算子の規則を次のとおり置き換える:
\mbox{SUM-L : }P\quad \stackrel{\alpha}{\longrightarrow}\quad P'\quad \wedge\quad Q\quad \stackrel{\mbox{\bf abort}}{\longrightarrow}\quad Q'\quad \Rightarrow\quad P\quad+\quad Q\quad\stackrel{\alpha}{\longrightarrow}\quad P'\quad|\quad Q'
\mbox{SUM-R : }P\quad \stackrel{\mbox{\bf abort}}{\longrightarrow}\quad P'\quad \wedge\quad Q\quad \stackrel{\alpha}{\longrightarrow}\quad Q'\quad \Rightarrow\quad P\quad+\quad Q\quad\stackrel{\alpha}{\longrightarrow}\quad P'\quad|\quad Q'
\mbox{SUM-ABT : }P\quad \stackrel{\mbox{\bf abort}}{\longrightarrow}\quad P'\quad \wedge\quad Q\quad \stackrel{\mbox{\bf abort}}{\longrightarrow}\quad Q'\quad \Rightarrow\quad P\quad+\quad Q\quad\stackrel{\mbox{\bf abort}}{\longrightarrow}\quad P'\quad|\quad Q'

ちゃんと定義できてるかどうかは知らない．