OCaml
AtCoder Beginner Contest の E 問題で2回続けてダイクストラ法が出題される昨今,いかがお過ごしでしょうか?[^1] その2つの E 問題のうち,先に出題された E - Come Back Quickly はいかにも典型的だなあといった問題なので良いのですが,後に出題された E…
この記事は ML Advent Calendar 2020 の14日目の記事です. リストの Church encoding と言えば List.fold_right で表現することが多いように思いますが,果たして List.fold_right だけしか使わずに様々なリストについての再帰関数を表現できるのか疑問に思…
この記事は言語実装 Advent Calendar 2020 の5日目の記事です. 一度でも型推論器を書いたことがあれば,そのあまりの邪悪さ,あるいはその複雑さに恐れ慄いたことでしょう. 参照を用いて単一化を実現しようものなら構文木は参照に汚染され,純粋関数型に実…
今年はそれらしきアドベントカレンダーが無いので,この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます. ML って本を正せば定理証明支援系由来ですし.最後にちょっと OCaml を使ってますし. Coq によって検証された正規表現エンジ…
以前から僕は単相の型推論アルゴリズムの健全性や完全性をCoqで検証していたのですが,最近*1let多相をサポートするように型推論器の実装と正当性の証明を修正したので記事にしておきましょう*2. *1:と言っても今年の1月ぐらいですが.本当はAdvent Calenda…
AtCoder Beginner ContestのC問題で全探索が出題されがちな今日この頃,いかがお過ごしでしょうか? C++で競プロをやってる人達は重複順列に対して全探索して解を得たい時なんかに,いちいち重複順列を列挙する処理も含んだ再帰関数を書き直してるらしいです…
OCamlでAtCoderの問題を解くのに昔書いたダイクストラ法の実装を使っていたんですが, どうも定数倍でTLEすることが多く,もどかしい気持ちになることもしばしばでした. 本記事では行儀の良いスタイルに囚われず以前の実装に定数倍高速化を施し,実際のコン…
僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが,Brzozowski derivativeに基づいて正規表現エンジンを実装し,あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです. 折角practicalなプログ…
以前二分探索の正当性をCoqで証明しましたが,この証明スクリプトからOCamlのコードを抽出して実際に競プロに用いようとすると,添字の動く範囲が保証されていないので添字エラーを起こすこともしばしばでした. そこで,依存型を活用して添字の動く範囲も保…
遥か昔にもOCamlでダイクストラ法を実装したことはあったんですが, 最も近い頂点を線形探索で求めている手抜き実装なので,O(V2)の計算時間を要する(a.k.a. 疎なグラフに対しては遅い)ものでした. 競プロだと入力が疎なグラフに限定されている場面が多々…
この記事はML Advent Calendar 2017の10日目(!?)のために書かれました. 皆さんOCaml標準ライブラリのList.sortは使っていますか? 頻繁にリストに対してのソートを行うようならデータ構造かアルゴリズムを考え直した方が良いでしょうが,競プロの様にち…
この記事は言語実装 Advent Calendar 2016のために書かれました。 元々僕はStandard MLで一からコンパイラを書こうとしていたんですが、ローレベルあんまり詳しくなくてネイティブコードを生成できるようにするのが面倒だったのと、Standard MLのsyntax suga…
二分探索は言わずと知れた探索アルゴリズムですが、 実際に実装しようとすると無限ループしたり正しい答えが得られなかったりする事も多いのではないでしょうか。 そこで、ここではCoqで二分探索を実装し、正当性の証明を行いました。
最近研究でCoqぐらいしか書いてないので、リハビリがてらAtCoderで 開かれるコンテストにOCamlで参加して遊んでます。 僕は個人的な趣味もあってOCamlを使う際は専ら言語処理系を書いていましたが、 競技プログラミングでは全く関係ない題材を扱う必要がある…
このエントリはML Advent Calendar 2015の14日目の記事です。 13日目の記事はよんたさんの関数型プログラミングにおける再帰関数の考え方でした。
このエントリはTheorem Prover Advent Calendar 2015と言語実装 Advent Calendar 2015の11日目の記事です。 言語実装 Advent Calendar 2015の10日目の記事はkeenさんのリージョンについてでした。
この記事はML Advent Calendar8日目の記事として書かれました。 7日目の記事はでこれきさんのfoldみぎひだりです。 Standard MLやOCamlをはじめとしたML系の言語は関数型言語として有名ですが、参照、配列、例外といった副作用を伴う機能も扱う事ができます…
この記事はML Advent Calendar 2014 24日目のために書かれました。 Standard MLをはじめとするML系言語の始祖として、よくLCF MLの名前が挙げられます。 ここでは、LCF MLの言語機能について解説しつつ後の言語に与えた影響について思いを馳せたいと思います…
よい実装かどうかは抜きにして、一般的な関数型言語ではリストに対するクイックソートを簡単に書く事ができます。 一方、そのようなよく見かける実装ではリストの結合を再帰内で用いていますが、 一般に関数型言語ではの時間計算量を要するため、リストの結…
CoqにはExtractionという機能があり、Coqで書かれたソースコードから対応する他の言語のソースコードを出力する事ができます。今回はそのExtractionをStandard MLに対応させた事について書こうと思います。
学校の課題でガウスの消去法を実装しました。言語は特に指定されなかったのでOCamlです。
EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。 *…
タイトルの通り、OCamlでOCamlのサブセットの型推論を書いたので、その事について纏めておこうと思います。
プログラミング言語の基礎概念と言う意味論や型理論の入門に良さげな本が有るんですが、この本は嬉しいことにオンライン演習システムが有るので実際に手を動かしながら内容を理解することができます。