AtCoder Beginner Contest の E 問題で2回続けてダイクストラ法が出題される昨今，いかがお過ごしでしょうか？[^1] その2つの E 問題のうち，先に出題された E - Come Back Quickly はいかにも典型的だなあといった問題なので良いのですが，後に出題された E…

この記事は言語実装 Advent Calendar 2020 の5日目の記事です． 一度でも型推論器を書いたことがあれば，そのあまりの邪悪さ，あるいはその複雑さに恐れ慄いたことでしょう． 参照を用いて単一化を実現しようものなら構文木は参照に汚染され，純粋関数型に実…

今年はそれらしきアドベントカレンダーが無いので，この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます． ML って本を正せば定理証明支援系由来ですし．最後にちょっと OCaml を使ってますし． Coq によって検証された正規表現エンジ…

以前から僕は単相の型推論アルゴリズムの健全性や完全性をCoqで検証していたのですが，最近*1let多相をサポートするように型推論器の実装と正当性の証明を修正したので記事にしておきましょう*2． *1:と言っても今年の1月ぐらいですが．本当はAdvent Calenda…

今となっては少々昔のことですが，AtCoder Beginner Contest 167のD問題で数列の循環検出が必要になった事がありました（問題の制約的にはダブリングでも解けますが）． 数列の循環検出はナイーブにに実装すると，循環している部分に至るまでの長さを，循環…

PPL 2019のポスター発表でZ定理[Dehornoy+08]なるものを知ったので，Coqで定式化してみる． それだけでは面白くないので，これを用いて簡約の合流性も証明する．

以前二分探索の正当性をCoqで証明しましたが，この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると，添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした． そこで，依存型を活用して添字の動く範囲も保…

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

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

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

この記事は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さんのリージョンについてでした。

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

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

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

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

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

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

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

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