2020-01-01から1年間の記事一覧
この記事は 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 167のD問題で数列の循環検出が必要になった事がありました（問題の制約的にはダブリングでも解けますが）． 数列の循環検出はナイーブにに実装すると，循環している部分に至るまでの長さを，循環…
AtCoder Beginner ContestのC問題で全探索が出題されがちな今日この頃，いかがお過ごしでしょうか？ C++で競プロをやってる人達は重複順列に対して全探索して解を得たい時なんかに，いちいち重複順列を列挙する処理も含んだ再帰関数を書き直してるらしいです…
OCamlでAtCoderの問題を解くのに昔書いたダイクストラ法の実装を使っていたんですが， どうも定数倍でTLEすることが多く，もどかしい気持ちになることもしばしばでした． 本記事では行儀の良いスタイルに囚われず以前の実装に定数倍高速化を施し，実際のコン…
