効率的な正規表現エンジンを Coq で検証する - fetburner.core今年はそれらしきアドベントカレンダーが無いので，この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます． ML って本を正せば定理証明支援系由来ですし．最後にちょっと OCaml を使ってますし． Coq によって検証された正規表現エンジンは既に存在していて，探せば他にもいくつもあると思うのですが， それらの実装は主として検証の簡単さに重きが置かれており，OCaml のコードを extract して使ってみると実用に堪えないものが多いように思います． 本記事では，以前 OCaml で書いた効率的な実装を Coq に移植して検証します． 加えて，extract によって OCaml のコードを再び生成し， AtCoder の問題に投げてみても TLE にならないことを確認します． 本記事で実装する正規表現エンジンと，その正当性の証明は GitHub に存在します．
