fetburner.core

コアダンプ

江戸の電話を長崎で取る

初めは音声信号に乗せたパケットを電話網で伝送してインターネットに接続していた筈が、いつしかUDPパケットに音声信号を乗せてIP網で伝送するようになり、当初は文字通り可搬式の電話だった携帯電話も情報端末として使う事の方が多くなってしまった昨今です…

NECのVPNルータをひかりTVに対応させる

前回の記事では実家のネットワークにNECのVPN対応ルータであるIX2215を導入しましたが、その際ひかりTVの対応に少し手間取ったのでメモがてら記事に残しておきます。 もっとも、本記事での設定は公式資料に裏打ちされたものではなく実機の挙動を基にしている…

NECのVPN対応ルータで自宅と実家の間にVPNを張った話

自宅サーバは一台あるだけで人生に彩りを与えてくれる素晴らしいものですが、帰省などで暫く家を留守にしていると、外出先からアクセスしたくなるもののインターネットに公開するのはセキュリティ的に怖い、といったジレンマが頭を擡げてきます。お正月の特…

どこのご家庭にもあるNASにPi-holeを導入して、ネットワーク側で広告を非表示にした話

例えば死、戦争、飢餓、この世には無くなった方が幸せになれるものが沢山存在しているが、Web広告もその一つだろう。 流石に死だとか戦争だとかは厳しいかもしれないが、広告に関してはネットワーク技術の力で消し去ることができる。 本記事では、我が家で常…

Synology DS920+を使って外付け光学ドライブをネットワークに共有する

光学ディスクの重要性が低下し、巷で売られているPCに読み取り用のドライブが標準搭載されなくなって久しくなりましたが、それでもCDの類を読み込みたくなる機会は度々訪れます。今ほどダウンロード販売が盛んではなかった頃に買ったソフトウェアのインスト…

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

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

List.fold_right で List.fold_left を書く

この記事は ML Advent Calendar 2020 の14日目の記事です. リストの Church encoding と言えば List.fold_right で表現することが多いように思いますが,果たして List.fold_right だけしか使わずに様々なリストについての再帰関数を表現できるのか疑問に思…

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

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

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

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

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

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

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

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

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

Coq

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

OCamlで色々列挙する

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

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

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

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

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

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

Coq

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

OCamlで正規表現を微分する

僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが,Brzozowski derivativeに基づいて正規表現エンジンを実装し,あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです. 折角practicalなプログ…

もっと二分探索に証明を付ける

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

OCamlでまともなダイクストラ法を実装する

遥か昔にもOCamlでダイクストラ法を実装したことはあったんですが, 最も近い頂点を線形探索で求めている手抜き実装なので,O(V2)の計算時間を要する(a.k.a. 疎なグラフに対しては遅い)ものでした. 競プロだと入力が疎なグラフに限定されている場面が多々…

ラマヌジャンの公式で円周率を計算する

要旨 ラマヌジャンの公式$$ \frac{4}{\pi}=\sum_{n=0}^{\infty} \frac{(-1)^n (4n)! (1123+21460n)}{882^{2n+1}(4^n n!)^4} $$を用いて,円周率を計算するプログラムをHaskellで書きました. メモリ8GBのPCで動作させたところ,2000万桁程度まで実用的な速度…

OCaml標準ライブラリのList.sortを読む

この記事はML Advent Calendar 2017の10日目(!?)のために書かれました. 皆さんOCaml標準ライブラリのList.sortは使っていますか? 頻繁にリストに対してのソートを行うようならデータ構造かアルゴリズムを考え直した方が良いでしょうが,競プロの様にち…

Coqによる型推論器の形式的検証

Coq

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

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

Coq

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

αβ法に証明を付ける

Coq

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

Term Rewriting and All Thatの練習問題をCoqで解く

この記事はTheorem Prover Advent Calendar 2016の8日目のために書かれました。 8日目の記事がまだ埋まっていないようなので、タイトルの通りTerm Rewriting and All Thatの練習問題で出てきた証明をいくつかCoqでやってみようと思います。

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

SML

この記事は言語実装 Advent Calendar 2016の9日目ために書かれました。 最近僕はcall-by-needに関連する研究をしており、気分を理解するためにcall-by-needを採用した言語のインタプリタをStandard MLで実装したりしました。今回はその時の事でも記事にして…

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

この記事は言語実装 Advent Calendar 2016のために書かれました。 元々僕はStandard MLで一からコンパイラを書こうとしていたんですが、ローレベルあんまり詳しくなくてネイティブコードを生成できるようにするのが面倒だったのと、Standard MLのsyntax suga…

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

Coq

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

二分探索に証明を付ける

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

OCamlで車輪を再発明する

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