ついに、Alloy を使って完全な λ計算 (β簡約) を表現できた…。（前回 は中途半端だった。） なかなか面白いのは、Alloy がうまくノードを使って無駄なくβ簡約しているところ（Ω=(λx.xx)(λx.xx) で Ω→Ωなど。後に載せる）。(8/22)フレーム条件のバグを直した…

フォロー記事あり前回 (Alloyでλ式をつくる) では、λ式を表現するグラフをAlloyで構築した。 今回は、λ計算の核となるβ簡約の一部をAlloyで記述してみる。 扱えるλ式の制限 面倒だったので、モデルに次の制限を導入した。 このため、正確にはβ簡約とはいいが…

Alloyでλ式を作ってみた。 フォロー記事あり あまり役に立たない気はするけど、関係の逆(~)を取ったり(反射)推移閉包(*,^)を使う良い練習になった。（バグがみつかり次第、色々修正している。以下のモデル図はソースを修正しながら作っているので、エンバグ…

Alloyの言語仕様をゴリゴリ読み進めていた。 非常に勉強になります。Software Abstractions (1st ed., p.288): So although a quantified constraint with multiple declarations may be regarded, for some quantifiers, as a shorthand for nested constra…

Alloyを使ってみた。 数年前に使ったときはなんでこんなの使うのと思っていたけど考えが変わったのだ。 ちょっとした規模のプログラムを書くには設計が必要だ。 コードを書く前に、問題の本質的な部分を知っておこう。 本質がわかっていれば、 適切な部分に…

やっぱりπ計算の前に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 (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…

ググれば出てきそうな気もしますが、がんばってみました。しかしあえなく轟沈。(証明どころか関数さえ書けない始末…情けない。)Coqではちゃんと停止する関数しか書けないです。これは再帰が書けないという事ではなく、再帰にはDefinitionの代わりにFixpoint…

「プロセス代数」π計算の話です。 Martin Bergerさん(イギリスのπ計算の研究者)のホームページに、π計算の発案者であるRobin Milner氏へのインタビューが掲載されています。An Interview with Robin Milner「なぜπ計算はπ計算と呼ばれているの？」と質問する…