世の中にはCooley-Tukeyの解説しかないんですよ。並列の時代なのでStockhamとか知りたいんですが…で、難しい英語の解説とか読まなくてもサンプルコードがあれば実装できるので別に問題ないんだけど、やっぱりちゃんと理解したい。FFTの解説ってΣをごにょごに…

メモ 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とする。 この段落は忘れてよい。に関する仮定は最後の最後まで使わない…