Blog

【採択論文紹介】Regular Expressions with Backreferences and Lookaheads Capture NLOG (ICALP 2024)


Algorithmsチームの上里です。理論計算機科学のトップカンファレンス ICALP 2024 に採択された論文
「Regular Expressions with Backreferences and Lookaheads Capture NLOG」を紹介します。 arXivの著者版へのリンク

論文のタイトルを日本語訳にすると以下の通りです:

  • 正規表現 (Regular Expressions) を
  • 後方参照 (Backreferences) と 先読み (Lookaheads) で拡張した体系が
  • 非決定性対数領域チューリングマシン言語 (NLOG; Nondeterministic Log-space) と呼ばれるクラスに対応する

これを「正規表現+後方参照+先読み=NLOGと書きますが、この等式が主定理の一つです。
この記事では、証明をお伝えするとまではいかないながらも、その雰囲気はお伝えできるように頑張ります。

§1. 定理の主張の内容と応用を、いきなり知りたいです

分かりました! どんなことが主定理から言えるかを、やや大味にはなりますが、書いてみます。

後方参照先読み は、後でもう少し丁寧に説明しますが、簡単に言うと正規表現の「拡張機能」です。
拡張とはいえ、多くの処理系やライブラリでサポートされているので、知らずに使ったことがあるかもしれませんね。
Pythonでも特に何もせずに使えるので、この記事では実際にPythonで動くコードも掲載しています。

とにかく「正規表現+後方参照+先読み」というのは、私たちが普段書ける範囲の(拡張)正規表現です。

一方で、NLOG は、計算量クラスです。3SAT をはじめとした高速に解くのが難しい問題が集まっていることで有名なクラス NP とは、以下の関係にあります(参考: https://en.wikipedia.org/wiki/PSPACE):$$\mathbf{NLOG} \subseteq \mathbf{P} \subseteq \mathbf{NP} \subseteq \mathbf{PSPACE}.$$

PSPACE もこの記事の後ろの方で出てくるので書いてしまいました。

計算量クラスというのは、「「文字列の集合(すなわち、言語)」の集合・族」になります。\(\subseteq\)の右側に進むほど、より多くの言語を含んでいることになるので、手強い・難しくなると言えます。

この中で クラスP は簡単かつ正確に説明できます。これは普通のプログラム(決定性チューリングマシン)で多項式時間で受理できる(=解ける、と思っても良いです)言語クラス、となります。

一方、残りの計算クラスを正確に述べるのは大変なので、代わりに各クラスの代表選手(各クラスで最も難しいと言って過言ではない言語)の紹介をします。
まず NP  3SAT です。これは 3CNF のうち、充足可能なもの全てからなる集合を意味します。正確には:

  • 3CNFは 「「変数 または 変数の否定 を 論理和\(\lor\) で 3つ 繋いだもの」を 論理積\(\land\)で好きなだけ繋いだもの」です:$$\text{例.}\  (a \lor b \lor c) \land (a \lor \neg b \lor c) \land (\neg a \lor \neg b \lor \neg c) \land (\neg a \lor b \lor \neg c)$$
  • 式が充足可能 (satisfiable) とは、変数に適当にtrue / falseを割り振ると、その式を真にできることを言います。
  • 上の例は、充足可能です。例えば \(a = \texttt{true}, b = \texttt{false}, c = \texttt{false}\) とします。

次に NLOG ですが、ここに 3SAT が入っているかどうか分かっていません。有名な P=NP 問題と同様に、NLOG=NP かどうかも NLOG=P かどうかも未解決です。ただし、NLOG には、3SAT を少し簡単にした 2SAT がいます。
これは 2CNF のうち、充足可能なもの全てからなる集合です。正確には:

  • 2CNF は「「変数か変数の否定を 論理和\(\lor\) で2つ繋いだもの」を 論理積 \(\land\)  で好きなだけ繋いだもの」です: $$\text{例.}\  (a \lor c) \land (b \lor c) \land (\neg b \lor a) \land (\neg c \lor b) \land (\neg a \lor b)$$
  • 充足可能性の定義は上と同じです。また、この例は充足可能ではない(=充足不能)です。

最後に PSPACE には TQBF (True Quantified Boolean Formula) という集合が入っています。これは $$\forall x. \exists y. \forall z. (x \lor \neg y \lor z) \land (\neg x \lor y \lor z)$$ のような、forall や exists がついたより一般的な式で、かつ、成立する (valid) 論理式全体からなります。2SAT 3SAT は exists が隠れているだけなので、forallもある TQBF はかなり難しい集合です。

さて、「正規表現+後方参照+先読み=NLOG」というのが論文の結果です。
この結果から、2SAT を受理(表現)できる拡張正規表現 \(E_{2SAT}\) が存在すると言えます。より直感的には、2CNFが与えられた時に、それが充足可能な時に限りマッチする正規表現 \(E_{2SAT}\) を作れると言えます。

注意してほしいのは、一つの \(E_{2SAT}\) 式で、全ての 2CNF を相手に充足可能性を判定しなければならない、ということです。式には幾つ変数が現れるか分からないのに「正規表現だけで」何とかしなくてはなりません。
仮に変数が 3つ \( a, b, c\) の式だけ相手にすれば良い。などと事前に分かっていればやりようもあるかもしれませんが、$$ (x_1 \lor \neg x_2) \land (x_2 \lor x_3) \land (\neg x_1 \lor x_4) \land \cdots \land (x_{123456} \lor x_{44444499})  $$ のような巨大な式をはじめとする無限個の式を、たった一つの正規表現 \(E_{2SAT}\)  で処理しなくてはなりません。

一見すると非常に難しいこの問題ですが、今回の結果から、そのような \(E_{2SAT}\) が作れると言えます!
さらには、このような集合が表現できるほど表現力が強いので、かなり難しいテキスト処理にも使えると言えますね!

§2. 登場人物の紹介

次の3節で主定理の証明、とまではいきませんが雰囲気をお伝えしたいので、この節ではそのために今回の登場人物を紹介します。既に NLOG は簡単に紹介したので、残りの「正規表現」「後方参照」「先読み」を説明します。

2.1. 正規表現

まず 正規表現 ですね。これは日常的なテキスト処理で使ったことがある方も多いと思います。
正確に定義まで書き始めると大変なことになるので、例を中心に述べていきます。

例えば、文字列の中に abracadabra が現れるかどうかをチェックしたいとします。
このとき、Pythonだと次のようにすれば良いです(お好きなプログラミング言語で書いてみてもらえると幸いです):

実行すると、w1abracadabra を含むが、w2 は含まない、という結果が正しく得られることがわかります。

※細かい けど 大事な話❗️ この記事、というより形式言語の理論では、文字列を全て消費出来る時に限りマッチとしたいので、文字列末尾を表す特殊シンボル  $ を積極的に使います。Pythonだとfullmatch を使っても良いです。

用語の導入 ▷ 正規表現 \(R\) とマッチする文字列全体のことを、\(R\) の受理する言語 \(\mathcal{L}(R)\) と言います。

上の正規表現abraの受理する言語は次のものです:
$$\mathcal{L}(\texttt{abra}) = \{ w : \text{$w$ は abracadabra を含む} \}.$$

2.2. 後方参照

後方参照 は、正規表現に「変数」を導入する拡張機能です。
マッチした文字列を変数に保存し、その変数を後から参照するという感じです。
環境ごとに構文は違いますが、Pythonだと以下のように書きます:

  • (?P<Var>...) と書いて、部分式 ... にマッチした文字列を変数 Var へ保存し;
  • (?P=Var) と書いてVarの中身を展開・参照する。

あれ?自分の知ってる後方参照とちょっと違うな?という方もいるかと思います。k番目のグループでキャプチャした内容を \k で参照するやつ、ですよね? 上で書いたのは正確には「名前付き後方参照」と呼ばれるものでして、変数名がある方が便利だよねということで、論文でもこの記事でも名前付きの方を使います。
Pythonの後方参照の構文については、公式のドキュメント も参考にしてもらえると幸いです。

さて、例として、次の言語を考えましょう:
$$L_{\text{search}} = \{ \mathit{pattern}\,\#\,w : \text{文字列 $w$ 中に}\ \textit{pattern}\ \text{が出現する} \}.$$
あえて日本語で説明すると、この言語が含む文字列とは:
  • #を区切り文字として、それ以前に出てくる文字列をパターンとした時に;
  • #以後に出てくる文字列が、パターンを含むようなもの

です。例えば abracadabra#xxxabracadabrayyy はOK、という感じです。

後方参照を使うと、Pythonでは次のように書けます:

見た目がやや大変ですが、やっていることは単純でして
  • (?P<X>([^#]*))# の部分で、# 以前の文字列=パターン文字列を変数 X に保存して
  • .*(?P=X).* の部分で、#以降に、Xに保存済みのパターン文字列が出現するどうかを探す
ということをしています。

正規表現 ⊊ 正規表現+後方参照

ひとつ前の例 \(\mathcal{L}(\text{abra})\) ではパターンごとに正規表現を作る必要があったともいえます。
その意味で、\(L_{\text{search}}\) は後方参照を活用した、より強力な言語だと言えるでしょう。
実のところ、この言語は後方参照のない古典的な正規表現では受理できません。正確には「\(L_{\text{search}}\) は正規言語ではない」と言います。ポンピング補題という言葉に覚えがある方は、それからすぐ証明できるので挑戦してみてください!

後方参照を追加すると表現力が増すということで、図式的に正規表現 ⊊ 正規表現 + 後方参照と書くことにします。

2.3. 先読み

先読み は、正規表現で条件分岐をするための拡張機能と言えます。プログラミング言語のif文やif式、あれを正規表現でもやろうというわけです。

例えば、次のようなfizz xor buzzチェック問題を考えましょう:
  • a だけからなる文字列 (w =) aaaa ... a を考える。
  • ただし、wの長さが 3の倍数「xor」5の倍数の時に限り受理する。つまり、
  • wの長さは 3の倍数 「または」 5の倍数の時 に受理するが、長さが 3の倍数「かつ」5の倍数の時 は受理しない。
文字列処理のプログラムとして考えるならば、次のようにすれば良いでしょう:

先読みを使うと、これと同じことが正規表現上で実現できます。Pythonでは次のようにすれば良いです:

何だか見た目が大変ですが、説明させてください。この例では二つの先読みを使っています。

まず (?!...) という形の先読み「否定先読み (negative lookahead)」 です。
これは式...とマッチ「しない場合」に計算を続けるよう指示しています。
今回は入力長が15の倍数では ない 時に限り計算を続けるようにしています。

次に(?=...)という形の先読み「肯定先読み (positive lookahead)」です。
これは式...とマッチ「する場合」に計算を続けるよう指示しています。
今回は (aaa)*$(入力長が3の倍数)または (aaaaa)*$(入力長が5の倍数)の時に限り計算を進めます。

先読みの重要な性質は「入力を消費せずに」文字列を検査できるところです。
これから処理することになる残りの入力を先読みして検査だけするわけですね。上の例では
  1. まず入力を消費せずに(先読みで)15の倍数であるかどうかを検査し
  2. 次に入力を消費せずに(先読みで)3の倍数か5の倍数であるかどうかを検査し
  3. 両方をパスしたら、そこで初めて .* を使って文字列を全て消費する
としています。

「正規表現 = 正規表現+先読み」

先読みは便利なのですが、正規表現の表現力を本質的に拡大しないことが知られています。
ですので「正規表現+先読み」で受理される言語は、先読みなしの古典的な正規表現でも受理できます!

図式的には「正規表現 = 正規表現 + 先読み」と書くことにします。

§3. 正規表現+後方参照+先読みの表現力

ここまでの内容を簡単にまとめると
  • 「正規表現 ⊊ 正規表現+後方参照」 後方参照を使うと正規表現では表せない言語が表現できる
  • 「正規表現 = 正規表現+先読み」 先読みを使っても正規表現より表現力が増えない
ということになります。これらはどちらも既知の結果です。

それでは両方を同時に使った場合、すなわち「正規表現+後方参照+先読み」の表現力はどうなるでしょうか?
 
先読みは表現力を変えず「正規表現+後方参照 = 正規表現+後方参照+先読み」となるのでしょうか?

何度も「正規表現+後方参照+先読み」と書くと長くて大変なので、以降は REWBLk と略します。
 

冒頭にも述べた通りREWBLkNLOGが成立し、これこそ論文の主要な結果の一つです。
また、この系として「正規表現+後方参照 ⊊ REWBLk」も言えます。

3.1「REWBLk=NLOG」の証明の雰囲気

証明を書き切るのは大変なので、代わりに、NLOG で最も難しいと言える言語(NLOG完全な言語
\(L_{\text{STCONN}}\) が、REWBLk で受理できることを説明させてください。
 
あれ、2SAT ではないんか!というツッコミもあると思うのですが、それをやるとあまりにも大変です。
代わりに、同じ NLOG完全 だがより扱いやすい方を使いますね。
 
REWBLk は NLOG の言語を全て表現出来る (\(\mathbf{NLOG} \subseteq \mathbf{REWBLk}\)) っぽいんや〜 というのが伝われば幸いです。
この逆、NLOG を超えない (\(\mathbf{REWBLk} \subseteq \mathbf{NLOG}\)) 方は証明が大変です。興味のある方は是非論文を読んでください!
 
ではまず、言語\(L_{\text{STCONN}}\)とは何なのか?ですが、これは次の「有向グラフ上の2点を結ぶ経路があるよ」言語です:$$L_{\text{STCONN}} = \{ s \# x_1 \to y_1 \# x_2 \to y_2 \# \cdots \# x_n \to y_n \# t : \text{$s$から$t$へのパスがある} \}.$$

急いで補足させてください。各文字列 \(s \# x_1 \to y_1 \# x_2 \to y_2 \# \cdots \# x_n \to y_n \# t\) は
  • \(n\) 個の有向辺 \(x_1 \to y_1, x_2 \to y_2, \ldots, x_n \to y_n\) からなる有向グラフ について
  • スタートを頂点 \(s\) とし、ゴールを頂点 \(t\)とするような経路があるかどうか?

という問題を表していて、\(L_{\text{STCONN}}\)は実際に経路があるものだけを要素とする言語だ、といえます。

この言語は、Pythonだと次の正規表現で受理できるハズです:

だいぶすごい式が出てきてしまいました…… しかし、やっていることは素朴なものでして:
  1.  最初の部分式 (?P<C>(a+))(?=#) で、スタート頂点を変数Cに格納する
    • 簡単のために、頂点は a...aa のように a を並べて表現しているとします
  2. 部分式 (?=(.* # (?P=C) -> (?P<C>(a+)) #))* がメインの計算をするパート。
    • 内側の (.* # (?P=C) -> (?P<C>(a+)) #) は、
    • 変数 C で現在覚えている頂点を \(x\) とすると、そこから伸びる辺 \(x \to y\) を探してきて、
    • \(y\) を新しく変数 C に格納する。
  3. これを (?=(...))* という先読みの繰り返しで包み、入力を消費せずひたすらグラフ上を 非決定的に 渡り歩く
  4. 最後の .*#(?P=C)$ で、現在訪れている状態が、運良くゴール頂点と一致しているか検査する

という感じです。非決定的にグラフ上をお散歩しているだけなので、なるほど、これなら出来そうですね。

3.2 後方参照と先読みの実装サポート状況

それでは早速実行してみましょう!!となるのですが、Pythonで動かそうとすると以下のエラーが出ます:
re.error: redefinition of group name ‘C’ as group 4; was group 1 at position 35

再定義が行われている云々ということが書かれています。
Pythonでは、一つの正規表現中で、同一変数へ複数箇所から保存することを禁じていて、それに関する文言です。
構文的に ...(?P<Var>...)...(?P<Var>...)... のようなものは弾いているわけですね。

(※ 2024年5月段階の、バージョンで言えばPython 3.12の話ですので今後は変わるかもしれません。)

ところで、Python以外だとどうでしょうか?
例えば C# では以下の等価な正規表現(C#とPythonでは構文が異なります)を実行することはできます:

できるのですが、エラーにならないだけで、文字列 a#a->aa#aa->aaa#aaa を受理しません。もちろん \(a \to aa \to aaa\) という経路を持つはずなので受理できるべきなのですが……

実際の実装でこのようになる理由についても、論文のSection 2で述べているので、興味のある方は読んでみてください。

とにかく、理論的にはできるはずのことが、現実ではまだ実装が追いついていないので出来ていないと言えます。
ただ、先読みも後方参照もどっちもフルサポートして、バグもなくして…… というのは物凄く大変な仕事だとも付け加えさせてください。少なくとも、自分が何とかしろと言われてしまうと、かなり困ってしまいますね……

§4. 今後とおわりに

この研究と論文は、正規表現を便利にするという目的で追加された後方参照と先読みが、実は理論的にも非常に美しい特徴づけ「正規表現+先読み+後方参照(REWBLk)= NLOG」をなしていた、ということを明らかにしました!

NLOGには、2SAT や、グラフ上の経路問題言語 \(L_{\text{STCONN}}\) 以外に、以下のようなタフな言語も住んでいます(厳密には、DLOG (⊆ NLOG) というより小さいクラスにいます):

  • \(a\)の長さが二重指数の速度で増加する言語 $$L_{\text{2exp}} = \{ a^{2^{2^n}} : \text{$n$は自然数} \} = \{ a^2, a^4, a^{16}, a^{256}, a^{65536}, \ldots \}.$$
  • \(a\)の長さが素数の言語 $$L_{\text{prime}} = \{ a^p : \text{$p$は素数} \}.$$
    • クイズ❗️❗️ この言語は、Python で動かせる拡張正規表現で受理できます!挑戦してみてください!
    • ヒント: 素数の前に、合成数を受理する正規表現を書いてみると良いと思います

こういった言語は、古典的な正規表現でも、正規表現+後方参照でも受理できないと示せます。
従って REWBLk の表現力はかなり高いと言えますし、表現力が高いので様々なテキスト処理を任せられますね。

高速な正規表現ライブラリ・エンジンの実装は大変?

表現力の高さは良いことです。が、その一方で REWBLk をフルサポートする 高速な 正規表現ライブラリの実装が難しいということを示唆しています。一般に表現力が上がると、それを最適化したり高速化するのは難しくなるという話ですね。

実はこれは単なる示唆に留まらず、実際にかなり難しくなることも、論文では示しています。
現実世界のテキスト処理で必要な計算量に関わる問題として、 membership問題というものがあります。これは

  1.  入力として正規表現 \(R\)と文字列 \(w\) の二つを受け取り
  2. \(w\) が \(\mathcal{L}(R)\) に含まれるかどうかを Yes/No で判定せよ

という問題です。
ここまで「正規表現の受理する言語」を扱って来ましたが、それと違う種類の話題であることに注意してください。
この問題は、正規表現が主体なのではなく、それすら操作対象(パラメータ)になるので、似てはいるが異なる話題です。
Pythonで re.fullmatch(正規表現, 文字列) や re.match(正規表現, 文字列) とした時に実際に解いているのはこの問題です。

さて、論文では、REWBLk のmembership問題が PSPACE完全」 という結果も示しました。
 
NP より難しいのが PSPACE なので、この結果は REWBLk をフルサポートしてなおかつ 高速 に動く正規表現エンジンを開発するのは、非常にチャレンジングな問題だと言っています。
 
実際、論文では PSPACE完全 な問題である TQBF を、membership問題に埋め込むということをしています。具体的には
  1.  例えば \(\phi = \forall x. \exists y. (x \lor y) \land (x \lor \neg y)\) という式が valid であることを調べる代わりに
  2. \(\phi\) から 拡張正規表現 \(E_\phi\) と文字列 \(w_\phi\) を(多項式時間で)生成して、\(w_\phi \in_? \mathcal{L}(E_\phi)\) を調べても良い

ということです。かなり一般的な論理式の判定を文字列マッチングで解けます!

具体的な構成は論文を見てもらいたいのですが、上の式 \(\phi\) の妥当性検査は次のPythonプログラムで出来るはずです:

(これは re.error: redefinition of group と言われて動きませんが……)

このような難しさも、REWBLk をフルサポートする実装がまだ存在していない理由の一つではないかと思います。 もっとも、バグのない実装をするのが大変だという要因の方が大きいとは思いつつ。

理論的な複雑さが分かったところで、どうするの?

このような理論的困難さを示しておくのは、実際の開発で役に立つと(これまでの経験から)思っています。

指針なく闇雲に実装して「異様に遅いぞこれは……」となって 早すぎる最適化 (premature optimization) に突入することを避けられますし、不可能なことをやろうとすることも回避できます。

何より、表現力が高すぎるんだから遅くても仕方がないという心の持ちようがあれば、後方参照と先読みとフルサポートするライブラリを実装してリリースまでこぎつけられると真面目に考えています。

もう一つは、「フルサポートが難しいのは分かったので、現実的に重要な範囲を切り出して、そこは高速化できないか?」という、理論的にも実践的にも一歩進んだ重要な問いが生まれます。

今回の理論的結果は、正規表現で現実と戦うための工夫(後方参照、先読み)から生じました。 この結果を、再び実践の場に還元することにより、そこから更に面白い正規表現の応用や拡張が生まれ、そしてそれが更に理論を発展させていくことになると信じています。

さて、チャレンジングということは やるしかない! ということで、
今後は、REWBLkをフルサポートしながらも、現実的な多くの場合で高速に動く、実用的な正規表現エンジンの開発に取り組んでいくつもりです!