後方参照のある正規表現の能力

定期的に出てくる話題ですが、プログラミングで出てくる正規表現正規表現ではないので、素数判定ができます。正確には、文字列の長さが素数かどうかを判定できます。2 文字以上のマッチが 2 回以上出現するかどうかを見ます。後方参照がポイント。

p (2..30).select{|x| !("X" * x)[/^(..+)\1+$/] }
  #=> [2, 3, 5, 7, 11, 13, 17, 19, 23, 29]

ところで、{ a^n | n は素数 } は文脈依存言語のはずなので、後方参照のある正規表現線形拘束オートマトン以上の表現力を持つことになるのでしょうか。でも、文脈自由文法である { a^nb^n | n は自然数 } や括弧の対応は書けなさそうです。ちょっと調べてみても、後方参照のある正規表現の能力はよくわかりませんでした。


とりあえずPerl の正規表現マッチングで 3-CNF-SAT が解けるそうです。つまり NP 完全。別に 3-CNF でなくても CNF なら同じ方法でできる気がします。(x_1 \vee x_2) \wedge (x_1 \vee \bar{x_2}) \wedge (\bar{x_1} \vee \bar{x_2}) (wikipedia より) を判定するマッチングは以下の通り。頭いいなあ。

str = "xx;x,x,x,"
re = /^(x?)(x?)x*;

    (\1|\2),    (?# (x1 || x2) )
    (\1|\2x),   (?# (x1 || !x2) )
    (\1x|\2x),  (?# (!x1 || !x2) )

$/x

str[re] #=> 充足可能ならマッチング成功、不能ならマッチング失敗

任意の CNF の充足可能性問題を文字列と正規表現に変換するプログラムも載っていましたが、Perl は読めないので Ruby に書き直してみました。

def regex_sat(v, clauses)
    # v : 変数の数
    # clauses : 論理式、x1 and x2 and (not x3) を [1, 2, -3] と書く

    str = "x" * v + ";" + "x," * clauses.size
    re = "^" + "(x?)" * v + "x*;"
    re +=
        clauses.map do |xs|
            "(" +
            xs.map {|x|
                "\\" + (x > 0 ? x.to_s : (-x).to_s + "x")
            end.join("|") +
            "),"
        end.join
    re += "$"
    re = Regexp.new(re)

    str[re] && $~[1..v].map {|x| x == "x" }
end

# (x1 || x2) && (x1 || !x2) && (!x1 || !x2) の判定
p regex_sat(2, [[1, 2], [1, -2], [-1, -2]]) #=> [true, false]
# x1 = true かつ x2 = false で充足可能

# (x1 || x2) && (x1 || !x2) && (!x1 || x2) && (!x1 || !x2) の判定
p regex_sat(2, [[1, 2], [1, -2], [-1, 2], [-1, -2]]) #=> nil
# 充足不能