概要 Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。 冗長な証明になっている可能性は大いにあります。Agda のサンプルコード…

2010-09-26 を見て同じ命題を Agda2 で証明してみた。 Functional Programming Memo: [Coq] Coq-99 : Part 1 agda-mode が証明するのを手伝ってくれるのでお気楽です。 module Practice1 where data True : Prop where tt : True data False : Prop where da…

iPad 買いました。おもしろいです。土日は iPad を持って外出してましたが、電池切れになることはありませんでした。あとは Evernote をプレミアムアカウントにしてローカルにファイルを保存できるようにすれば、今週は寮に MacBook を持ってく必要がないか…

f(n) = n*n + an + b, |a|素数が連続して最も長く出現するような a, b の値を求めよ。 こっちもがっちり C で。何も考えなくても Haskell より速い。素敵。 #include <stdio.h> #define MAX 1000 int isPrime(int x){ int i; for (i=2;i</stdio.h>

現在は工場実習中で毎日肉体労働をしてるので、休日くらいはプログラムを書きたくなります。というわけで超久しぶりに Project Euler をやってみたよ。 問題23。正の整数 n の約数の和が n をより大きいとき、 n を過剰数(abundant number)という。2つの過剰…

背景 修論で追い詰められた学生が、「twitter クライアントはたくさんあるけど、実際ブラウザで十分なんじゃね。他の拡張と組み合わせれば、かえって操作性が上がるかもしれない。」と思いつき、嫌だ力を駆使して集中力が切れるたびに少しずつ書いた拡張機能…

LablGTK(http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html) は、OCaml のための GUI ライブラリです。素敵です。 背景 研究のためにサンプルプログラムを書く必要があった マルチスレッドと GUI のライブラリが必要だった Haskell + wxHaskell で…