Event.wrap_abort を π計算で表現してみるその2

ひとつ前のエントリでテキトーに作った abort 演算子を使って、OCamlプログラムのコード例を追ってみる。

open Event

let start_server () =
  let in_ch = new_channel ()
  in
  let rec loop () =
    let (x, ret_ch, nack_ch) = sync (receive in_ch) in
    loop (select [send ret_ch (x * 2); receive nack_ch])
  in
  ignore (Thread.create loop ());
  in_ch

let calc3 in_ch x =
  guard (fun () ->
    let ret_ch,nack_ch = new_channel (), new_channel () in
    sync (send in_ch (x, ret_ch, nack_ch));
    wrap_abort (receive ret_ch) (fun () -> ignore (Thread.create (fun () -> sync (send nack_ch ())) ())))

こいつを上の abort演算子を追加したπ計算で書いてみる。
まずサーバー
$Server\stackrel{\tiny def}{=} in(x,ret,nack).(\overline{ret}\langle x*2\rangle.Server+nack.Server)$
クライアント
[tex:Client\stackrel{\tiny def}{=}(\mbox{\bf \nu} ret,nack)(\overline{in}\langle 123,ret,nack\rangle.*1]
ここで $P$ はクライアントの継続， $Q$ は他のイベント．

紙の上で計算

最初の1ステップ

$Server|Client$
$\stackrel{\tau}{\rightarrow}\quad (\mbox{\bf \nu} ret,nack)(\overline{ret}\langle 246\rangle.Server+ nack.Server\quad|\quad(ret(y).P \quad \mbox{\bf abort} \quad \overline{nack}.0) + Q)$
普通の通信．この後，次の2通りに分岐する：

1. $ret$ で通信した場合

$Q \stackrel{\mbox{\bf abort}}{\longrightarrow} Q_{abt}$ とする．
$\cdots \stackrel{\tau}{\rightarrow}\quad (\mbox{\bf \nu} ret,nack)(Server|0|P[246/y]|Q_{abt})$

無事 $y$ に 123 * 2 = 246 が代入される．

2. $Q$ が環境と通信した場合

$Q\stackrel{\alpha}{\rightarrow}Q'$ なる $\alpha$ , $Q'$ が存在して，
$\cdots \stackrel{\alpha}{\rightarrow}\quad (\mbox{\bf \nu} ret,nack)(\overline{ret}\langle 246\rangle.Server+ nack.Server\quad|\quad\overline{nack}.0\quad|\quad Q')$
その後 $nack$ で通信して
$\cdots \stackrel{\tau}{\rightarrow}\quad (\mbox{\bf \nu} ret,nack)(0|Server|0|Q')$
となってくれる． …多分.