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するのも遠慮しておこうかなと
OCaml標準ライブラリのList.sortを読む
この記事はML Advent Calendar 2017の10日目(!?)のために書かれました.
皆さんOCaml標準ライブラリのList.sort
は使っていますか?
頻繁にリストに対してのソートを行うようならデータ構造かアルゴリズムを考え直した方が良いでしょうが,競プロの様にちょっとしたプログラムを書く時には僕もよくお世話になります.
マニュアルによると,そのList.sort
はマージソートで実装されているようですが,僕のような者がちょっとやそっと工夫した程度では敵わないような最適化が施されています.今回はそのソースコードを読んでみましょう.
Coqによる型推論器の形式的検証
この記事は言語実装 Advent Calendar 2017の10日目(!?)のために書かれました. 9日目の記事は@ukitakaさんのSwiftコンパイラで採用されているパターンマッチの網羅性チェックの理論と実装です.
続きを読む