fetburner.core

コアダンプ

OCamlで正規表現を微分する

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

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

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

続きを読む

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

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

続きを読む

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

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

続きを読む

ラマヌジャンの公式で円周率を計算する

要旨

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

続きを読む

OCaml標準ライブラリのList.sortを読む

 この記事はML Advent Calendar 2017の10日目(!?)のために書かれました.

 皆さんOCaml標準ライブラリのList.sortは使っていますか? 頻繁にリストに対してのソートを行うようならデータ構造かアルゴリズムを考え直した方が良いでしょうが,競プロの様にちょっとしたプログラムを書く時には僕もよくお世話になります. マニュアルによると,そのList.sortマージソートで実装されているようですが,僕のような者がちょっとやそっと工夫した程度では敵わないような最適化が施されています.今回はそのソースコードを読んでみましょう.

続きを読む

Coqによる型推論器の形式的検証

 この記事は言語実装 Advent Calendar 2017の10日目(!?)のために書かれました. 9日目の記事は@ukitakaさんのSwiftコンパイラで採用されているパターンマッチの網羅性チェックの理論と実装です.

続きを読む

最左最外簡約の性質をCoqで証明する

正規形を持つ項は最左最外簡約によってもその正規形に簡約されるのは有名な話. これはかなり嬉しくて,最左最外簡約は値呼びとは何だったのかと言わんばかりの優秀な評価戦略と言えるでしょう.

しかし,この性質は有名な割に定理証明支援系を使った証明を見ない気がします. みんな格好良い型の付いた言語に夢中なんでしょうか?ひとつCoqで証明してみましょう.

続きを読む