日々の流転

λ. RegEx Tシャツ

「軽量言語の次はこれ！」らしいですよ。

http://explanation-guide.info/image/180px-Airkz_20040617_jon_regular_expression.jpg.html

λ. Bisimulation Algorithm

このままじゃ恥ずかしすぎるので、hyperset.rb(と未公開のHaskell版実装)を直そうと思いたったのだけど、また自分で考えると何か間違えそうなので、既存のアルゴリズムを探すことに。そこでGoogle先生に尋ねると A. Dovier, C. Piazza, and A. Policriti. A fast bisimulation algorithm. TR UDMI/14/00/RR, Udine, 2000. というのがあったので、これを使わせてもらおう。Non-Wellfounded な場合にはそうやってrankを定義できるのかぁ。なるほど、なるほど。

で、Haskellで試しにコードを書いてみようとしたのだけど、Paige-Tarjan の手続きを呼ぶとしか書かれてない部分があって困ってしまった。R. Paige and R. E. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973-989, 1987. に書いてるらしいのだが、この論文Web上にはないし、調べるの面倒なので、試しにこれ抜きでやってみる。幾つかの例を試すとこれでも正しく動作しているように見えるが……ダメな例を早速発見。Ω={Ω} として、α = {Ω,φ} と β = {Ω,φ,{Ω,φ}} が区別できないな。この二つは共にrankが1で、rankがこれより小さいのはrankが−∞のΩとrankが0のφ。α,βは共にΩとφを含んでいるので、Ωとφによる分割だけではα,βは区別できない。同じrank内でさらに分割する必要があるけど、それにはどうしたら良いのかなぁ。うーむ。

何が足りないのかとしばし悩んで(足りないのは Paige-Tarjan の手続きに決まってるけど)、{{Ω},{φ},{α,β}} という分割(によって定義される同値関係)はstableでないことに気付く。

ちなみに、関係R⊆N×Nが与えられたとき、Nの分割Pの任意のブロックB₁,B₂に対して、B₁⊆R^-1(B₂)とB₁∩R^-1(B₂)=φのいずれかが成り立つとき、Pは関係Rに関してstableだという。あるいは、分割Pによって定義される同値関係を≡_Pとして、(∀a,a',b∈N)((a≡_Pa' ∧ a R b) ⇒ (∃b'∈N)(b≡_Pb' ∧ a' R b')) という定義の方が直観的かな。

閑話休題。さっきの例だと N = {Ω,φ,α,β}, R = ∋ なので、P = {{Ω},{φ},{α,β}} だと、B₁ = B₂ = {α,β} としたとき、R^-1(B2) = {y | x∈{α,β}, y∈N, y ∋ x} = {β} となってしまい、Pはstableな分割ではないことがわかる。maximal bisimulation はstableであるはずなので、この同値関係は大きすぎる(i.e. 分割が粗過ぎる)ことが判定できる。試しにstabilizationの処理を素朴に実装して見たら、αとβは区別できるようになったし、試した限りでは他の例でも正しく動いているように見える。

ということは、Paige-Tarjan の手続きってのはstabilizationのための効率的なアルゴリズムのことなのかな? (ぉぃ

……とか書いてたら、バークレイ大のCS 294-1: Model Checking, EE 219C: Computer-Aided Verificationという授業の講義資料に Graph Minimization というのを発見。まだ読んでないけどとても良さそう。

あと、A fast bisimulation algorithm の著者のサイト にC++のコードがあるのも発見。