チラシの裏

プログラミングとか色々

Coq

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

Coq

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

αβ法に証明を付ける

Coq

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

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

Coq

この記事はTheorem Prover Advent Calendar 2016の4日目のために書かれました。 少し季節外れの記事になりますが、前期はプロ演A[^1]の季節でしたね。 僕のTLでもC言語の課題に苦しめられた学部生のツイートが良く回ってきましたが、 とりわけ彼らが苦戦して…

二分探索に証明を付ける

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

型推論の健全性の証明

このエントリはTheorem Prover Advent Calendar 2015と言語実装 Advent Calendar 2015の11日目の記事です。 言語実装 Advent Calendar 2015の10日目の記事はkeenさんのリージョンについてでした。

単一化の証明

Coq

この記事はTheorem Prover Advent Calendar 2015の7日目のために書かれました。 6日目の記事はmathinkさんのCoq で環のイデアルを作ってみるです。

Coqでちょっと複雑なデータ構造を書こうと思ったらハマった

Coq

何となくMinCamlにCoqで証明を付けたいと思い立ったのでOccurrence checkの検証を証明しようと思ったのですが、ちょっとした問題に遭遇したのでメモ。

SMLでソート

この記事はML Advent Calendar 2014 8日目のために書かれました。 多くの言語においてソートは標準ライブラリで提供されていますが、Standard ML Basis Libraryにはソートを行う関数が存在しません。 処理系依存で良ければSML/NJのListMergeSort.sortの様に…

CoqからSMLへ

CoqにはExtractionという機能があり、Coqで書かれたソースコードから対応する他の言語のソースコードを出力する事ができます。今回はそのExtractionをStandard MLに対応させた事について書こうと思います。

簡単な式の評価器を証明駆動開発

EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。 *…

EvalML2における評価の一意性の証明

前回、前々回は四則演算程度しか持たない導出システムについての証明でしたが、今回は変数束縛や環境を持つ導出システム、EvalML2における評価の一意性を証明しようと思います。例によって元ネタはプログラミング言語の基礎概念です。

EvalML1Errにおける評価の全域性の証明

前回はプログラミング言語の基礎概念に出てくるEvalML1についての定理を証明したので、ついでに実行時エラーも扱うEvalML1Errにおける評価の一意性を証明したいと思います。

EvalML1における評価の一意性の証明

Coqの練習にプログラミング言語の基礎概念に出てくる、EvalML1における評価の一意性について証明したので公開したいと思います。