こういう問題が解ければ目的の問題は解けるんじゃないかしら。 ダムがいくつかあり、グループAとグループBに分かれている。 水道局がいくつかあり、各水道局はグループA, グループBそれぞれ1つずつのダムとつながっている。 グループA, Bそれぞれから3つずつ…

現代数理論理学序説 p.45 自然推論NJでは、論理記号'⊥'を含まない論理式αに至る正規な証明図に現れる論理式はαの部分論理式だけである これの証明のチャレンジしてみました。 正規な推論図であることの別定義 推論図が正規形であることは、以下で定義される…

行列と分数のための表現を使って無理に証明図を描いてみるなど \frac{\begin{matrix} \Pi_1 \\ M: \alpha \supset \beta \end{matrix} \qquad \begin{matrix} \Pi_2 \\ N: \alpha \end{matrix}}{MN: \beta}

選り分けを実装した。エントリーの総数を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 ⇒…

補助定理1.2.34(3) 任意のラムダ項Mに対して次のようなラムダ項Nが存在する M ≡α N かつ FN(N) ∩ BV(N) = ∅ 以下の二つの命題と本の中の補助定理1.2.34(3)よりも前に登場する定理を既知とする。 主張A: BV([y/x]M) = BM(M) (y ∉ BV(M)) 主張B: [z/y][y/x]M ≡…

現代数理論理学序説は今α同値をやっています。次の(本には証明の書かれていない)定理の証明が存外手間がかかったので記しておきます。 補助定理1.2.32(2) (の⇒の部分) V(λxy.MN)に属さない任意の変数zに対してλx.M ≡α λy.N ⇒ [z/x]M ≡α [z/y]N この定理は次…

3DSのソフト一覧から安いものだけを表示して、安い順にソートして、印刷用に見た目を調整するスクリプト。 検索結果を開いて、URLに&limit=1000などと追加して全件表示して、以下のスクリプトをFirebugで実行する。 function price(x) x.querySelector(".pri…

sid-searchを作り直してみた - oupoの日記で書いたFirefoxだけ劇遅というのはFirebugのコンソールパネルが起動していたからであって消してみたら別に劇遅ではなかった。今回の記事のベンチマークはそれに気づかずに書いたものであるが、ベンチマーク結果をと…

続きの記事: 線形合同法であるseedが0からいくつ進めたものかを得る その2 - oupoの日記 続きの続きの記事: 線形合同法であるseedが0からいくつ進めたものかを得る その3 (法が2のべきとは限らない一般の場合) - oupoの日記 sid-searchを作り直してみた - ou…

新バージョン: くじ番号から裏ID ローカル検索バージョン - oupoの日記 http://sid-search.digi2.jp/ ソースコード 経緯 http://oupo.xrea.jp/sid-search/で公開していたsid-searchだがこれはXREAの有料プランを使っていた。有料プランの期限が切れるという…

前回の記事の要約: N未満の非負整数を乱数を使って重複なくM個選ぶ手続きがあり、これを実行したあとの乱数列のインデックスがある特定の値になるような、開始インデックスをすべて求めるプログラムを書けという問題。これは無事に解けた。 でも、当初のきっ…

問題 次のようなN未満の非負整数を重複なくM個選ぶ手続きを考える。 擬似乱数は線形合同法とする。 つまり現在のseed値(=乱数生成機の状態変数)からひとつ前のseed値がわかることを前提とする。 def take() list = [] while list.length < M v = rand(N) if …

最近現代数理論理学序説を読み始めました。今日は体系CLwで遊びました。Lazy Kを触ったことがあったので、この体系にはどういう意図があるのかはなんとなくわかった上で進められました。 本に載っていない命題で、次のようなものを見つけて証明しました は許…

高校数学は今体積をやっている。立体図形難しいよ(>_ 青と赤の部分の面積が等しいとしてしまうミスをしたアカウントがこちらになります余談：この図はJavaScriptとCanvasを使って描きました。ちょっと楽しい https://github.com/oupo/dotfiles/blob/public/s…

数学ガールゲーデル編では表現定理の証明が省略されている 体系には足し算なんて用意されていないのにたとえばどうやって三項関係を表現するんだろうと気になる。これはだいたい予想がついた。 二項関係を表現する論理式は、が属していて任意のについてが属…

最近ゲーデルの不完全性定理の証明に登場する形式的体系で遊んでます。 数学ガール ゲーデル編を読んで以来、からが導けるという推論規則がなんであるのか、を公理とするのではだめなのか気になっていました。その疑問が解決しました。任意の論理式について…

この前の記事の図版は全部JavaScriptでdiv要素を配置させて作りました この図の波括弧の部分もCSSのborder-radiusを使って書いたりという謎の努力！上の図はこんな感じ (なぐり書きコード) blog-entry-lcg-period/image.html at master · oupo/blog-entry-lc…

先日の記事を書くときは、いちいちコピーして、編集画面を開いて貼りつけてなんてやってて面倒だったので。 自分が使うことしか考えていないので要Vimperatorfile:///dev/null?hatenadiary-forward,/path/to/entry_text.txtみたいなURLが開かれることをVimpe…

(追記)もっと簡潔な証明を得ました: 線形合同法数列が最大周期になる条件(ただし法が2のべきの場合) その2 - oupoの日記 はじめに 一部界隈の皆さんはよくご存知の線形合同法数列 (は初期シード) は最大周期となることが知られています。 すなわち, , ... と…

ベースになっているのはtrunkのリビジョン3771 diff: http://gist.github.com/587467 win32用実行バイナリ: http://oupo.xrea.jp/misc/DeSmuME-my-r3771.zip 改造箇所: PUSH_LR命令が実行されたときに呼ばれるemu.registerenterfunc 命令アドレスごとの条件…

※ いつものことですが間違っている可能性があります (通常乱数 % 100) で出てくるポケモン決定 (通常乱数 % (レベルmax - レベルmin + 1) + レベルmin) でレベル決定 先頭特性がはりきりかやるきかプレッシャーの場合、(通常乱数 % 2)が1だとレベルがレベルm…