TLE 2015 だった。最初は 2/7 にやるよ！って書いてあったような気がするんだけど、いつのまにか 2/11 → 2/12 → 2/27 → 2/28 にどんどん延期されていってやばかった。そのせいか参加者少なすぎ。問題一覧はここを見るとよい http://d.hatena.ne.jp/ku-ma-me/…

初日問題だけ読んで、/myproblemsを送ってみるのを試して仕事に行く。23時ごろから作業開始。 とりあえず、JSONとかHTTPとかをCとかで書きたくないので、Rubyで適当に書いたドライバとopen3で通信するソルバ群にしようということにする。最初のソルバは「xor…

圏論で可換図式をおっかけて証明するようなときに、合成とか並べていたら読みにくくてしょうがないというのは実はみんな思ってることらしい。たまたま読んでたNorthcott「ホモロジー代数入門」に分かりやすい記法が載っていました。AとBとCを対象として、射A…

[数学] ひとりアドベントカレンダー二日目なんだか、確率とか統計とか幾何的なイメージが出てこないから難しいし、情報幾何とか先に知っておくと分かりやすくなるんじゃね。知らんけど、たぶん。確率測度の族を多様体だと思って微分幾何をやろうって話。PRML…

d次元確率変数 X が平均μ、正定値対称分散共分散行列Σ に従うときの話。直行行列PでΣを対角化して、になったときに、対角成分の平方根をとったりすると元の行列も平方根っぽいものになって、ようするににすれば当たり前だけど指数法則を満たしたりして、とす…

めんどくせー。格子点の方向にだけ光線を飛ばせばいいのはすぐにわかった。でも四角との交点の座標が有理数になる。めんどくせえー。 最初はboostの有理数ライブラリを使って、直線と直線の交点を求めたりくそ複雑なコードを書いてみたんだけど、遅すぎるう…

非常にやるきがないので適当https://gist.github.com/2391811

やるきがなくなってきたので、後の問題は適当にやった。B問題はやるだけ。https://gist.github.com/2391806

https://gist.github.com/2391779ヒントの制約からなんとか関数を自動で生成したかった。 eexists (fun ch => match ch with | "a" => _ | "b" => _ | "c" => _ | "d" => _ | "e" => _ | "f" => _ | "g" => _ | "h" => _ | "i" => _ | "j" => _ | "k" => _ |…

証明できそうな問題がないかなと探したところA問題だけだった。BとCもできるかもしれないけどめんどくさいからいいや

この記事はTheorem Proving Advent Calendar 2011の13日目の記事です。 ssreflectライブラリ紹介 この前はssreflectのtacticの紹介をやったので、ライブラリの紹介をします。ライブラリの概要は http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/ を見れ…

モナドを実行するインタープリタを書かないといけません。必要なのはaicmdを受け取って、次に実行するコマンドと残りのaicmdを返す関数です。OCaml側がその関数を順に呼び出します。とりあえずの実装なので、動くんだけど効率とかよくないし直したい。継続を…

Coqのセクションという機能を使うとグローバル変数みたいなのを使えます。 Section Hoge. Variable x : nat. Definition foo := x + 1. Definition bar := foo + 2. (* Section の中では x はグローバル変数みたいに使える *) End Hoge. (* Section を閉じる…

https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltgmonad.v二つのモナドを用意しました。cmdexモナドとaicmdモナドです。cmdexモナドは一つのスロットで実行される命令列を作ります。 putl;; zeror;; succl;; dbll;; getlこんな感じに書くと、左put…

インタープリタ https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltg.vここは急いで書いたのでバグがあるかもしれない。ただ、ここはデバッグするよりも証明したほうが早いと思う。 Inductive evalue : Set := | EValue : value -> evalue | EApp : e…

https://github.com/kik/ICFPC2011 インタープリタ ゲーム中に存在する全ての値を type value = | ValNum of int | ValI | ValSucc | ValDbl | ValGet | ValPut | ValS | ValSf of value | ValSfg of value * value | ValK | ValKx of value | ValInc | ValD…

例年のごとく一人で参加。時刻は全てUTCで 17日 00:00 問題が公開されたので読む。予想通り殴り合いゲーだ。 01:00 大体問題を理解したので、インタープリタを書き始めてみる。言語はOCamlを選択。というかこれ以外に選択肢がない 03:00 電車で会社に移動し…

https://gist.github.com/971586色々と工夫してみた。ロボットと指令の定義。これは前と同じ。 Inductive Robo : Set := Blue | Orange. Inductive Order : Set := order : Robo -> Z -> Order. Definition robo_inv (robo: Robo) := match robo with | Blue…

微妙に使いにくいじゃないですか。ssreflectを読んでたら、こういうのを簡単に Leibniz equality にする方法が分かったので書いてみた。https://gist.github.com/971135まず、ZP = Z * positive の上に普通に同値関係を定義する ZP_eq : ZP -> ZP -> Prop。…

ここまでくれば、どんな手順を渡されても、最初の一手は基本的にロボットを一歩動かすだけなので、簡単な作業になります。最初の一手は青の動かし方が４通りあって、橙の動かし方が４通りありますから全部で (coq Scripting *16 SUBGOALS* Holes)---------残…

ここまで証明できればあと少しです。初期位置の違いはゆとりポイントの初期値の違いと等価なはずです。 Lemma min_trans_1_0: forall (os: list Order) (bp op bp' op' bd:Z), Zabs bd = 1 -> exists d, Zabs d = 1 /\ min_trans bp op (bp'+bd) op' os = mi…

とりあえずロボットの初期位置をひとつだけずらした状態でmin_transを呼び出すと値が２以上減ることはないということを証明しましょう。 Lemma min_trans_le: forall (os: list Order) (bp op bp' op' bd od :Z), -1 <= bd <= 1 -> -1 <= od <= 1 -> min_tra…

状態Ａから適当に１ターン動かして状態Ｂになったとします。Ａでの結果をmin_trans(A)としてＢのときをmin_trans(B)と書くことにすると min_trans(A) ≦ min_trans(B) + 1であることを証明できれば、min_transより短い手順で解くことは出来ません。どんなにが…

これより短い手順がないことを証明するには、手順とはなにかを定義しないといけません。 Inductive Move : Set := Left | Right | Push | Stay. Inductive Moves : Set := moves : Move -> Move -> Moves.各ロボットは１ターンに４種類の行動ができて、青の…

なんとなく、押すボタンの位置を前回の位置からの相対距離で覚えておいたほうが簡単かなあと思っちゃったんですよ。で、相対位置に変更した命令の型と相対位置に変換する関数。 Inductive OrderRel : Set := orderRel : Robo -> comparison -> Z -> OrderRel…

証明することは、この関数が最小手数を返していることです。最小手数であるというのはどういうことかというと、 どんな手順でロボットを動かしても、これより短くできない手数 のことです。というのは残念ながらよくある間違いです。 ある手順でロボットを動…

起きたらすでに残り14時間とかどこかおかしい。A問題はこんなかんじ 青と橙のロボットがいます。ロボットを動かして指令通りの順番でボタンを押させます。指令は「O 2, B 1, B 2, O 4」のようにどのロボットがどのボタンを押すかの列で与えられます。各ロボ…

http://d.hatena.ne.jp/nishiohirokazu/20110217こういう話は確率の問題をどのように数学で定義しているかっていう哲学的な話が繋がってないから、数式だけ見てこれとこれの違いが分からないってことになってるんだと思う。確率は突き詰めていくと、いつかは…

COUNTI: がんばった３位 HASH: がんばったのに８位 LETTER: やる時間なかった KD: がんばった３位 ARRNG: 通しただけ８位 HEART: 遊びすぎた ODDEVEN: がんばった３位 OPTI: ひょろっと書いたモンゴメリ乗算だけでは30倍遅い こんなもん作ってないで真面目に…

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