2007-01-01から1年間の記事一覧
Rule 30 (http://golf.shinh.org/p.rb?Rule+30#z80) はかなり簡潔に書けた。 LD A, 0x76 PUSH DE PUSH AF CALL 8003H RL E RRA RL C LD A, C DEC A AND 4 NEG ADC A, '#' RET参考にしたコード(http://longlong.way-nifty.com/blog/2007/12/card.html#more , …
有明の某所にいってる間に、やねうらお先生が19Bに到達してしまった(id:yaneurao:20071230)。 悔しいので色々いじっていたら、20Bのコードはわりと色々書き方が見つかったり、 最初に自分が書いたコードがあまりにもきもいことが分かったので公開してみる。 …
やねう先生のところで読んだので、少し頑張ってみたら20Bになった。ループを使うのをやめて、PUSH/JMPすれば'He'をジャンプの飛び先にできそうだったので、 その方針で作ってみたのだが、いくつかの諸事情によりHello, world!は逆順に配置することになった。…
ってのが、id:mame っちのところにあったので似非実装 char code[1024]; char input[1024]; struct V { #define REEVAL 0 #define RETURN 1 #define COMPLETE 2 int state; int value; }; /* * ret_step ステップ実行した後の * ret_cursor の値を返す。 */ …
NHKのポアンカレ予想の番組見て思ったんだけど、これ一般人が見たら、数学屋が思ってる丸い対象とは違ったものを想像するよね。宇宙がリンゴみたいな形をしてるか、ドーナツみたいな形をしてるかを考えてるような誤解を与えるけど、正確に地球の形の例えと宇…
しりとりで しょうぶじゃーっ！ わしから いくぞ！ 「エアーマンがたおせない」じゃっ！ 「い」ではじまるのは どれだ画像協力 id:Alhambra。ネタを出したら一晩で作ってくれました。
ゴルフの逆問題というネタがふっとでてきたので、適当に作って適当にあなごるに追加してみた。 brainf*ckとbefungeのどちらを問題にするかで悩んだが、結局befungeになった。最初の目標は、なんだかよく分からない入力と結果とBefungeだと十数バイトで解ける…
数セミの問題を見せてもらったのだが、帰りの電車で脳内17両まで減らした。帰ってから16両まで減らしたが、インタープリタがないのでテストできない。15って無理な気がする。とかやってたら、まめっちが15にした。漏れもなった。これ以上は無理。
DNAの構文でなぜかIFだけが3-acidになっている。 そして、DNAを解析してて気づくのはIF命令は常に「IFF」の形で始まることだ。 ほかに「IF」が入る命令は「IIF」しかないが、これもまったく使われていない。等価な「IIC」だけだ。コード以外のデータ構造では…
20日 dna2rnaをRubyで書く。遅くてバギーで話にならん。 21日 日が変わったころにドキュメントの最後にプレフィックス例が載ってたのに気づく。実行してみるが真っ黒。朝になって、直線の描画にバグがあることに気づく。やっと、テスト画面が表示される。 dn…
shinhさんのBrainstuck(id:shinichiro_h:20070714#1184371977)でBrainf*ckを実装する方法を思いついたのだが、書く時間がない。 以下アイデア 必要なBFのセルは1ステップ実行するごとに最大で一個しか増えないので、1ステップ実行するごとにスタック上のBFの…
一郎二郎三郎の三兄弟がいました。以下から彼らの年齢を当ててください。 一郎 「私は20歳だけど、三男は25歳だと勘違いしてるよ。勘違いしてるのは三男だけだよ。」 二郎 「一郎とは6歳離れていて、長男は5歳鯖をよんでるよ。鯖を読んでるのは長男だけだよ…
http://dev.rubyonrails.org/ticket/8642Rails と SQLite 使ってて BusyException で死んだまま復活しなければこれ。 ほかのDBでも起こりうると思うけど。
なんかλ計算みたいになってきた… &\v v$|&&4:! ;; [G] G=(stdio, print_int, fact, 4) ============================================== print_int n r ============================================== v|>&\:?v ;; [G', G, stdio, print_int, fact, 4] !:|…
を思いついたわけだ。フレームはチャンネルにメッセージとして保存する。チャンネルごとに１フレーム、１メッセージとする。メッセージ(=フレーム=チャネル)のフォーマットは Γ' = (Γ, v1, v2, v3, …, vn, n+2)ここで、Γはひとつ上のフレームを保存したチャ…
pefungeのGはスタックの奥底に眠ってる値をトップにコピーする命令だ。pefunge自身でGを実装しようとしたときに何が問題になるかというと、スタックの先頭二つしか入れ替えられないことだ。深さnから値を取り出す関数が呼び出された直後のスタックは […,v3, …
http://as305.dyndns.org/wiki/index.php?Coq
http://d.hatena.ne.jp/ku-ma-me/20070529/で「G」はなくてもPefungeで記述できるので無駄ではないかとまめにいったら、 スタックの先頭しか入れ替えられないので、無理ではないかというので、 とりあえず画期的な方法で実装してみる。 "Hello, world!" v ge…
なんかいろんな言語で FizzBuzz が書かれているようなので、Coq でも書いてみる。Coq の FizzBuzz は他のとは一味違う！なんとプログラムが正しく動くことが証明できるのだ！とりあえず、書いたプログラム Require Import Arith. Require Import List. (* Fi…
方程式の解のことを根と呼ぶ人々がいる。 昔はそう習ったんだから、そのように呼ぶ人が残っていることはしかたのないことだ。微分方程式の解のことを根と呼ぶ人はいない。何か不思議な語感があって、これは根とは呼ばないっぽい。 方程式の解のうちで根と呼…
VC++が定数による除算を乗算に変換する最適化をしてるのは、吐いたコードを見たことある人なら知ってることだと思うけど、なんとなくhttp://www.wikihouse.com/x86clocker/index.php?plugin=attach&refer=%B2%E1%B5%EE%A5%ED%A5%B0&openfile=x86%CC%BF%CE%E1…
δ-reduction δ-reduction は変数をその定義で置き換える。まず何か定義して、 Coq < Definition hoge := fun x:nat => 2+x. hoge is definedcbvを実行してみる。 Coq < Eval cbv delta [hoge] in (hoge 3). = (fun x : nat => 2 + x) 3 : natこの場合は「hog…
change term ゴールとtermが変換可能なときに、ゴールをtermで置き換える tacic。simpl とかを適当に使った結果、やりすぎていらんとこまで置き換えてしまった場合とか、逆に何をどう使えばもっと簡単に置き換えることができるのか分からない場合に使うとよ…
assert form ゴールを直接の証明が簡単には書けないので、とりあえず簡単に証明できる中間結果を教えるtactic。 ringとかomegaで一発で証明するには複雑すぎるときに、問題を二つに分けるとよいことがある。中間結果 form を指定すると、サブゴールにformが…
Coq in a Hurryの練習問題の一番最後。 とすると であるから、となる正の整数の組のなかで、最小のをとってくる。 すると、であるから。これは矛盾であり２の平方根が有理数でないことの証明になっている。 この証明をCoqを使って書け。 これはとてつもなく…
assumption この tactic は忘れてもよい。仮定の中に結論と一致しているものがある場合に使うと一発で証明が終わる。でも、auto を使えば同じことができる。 intro この tactic はチュートリアルで普通に理解できる以上の機能はない。 結論が「forall x:T, U…
Coqでの証明はtacticと呼ばれるコマンドを並べて次々に実行ことによって行われる。 このtacticの語彙が多いほど証明の記述は楽になる。 しかし、語彙を増やすようなドキュメントはオンラインに見つからないので、書きやすいところから書いてみる。 exact ter…
久しぶりに行った神保町で、前原昭二著「数学基礎論入門」なる本を1000円で買ってきた。 不完全性定理の証明にゲーデルの論文をほぼそのまま使っているのがこの本のポイント。 今までまじめに不完全性定理の証明なんて読んだことなかったので、まじめに読ん…
Coqにおける等号は「Leibniz Equality」というもので、 (forall P: Prop, P x -> P y) <-> x = y.つまり「任意の命題に関して、同じ結論を与えるなら二つは等しい」というのが等しいの定義らしい。等しくないことを示すにはどうすればよいかというと、結果が…
メイドさんに教わったCoqというものをマニュアルと格闘しながら理解したつもり。 Variables A B : PropA と B は命題だよ。 Theorem mp : (A->B)->A->B. auto. Qed.modus ponens ぐらいは自動で証明できるよ。 Variable p : A->B. Variable a : A.なぜか知ら…
