2009-01-01から1年間の記事一覧

定理証明の会で実演した中間値の定理の証明

Coq

はhttp://github.com/kik/sandbox/blob/f41bc1346d4491f937b3fb78da38a07c746acf1c/coq/ivt.vにあります。試すにはcoqを適当にインストールしてcoqideを起動して、このファイルを開く。 あとはツールバーから適当に下に進むボタンを押してれば証明の様子が分…

戦場のヴァルキュリアは

最近やったゲームの中では一番に面白かった。とりあえず記録 ステージ ランク ターン数 コメント 序 A 2 1 C 5 2 S 3 3 B 5 1ターンクリアでSとか頭おかしい。たぶん、挑戦してないけど 4 B 5 2ターンクリアで同上 5 B 9 このマップは苦労した。進む方向に気…

ハノイの塔

Coq

久しぶりにCoqで遊ぼうかと思って、いい問題はないかと考えたところ、ハノイの塔あたりが面白いんじゃなかろうかということで証明してみた。証明したいことはハノイの塔を完成させる最短手数は2^n-1であること…と思って少し書いてみたんだけど、これはかなり…

ちょっと読んでみた

ちょうど読みたかった内容の入門書で薄くて楽そうだったのが明倫館にあったから読んでみてるのだが、この本はだめだ……とりあえず層の定義より前の部分(関数論と位相と多様体の定義の復習)はさらっと読めて、層の定義からが知らない内容なんだけども誤植と非…

連休に頑張って書いたコード

C++

http://github.com/kik/cpppeg に置いた。 http://wiki.github.com/kik/cpppeg/usage 説明はここ。 まだ色々と不完全

大量の意味不明なエラーメッセージと格闘した結果

C++

今回のターゲット文法は epxr ::= int_lit | '(' op expr expr ')' int_lit ::= token(int_lit_s) op ::= token(op_s) int_lit_s ::= digit digit* op ::= alpha alpha* token(T) ::= T ' '*token(T)はジェネリックなルールであり、Tに対してTの後ろの空白文…

C++で再帰下降パーザライブラリ

C++

再帰下降パーザを書くだけなら誰でもできることなのだが、本当に一日中悩んでやっと低機能なものが動くようになった。 最終的にはPEGをサポートしたいところである。たとえば <hoge> ::= alpha alpha digit <foo> <foo> ::= digitなんて文法があったら #include <iostream> #include "p</iostream></foo></foo></hoge>…

C++

struct X { typedef int Y; }; struct Y { struct Z { X foo(); }; }; struct Z { X::Y foo(); }; X::Y::Z::foo() { return 0; } これだと、最後の関数定義は X::Y (::Z::foo)();を定義してるのね

C++の文法が複雑すぎて分からない

C++

struct X { struct Y { struct Z { }; }; }; struct Y { struct Z { X foo(); }; }; struct Z { X::Y foo(); }; X::Y::Z foo(); X::Y::Z::foo() { return 0; } 最後の関数定義はいったいどの関数を定義しているのだろう…。C++の仕様書の生成規則だと X::Y::Z…

チルダ

チルダ「やあやあ、キョンくん 半角/全角キーはどこだい?」 キョン「Alt+〜ですよ」 チルダ「にょろ〜ん」 にょろ〜んチルダさん 完…頭が沸いてるな

95Bきたー!ていうかハノイの塔重要じゃん

昨日少し考えてみたんだがさっぱり分からない>C 10xバイトにもたどり着けないじっと眺めてたら、これハノイの塔じゃん!って気づいたんだけど すでにうぃきぺに書いてあってしょぼんぬ

AJPCファイナル

というわけで、今日はAJPCのファイナルトーナメントの初日でした。まず、朝10時に会場に行かないといけない時点で無理 でもまあなんとか頑張って起きてギリギリに着きましたよ3ラウンド目くらいからチップ量が10BB切り始めて、 4ラウンド目の最初のゲームがB…

herumiさんに少し教えてもらったのだが

http://en.wikipedia.org/wiki/Riemann-Roch_theorem を少し読んでみた。 These spaces are all finite dimensional. In case g = 0 we can see that the sequence of dimensions starts 1, 2, 3, ...: this can be read off from the theory of partial fra…

MTの状態空間ワープ

ようするにnum_rand回のループなんだから、状態空間をnum_rand/2進んだ状態までワープさせてやれば、 0からnum_rand/2とnum_rand/2からnum_randを並列に計算できる。 と考えていた時期があって、色々と考えてみた。 行列の冪をlog(n)でやる例のアレ 一番最初…

Hack the Cell

優勝しますた。部屋を片付けてテレビ置く場所を作ります。

dddddmapとか作るとよくね?

http://d.hatena.ne.jp/ku-ma-me/20090312 を見て思ったんだけど、 x.ddmap.f ==> x.dmap.f.dmap x.dddmap.f ==> x.dmap.f.ddmap x.ddddmap.f ==> x.dmap.f.dddmapとか作れば x.map{|y|y*3/5+2}とかが x.dddmap*3/5+2ってできて便利じゃね。適当にこぴってき…

コード公開

http://as305.dyndns.org/~kik/public/mt_mine.c とりあえず置いてみた。実行環境がないんとasm化は大変だなあ。

懇親会

平日かー。行けるかなー。28日は行けるけど。

結果

ORIGNAL: sum=3c927c56, 292970508 ticks MINE: sum=3c927c56, 2313630 ticks ORIGNAL: sum=2e987a4d, 422626291 ticks MINE: sum=2e987a4d, 3328071 ticks ORIGNAL: sum=ef1b6aef, 310977433 ticks MINE: sum=ef1b6aef, 2454426 ticks ORIGNAL: sum=eedd251…

総和

sum = 0; for (i = 0; i < 16; i++) { s0 = cntb(y[i]); s1 = cntb(y[i+16]); s2 = sumb(s0, s1) sum += s2 << i; }以上。じゃなくて、ところどころシャッフルにしたけどね。herumiさんと同じでまとめてやろうとすると、gccがレジスタ割り当てに失敗して酷い…

これは偶然

これは本当に偶然で、そうである必然性はないはずなのですが、 12 + 29 * 4 = 128になります。この関係があるために、上の回転量は1と-4とか-1と4とかになります。この関係をうまく使って、最初から適当にずらしておきます。 下のほうのビット並び替えを使っ…

更新処理

普通に頭からビットを詰めていったら更新処理はこんな感じになります。 for (; count != 0; count -= 1) { <%= gen_update(0, 3, 4, 12, 12, "mask1") %> <%= gen_update(1, 4, 0, 12, 29, "mask2") %> <%= gen_update(2, 0, 1, 29, 29, "mask2") %> <%= gen…

ちょっとTemperingの話

本当は行列の計算を色々試してて気づいたんだけど y = y >> 1; y = y ^ (y >> 11);と y = y ^ (y >> 11); y = y >> 1;って、結果を見るとあまり差がないよね。ほんの少し正確に書くと word T1(word y) { return y ^ (y >> 11); }って関数を考える。T1の逆関…

ビット転置

69倍になったあとは、一ヶ月ずっとビット転置のやり方を考えてました。 ワード単位のときのような頭のおかしい配置方法があるんじゃないかと探してたんです。結局みつからなかったので、頭から順番にビットを詰めていく方法になりました。 qword mt_bs[32][5…

せっかくのgather命令

バイト単位じゃないともったいない。 z = si_lqx(spu_slqw(spu_gather(y), 4), mag_lut); r = spu_xor(spu_rlmaskqw(y,-1), z);これだと、ワード単位のgatherになっちゃって結果が4ビットしか得られないんですよ。 1命令使って、結果がたったの4ビットですよ…

Even命令が大幅に過剰

みんなそうだと思うけど、even命令が大幅に過剰になっちまった。 しかも、僕のコードは1ワード1ロードシャッフル無しだから、それはもう多すぎてhttp://d.hatena.ne.jp/kikx/20090120これはループのアンロール前で内側に14回のループが残ってたんだけど、 こ…

herumiさんのコードも読んだ。

革命的な方法はビット単位で計算したときにでてくるqwordの29ビット回転を1命令でやる方法です。 その話は次の次の次の次あたりかな。

擬似コード

謎の表の順番で更新すれば1ワード1ロードにできるのを擬似コードにしてみた。 ベクトル化はなし。 #define N 624 #define N 397 word mt[N]; word mtx[N]; void transform(word dst[N], word src[N]) { for (int i = 0; i < N; i++) { // 謎の表の通りに並び…

even*1+odd*3

(y >> 1) ^ mag01[y & 1]をeven*1+odd*3でやる話。XORはevenでやらないといけないから右シフトは当然qword右シフトになる。 mag01[y & 1] は gb してテーブルルックアップすることにすると z = si_lqx(spu_slqw(spu_gather(y), 4), mag_lut); r = spu_xor(sp…