2008-07-27 [長年日記]
λ. MONAで正規表現にマッチする例を生成する
論理と計算のしくみ(萩谷 昌己/西崎 真也) にWS1S(Weak Second-order monadic logic of 1 Successor, 後継者のみの単項二階論理)の論理式と有限状態オートマトンとが対応するとか書いてあった。 それなら、正規表現に対応する有限状態オートマトンをWS1Sの論理式で記述して、モデル探索を行えば、与えられた正規表現からマッチする文字列の例を生成するようなことが出来るんじゃないかと思ったのだった。
『論理と計算のしくみ』の場合
ただ、『論理と計算のしくみ』での説明は良く分からなかった。 この本での説明は、萩谷先生の講義録「高階述語論理とその部分体系」でなされている以下の説明とほぼ同じなのだけど、「i>j ==> not i∈Xj」という条件をどう考えればよいのかが分からない。
n個の自然数の集合X1,...,Xnと、{0,1}^nをアルファベットとする語wを対応させる。
X1,...,Xn <--> w=a0a1a2...am where ai = (b1,...,bn) bj=1 iff i∈Xj i>j ==> not i∈Xj
しばらく考えてもわかんなかったので、とりあえずWS1Sの検査などを行えるシステムとして有名なMONAを見てみることにした。
MONAの場合
MONAについてはよく知らなかったのだけど、MONAのサイトを見てみると、以下のように書いてあった。なるほど、オートマトンに変換してやっているのね。モデル検査っぽいなぁ。
MONA is a tool that translates formulas to finite-state automata. The formulas may express search patterns, temporal properties of reactive systems, parse tree constraints, etc. MONA analyses the automaton resulting from the compilation and prints out "valid" or a counter-example.
で、ダウンロードして見てみると、regexp.mona として正規表現「a*(ab*)」を WS1S にエンコードしている例があった。 これが非常に分かりやすくて、ごく一部のMONA固有の機能を除けば、前提知識無しで読むことが出来るものだった。 また、「論理と計算」での取り扱いよりも単純で分かりやすい。
ポイント:
- 位置 p で性質 P が成り立つことを、二階の変数 P を用いて、p∈P で表現する。
- そのような性質として、bit1,…,bit7 を用意して、各ビットが1であることを表現する。
- WS1Sだと(一階の)領域は自然数全体なのに対して、文字列の場合には位置は有限なので、下に閉じた二階の変数 $ を用意して、通常の変数は $ の要素や部分集合のみを動くようにする。(そうしないと、全ビットが0であるような文字の繰り返しが終端に現れるような文字列を正しく扱えない)
- 正規表現は、「開始位置」と「終了位置+1」をとって、開始位置から終了位置までの文字列が正規表現にマッチする場合に真になるような述語として表現。(差分リスト方式)
- 正規表現全体を表現した述語(この場合にはis_a_star_ab_star)を使って、「is_a_star_ab_star(0, max($)+1)」という論理式にする。これで文字列全体がこの正規表現にマッチすることが表せる。
MONAの実行例
で、「mona.exe regexp.mona」を実行してみる。 そうすると、色々出てくるが、結果の中の以下のような部分が正規表現にマッチする具体的な文字列を表している。
A satisfying example of least length (0) is:
bit0 X
bit1 X
bit2 X
bit3 X
bit4 X
bit5 X
bit6 X
bit7 X
bit0 = {}
bit1 = {}
bit2 = {}
bit3 = {}
bit4 = {}
bit5 = {}
bit6 = {}
bit7 = {}
この場合だと空文字列になっている。 これだと面白くないので、「5 in $」という論理式を加えて、長さが6以上のものを探させると、こんなのが出てくる。
A satisfying example of least length (6) is:
bit0 X 101010
bit1 X 010101
bit2 X 000000
bit3 X 000000
bit4 X 000000
bit5 X 111111
bit6 X 111111
bit7 X 000000
bit0 = {0,2,4}
bit1 = {1,3,5}
bit2 = {}
bit3 = {}
bit4 = {}
bit5 = {0,1,2,3,4,5}
bit6 = {0,1,2,3,4,5}
bit7 = {}
最初の行からこの具体例の長さが6であることがわかり、続く表の各カラムを見ると各位置の文字のビットパターンがわかる。これをデコードすると「ababab」という文字列になっている。 で、後半部分は変数の割り当て。
あとは、複数の具体例を順番に出したりする機能があると面白いのだけど、残念ながらMONAにはそういった機能はないようだ。
参考
λ. 今日の日記
午前中、近くのプールでまた1km泳ぎ、午後は第6回 RHGの逆襲へ参加。 こっちの読書会にはどんな人が参加しているのかな、という好奇心で参加してみたのだけど、色々な人に会えて、やっぱり楽しかった。でも、行く前に svn update していけば良かったな。そこはちょっと失敗。
あと、新橋の駅前で小銭入れを買った。
![[小銭入れ]](./images/20080727_1.jpg)
