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

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

今回はアキュムレータを用いる事でリストの結合を用いずにクイックソートを実装したいと思います。

CoqからSMLへ

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

貧乏帰省の顛末

現在東北の大学に通っているんですが、実家から遠くに住んでいると帰省の交通費が馬鹿になりません。*1そこで、何とかして安く帰ろうとしたのですが一悶着あったという話。

*1:仙台高松間を新幹線で往復すると5万円程度にもなる

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

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

モータドライバの設計

動機

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

ガウスの消去法

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

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

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

*1:プログラミング言語の基礎概念に登場する、MLのサブセットのような言語