No Such Blog or Diary

たかが結合則と分配則ごときを１日かけても証明できないとは……　なるべくプログラムの等式変換で証明しようとしているから面倒なのかね．うまい具合に述語を定義してやれば結構簡単にきそうな気配だけど．

閑話休題．

広いセミナー室に二人ほぼ会話なしで６時間ぶっ続けて証明を書き続けるとかいうことをしても敵は依然として大きいまま．Leibniz equality でなく任意の同値関係を使えるように定式化しようとすると色々な既存の資源が使えなくなるので面倒この上ない．少なくとも Proper のインスタンスを大量に用意せんと身動き取れないし．

閑話休題．

さて，帰り支度をするか．

正しく証明できた定理の上部で後から必要になったライブラリのモジュールをインポートしたら証明が破綻した．原因はライブラリ内で Obligation Tactic が上書きされててそれがグローバルに影響をもたらしてくれてるからで……　副作用ありまくりだなぁ．デフォルトが何なのかわからんが Show Obligation tactic で見る限り "Obligation Tactic := unfold complement, equiv; program_simpl." あたりっぽい？

モジュールを読み込んで泣く別のパターンとしては型クラスのインスタンスの優先度が変わってしまって implicit な引数に思ったものがハマってくれなくなるという現象が起きる．使って欲しいインスタンスを Existing Instance でトップに持ってきておけばなんとか大丈夫っぽいけれど．

色々と副作用がありまくりなので透明なライブラリとか頑健なライブラリとか気をつけないと書くことができないと理解した．

20時過ぎに作業してたら19:30で建物閉めるんだからさっさと出てけクソがと警備の人たちに追い出された．なんでやねん．カードキー持っとるので幾らでも出入りできるのに……

どうも時間外に作業するには向いていない環境な気がする．

サーチがお馬鹿すぎる．あさっての方向を向いてどんどん突き進んでいく……

どうも引数の構造が「沢山の単純なインスタンス＋それらの関係を示すインスタンス」になっていると単純な方を先にサーチしに行ってどんどんアホになるらしい．まあ，そりゃそうだろうけど．

とりあえず，単純なインスタンスを関係を示すインスタンスの奥底においてやったら頭良くなった．

閑話休題．

どっかにサーチのアルゴリズムを詳細に述べたものとかないんかな？　C++のテンプレートのサーチの方がまだ分かりやすい挙動をしてくれる気が……

なんでやねん．どうも型クラスのリゾルバが正しいインスタンスを探すのにアホなサーチをしてる気がするのだけど……　コードを綺麗にしてより般化されたのでサーチにさらに時間がかかるようになってしまった．とりあえず，型クラスのリゾルバを３時間も待った人間はそうはいまい．

余計な引数を渡すようにして無駄なサーチが走らないように縛りを入れないとダメかなぁ．ぶっちゃけ型クラスの使い方間違ってるかもね．

閑話休題．

ネタとしては笑いを取れた．

閑話休題．

お菓子の買いだめが切れたので何となく作業しづらい．スーパーはもう閉まっとるし，自販機はあるけど高いし．

そして角砂糖をそのまま食べるという手段に出る．

閑話休題．

無駄なサーチが走らないように型にタグを付けてみたり無駄なインスタンスを省いてみたりしたら15秒に縮んだ．ばんざい．

それにしても狙ったところに行かせるにはなかなか苦労するなぁ．コードも汚くなっちまうし．自由度高いので自動でやらせるのは色々としんどいのね……

ふつうのコトなのか頭おかしいのかよくわからん．Typeclass 使いまくりなのが原因だけど．i5-2540M なのでそんなに頭悪くないと思うのだけど……　まあ，C++でも template でメタプログラミングすればコンパイルに時間かかるから普通かね．

だがしかし，その定義の上部に行って何かを修正して帰ってくると泣ける．

閑話休題．

Let'snote の排熱が熱すぎるんだけど大丈夫かなぁ．