fetburner.core

コアダンプ

let多相を扱える型推論器をCoqで検証する

以前から僕は単相の型推論アルゴリズム健全性完全性をCoqで検証していたのですが,最近*1let多相をサポートするように型推論器の実装と正当性の証明を修正したので記事にしておきましょう*2

*1:と言っても今年の1月ぐらいですが.本当はAdvent Calendarに間に合わせたかったんですが,間に合わなかったんですよね.

*2:健全性の検証についての記事を書いたのが2015年ですから,随分間が空いてしまいました.いくつになってもこんなことばかりやってるな…

続きを読む

Coqでフロイドの循環検出法を検証する

今となっては少々昔のことですが,AtCoder Beginner Contest 167のD問題で数列の循環検出が必要になった事がありました(問題の制約的にはダブリングでも解けますが).

数列の循環検出はナイーブにに実装すると,循環している部分に至るまでの長さを\mu,循環の長さを\lambdaとするとO(\mu+\lambda)のメモリが必要になってしまいますが,これをO(1)で計算するアルゴリズムとして,フロイドの循環検出法が知られています. 中々巧妙なアルゴリズムなもので,これを実装して本当に循環検出ができているのか少々不安に思うところもありますし,この際Coqで正当性を保証してやりましょう.

続きを読む

OCamlで色々列挙する

AtCoder Beginner ContestのC問題で全探索が出題されがちな今日この頃,いかがお過ごしでしょうか? C++で競プロをやってる人達は重複順列に対して全探索して解を得たい時なんかに,いちいち重複順列を列挙する処理も含んだ再帰関数を書き直してるらしいですが,我々からすれば重複順列を列挙する処理を切り出して使い回せるようにしたいと考えるのが自然ではないでしょうか.

本記事では順列,組み合わせ,重複順列,重複組合せについて,十分速い時間で全列挙できる関数をOCamlで実装します.

続きを読む

OCamlでのダイクストラ法の実装を改良する

OCamlAtCoderの問題を解くのに昔書いたダイクストラ法の実装を使っていたんですが, どうも定数倍でTLEすることが多く,もどかしい気持ちになることもしばしばでした. 本記事では行儀の良いスタイルに囚われず以前の実装に定数倍高速化を施し,実際のコンテストでの使用に堪える実装を得ることを目標とします.

続きを読む

交差型を持つ単純型付きλ計算の型付け可能性について

これは型 Advent Calendar 2019 15日目の記事です. 交差型についてのよく知られた事実——交差型を持つ単純型付きλ計算において,強正規化する項は型付け可能であることを解説します.

続きを読む

CoqによるZ定理(及び,β簡約の合流性)の証明

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

続きを読む

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するのも遠慮しておこうかなと

続きを読む