以前二分探索の正当性をCoqで証明しましたが,この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると,添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした. そこで,依存型を活用して添字の動く範囲も保証しようと思います.
続きを読むOCaml標準ライブラリのList.sortを読む
この記事はML Advent Calendar 2017の10日目(!?)のために書かれました.
皆さんOCaml標準ライブラリのList.sort
は使っていますか?
頻繁にリストに対してのソートを行うようならデータ構造かアルゴリズムを考え直した方が良いでしょうが,競プロの様にちょっとしたプログラムを書く時には僕もよくお世話になります.
マニュアルによると,そのList.sort
はマージソートで実装されているようですが,僕のような者がちょっとやそっと工夫した程度では敵わないような最適化が施されています.今回はそのソースコードを読んでみましょう.
Coqによる型推論器の形式的検証
この記事は言語実装 Advent Calendar 2017の10日目(!?)のために書かれました. 9日目の記事は@ukitakaさんのSwiftコンパイラで採用されているパターンマッチの網羅性チェックの理論と実装です.
続きを読む最左最外簡約の性質をCoqで証明する
正規形を持つ項は最左最外簡約によってもその正規形に簡約されるのは有名な話. これはかなり嬉しくて,最左最外簡約は値呼びとは何だったのかと言わんばかりの優秀な評価戦略と言えるでしょう.
しかし,この性質は有名な割に定理証明支援系を使った証明を見ない気がします. みんな格好良い型の付いた言語に夢中なんでしょうか?ひとつCoqで証明してみましょう.
続きを読む