覚え書き: 先読み・後読みを含む正規表現の数学的定式化

いかにも既知な気がしますが、ぱっと既存の議論が探せないのでとりあえず書き出してみます。

※用語は独自のものです。また、証明・定義は厳密に検証しているわけではないので誤りがあるかもしれません。

この定義でカバーできること

• 先頭 ^
• 末尾 $
• 肯定先読み (?= ... )
• 否定先読み (?! ... )
• 肯定後読み (?<= ... )
• 否定後読み (?<! ... )

この定義でカバーしないこと

• 選択の左右の優先度 (r1|r2 vs. r2|r1)
• 最長優先と最短優先の区別 (r* vs. r*?)

基本の正規表現

基本の正規表現は通常以下のように定義されます。 $Σ\Sigma$ はアルファベットで有限サイズとします。

• 文字リテラル $aa$ ($aa$ は文字 $a∈Σa \in \Sigma$)
• 空文字列 $ϵ\epsilon$ と連接 $R1R2R_1R_2$ ($R1R_1$, $R2R_2$ は正規表現)
• 空集合 $∅\emptyset$ と選択 $R1∣R2R_1 | R_2$ ($R1R_1$, $R2R_2$ は正規表現)
• 繰り返し $R1*R_1\text{*}$ ($R1R_1$ は正規表現)

また具象構文レベルでは演算子のグルーピングのために括弧 $(?:R1)(\text{?:}R_1)$ が使われます。

派生規則 (既存の構文の組み合わせとして書けるルール) として以下のようなものがあります。

• 文字クラス …… 文字リテラルの選択として書ける。
• 回数指定の繰り返し ($R1?R_1\text{?}$, $R1+R_1\text{+}$ など) ... 連接、選択、繰り返しの組み合わせで書ける。
• 空文字列は通常プリミティブに含めるが、空集合の繰り返しとして書けるので省略することも可能。

また、容認規則 (正規表現を分解・再構築する演算として書けるルール) として以下のようなものがあります。

• 否定 ($!R1\text{!}R_1$) …… DFAに翻訳し、受理状態を逆転させてからFloyd-Warshallで正規表現を再構築する。
• 共通部分 ($R1&R2R_1 \text{\&} R_2$) …… NFAに翻訳し、状態集合の直積を作る。両方が受理状態であるときに受理と定義し、Floyd-Warshallで正規表現を再構築する。

基本の正規表現は、ある文字列 ($w∈Σ∗w \in \Sigma^*$) にマッチするかしないかという述語として解釈されます。

文脈つき正規表現

先読みや後読みを解釈するには、文字列の3つ組 $(l,s,r)(l, s, r)$ に対する述語を考えることになります。 $ss$ がマッチした部分で、 $ll$ はその左文脈、 $rr$ は右文脈を意味します。

言い換えると、これは全体文字列 $lsrlsr$ のある範囲 ($ss$) に対してマッチするかどうかを答える述語ということになります。

まず基本の正規表現をこの形に拡張します。

• リテラル: $(l,s,r)=∼a(l, s, r) \mathop{=\sim} a$ ($a∈Σa \in \Sigma$) $⟺ \iff$ $s=as = a$
• 空文字列: $(l,s,r)=∼ϵ(l, s, r) \mathop{=\sim} \epsilon$ $⟺ \iff$ $s=ϵs = \epsilon$
• 連接: $(l,s,r)=∼R1R2(l, s, r) \mathop{=\sim} R_1R_2$ $⟺ \iff$ 次を満たす $s1s_1$, $s2s_2$ が存在: $s=s1s2s = s_1s_2$, $(l,s1,s2r)=∼R1(l, s_1, s_2r) \mathop{=\sim} R_1$ かつ $(ls1,s2,r)=∼R2(ls_1, s_2, r) \mathop{=\sim} R_2$
• 空集合: 常に $(l,s,r)̸=∼∅(l, s, r) \not\mathop{=\sim} \emptyset$
• 選択: $(l,s,r)=∼R1∣R2(l, s, r) \mathop{=\sim} R_1|R_2$ $⟺ \iff$ $(l,s,r)=∼R1(l, s, r) \mathop{=\sim} R_1$ または $(l,s,r)=∼R2(l, s, r) \mathop{=\sim} R_2$
• 繰り返し: $(l,s,r)=∼R1*(l, s, r) \mathop{=\sim} R_1\text{*}$ $⟺ \iff$ 次を満たす $n∈Nn \in \mathbb{N}$ (0を含む) および $s1s_1$, $s2s_2$, ... $sns_n$ が存在: $s=s1s2…sns = s_1s_2\ldots s_n$ かつ、任意の $i∈Ni \in \mathbb{N}$, $1≤i≤n1 \leq i \leq n$ に対して $(ls1s2…si−1,si,si+1si+2…snr)=∼R1(ls_1s_2\ldots s_{i-1}, s_i, s_{i+1}s_{i+2}\ldots s_nr) \mathop{=\sim} R_1$

すると、これらの基本の構成のみからなる正規表現は $ll$, $rr$ に依存せず同じ結果を返すことがすぐに確認できます。これは元々の正規表現の解釈と一致します。

これらを導入したのは、新たにアサーションを含む正規表現の意味論を定義するためでした。これは以下のように定義されます。

• 開始: $(l,s,r)=∼＾(l, s, r) \mathop{=\sim} ＾$ $⟺ \iff$ $l=ϵl = \epsilon$ かつ $s=ϵs = \epsilon$
• 終了: $(l,s,r)=∼＄(l, s, r) \mathop{=\sim} ＄$ $⟺ \iff$ $s=ϵs = \epsilon$ かつ $r=ϵr = \epsilon$
• 肯定先読み: $(l,s,r)=∼(?=R1)(l, s, r) \mathop{=\sim} (\text{?=}R_1)$ $⟺ \iff$ $s=ϵs = \epsilon$ かつ、次を満たす $r1,r2r_1, r_2$ が存在: $r=r1r2r = r_1r_2$ かつ $(l,r1,r2)=∼R1(l, r_1, r_2) \mathop{=\sim} R_1$
• 否定先読み: $(l,s,r)=∼(?!R1)(l, s, r) \mathop{=\sim} (\text{?!}R_1)$ $⟺ \iff$ $s=ϵs = \epsilon$ かつ、任意の $r1,r2r_1, r_2$ に関して、 $r=r1r2r = r_1r_2$ ならば $(l,r1,r2)̸=∼R1(l, r_1, r_2) \not\mathop{=\sim} R_1$
• 肯定後読み: $(l,s,r)=∼(?<=R1)(l, s, r) \mathop{=\sim} (\text{?<=}R_1)$ $⟺ \iff$ $s=ϵs = \epsilon$ かつ、次を満たす $l1,l2l_1, l_2$ が存在: $l=l1l2l = l_1l_2$ かつ $(l1,l2,r)=∼R1(l_1, l_2, r) \mathop{=\sim} R_1$
• 否定後読み: $(l,s,r)=∼(?<=R1)(l, s, r) \mathop{=\sim} (\text{?<=}R_1)$ $⟺ \iff$ $s=ϵs = \epsilon$ かつ、任意の $l1,l2l_1, l_2$ に関して、 $l=l1l2l = l_1l_2$ ならば $(l1,l2,r)̸=∼R1(l_1, l_2, r) \not\mathop{=\sim} R_1$

なお、この中では否定先読みと否定後読みがあれば他のものは再現できます。

• 開始: (?<!.) (. は全ての文字にマッチする正規表現とする)
• 終了: (?!.)
• 肯定先読み: (?!(?! ... ))
• 肯定後読み: (?<!(?<! ... ))

またプログラミングで出てくる正規表現では空集合リテラル $∅\emptyset$ が存在しない場合があり、その場合でもかわりに否定先読みなどを使って (?!) などと書けることが多いです。空集合はれっきとした正規言語であるため、これが書けない場合は理論的には正規表現に期待される表現力を持たないことになります。

その他、行境界 (言語によっては ^ や $ がこの意味になる)、単語境界 (\b, \<, \>) なども上記のアサーションプリミティブの組み合わせで書けます。

正規言語

$Σ∗\Sigma^*$ の部分集合を言語といいますが、ここで一般化した正規表現は $Σ∗×Σ∗×Σ∗\Sigma^* \times \Sigma^* \times \Sigma^*$ の部分集合を定めます。これを文脈つき言語と呼ぶことにします。

正規表現で表される言語は正規言語として様々な方法で特徴づけられるので、文脈つき正規表現で表される文脈つき言語にも特徴づけを考えたくなります。ここでは以下のように定義してみます。

定義1.1 (文脈つき正規言語) $L⊆Σ∗×Σ∗×Σ∗L \subseteq \Sigma^* \times \Sigma^* \times \Sigma^*$ が正規である $⟺ \iff$ $Σ\Sigma$ にない記号 $↓↓$ を用いて、 ${l↓s↓r∣(l,s,r)∈L}\{ l↓s↓r \mid (l, s, r) \in L \}$ として定義した言語が $(Σ∪{↓})∗(\Sigma \cup \{↓\})^*$ の正規言語である

この定義が正規表現側の性質と一致することはあとで確認します。

DFA, NFA

上で正規言語を定義するにあたって $l↓s↓rl↓s↓r$ という文字列にエンコードしました。DFAやNFAに関しても同様に $l↓s↓rl↓s↓r$ を入力にとるオートマトンを考えればいいので話は簡単になります。

ただし、 $l↓s↓rl↓s↓r$ の形式では $↓↓$ という文字は必ずちょうど2回登場するため、以下のように定義を改変したほうが議論が綺麗になります(おそらく)。

• 状態集合を3つに分割し、 $Q=Q0∪Q1∪Q2Q = Q_0 \cup Q_1 \cup Q_2$ ($Q0Q_0$, $Q1Q_1$, $Q2Q_2$ は互いに共通部分を持たない) とする。
• 受理状態は $F⊆Q2F \subseteq Q_2$ に限定する。
• $↓↓$ 以外の文字を入力したときの遷移先は同じ集合にとどまる。 ($QiQ_i$ からは $QiQ_i$ にのみ遷移する)
• $Q0Q_0$ から $↓↓$ を入力したときの遷移先は $Q1Q_1$ に限る。
• $Q1Q_1$ から $↓↓$ を入力したときの遷移先は $Q2Q_2$ に限る。
• $Q2Q_2$ から $↓↓$ を入力したときの遷移は定義しない。

この改良版のDFA・NFAとオリジナルのDFA・NFAには適当な対応関係を考えることができます。ただし、どんなsuffixも受理しない状態の扱いには以下のような注意が必要です。

• オリジナルの定義では、そのような状態があれば $↓↓$ を入力しても自分自身に遷移することが可能だが、改良版では $Q0Q_0$, $Q1Q_1$, $Q2Q_2$ で階層化されているため定義を分ける必要がある。
• オリジナルの定義では、 $↓↓$ が多すぎる文字列の対応のためにそのような状態を残しておく必要があるが、改良版では定義しなくても問題ない。

正規表現からNFAへ

定理1.2 (正規表現の解釈の正規性) 文脈つき正規表現があらわす文脈つき言語は正規である。

証明. 正規表現の構造にそって、対応するε-NFAを構成する。ここでは多数ある場合分けのうちいくつかのみ示す。

連接 $R1R2R_1R_2$ の場合。 $R1R_1$ からε-NFAの状態集合 $Q0Q_0$, $Q1Q_1$, $Q2Q_2$ を、 $R2R_2$ からNFAの状態集合 $Q0′Q'_0$, $Q1′Q'_1$, $Q2′Q'_2$ を得る。これを用いて $R1R2R_1R_2$ に対応するε-NFAの状態集合を以下のように定める。

• 左文脈用の状態
  • $Q0×Q0′Q_0 \times Q'_0$
    • 次のステップへの遷移: $↓↓$ が入力されたら $R1R_1$ のオートマトンに $↓↓$ を入力して遷移する
• マッチ範囲内の状態
  • $Q1×Q0′Q_1 \times Q'_0$
    • 次のステップへの遷移: $ϵ\epsilon$ が入力されたら $R1R_1$, $R2R_2$ の両方のオートマトンに $↓↓$ を入力して遷移する
  • $Q2×Q1′Q_2 \times Q'_1$
    • 次のステップへの遷移: $↓↓$ が入力されたら $R2R_2$ のオートマトンに $↓↓$ を入力して遷移する
• 右文脈用の状態
  • $Q2×Q2′Q_2 \times Q'_2$

選択 $R1∣R2R_1|R_2$ の場合。各々の状態集合の合併をとり、初期状態と受理状態もそれぞれ元のオートマトンの合併とする。

繰り返し $R1*R_1\text{*}$ の場合。 $R1R_1$ からε-NFAの状態集合 $Q0Q_0$, $Q1Q_1$, $Q2Q_2$ を得る。これを用いて $R1*R_1\text{*}$ に対応するε-NFAの状態集合を以下のように定める。このとき、繰り返し部分の状態を保存するために冪集合構成を用いる。

• 左文脈用の状態
  • 状態A: $Q0Q_0$
    • 次のステップへの遷移: $↓↓$ が入力されたら、 $Q0Q_0$ を保存して状態Bに移る。このとき冪集合 $P(Q2)\mathcal{P}(Q_2)$ 部分には $∅\emptyset$ を保存する。
• マッチ範囲内の状態
  • 状態B: $Q0×P(Q2)Q_0 \times \mathcal{P}(Q_2)$ (内部遷移を持たない)
    • 次のステップへの遷移: $ϵ\epsilon$ が入力されたら、元の状態を保存しつつ $↓↓$ を入力した結果も得て状態Cに遷移する。
    • または、状態Dに遷移する。
  • 状態C: $Q0×P(Q2)×Q1Q_0 \times \mathcal{P}(Q_2) \times Q_1$
    • 次のステップへの遷移: $ϵ\epsilon$ が入力されたら、 $Q1Q_1$ 部分に $↓↓$ を入力して $Q2Q_2$ の状態を得、 $P(Q2)\mathcal{P}(Q_2)$ に追加して状態Bに戻る。
  • 状態D: $P(Q2)\mathcal{P}(Q_2)$

肯定先読み $(?=R1)(\text{?=} R_1)$ の場合。 $R1R_1$ からε-NFAの状態集合 $Q0Q_0$, $Q1Q_1$, $Q2Q_2$ を得る。これを用いて $(?=R1)(\text{?=} R_1)$ に対応するε-NFAの状態集合を以下のように定める。

• 左文脈用の状態
  • $Q0Q_0$
    • $↓↓$ が入力されたら、内部のオートマトンにも $↓↓$ を入力して次の状態に遷移する。
• マッチ範囲内の状態
  • $Q1Q_1$ (内部遷移を持たない)
    • $↓↓$ が入力されたら、そのまま次の状態に遷移する。
• 右文脈用の状態
  • $Q1Q_1$
    • $ϵ\epsilon$ が入力されたら、内部のオートマトンに $↓↓$ を入力して次の状態に遷移する。
  • $Q2Q_2$

NFAから正規表現へ

定理 1.3 (正規表現の表現力) 全ての文脈つき正規言語は文脈つき正規表現であらわせる。

証明. NFAの $Q0Q_0$, $Q1Q_1$, $Q2Q_2$ の各状態集合に対してそれぞれFloyd-Warshallを適用して、状態対に対応する正規表現を得る。

始状態, $Q0Q_0$ から $Q1Q_1$, $Q1Q_1$ から $Q2Q_2$ への可能な遷移, 終状態の組み合わせをそれぞれ列挙する。これを $q0∈Sq_0 \in S$, $q0′→q1q'_0 \to q_1$, $q1′→q2q'_1 \to q_2$, $q2′∈Fq'_2 \in F$ とする。このとき $q0q_0$ から $q0′q'_0$, $q1q_1$ から $q1′q'_1$, $q2q_2$ から $q2′q'_2$ に対応する正規表現を $R0R_0$, $R1R_1$, $R2R_2$ とすると $q0q_0$ で始まり $q2′q'_2$ で終わる遷移に対応する言語は $＾(?<=R0)R1(?=R2)＄＾(\text{?<=}R_0)R_1(\text{?=}R_2)＄$ と書ける。これを全ての組み合わせに対し計算して選択で繋ぎ合わせることでNFAが表す言語に対応する正規表現になる。

パーティションに基づいた正規性

ここまでの議論ではカーソルに $↓↓$ という特別な文字を入れることで正規性を定義しました。これは既存の正規言語との関係を考える上ではわかりやすいですが、3つの文字列を独立して扱う議論をする上では便利ではない面もあります。そこで3つの文字列の独立性を高めた定義を考えます。

まず集合の分割の正規性を考えます。

定義1.4 (集合の分割) 集合 $SS$ の分割とは、 $SS$ の部分集合の族 $P⊆P(S)P \subseteq \mathcal{P}(S)$ であって、 $S=⋃V∈PVS = \bigcup_{V \in P} V$ かつ任意の $V,W∈PV, W \in P$ に対して $V∩W≠∅V \cap W \neq \emptyset$ ならば $V=WV = W$ となるもののことである。

定義1.5 (正規な分割) $Σ∗\Sigma^*$ の有限分割 $P⊆P(Σ∗)P \subseteq \mathcal{P}(\Sigma^*)$ が正規であるとは、 $PP$ の各要素が $Σ\Sigma$ 上の正規言語であることである。

すると文脈つき言語の正規性は以下のように言い換えられます。

定理1.6 (パーティションに基づいた正規性) $L⊆Σ∗×Σ∗×Σ∗L \subseteq \Sigma^* \times \Sigma^* \times \Sigma^*$ が正規である $⟺ \iff$ $Σ∗\Sigma^*$ の正規な分割 $P1P_1$, $P2P_2$, $P3P_3$ であって以下を満たすものが存在する: 任意の $V1∈P1V_1 \in P_1$, $V2∈P2V_2 \in P_2$, $V3∈P3V_3 \in P_3$ について、$V1×V2×V3⊆LV_1 \times V_2 \times V_3 \subseteq L$ または $V1×V2×V3⊆Σ∗×Σ∗×Σ∗∖LV_1 \times V_2 \times V_3 \subseteq \Sigma^* \times \Sigma^* \times \Sigma^* \setminus L$ である。

証明. ($⇒\Rightarrow$) $LL$ を $(Σ∪{↓})∗(\Sigma \cup \{↓\})^*$ の言語としてみたときのSyntactic monoid (両側同値類) は有限モノイドになる。そのため、以下の同値類も有限になる。

• $Σ∗/{(l1,l2)∈Σ∗∣∀s,r∈Σ∗. (l1,s,r)∈L⇔(l2,s,r)∈L}\Sigma^* / \{ (l_1, l_2) \in \Sigma^* \mid \forall s, r \in \Sigma^*.\ (l_1, s, r) \in L \Leftrightarrow (l_2, s, r) \in L \}$
• $Σ∗/{(s1,s2)∈Σ∗∣∀l,r∈Σ∗. (l,s1,r)∈L⇔(l,s2,r)∈L}\Sigma^* / \{ (s_1, s_2) \in \Sigma^* \mid \forall l, r \in \Sigma^*.\ (l, s_1, r) \in L \Leftrightarrow (l, s_2, r) \in L \}$
• $Σ∗/{(r1,r2)∈Σ∗∣∀l,s∈Σ∗. (l,s,r1)∈L⇔(l,s,r1)∈L}\Sigma^* / \{ (r_1, r_2) \in \Sigma^* \mid \forall l, s \in \Sigma^*.\ (l, s, r_1) \in L \Leftrightarrow (l, s, r_1) \in L \}$

また、これらの元は全て正規である。 (syntactic monoidの特定の部分集合の引き戻しとして表せるため)

これらを $P1P_1$, $P2P_2$, $P3P_3$ とおくと、所定の性質を満たす。

($⇐\Leftarrow$) $P1P_1$, $P2P_2$, $P3P_3$ が正規な分割であることから、これらに対応するDFA $A1A_1$, $A2A_2$, $A3A_3$ が存在する。これをもとに以下の3種類の状態を持つDFAを作る。

• 第1段階: $A1A_1$ の状態がそのまま入っている。
• 第2段階: $A2A_2$ の状態 $×\times$ $P_1$ だけの状態が入っている。
• 第3段階: $A_3$ の状態 $\times$ $P_1$ \times $P_2$ だけの状態が入っている。

これらの状態を繋ぎ合わせて $↓$ の遷移を適切に定義すると、 $L$ を認識するオートマトンになる。

実際の検索関数との関係

ここで定義したのは、文字列中の始点と終点を指定したときに、それがマッチするかどうかという条件です。

function matchRange(r: RegExp, s: string, start: number, end: number): boolean;

実際の正規表現ライブラリではこの形でAPIが提供されていることは稀で、さらに以下のような構成を経たものが使われます。

1. 始点から終点を決定する処理 (終点を決定しなくてよい)
2. 始点を決定する処理 (始点も決定しなくてよい)

たとえばJavaScriptの場合、1の構成を経たAPIとして「sticky search有効時のexec」があります。これはlastIndexで指定した始点からのみ探索を行うものです。

さらに、2の構成を行ったAPIとしては以下のようなものがあります。

• 通常のexec (一番手前の有効な始点を返す)
• global search有効時のexec (lastIndexで指定した位置以降で、一番手前の有効な始点を返す)
• global searchやsticky searchが有効な場合のmatchAllやreplaceAll (直前の検索結果の終点をもとに、次の始点の制約を決定する)

今回の定式化では、この「始点から終点を決定する処理」を記述するには不十分です。バックトラックベースの正規表現エンジンでは、分岐の優先度に依存して挙動が変わりますが、今回定義したモデルではこの情報を捨ててしまっているからです。たとえば a|ab と ab|a は挙動が違いますし、 a+ と a+? も挙動が違いますが、このことを説明できるモデルになっていません。

また、今回定義したモデルだけでは \0 以外のキャプチャグループの振る舞いも表現できません。このあたりを定義するにはさらなる工夫が必要です。

関連

• 元ツイート
• kinabaさんに教えてもらった論文