メモ sqlite3 /home/aps/aps/aps-server/db/production.sqlite3 'SELECT file FROM answers' | ruby -e 'puts $<.read.scan(/\w+/)'

HDCPは仕様が公開されてるので誰でも読めるので、読んでみた。世の中ではHDCP機器を40台ほど集めてきてもぞもぞと解析すれば、すぐにマスターキーが作れそうな漢字で2001年の論文の話が紹介されてるようだが、それだけでは全然不十分なようだ。 HDCP機器認証…

http://as305.dyndns.org/aps/ サブミットのしかた。 DefinitionsがあるときはDefinitions.vに保存してコンパイルTheoremをTheorems.vに保存。Proof.〜Admitted.の間を埋めて証明できたら、Admitted. をQed. にしてファイルを送信 問題の作成 http://as305.d…

ちまちまと進めてたんだけど、だいたいきれいになってきたので公開http://github.com/kik/TaraiTermination元にした証明は http://d.hatena.ne.jp/kururu_goedel/20100719Coq庵 http://atnd.org/events/6022 でちょっと解説する予定。参考資料 http://www.km…

下に書いたのから、よく考えたらおかしいところを直して、option Z とかいらないじゃんとか思い直した。ここに最新のが置いてある。http://github.com/kik/sandbox/blob/master/coq/tarai.v

http://d.hatena.ne.jp/kururu_goedel/20100702これを見て、とりあえず綺麗に書き直そうとしてみたら一日かかった。 しかし、これで一般たらいまわしへの道も見えてきたかも？ここに置いた。http://github.com/kik/sandbox/blob/master/coq/tarai.v多少、解…

http://d.hatena.ne.jp/m-hiyama/20100629/1277774676 を証明してみた。とりあえず、問題設定 Axiom A : Set. Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }. Axiom A_mul : A -> A -> A. Axiom A_zero: A. Axiom A_one: A. Infix "*" := A_mul. N…

問題設定とかは http://d.hatena.ne.jp/ku-ma-me/ を見ればいいとして、 金曜日21:00〜23:00 問題読みタイム。さっぱりわからないが、一番下に最初にやるべきことが書いてあったので、0を送ればいいっぽい、サーバが死に掛けてて全く送れない。やっと反応が…

昨日がんばってIOモナドの実装がどうなってるのか考察したので、答えを見たhttp://itpro.nikkeibp.co.jp/article/COLUMN/20070206/260872/ から参考文献をたどって http://homepages.inf.ed.ac.uk/wadler/topics/monads.html#imperativeを読んでみたところ、…

色々入門書を読んでみたのだが、IOモナドというものがどういうものなのか分からない。 使い方は分かるんだが、なんでこうなってるのとか、どういう風に実装されてるのかとかさっぱり理解の外である。ということで、まず、NiseIOモナドを自分で作って見てある…

とりあえず少し書いておくと、まず第１回で書いたようにROMは作れた。 A0 0 0 A1 0 0 A2 0 0 ... Ae 0 0 Af 1 1 ## こんな感じにADDR <- 0x7FFF みたいに、アドレスをセットして ## ROMのコードに突っ込むと ## BEGIN ROM if (ADDR-- == 0) { DATA <- 'H'; }…

kik@shadowgate:~/work/sandbox/fernando$ ruby quinecode.rb >quine.mem kik@shadowgate:~/work/sandbox/fernando$ ruby quinegen.rb quine.mem >q.nand kik@shadowgate:~/work/sandbox/fernando$ time ./ferc q.nand >q.nand.out real 2055m44.082s user 2…

プログラムの最初に 1 1 1と書いておけば、以降変数1は定数1として使える 0 0 1 0 1 0 0 0これで、「H」が出力できる。頑張って並べれば「Hello, world!」が書ける基本的な計算 ### X <- !Y X Y Y ### X <- Y X Y Y X X X ### X <- Y & Z X Y Z X X X ### X …

最近ゴルフ場にferNANDo(http://esolangs.org/wiki/FerNANDo)とかいうまた頭のおかしい言語が追加されていたので、Quineを書いてみた。というか書いてる途中。というか書いて実行中。 まず、ferNANDoの簡単な解説 変数は全て1ビットの値を持ち、初期値は0で…

今週末はSPOJのPRIC(http://www.spoj.pl/problems/PRIC/)をやってるのだが、なぜか素数判定にヒープソートを使うというわけの分からない実装ができてしまった。まず、等差数列を素数で割ったあまりを考えると an mod 3 mod 5 mod7 mod 11 mod 13 1 1 1 1 1 1…

色々あって解決した途中で書いたコラッツ計算機 https://spreadsheets.google.com/ccc?key=0AodXTYWJICjQdGZqeEFTNGFQT2tYSXNlQnRDYS1kemc&hl=en以下メモ 証明(0) 略 Xn = (3Xn+1)/2^mnとする。 この段落は忘れてよい。に関する仮定は最後の最後まで使わない…

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

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

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

今回のターゲット文法は 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の後ろの空白文…

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

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)();を定義してるのね

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

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…