閏年を判定する正規表現を構築し、その完全性を理論的に検証 

入力された文字列を十進数とみなしたときにそれが（グレゴリオ暦のルールでの）閏年かどうか判定する。

```text:閏年を判定する正規表現（完全一致）
[0-9]*((0[48]|[2468][048]|[13579][26])(00)?|0000)|[048]?(00)?
```

部分一致のツールで使うときは、全体を `\A(...)\z` か `^(...)$` というように囲む。

```bash
PATTERN='^([0-9]*((0[48]|[2468][048]|[13579][26])(00)?|0000)|[048]?(00)?)$'
seq 2001 2400 | grep -c -E "${PATTERN}"   #=> 97   # 閏年が400年に97回あることと整合的
```

## 正規表現の構築過程
かなり場当たり的。

* 倍数を表す
	* 4の倍数を表現：末尾2桁で判別 → `[0-9]*([02468][048]|[13579][26])`
	* 100の倍数を除去：末尾が00となる場合を除去 → `[0-9]*(0[48]|[2468][048]|[13579][26])`
	* 400の倍数を追加：4の倍数から00を続けてもいい → **`[0-9]*(0[48]|[2468][048]|[13579][26])(00)?`**
* 取りこぼしを集める
	* 100の倍数に00が続く数、つまり1万の倍数（例：10000） → **`[0-9]*0000`**
	* 0～1桁な4の倍数（空文字列, 0, 4, 8）と、それに00をつけた400の倍数 → **`[048]?(00)?`**
* 正規表現をまとめる
	* 太字で書いた3つの正規表現を `|` で合成
	* 共通しているパーツは括弧で括り出し（ `[0-9]*` または `(00)?` のどちらか）

最初に作ったときは、取りこぼしのことに全く気付いていなかった。（2001～2400に出てこないから）

## 正規表現の検証
他に取りこぼしが無いか、あるいは逆に閏年でない数にマッチしていないか、というのの自信が持てない。いくら大量の文字列に対して実験しても、思いつかなかったパターンがあるかもしれない。

そこで、**作成した正規表現を決定性有限オートマトン（DFA）に変換して、[他の考え方で作成したDFA](9aba98909b209f3bb966)[^ref-dfa]と一致するか調べる**。以下のDFAと同型になればいい。

![dfa_leap_year_simple.png](https://qiita-image-store.s3.amazonaws.com/0/127130/fe1f0f19-eafb-fc15-622f-19e3662fdcfd.png)

※全ての矢印を描くと見づらくなるため、一部は右の括弧内に括り出した。

状態遷移表だと以下の通り。それぞれの状態についての情報を1行に書いてあり、入力された文字に応じて次の状態が何か（上図の矢印の行き先）、入力が終わったときにその文字列がマッチしたと判定されるのか（上図の二重丸）がわかる。なお、初期状態は常にひとつなので表で一番上に置いて表すこととした。

| 状態 | 終 | | `0` | `[48]` | `[26]` | `[13579]` |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|
|   **0** | ○ | |   0 |   0 |   2 |   1 |
|   **1** |   | |  10 |   2 |   0 |   1 |
|   **2** |   | |  20 |   0 |   2 |   1 |
|  **10** |   | | 100 |   0 |   2 |   1 |
|  **20** | ○ | | 200 |   0 |   2 |   1 |
| **100** |   | | 200 |   0 |   2 |   1 |
| **200** |   | |   0 |   0 |   2 |   1 |

[^ref-dfa]: 「入力された数を400で割った余り」によって閏年判定するように作ったもの。

### （参考）正規表現の可視化
正規表現がグラフとして表せるというのはピンとこないが、[**Regexper**というサービスで試す](https://regexper.com/#%5B0-9%5D*%28%280%5B48%5D%7C%5B2468%5D%5B048%5D%7C%5B13579%5D%5B26%5D%29%2800%29%3F%7C0000%29%7C%5B048%5D%3F%2800%29%3F)とイメージがつきやすい。

![regexper.png](https://qiita-image-store.s3.amazonaws.com/0/127130/4b1b991c-7926-9edf-bf3f-c837a0720295.png)

* 表示された図で左端から右端へ自由な経路をたどり、途中で指示通りに文字を拾っていけば、元の正規表現にマッチする文字列が完成する。
* 逆に、適当な文字列を用意して、指示通りに文字を消費させながら左端から右端へ行ける経路を見つけられれば、その文字列は元の正規表現にマッチすると判定できる。

図を部分的に見てみると、例えば「One of "0"-"9"」というところ付近には何度も繰り返せる経路とスキップできる経路がある。これは正規表現の一部 `[0-9]*` が0回以上の繰り返しを表すことと対応している。他にも `|` はルート分岐、 `?` はスキップ可、というふうに正規表現の基本構文はグラフでの表し方が決まっている。

### ε-NFAへの変換

```text:閏年を判定する正規表現（再掲、目盛つき）
 [0-9]*((0[48]|[2468][048]|[13579][26])(00)?|0000)|[048]?(00)?
/\        /\        /\        /\        /\        /\        /\
 0        10        20        30        40        50        60
```

先に答えを描いてしまうと、上の正規表現は以下の**ε動作付き非決定性有限オートマトン**（ε-NFA）で表せる。

![nfa_leap_year.png](https://qiita-image-store.s3.amazonaws.com/0/127130/7cca19c0-34ff-816b-1195-9a3f0e75fff4.png)

前節のRegexperは経路に注目していたが、有限オートマトンでは文字を読み込む毎の「状態」を意識する（今回、状態の名前には「正規表現文字列の位置」を割り当てた）。表し方は微妙に異なるものの、正規表現の `*` に対応するループや `|` に対応する分岐ができている。

「非決定性」というのは、入力した文字に対する行き先がひとつとは限らない（分岐も行き止まりもありうる）ということ。これは一種の**迷路**のようなものになる。入力された文字列に従い迷路を進んでいって、ちょうど最終状態でゴールする経路がひとつでもあれば、その文字列はNFAにマッチすると判定される[^sugoroku]。

状態遷移を指示する矢印には、文字 `0-9` に加えて `ε` というのが使われている。 `ε` は空文字列 `""` を表す記号で、これが書かれた遷移（ε遷移）は文字を読み込まずに移動していい。例えばε遷移だけで 0 → 56 → 61 とスタートからゴールに進めるので、空文字列はこのNFAにマッチする。

状態遷移表で書くと、DFAと異なり行き先がひとつと限らなくなったため、遷移先の候補を集合で表す。また、普通の文字に加えてε遷移による遷移先も示すことになる。

| 状態 | 終 | | `0` | `[48]` | `[26]` | `[13579]` | ε |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|:---:|
|  **0** | | | {56} | {56} | {} | {} | {0',56} |
| **0'** | | | {0'} | {0'} | {0'} | {0'} | {6} |
|  **6** | | | {9,45} | {20} | {20} | {33} | {} |
|  **9** | | | {} | {38} | {} | {} | {} |
| **20** | | | {38} | {38} | {} | {} | {} |
| **33** | | | {} | {} | {38} | {} | {} |
| **38** | | | {40} | {} | {} | {} | {61} |
| **40** | | | {61} | {} | {} | {} | {} |
| **45** | | | {46} | {} | {} | {} | {} |
| **46** | | | {47} | {} | {} | {} | {} |
| **47** | | | {61} | {} | {} | {} | {} |
| **56** | | | {58} | {} | {} | {} | {61} |
| **58** | | | {61} | {} | {} | {} | {} |
| **61** | ○ | | {} | {} | {} | {} | {} |

---

ちなみに、図や表から予想がつくが、いくつかの状態は区別する必要が無くまとめられる（0'=6, 9=45, 38=56, 40=47=58）[^rule]。手作業で進める場合は今のうちに状態を減らしておくと後々楽。

また、次節～次々節で考えるのが楽になるよう、現在の初期状態 0 へε遷移するだけの便宜的な初期状態 # を作っておく。

![nfa_leap_year_mod.png](https://qiita-image-store.s3.amazonaws.com/0/127130/5ea5e389-95b4-483a-37f0-95791c380bd4.png)

| 状態 | 終 | | `0` | `[48]` | `[26]` | `[13579]` | ε |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|:---:|
|  **#** | | |  |  |  |  | {0} |
|  **0** | | | {38} | {38} | {} | {} | {0',38} |
| **0'** | | | {0',9} | {0',20} | {0',20} | {0',33} | {} |
|  **9** | | | {46} | {38} | {} | {} | {} |
| **20** | | | {38} | {38} | {} | {} | {} |
| **33** | | | {} | {} | {38} | {} | {} |
| **38** | | | {40} | {} | {} | {} | {61} |
| **40** | | | {61} | {} | {} | {} | {} |
| **46** | | | {40} | {} | {} | {} | {} |
| **61** | ○ | | {} | {} | {} | {} | {} |

[^sugoroku]: 単なる迷路より、「双六の[桃鉄](https://www.konami.com/games/momotetsu/)で30マス移動して目的地に到着できるか」みたいなイメージの方が近いかもしれない。
[^rule]: 簡単に言えば「ε遷移で双方向に移動してもNFAのマッチに影響しない状態同士はまとめられる」。例えば、ε遷移 6→0' は追加しても問題ないので双方向になりまとめられるが、 0'→0 は追加すると `[0-9]*[048]?(00)?` にマッチしてしまうのでダメ。

### ε遷移の除去
ε遷移は文字を読み込まずに進めるため、1文字読んだだけで何状態も進んだり最悪無限ループにはまったりしてしまう。その辺に気を付けられるのならこの節は飛ばしても構わないのだが、かなり頭が混乱するため、事前にε遷移の除去をしておく。

ε遷移のひとつに 38 → {61} というのがあった。これはつまり、例えば 0 → {0',38} という遷移ではさらに {61} にも進めることを意味し、結果として 0 → {0',38,61} と書き直せる。このようにして、あるε遷移を他の遷移に取り込んでしまえば、もうそのε遷移を書く必要は無くなる。全て除去後の状態遷移表は以下の通り。（※特別な初期状態 # からのε遷移だけは残しておく）

| 状態 | 終 | | `0` | `[48]` | `[26]` | `[13579]` | ε |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|:---:|
|  **#** | | |  |  |  |  | {0, 0',38, 61} |
|  **0** | | | {38, 61} | {38, 61} | {} | {} |
| **0'** | | | {0',9} | {0',20} | {0',20} | {0',33} |
|  **9** | | | {46} | {38, 61} | {} | {} |
| **20** | | | {38, 61} | {38, 61} | {} | {} |
| **33** | | | {} | {} | {38, 61} | {} |
| **38** | | | {40} | {} | {} | {} |
| **40** | | | {61} | {} | {} | {} |
| **46** | | | {40} | {} | {} | {} |
| **61** | ○ | | {} | {} | {} | {} |

ちなみにε遷移の消し方には、今回と逆に「ε遷移先の状態の情報を現在の状態に取り込む」方法もある。それなら # という変な状態を使わずに真のNFAを構築できる。一方で次節でのNFA探索時に、その動作が元のε-NFAと異なるため理解しにくいという問題がある。

### DFAへの変換
NFAは一種の迷路とみなせるので迷路の解き方が参考になる。迷路を解く単純な方法には主に深さ優先探索と幅優先探索があるが、DFAへの変換にはこの**幅優先探索**のような考え方を使う[^depth]。

ある状態から1文字の入力で次の状態に移るとき、可能な全ての分岐に対して分身を割り当てることで並行して迷路を進んでいく。分身全員をまとめた現在位置は、NFAの状態の集合として表せる。全ての文字列を読み終わったときに、分身のだれかひとりでもゴールに立っていれば、その文字列はNFAにマッチしたことが言える。

閏年判定NFAで具体的に考えていく。初期状態はNFAとしては # のみだが、そこからε遷移によって移動できる {0,0',38,61} という状態集合を実際のスタート地点にする[^nfa-start]。スタート地点から `0` を入力して遷移できるところは、状態集合の和として求まり {38,61} ∪ {0',9} ∪ {40} ∪ {} = {0',9,38,40,61} である（事前にε遷移を除去したため、ε-NFAでの {61} へも移動できることがすぐにわかる）。他の入力文字も考えつつ繰り返すといつかは状態集合が出尽くして、以下のような状態遷移表になる。この場合の最終状態は、集合の中にNFAでの最終状態（今回は {61} ）を1つでも含んでいるかどうかである。

| 状態集合 | 終 | | `0` | `[48]` | `[26]` | `[13579]` |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|
| **{0,0',38,61}**    | ○ | | {0',9,38,40,61} | {0',20,38,61} | {0',20} | {0',33} |
| **{0',9,38,40,61}** | ○ | | {0',9,40,46,61} | {0',20,38,61} | {0',20} | {0',33} |
| **{0',20,38,61}**   | ○ | | {0',9,38,40,61} | {0',20,38,61} | {0',20} | {0',33} |
| **{0',20}**         |   | | {0',9,38,61}    | {0',20,38,61} | {0',20} | {0',33} |
| **{0',33}**         |   | | {0',9}          | {0',20} | {0',20,38,61} | {0',33} |
| **{0',9,40,46,61}** | ○ | | {0',9,40,46,61} | {0',20,38,61} | {0',20} | {0',33} |
| **{0',9,38,61}**    | ○ | | {0',9,40,46}    | {0',20,38,61} | {0',20} | {0',33} |
| **{0',9}**          |   | | {0',9,46}       | {0',20,38,61} | {0',20} | {0',33} |
| **{0',9,40,46}**    |   | | {0',9,40,46,61} | {0',20,38,61} | {0',20} | {0',33} |
| **{0',9,46}**       |   | | {0',9,40,46}    | {0',20,38,61} | {0',20} | {0',33} |

それぞれの状態集合を新しい状態とみなせば、各状態において入力に対する遷移が1つに決まっているので、DFAとなっている。集合のままだと見づらいので別の名前に変えておく。

| 状態 | 終 | | `0` | `[48]` | `[26]` | `[13579]` |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|
| **A** | ○ | | B | C | D | E |
| **B** | ○ | | F | C | D | E |
| **C** | ○ | | B | C | D | E |
| **D** |   | | G | C | D | E |
| **E** |   | | H | D | C | E |
| **F** | ○ | | F | C | D | E |
| **G** | ○ | | I | C | D | E |
| **H** |   | | J | C | D | E |
| **I** |   | | F | C | D | E |
| **J** |   | | I | C | D | E |

[^depth]: 深さ優先探索を正規表現（→ε-NFA）に適用する方法もある。正規表現の動作説明に出てくる[バックトラッキング](https://ja.wikipedia.org/wiki/バックトラッキング)とは、元々は深さ優先探索で使う一般的な手法。
[^nfa-start]: 元のε-NFAで言えば、初期状態 0 からε遷移のみで到達できる状態の集合。

### 状態数の最小化
できあがったDFAは10状態あり、どう見ても答えのDFAと違う。しかし文字列の判定まで違うと決めつけるのは早計で、正しく比較するにはDFAの状態数を最小化する必要がある。（ε-NFAの構築時にズルしたのと同じく）DFAの状態には互いに区別する必要のないものが含まれていることがあり、それは比較の邪魔となる。

この程度のDFAなら同じ状態を見つけるのは簡単だが、一見違う状態が同じということもある。そのため逆に考えて、互いに区別できる状態を見つけ出していき、最後まで区別できなかったものを同じ状態と判定する。手作業で進めるなら状態の組合せ表を書いて印をつけていく。

まず区別できるのは「最終状態かそうでないか」。 {A,B,C,F,G} と {D,E,H,I,J} の交わるマス全てに仮の印をつける。

![minimize_table_1.png](https://qiita-image-store.s3.amazonaws.com/0/127130/fe76d4a3-139b-6d2b-2c18-099be951b58a.png)

ここからは仮の印を頼りに区別を進める。仮の印がついた状態の組をひとつ選び、「同じ文字で遷移してその組の状態が別れる」状態も区別できる。全ての文字で調べたらチェック完了の印に変える。具体的に進めてみると、

0. C x D を選ぶと、文字 `[48]` のときに {E以外} と {E} 、 `[26]` のときに {E} と {E以外} が区別できる
0. F x I を選ぶと、文字 `0` のときに {B,F,I} と {G,J} が区別できる
0. B x I を選ぶと、文字 `0` のときに {A,C} と {G,J} が区別できる

![minimize_table_2.png](https://qiita-image-store.s3.amazonaws.com/0/127130/97a9c825-1d31-347d-1861-b8720d507c10.png)

これを続けていくと全てチェック完了し、一部だけ空白のままになる。空白マスの表す状態の組合せは互いに区別できないことが確定する。

![minimize_table_3.png](https://qiita-image-store.s3.amazonaws.com/0/127130/27818947-8711-faf1-c85b-1e1477f9bdc1.png)

最終的に A=B=C=F ということが分かったので、状態遷移表を書き直す。

| 状態 | 終 | | `0` | `[48]` | `[26]` | `[13579]` |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|
| **A** | ○ | | A | A | D | E |
| **D** |   | | G | A | D | E |
| **E** |   | | H | D | A | E |
| **G** | ○ | | I | A | D | E |
| **H** |   | | J | A | D | E |
| **I** |   | | A | A | D | E |
| **J** |   | | I | A | D | E |

参考までに比較対象のDFAの表を以下に再掲する。とても似ている気がする。

| 状態 | 終 | | `0` | `[48]` | `[26]` | `[13579]` |
|:---:|:-:|:-:|:---:|:---:|:---:|:---:|
|   **0** | ○ | |   0 |   0 |   2 |   1 |
|   **1** |   | |  10 |   2 |   0 |   1 |
|   **2** |   | |  20 |   0 |   2 |   1 |
|  **10** |   | | 100 |   0 |   2 |   1 |
|  **20** | ○ | | 200 |   0 |   2 |   1 |
| **100** |   | | 200 |   0 |   2 |   1 |
| **200** |   | |   0 |   0 |   2 |   1 |

### 最小DFAの比較
正規表現から変換していってできあがった最小DFAは、答えのDFAとかなり似ている。しかし状態の名前が異なるので、完全に同じ形かはまだ分からない。そこで状態が矛盾なく対応づくか調べていく。

* 初期状態はひとつだけなので、対応付けの起点となる： A ⇔ 0
* 初期状態から1文字読み込んでの遷移を考える（Aと0の行を見る）と、 `0` : A ⇔ 0 / `[48]` : A ⇔ 0 / `[26]` : D ⇔ 2 / `[13579]` : E ⇔ 1 となる。 A, D, E がわかり、まだ矛盾は出ていない。
* さらに遷移を繰り返して、 G ⇔ 20, H ⇔ 10, I ⇔ 200, J ⇔ 100 も矛盾なく定まる。
* 最終状態の集合は {A,G} ⇔ {0,20} で、ここも矛盾は無い。

よって2つのDFAは完全に一致する。

---

以上より、冒頭の正規表現は正確に閏年を判定している。 ∎

※あくまで「入力文字列を十進数とみなしたとき」などの条件をおいたときの判定であり、条件が変われば正しい正規表現も変わる。また、正規表現は色々な表し方ができるため、同じ判定ができるもっと短いパターンも作れるかもしれない。