fetburner.core

コアダンプ

αβ法に証明を付ける

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

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

続きを読む

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

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

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

続きを読む

MinCamlに簡単な最適化を追加する

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

元々僕はStandard MLで一からコンパイラを書こうとしていたんですが、ローレベルあんまり詳しくなくてネイティブコードを生成できるようにするのが面倒だったのと、Standard MLのsyntax sugarがあまりにも無糖だったので辛くなってきました。 いろいろ最適化を実装して楽しみたいだけなのに自作に固執しなくても良い気がしたので、今度はMinCamlに自作のコンパイラで実装していた最適化を導入して遊ぶことにします。

続きを読む

Coqで証明付きのマージソートを書く

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

少し季節外れの記事になりますが、前期はプロ演A[^1]の季節でしたね。
僕のTLでもC言語の課題に苦しめられた学部生のツイートが良く回ってきましたが、 とりわけ彼らが苦戦していたのはマージソートを書く課題のようでした。
面白そうなので僕もCoqで実装してみましょう。 もちろん、証明付きで。

続きを読む

二分探索に証明を付ける

二分探索は言わずと知れた探索アルゴリズムですが、 実際に実装しようとすると無限ループしたり正しい答えが得られなかったりする事も多いのではないでしょうか。

そこで、ここではCoqで二分探索を実装し、正当性の証明を行いました。

続きを読む

OCamlで車輪を再発明する

最近研究でCoqぐらいしか書いてないので、リハビリがてらAtCoderで 開かれるコンテストにOCamlで参加して遊んでます。 僕は個人的な趣味もあってOCamlを使う際は専ら言語処理系を書いていましたが、 競技プログラミングでは全く関係ない題材を扱う必要があるので新鮮な感じですね。

それに伴って有名なアルゴリズムもいくつか実装したので、 ここではそういうアルゴリズムをMLではどう書いたのか紹介したいなと思います。

続きを読む