チラシの裏

プログラミングとか色々

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

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

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

続きを読む

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

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

続きを読む

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

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

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

続きを読む

普通の大学院生が【バイク】乗ってみた。あるいはCBR250Rのインプレ

月日は百代の過客にして,行かう年もまた旅人なり. 今年の3月末頃にCBR250Rというバイクを購入して早3ヶ月,様々な土地を放浪して走行距離3000kmに達するまでになりました. 区切りが良いのでこのバイクについて感じたことなどを書き留めておきたいと思います.

続きを読む

αβ法に証明を付ける

最近、オセロのAIを作ろうと思ってOCamlでαβ法を実装したのですが、実装にバグがあって思ったように性能が出ませんでした。 この不具合が厄介で、合法手がちゃんと返っているので実際に対戦させてみないと悪い手を打っている事に気付けないのです。

こんな時はやはりCoqで証明を付けるに限ります。

続きを読む

Term Rewriting and All Thatの練習問題をCoqで解く

この記事はTheorem Prover Advent Calendar 2016の8日目のために書かれました。

8日目の記事がまだ埋まっていないようなので、タイトルの通りTerm Rewriting and All Thatの練習問題で出てきた証明をいくつかCoqでやってみようと思います。

続きを読む

Call-by-needを採用した言語のインタプリタの実装

この記事は言語実装 Advent Calendar 2016の9日目ために書かれました。

最近僕はcall-by-needに関連する研究をしており、気分を理解するためにcall-by-needを採用した言語のインタプリタStandard MLで実装したりしました。今回はその時の事でも記事にしておきましょう。

続きを読む