僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが，Brzozowski derivativeに基づいて正規表現エンジンを実装し，あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです．

折角practicalなプログラムを書いたのにCoqの中に閉じ込めておくのも勿体ないですし， OCamlで同様の正規表現エンジンを実装し，実行速度を見てみようと思います． *1

2018/12/16 Brzozowski derivativeの定義に誤りがあったため修正

Brzozowski derivativeとは？

ある正規表現 $R$ が受理する言語 $L(R)$ の先頭から，文字 $a$ を取り除いて得られる言語 $\{u \in\Sigma^*| au\in R\}$ *2を受理する正規表現 $D_a(R)$ をBrzozowski derivativeといい，以下のようにsystematicに求められます．

${\displaystyle \begin{array}{l} D_a(\emptyset) = \emptyset \\ D_a(\epsilon) = \emptyset \\ D_a(b) = \left\{ \begin{array}{l} \epsilon~(a=b) \\ \emptyset~(\mbox{others})\\ \end{array} \right. \\ D_a(R \cup S) = D_a(R)\cup D_a(S) \\ D_a(R \cdot S) = \left\{ \begin{array}{l} D_a(R)\cdot S \cup D_a(S) ~(\epsilon \in L(R)) \\ D_a(R)\cdot S~(\mbox{others})\\ \end{array} \right. \\ D_a(R^*) = D_a(R)\cdot R^* \\ \end{array} }$

ある正規表現が空文字列を受理するかどうかは比較的簡単に判定できますから，文字列に含まれる文字について順番に $D_a$ を適用していけば，与えられた正規表現が文字列を受理するかどうか判定するプログラムが実装できることでしょう．

OCamlによる実装

元々の練習問題の実装はまずASTを定義し，

Inductive reg_exp {T : Type} : Type :=
| EmptySet : reg_exp
| EmptyStr : reg_exp
| Char : T -> reg_exp
| App : reg_exp -> reg_exp -> reg_exp
| Union : reg_exp -> reg_exp -> reg_exp
| Star : reg_exp -> reg_exp.

ASTを受け取る再帰関数として，空文字列を受理するかの判定や

Fixpoint match_eps (re: @reg_exp ascii) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

ある文字で微分した正規表現

Fixpoint derive (a : ascii) (re : @reg_exp ascii) : @reg_exp ascii
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

などを記述するものでした．いわゆるdeep embeddingですね．

まぁしかしいちいちASTを作ってたらメモリが勿体ないので，関数型の人はこういうDSLっぽいのはshallow embeddingで書くんじゃないでしょうか？この例でいうと正規表現自体を，空文字列を受理するかの真偽値と微分結果のレコードにしてしまう感じのやつです．

(* 正規表現 *)
type reg_exp = { match_eps : bool; derive : char -> reg_exp }

(* 空集合を表す正規表現 *)
let rec empty_set =
  { match_eps = false;
    derive = fun _ -> empty_set }

(* 空文字列を表す正規表現 *)
let empty_str =
  { match_eps = true;
    derive = fun _ -> empty_set }

(* 1文字を表す正規表現 *)
let char c =
  { match_eps = false;
    derive = fun c' -> if c = c' then empty_str else empty_set }

(* 選言 *)
let rec union re1 re2 =
  { match_eps = re1.match_eps || re2.match_eps;
    derive = fun c -> union (re1.derive c) (re2.derive c) }

(* 連接 *)
let rec app re1 re2 =
  { match_eps = re1.match_eps && re2.match_eps;
    derive = fun c ->
      union
        (app (re1.derive c) re2)
        (if re1.match_eps then re2.derive c else empty_set) }

(* Kleene star *)
let star re0 =
  let rec re =
    { match_eps = true;
      derive = fun c -> app (re0.derive c) re } in re

(* 与えられた正規表現がある文字列を受理するかの判定 *)
let regex_match s re =
  (List.fold_left (fun re -> re.derive) re s).match_eps

もっとも，正規表現の型が実装丸出しで格好悪いので，こういうのはモジュールで隠しておくことにしましょう．

module RegExp : sig
  type t
  val empty_set : t
  val empty_str : t
  val char : char -> t
  val app : t -> t -> t
  val union : t -> t -> t
  val star : t -> t

  val matches : char list -> t -> bool
end = struct
  type t = { match_eps : bool; derive : char -> t }

  let rec empty_set =
    { match_eps = false;
      derive = fun _ -> empty_set }

  let empty_str =
    { match_eps = true;
      derive = fun _ -> empty_set }

  let char c =
    { match_eps = false;
      derive = fun c' -> if c = c' then empty_str else empty_set }

  let rec union re1 re2 =
    { match_eps = re1.match_eps || re2.match_eps;
      derive = fun c -> union (re1.derive c) (re2.derive c) }

  let rec app re1 re2 =
    { match_eps = re1.match_eps && re2.match_eps;
      derive = fun c ->
        union
          (app (re1.derive c) re2)
          (if re1.match_eps then re2.derive c else empty_set) }

  let star re0 =
    let rec re =
      { match_eps = true;
        derive = fun c -> app (re0.derive c) re } in re

  let matches s re =
    (List.fold_left (fun re -> re.derive) re s).match_eps
end

ベンチマーク

プログラムを書いたのに動かさないのは勿体ない！適当なベンチマークにでも放り込んでみたいところですが，そういうのは不慣れなのでAtCoderで正規表現を使う問題を見繕って投げることにしましょう． C - Daydreamなんか良さそうですね．想定解法は後ろから見ていくやつですが，正規表現を使えば脳死でACできることでしょう．

そして実際にこの正規表現エンジンの実装を用いた解法を投げてみたんですが，あえなくTLE． beta.atcoder.jp

実装の改善

あまりパフォーマンスが出なかった原因，それは連接の微分にありそうです．

${\displaystyle D_a(R \cdot S) = \left\{ \begin{array}{l} D_a(R)\cdot S \cup D_a(S) ~(\epsilon \in L(R)) \\ D_a(R)\cdot S~(\mbox{others})\\ \end{array} \right. }$

こいつがどんどん導関数を大きくしてしまうせいで，計算時間が指数関数的に増えているようですね．

空集合を微分しても空集合ですし，空文字列や文字を何回か微分すると空集合に行き着くように，大概の正規表現は何回も微分すると空集合になります．ならないのはKleene starの混じってるやつぐらいでしょうか．空集合や空文字列の混じった正規表現を簡約してやれば速度が改善できそうです．

そのために，正規表現を表す型に空集合や空文字列かどうかの情報も追加してやります．

type t = { sort : sort; match_eps : bool; derive : char -> t }
and sort = EmptySet | EmptyStr | Other

let rec empty_set =
  { sort = EmptySet;
    match_eps = false;
    derive = fun _ -> empty_set }

let empty_str =
  { sort = EmptyStr;
    match_eps = true;
    derive = fun _ -> empty_set }

let char c =
  { sort = Other;
    match_eps = false;
    derive = fun c' -> if c = c' then empty_str else empty_set }

あとは一般常識に基づいて簡約を入れていきます．

let rec union re1 re2 =
  match re1, re2 with
  | { sort = EmptySet }, _ -> re2
  | _, { sort = EmptySet } -> re1
  | _, _ ->
      { sort = Other;
        match_eps = re1.match_eps || re2.match_eps;
        derive = fun c -> union (re1.derive c) (re2.derive c) }

let rec app re1 re2 =
  match re1 with
  | { sort = EmptyStr } -> re2
  | { sort = EmptySet } -> empty_set
  | _ ->
      { sort = Other;
        match_eps = re1.match_eps && re2.match_eps;
        derive = fun c ->
          union
            (app (re1.derive c) re2)
            (if re1.match_eps then re2.derive c else empty_set) }
let app re1 = function
  | { sort = EmptyStr } -> re1
  | { sort = EmptySet } -> empty_set
  | re2 -> app re1 re2

let star = function
  | { sort = EmptySet }
  | { sort = EmptyStr } -> empty_str
  | re0 ->
      let rec re =
        { sort = Other;
          match_eps = true;
          derive = fun c -> app (re0.derive c) re } in re

これでどうでしょうか？ beta.atcoder.jp ……今度は十分高速に動いているようです！

まとめ

Brzozowski derivativeに基づく正規表現エンジンの実装をshallow embeddingで与えました．ナイーブな実装では正規表現が指数関数的に大きくなってしまいパフォーマンスが出ませんでしたが，簡単な簡約を入れてやることで十分な速度で動作する実装が得られました．

ちょっとベンチマークが適当なところもあるので，真面目なベンチマークに対して速度が出るのか試してみても良さそうですね．

*1:Software Foundationsには"Please do not post solutions to the exercises in a public place."と書いているので，Coqのコードから直接Extractするのも遠慮しておこうかなと

*2:left quotient

fetburner.core

コアダンプ

OCamlで正規表現を微分する

Brzozowski derivativeとは？

OCamlによる実装

ベンチマーク

実装の改善

まとめ