チラシの裏

プログラミングとか色々

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

Coq

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

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

Coq

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

普通の大学院生が【バイク】乗ってみた。あるいはCBR250Rのインプレ

月日は百代の過客にして,行かう年もまた旅人なり. 今年の3月末頃にCBR250Rというバイクを購入して早3ヶ月,様々な土地を放浪して走行距離3000kmに達するまでになりました. 区切りが良いのでこのバイクについて感じたことなどを書き留めておきたいと思いま…

αβ法に証明を付ける

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を使う際は専ら言語処理系を書いていましたが、 競技プログラミングでは全く関係ない題材を扱う必要がある…

SMLでコンパイラを書いた

SML

このエントリはML Advent Calendar 2015と言語実装 Advent Calendar 2015の20日目の記事です。 言語実装 Advent Calendar 2015の19日目の記事はh_sakuraiさんのJavaのサブセットコンパイラの作成でした。

GADTを用いた二項ヒープの実装

このエントリはML Advent Calendar 2015の14日目の記事です。 13日目の記事はよんたさんの関数型プログラミングにおける再帰関数の考え方でした。

型推論の健全性の証明

このエントリはTheorem Prover Advent Calendar 2015と言語実装 Advent Calendar 2015の11日目の記事です。 言語実装 Advent Calendar 2015の10日目の記事はkeenさんのリージョンについてでした。

手続き型言語OCaml

この記事はML Advent Calendar8日目の記事として書かれました。 7日目の記事はでこれきさんのfoldみぎひだりです。 Standard MLやOCamlをはじめとしたML系の言語は関数型言語として有名ですが、参照、配列、例外といった副作用を伴う機能も扱う事ができます…

単一化の証明

Coq

この記事はTheorem Prover Advent Calendar 2015の7日目のために書かれました。 6日目の記事はmathinkさんのCoq で環のイデアルを作ってみるです。

Coqでちょっと複雑なデータ構造を書こうと思ったらハマった

Coq

何となくMinCamlにCoqで証明を付けたいと思い立ったのでOccurrence checkの検証を証明しようと思ったのですが、ちょっとした問題に遭遇したのでメモ。

"Syntactically, SML is a nightmare"

SML

現在僕は趣味でStandard MLのサブセットの処理系を実装しようとしているのですが、皆さんのご存知の通り、Standard MLの構文解析は非常に難しい事が知られています。 今回はML Kitの実装に関する文書を参考に構文解析器を実装した時の事について書きたいと思…

演算子順位構文解析

普段日常生活を営んでいると何となくコンパイラを作りたくなる事はありませんか?僕はあります。 演算子順位構文解析を用いることでStandard MLで行なわれているような演算子の順序の入れ替えを実現できるのではないかと思い、試しに実装してみました。

LCF MLについて

この記事はML Advent Calendar 2014 24日目のために書かれました。 Standard MLをはじめとするML系言語の始祖として、よくLCF MLの名前が挙げられます。 ここでは、LCF MLの言語機能について解説しつつ後の言語に与えた影響について思いを馳せたいと思います…

SMLでソート

この記事はML Advent Calendar 2014 8日目のために書かれました。 多くの言語においてソートは標準ライブラリで提供されていますが、Standard ML Basis Libraryにはソートを行う関数が存在しません。 処理系依存で良ければSML/NJのListMergeSort.sortの様に…

ニュートン法とDKA法の実装

SML

大学でニュートン法とDKA法で方程式の解を求める課題が出たので、今回は趣向を変えてStandard MLで実装しました。

ちょっとだけクイックソート

よい実装かどうかは抜きにして、一般的な関数型言語ではリストに対するクイックソートを簡単に書く事ができます。 一方、そのようなよく見かける実装ではリストの結合を再帰内で用いていますが、 一般に関数型言語ではの時間計算量を要するため、リストの結…

CoqからSMLへ

CoqにはExtractionという機能があり、Coqで書かれたソースコードから対応する他の言語のソースコードを出力する事ができます。今回はそのExtractionをStandard MLに対応させた事について書こうと思います。

貧乏帰省の顛末

現在東北の大学に通っているんですが、実家から遠くに住んでいると帰省の交通費が馬鹿になりません。*1そこで、何とかして安く帰ろうとしたのですが一悶着あったという話。 *1:仙台高松間を新幹線で往復すると5万円程度にもなる

改良オイラー法とルンゲクッタ法

学校の課題で改良オイラー法とルンゲクッタ法を実装しました。今回も言語の指定は無かったのでOCamlです。

モータドライバの設計

動機 昔、モータードライバを自作しようと試みた事がありました。しかし、自作のドライバはロボコンで用いられていた既製品に対して信頼性で劣っており、既製品の出力に不満が無かったために置き換えられませんでした。

ガウスの消去法

学校の課題でガウスの消去法を実装しました。言語は特に指定されなかったのでOCamlです。

簡単な式の評価器を証明駆動開発

EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。 *…

EvalML2における評価の一意性の証明

前回、前々回は四則演算程度しか持たない導出システムについての証明でしたが、今回は変数束縛や環境を持つ導出システム、EvalML2における評価の一意性を証明しようと思います。例によって元ネタはプログラミング言語の基礎概念です。

FreeBSDにAjhcをインストールするときに躓いたこと

Haskellで書かれたプログラムをマイコンで動かすことができると某界隈に衝撃を与えたAjhcですが、FreeBSD機にインストールする時に躓いた事が有りましたのでまとめておきたいと思います。