選り分けを実装した。エントリーの総数を30, 対戦回数を4としたときナイーブ版と100個のseedで全て同じ結果になることを確認した。 ソースコード: https://github.com/oupo/factory-predictor/tree/master/simplified-version そういうわけで、 エントリーの…

前回の記事で書いた貪欲法の詳細について書きます。現在位置から先のアイテムaを規制しているゲートの番号の最小値のことをaのcaughtと呼ぶことにします。 ただしそのようなゲートがない場合はN-1を表すことにします（ゲートの番号の最大値がN-2なので）。ま…

まだ仕上がっていませんが、正しい結果かどうかの選り分けはなんとかうまくいきそうです。 選り分けは次のような問題に変換して考えることにしました。 以下のように並んだ地図がある。 shop 0, gate 0, shop 1, gate 1, ..., shop N-2, gate N-2, end 旅人…

ファクトリーの問題について考えていたと思ったら、謎の問題を考えていた。 仕事がn個あり、各仕事は時刻s_kに始まり、時刻e_kに終わる。(e_kを含む) 各仕事をm個のラインに割り当てる。 ここで1つの仕事は1つのラインで完全にやりとげなければならず、また1…

エントリーの衝突判定が種族とアイテムの二つあるのは複雑なので、衝突判定はエントリーのIDだけによるものとする という設定はそのままで、複数回の戦闘と戦闘ごとの交換を設定に入れて作ってみた。実際にはありえない結果も混じる出力を出すプログラムを作…

ずうっと前から構想していたのだけれど、バトルファクトリーで選出や交換で変わってくる7戦分の敵のパーティの全ての組み合わせを計算するプログラムを作りたいなあと考えていた。2010/2/22頃にCで愚直に全通り(6C3 * 10^5)試すプログラムを書いたのだけれど…

終わったと同時に記事に書き起こす気力があまりなくなりましたが重要な部分だけ書きます。 「束縛変数が与えられた有限集合と重なりがないようにα変換できる」を有効に活用することでなんとか証明が完成しました。 証明の中で命題を適用する際の細かい前提条…

前回の記事の要約: (A): M →1β N, M ≡α M' ⇒ M' →1β N (B): M ▷1β N ⇒ [t/s]M →1β [t/s]N という二つの命題を証明しようとしたが(A)と(B)の証明が相互依存になってしまって、それを二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法を…

そこそこ速度が必要になるプログラムを書くとき、そうはいっても今時Cは使いたくないかなーと思ったので代替になりそうな言語でベンチマークをとってみた。 今回のベンチマークに使ったのは32ビットの整数演算の実行速度が問われるMTの計算。1000000未満の各…

二つの命題が相互依存になって、二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法になってしまった。 既知とする命題 既知の命題1: λx.Q ≡α λy.Q' ⇔ Q' ≡α [y/x]Q かつ [x≡y または y ∉ FV(Q)] 既知の命題2: R' ≡α R, λy.Q' ≡α λx.Q ⇒…