fetburner.core

コアダンプ

ダイクストラ法の一般化と,その正当性の Coq を用いた検証

 AtCoder Beginner Contest の E 問題で2回続けてダイクストラ法が出題される昨今,いかがお過ごしでしょうか?[^1]

 その2つの E 問題のうち,先に出題された E - Come Back Quickly はいかにも典型的だなあといった問題なので良いのですが,後に出題された E - Train は一筋縄ではいかないものでした.典型的な最短経路問題は辺の長さが定数であるようなグラフを対象としていますが,その問題では辺の長さが,その辺に辿り着くまでの経路長に依存するようなグラフに対してダイクストラ法を適用するのが想定解だったからです.

 本記事では,頂点uに辿り着くまでの経路長 c に頂点 u から頂点 v に伸びる辺の長さを加えたものが関数 d_{uv}(c) として与えられた際に,d_{uv}(c) が単調増加関数かつ  {c \leq d_{uv}(c)} を満たせばダイクストラ法が最短経路を返すことを解説します.加えて,ナイーブな実装ではありますが,そのようなグラフに対してのダイクストラ法が最短距離を返すことを Coq で証明します.

続きを読む

List.fold_right で List.fold_left を書く

 この記事は ML Advent Calendar 2020 の14日目の記事です.

 リストの Church encoding と言えば List.fold_right で表現することが多いように思いますが,果たして List.fold_right だけしか使わずに様々なリストについての再帰関数を表現できるのか疑問に思う人も多いのではないでしょうか? 本記事では,List.fold_right を用いて List.fold_left を実装する方法を紹介します.後者は末尾再帰なのでわざわざ回りくどいことをせずに直接使った方が良いのはもっともなのですが,foldr/build なんかを考える時に頭の片隅にあると便利かもしれません.

続きを読む

Deforestation で強連結成分分解を改善する

 この記事は ML Advent Calendar 2020 の10日目の記事です.

 本記事では,強連結成分分解を行うアルゴリズムの一種である Kosaraju のアルゴリズムに対して deforestation を施し,トポロジカルソートの結果をリストとして保持することなく計算できることを観察します.

12/11 Kosaraju のアルゴリズムを勘違いしていたので実装を修正しました.根本的な勘違いのせいで TaPL 27章みたいな事になっており,厳しい…

続きを読む

ML のサブセットの型推論器を Coq で検証する

 この記事は言語実装 Advent Calendar 2020 の5日目の記事です.

 一度でも型推論器を書いたことがあれば,そのあまりの邪悪さ,あるいはその複雑さに恐れ慄いたことでしょう. 参照を用いて単一化を実現しようものなら構文木は参照に汚染され,純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる. これは Hindley-Milner 型推論器を実装する上での宿命のようなものです.

 本記事では,MLのサブセット——型付きλ計算をletと参照で拡張した,let多相をサポートする言語——の型推論器を Coq で実装し,その正当性を証明します. Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され,枕を高くして眠ることができることでしょう. もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証明していて, あとは対象言語を参照で拡張するだけという話もありますが.

続きを読む

効率的な正規表現エンジンを Coq で検証する

 今年はそれらしきアドベントカレンダーが無いので,この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます. ML って本を正せば定理証明支援系由来ですし.最後にちょっと OCaml を使ってますし.

 Coq によって検証された正規表現エンジンは既に存在していて,探せば他にもいくつもあると思うのですが, それらの実装は主として検証の簡単さに重きが置かれており,OCaml のコードを extract して使ってみると実用に堪えないものが多いように思います. 本記事では,以前 OCaml で書いた効率的な実装を Coq に移植して検証します. 加えて,extract によって OCaml のコードを再び生成し, AtCoder の問題に投げてみても TLE にならないことを確認します.

続きを読む

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で正当性を保証してやりましょう.

続きを読む