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

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

遥か昔にもOCamlでダイクストラ法を実装したことはあったんですが， 最も近い頂点を線形探索で求めている手抜き実装なので，O(V2)の計算時間を要する（a.k.a. 疎なグラフに対しては遅い）ものでした． 競プロだと入力が疎なグラフに限定されている場面が多々…

要旨 ラマヌジャンの公式$$ \frac{4}{\pi}=\sum_{n=0}^{\infty} \frac{(-1)^n (4n)! (1123+21460n)}{882^{2n+1}(4^n n!)^4} $$を用いて，円周率を計算するプログラムをHaskellで書きました． メモリ8GBのPCで動作させたところ，2000万桁程度まで実用的な速度…