WordPress 2.5 RC2 が出ていたので人柱になってみた。
正式版がでたら他の人の分もアップデートする予定。
見た目はなーんにも変わってないけど、管理ツールががらりと変わっていていろいろ便利になっているのでみんなも使いたいと思うはず。

上の方にあるのはサカさんが書いてくれたロゴ、カッコいいけどどっかで見たような気がするなぁ。元々の絵はキレイだったんだけど gimp で縮小したらギザギザになって台無し。

あと permlink を変えようと思ったんだけど既存の permlink に影響が出ないように変更するのがムリっぽくて断念した。
permlink は変わらないからこそ permlink なんだけど、コメントとトラックバックが打てないそもそもの原因は、permlink が関係しているので何とかしたいなー。

自動証明処理系の coq を使って簡単な3段論法を証明してみる。

まず coq を起動する。

% coqtop
Coq <

命題 A B C について考えてみるよ。

Coq < Variables A B C : Prop.
A is assumed
B is assumed
C is assumed

「A ならば B 」というのは命題だよね?

Coq < Check (A -> B).
A -> B
: Prop

じゃあ簡単なトートロジー「A ならば B ならば C」ならば「A ならば B」であり「A ならば C」を証明するよ。

Coq < Goal (A -> B -> C) -> (A -> B) -> A -> C.
1 subgoal

============================
(A -> B -> C) -> (A -> B) -> A -> C

導入する。

Coq < intro H.
1 subgoal

H : A -> B -> C
============================
(A -> B) -> A -> C

いっぺんに同時に導入できるよ。

Coq < intros H’ HA.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
C

仮説 H を適用します。

Coq < apply H.
2 subgoals

H : A -> B -> C
H’ : A -> B
HA : A
============================
A

subgoal 2 is:
B

仮説 HA は正しいよ。

Coq < exact HA.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
B

そして H’ を適用します。

Coq < apply H’.
1 subgoal

H : A -> B -> C
H’ : A -> B
HA : A
============================
A

Coq < assumption.
Proof completed.

証明終わり。

うー、もっとカッコイイ証明をいろいろやってみたいんだけど圧倒的に脳みそが足りない。

土曜の夜。sige君が「純米大吟醸寒しずく」をどこからか大量に仕入れてきた。
限定 3000 本しか売ってないはずなのにこの部屋に 10 本もあるなんて!
(写真にあるように瓶にはロット番号が打ってある)
起きたら、2本しか残って無くてガッカリした。(3人しかいなかったよね？
# 酔っぱらった人たちは中国国内から great firewall を超える為の技術的方法とビジネスモデルについて朝まで話してた様な気がするけどあまり思い出せない、議事録を取らないとダメだな。
昼に起きてそのまま PHP 拡張勉強会に行く
頭が痛くて呂律が回らなかったような気がするけどうまく喋れただろうか。
ustream で撮って頂いた様なので後で探す。

http://events.php.gr.jp/event.php/event_show/39

その後飲み会。お疲れさまでした!

なんとなく GNU tar のソースコードを読んでたら、LZMA オプション発見。
最近 GNU のプロダクトで .tar.lzma ってファイルを見かけるようになったのでいつか tar で扱えるようになるだろうなと思ってたところ。
tar-1.19 ではまだ対応して無くて tar-1.19.1 のスナップショットから使えるみたい。

ftp://download.gnu.org.ua/pub/alpha/tar/tar-1.19.1-20071030.tar.gz

今のところ -a オプションだけど今後変更されるかもしれない。

static struct zip_magic const magic[] = {
  { ct_none, },
  { ct_compress, 2, “\037\235″, “compress”, “-Z” },
  { ct_gzip,     2, “\037\213″, “gzip”, “-z”  },
  { ct_bzip2,    3, “BZh”,      “bzip2″, “-j” },
  { ct_lzma,     6, “\xFFLZMA”, “lzma”, “-a” }, /* FIXME: ???? */
};

中では lzma を clone(2) するので予め lzma をインストールしておく必要がある。
# debian だと apt-get install lzma

これで、

$ tar cvaf dir.tar.lzma dir

と言うように lzma の tar アーカイブを作成することが出来るが、まだ展開は対応してない様なので unlzma を使うひつようがある。（そのうち対応されるだろうけど。

おしりに火がついてきたのでいいかげん確定申告をする。
e-tax って linux で出来るのか出来ないのか判らないけど、どのみち今から準備するのは間に合わないのでe-tax の準備と、オフラインの書類作成を同時進行でやる。

まず
https://www.keisan.nta.go.jp/h19/ta_top.htm
を開いてみると、このサイトは javascript を有効にしないと進めないので有効にする。

e-tax の準備に進む。
パソコンの推奨環境に linux は含まれていない、解ってたけどね。
でもせめて対応ブラウザに firefox を入れて欲しかった。

次に root CA 証明書のインストールを促された。
ダウンロードしようとすると exe ファイルだった。(2.2Mbyte)
挫折しようとしたところ、「別手順によるルート証明書のインストール」を見つけた。
インストールした証明書は以下の2つ

% openssl x509 -issuer -subject -noout -inform DER -in MOF_Root.cer issuer= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Root CA
subject= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Root CA

% openssl x509 -issuer -subject -noout -inform DER -in zaimu.cer
issuer= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Certification Authority
subject= /C=JP/O=Japanese Government/OU=Ministry of Finance/OU=MOF Certification Authority

次に開始届出を、作成しようとすると、xpdf が起動した。
テキストボックスやリスボックスの様なUI が表示されるけど当然入力出来ないので acroread で開いてみるとこんなエラーが出た。

という訳で、今年は e-tax での確定申告を断念した。
来年また再挑戦してみたい。

確定申告のページのトップから「eTax を使用しない場合又は作成を再開する場合はこちら」のボタンを押すと、URL バーのないウィンドウが新たに開かれた。
これはセキュリティ上問題があるので直して欲しい。

ねむいので続きは朝早く起きて書類を作る。

秋元さんの blog経由でこんなの発見
http://codepad.org/

がーん、似たようなものを作ろうとしてたのに先越されてしまった。
でもさすがに実行出来るページを公開しようとは思ってなかったな。
Cのコードを実行出来るなんてとっても危険な予感がする。破れるものなら破ってみろ見たいな事が書いてあるのでいろいろイタズラをしてみたけどほとんどのシステムコールは無効にされている様子。どのレベルで防いでいるのか解らなかったのでスタックに置いたコードから system call を呼んでみる。

http://codepad.org/h9rGgGop

これは、「/etc/passwd を open(2) して返値を表示するコード」をスタックに置いて実行するプログラム。アセンブリコードは以下の通り

segment .text
global _start
_start:
        push    ebp
        mov     ebp, esp
        mov     eax, 0x00647773
        push    eax
        mov     eax, 0x7361702f
        push    eax
        mov     eax, 0x6374652f
        push    eax
        mov     eax, 5  ;write
        mov     ebx, esp
        mov     ecx, 0
        int     0x80
        add     eax, '0'
        push    eax
        mov     eax, 4  ;write
        mov     ebx, 1  ;stdout
        mov     ecx, esp
        mov     edx, 1
        int     0x80
        leave
        ret

上手くいけば open(2) したファイルディスクリプタが表示されるはずなんだけど、がっちり防がれている。
kernel に 手を入れて system call 制御しているのかなと思ったんだけど、良く読むと ptrace で制御しているんだそうな。ptrace ってデバッグ用のシステムコールだと思ってたんだけどこんな事もできるんだな。今度使ってみたい。

データ圧縮の究極より

25 名前： 名無しさん＠１周年 投稿日： 2000/11/09(木) 20:42
円周率は、それを任意の桁まで求めるプログラムによって
完全に表現できるじゃん？
これこそ、究極の圧縮。

26 名前： >25 投稿日： 2000/11/09(木) 20:56
確かに圧縮率は飛び抜けて良いが、復元速度が鬼のように遅ぞ。

このアルゴリズム。定期的に見かけるけど、冗談抜きで実用的なんじゃないかと思う。
円周率をインデックシングしたデーターベースで保持することでパフォーマンスの問題は解決するし、容量が問題になるならネットワーク越しに得ればよい。
#ネットワークストレージが使えるんなら THcompこそ究極なんだろうけど、世界共通の円周率を外部記憶に外出しするという意味では優位性がある。例えば任意の桁から任意の長さの円周率を返す πサーバーが世界の何処かに在ればよい。
どれくらいの桁の円周率でどれほどの圧縮率が得られるのか知りたい。誰か実装した人はいるんだろうか。
後で調べる。

この前フィボナッチ関数のグラフを gnuplot で描いた時に sakaik さんから詳しい書き方を聞かれたので、今回はリュカ数をプロットしてその手順を詳しく書いてみる。

リュカ数列とは、フィボナッチ数列が

と定義されるのに対し初期値を

とした時の数列をリュカ数列と呼ぶらしい。see リュカ数 - Wikipedia
具体的には

2, 1, 3, 4, 7, 11, 18, 29

みたいな感じ。
この数列を実数(複素数)の世界に拡張して、入力を z(レンジは -5 〜 5), 出力の実部を x 軸, 虚部を y 軸にプロットしてみる。

ソースコード(lucas.c)

#include <stdio.h>
#include <stdlib.h>
#include <math.h>
#include <complex.h>

#define THETA 1.618034

double complex clucas(double i)
{
    double complex c = cpow(-THETA, -i);
    return (pow(THETA, i) + creal(c)) + cimag(c) * I;
}

void plot_clucas(double min, double max)
{
    double z;
    double complex c;
    for(z=min; z<max; z+=0.1){
        c = clucas(z);
        printf("%lf\t%lf\t%lf\n", creal(c), cimag(c), z);
    }
}

int main(int argc, char *args[]){
    plot_clucas(-5, 5);
    return EXIT_SUCCESS;
}

これをコンパイルして実行する

% gcc -lm lucas.c -o lucas
% lucas > lucas.dat

次にこんな感じの plt ファイル(lucas.plt)を用意して

set term png
set output "lucas.png"
splot "lucas.dat" with lines

gnuplot を実行すると・・・

% gnuplot lucas.plt

グラフの出来上がり!

ついでなので fibonacci 関数と混ぜてみる。

赤がリュカ数で緑がフィボナッチ。

ブックマーク管理ツールの sitebar を長らく使ってきたんだけど、この sitebar の欠点は最大 500 リンクまでという制限があること。今日その 500 に達してしまったので別のブックマークツール選定中。(自前で sitebar を運用するってう手もあるんだけど、sitebar のバージョンアップが割と頻繁にあって最新版に追従するのが面倒になって止めた経緯がある)
Bookmark ツールで有名所は del.icio.us, furl, spurl あたりかな。知名度で言えば圧倒的に del.icio.us の一人勝ちのような感じ(alexa調べ)だけど機能面ではどうだろうか。
特に furl と spurl に在るコンテンツのまるごとキャッシュ機能が素晴らしい。何が良いってブックマークの全文検索が出来る。 (タグとか付けなくて良い)
しばらく furl と spurl を両方使ってみて気に入った方を使い続けようかな。他にオススメのブックマークツールがあったら教えて下さいな。

# digg, reddit、はてブはどちらかというとソーシャルニュースサイトの様なきらいがあるので避けた。