OCamlで色々列挙する

AtCoder Beginner ContestのC問題で全探索が出題されがちな今日この頃，いかがお過ごしでしょうか？ C++で競プロをやってる人達は重複順列に対して全探索して解を得たい時なんかに，いちいち重複順列を列挙する処理も含んだ再帰関数を書き直してるらしいですが，我々からすれば重複順列を列挙する処理を切り出して使い回せるようにしたいと考えるのが自然ではないでしょうか．

本記事では順列，組み合わせ，重複順列，重複組合せについて，十分速い時間で全列挙できる関数をOCamlで実装します．

OCamlでのダイクストラ法の実装を改良する

OCamlでAtCoderの問題を解くのに昔書いたダイクストラ法の実装を使っていたんですが， どうも定数倍でTLEすることが多く，もどかしい気持ちになることもしばしばでした． 本記事では行儀の良いスタイルに囚われず以前の実装に定数倍高速化を施し，実際のコンテストでの使用に堪える実装を得ることを目標とします．

交差型を持つ単純型付きλ計算の型付け可能性について

これは型 Advent Calendar 2019 15日目の記事です． 交差型についてのよく知られた事実——交差型を持つ単純型付きλ計算において，強正規化する項は型付け可能であることを解説します．

CoqによるZ定理（及び，β簡約の合流性）の証明

PPL 2019のポスター発表でZ定理[Dehornoy+08]なるものを知ったので，Coqで定式化してみる． それだけでは面白くないので，これを用いて簡約の合流性も証明する．

OCamlで正規表現を微分する

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

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

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

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

もっと二分探索に証明を付ける

以前二分探索の正当性をCoqで証明しましたが，この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると，添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした． そこで，依存型を活用して添字の動く範囲も保証しようと思います．

OCamlでまともなダイクストラ法を実装する

遥か昔にもOCamlでダイクストラ法を実装したことはあったんですが， 最も近い頂点を線形探索で求めている手抜き実装なので，O(V²)の計算時間を要する（a.k.a. 疎なグラフに対しては遅い）ものでした． 競プロだと入力が疎なグラフに限定されている場面が多々あって[^1]， それを前提に制限時間が決まっているので結構つらいです． 破壊的代入を濫用しているのも気になってましたし，純粋関数型かつ疎なグラフに対して高速な実装を与えます．