前回の OCaml-Nagoyaで Haskellの遅延評価とvalue recursionを使ったネタの記事を紹介したら皆けっこうおもしろがってくれた。 で、OCaml や SML といった 遅延評価モジュールがある言語ではどう書く？ というネタで さらに少し盛り上がった。rp_min は lazy…

やっぱりπ計算の前にCCSだよねーということで Implementing CCS in Maude2 (著者による.ps) を軽く読んだ。 ラベル付き遷移を書き換えでやるのは案外面倒らしく、せっかくの | や + がfrozenになってしまっている(前回のπ計算ではラベル無しのreduction(τ遷…

ここ で書いた abort 演算子を Maudeで実装した。 CCSの構文と意味は先ほどのエントリのものをつかった(ちょっと変えたけど)。http://www.agusa.i.is.nagoya-u.ac.jp/person/sydney/ccs-abort.maude 演算子を追加 op _:_abort_ : Act Process Process -> Pro…

http://www.agusa.i.is.nagoya-u.ac.jp/person/sydney/ccs-abort.maude ←今日のエントリで使っているMaudeのソースコードものぐさなので ちゃんと解説を書くのがめんどいのです… 問題 abort 演算子のチェックのために eq context = ('AbtTest =def (('a : 'b…

Maudeは書き換え論理(rewriting logic)だとかメンバシップ等式論理(membership equational logic)の項を書いたり動かしたりできる。 今の僕の理解ではMaudeは項書き換え系のめっちゃリッチな実装とだけ思っている。 →の前後が等価であれば CafeOBJ みたいな…

OCaml-Nagoyaの会にて、id:osiireさんの concurrent cell (OCamlの並行プログラミングの拡張) の話を伺った。 当日の話について詳しくは ocaml-nagoya : ivarの必要性 より。当初、問題そのものがちょっとよくわからなかったのだけど、要するに OCamlの標準…

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 f…

ひとつ前のエントリ でテキトーに作った 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 (s…