日々の流転

λ. 正規表現にマッチする文字列をAlloyで生成する

• 正規表現からその正規表現にマッチするような例を生成する - soutaro#nikki()
• 正規表現にマッチする例 - d.y.d.
• 大人げ - sumiiの日記

辺りの話を思い出し、そういえばこれってモデル生成の話だから、Alloy Analyzer で出来そうだなと思ってやってみた。 結果としては特に面白くもなかったけど。 Regex.als

まず、文字列を表すための指標を用意。 個々の文字はCharをextendsする指標として定義する。

abstract sig Char {}

abstract sig String {}
one sig Nil extends String {}
sig Cons extends String {
　 head : one Char,
   tail : one String
}
fact {
   all s : Cons | not (s in s.^tail)
}

でもって、正規表現を文字列に関する論理式に変換するのだけど、DCG方式で差分リストに対する述語として定義する。 そうすると、大体以下のような感じで解釈することになる。

• [[ ]](x,y) = (x==y)
• [[ . ]](x,y) = (x.tail==y)
• [[ c ]](x,y) = (x.tail==y && x.head==c)
• [[ e1 e2 ]](x,y) = some z : String | [[ e1 ]](x,z) && [[ e2 ]](z,y)
• [[ e1|e2 ]](x,y) = ([[ e1 ]](x,y) || [[ e2 ]](x,y))
• [[ e? ]](x,y) = ([[ e ]](x,y) || x==y)
• [[ e* ]](x,y) = some r : String -> String { (all x,y : String | y in x.r <=> [[ e ]](x,y)) && y in x.*r }
• [[ e+ ]](x,y) = some r : String -> String { (all x,y : String | y in x.r <=> [[ e ]](x,y)) && y in x.^r }
• [[ [ab...] ]](x,y) = (x.tail==y && x.head in a+b+...)

Alloyでは述語の帰納的な定義が出来ないので、繰り返しはreifyした関係の(反射)推移閉包を使って表現するのがポイント。 というか、それをしたかったので差分リストに対する述語として形式化したんだけどね。 なお、今回は否定や補集合は扱っていないけど、それらを扱う際には関係rの量化と定義を否定の内側ではなく一番外側に持ってくる必要があるので注意。

そうすると、例えば「goo+gle」という正規表現は以下のようになる。

pred google(x : String) { google[x, Nil] }
pred google(x, y : String) {  
  some a, b, c, d, e : String {
    x.head==C_g
    x.tail==a
    a.head==C_o
    a.tail==b
    many1_o[b,c]
    c.head==C_g
    c.tail==d
    d.head==C_l
    d.tail==e
    e.head==C_e
    e.tail==y
  }
}

-- o+
pred many1_o(x, y : String) {
  some r : String -> String {
    all x, y : String | y in x.r <=> x.head==C_o && x.tail==y
    y in x.^r
  }
}

でもって、テスト。

pred test_google() {
  some x : String {
    google[x]
    all y : String | y in x.*tail
  }
}

run test_google for 10

runすると、それっぽい結果が出てくる。

お題の正規表現についても同様。

λ. 世にも奇妙な物語 — SMAPの特別編

懐かしいなぁ。 最初の「エキストラ」の話は以前は見逃していた気がする。

λ. 「形式的体系の定理証明支援系上での実現法」資料

を読んだ。 AgdaによるHoare論理の形式化と、whileプログラムの遷移系での解釈に対するHoare論理の健全性の証明の話。 ところで、「ホア論理」という呼び方は初めて見た……