2012年11月

というか作業日？　数の暴力にて作業が捗る．実装班の能力が微妙に足りない気がしたけど．

閑話休題．

かつおのたたきを食べて体力回復．ただし灰を吸い込んでダメージ増．つーか，呼吸が辛い．

風邪を引いた状態で飛行機に乗ると地獄を見るの罠．客室の気圧変化の少ない飛行機がいいなぁ．

ルール上は破棄できないので場所代だけ掛かりまくるゴミ未満の物体でしか無い．

さてどう処理したものか．いや，処理できないのだけど．

閑話休題．

そうか，借りてる扱いなら返却が可能なはずか．

もう一箱買ってくるか？　

閑話休題．

暖房は来週からか……

寒い図書室で本の仕分けを……　どう考えても風は悪化するしかない．

きのう飛行機を待っている頃から何かおかしいなぁと思っていたら，一気に風邪の症状が出た．全然認識していなかったのだけど大分体力を消耗してたらしい．アホみたいにいい天気なのに出かけられん……

蒲生田岬からR55を下りつつ途中で睡眠を取り室戸岬に行って日の出を拝んだ．まあ，天気悪くて残念だったのだけど．

とりあえずススキの季節だねぇ．

ちなみに室戸岬は完全に観光地化されているので他の４箇所の岬と違って訪れるのに何の苦もない．

んで，そのままR55を室戸岬で折り返して北上し，高知を経由してR32を登って大歩危小歩危の辺りを眺めてきた．やっぱちょっと遅かったのかなぁと思いつつ，混みすぎているので大歩危小歩危は素通りし祖谷渓は道が狭そうなので回避し適当にそこらの道の駅で見つけた紅葉を撮るとかいうヘタレ進行．

とりあえずR32は走りやすいしワインディングがよろしい感じ．バイクも沢山いた気がする．

閑話休題．

昨日今日でトータル 1167km の旅になった．ヴィッツの排気量 1L のを借りたのだけど（初代の後期型か？），ガソリン消費量が 57リットル弱で燃費が 20.5km/L ほど．同様に未明から昼間にかけて高速とか山とかを走ったアクアが25.4km/Lだったのを考えると，ハイブリッドカーにしてもガソリン代が 20% 程度減るだけなのね……　本体価格の差を燃料費で回収するのは無理だな．街中だけを乗った場合にどの程度の差になるかわからんが．

閑話休題．

GPSのトラックデータのログ領域が溢れて最初の100キロほどのデータが上書きされてた……　どうも SDカードでなく内部のメモリ領域にログを保存する設定になってたっぽい？　　

あと１往復飛行機に乗ればゴールドになるから……　とかいう理由で高知に飛び，車を借りて四端に行ってみた．

最初は南端の足摺岬（駐車場）．

高知のホテルを3時間ほど寝ただけでチェックアウトし，R56→R321→r348と雨の中を走って日の出前に到着．いつの間にか雨上がってた．とりあえず，車の運転技能的にここが一番簡単だった．

足摺岬の展望台より灯台を眺める．面倒だし先は長いので灯台には行かなかった．

ついでに展望台の石碑．

次に西端の佐多岬（灯台）．

昼頃？　たぶん，r348→R321→R56→R197→r256というルートだったと思う．とりあえず灯台に至る最後の10キロほどの道が狭くて大変だった．幸いにしてすれ違いできずにバックしたのは1回だけだったけど．行くのは３番目に簡単（２番めに面倒）だと思う．

改めて地図で見ると端っこだなぁと実感できる．

どうでもいいけど駐車場から灯台までの道で見かけた青い岩に黄色い花が印象的だった．

次に北端の竹居岬（竹居観音岬？）．

高速使っても日没には間に合わなかった．r256→R197→松山自動車道→R11→r36というルートのはず．佐多岬に比べれば行きやすいが，この時計というかオブジェが有るところへは竹居観音岬の看板のあるところからかなりの急坂を降らなければならずちと怖い．降りた先に駐車場があるのだけど，日和って道なりに峠を降りたところに車を止めて歩いて行った．とりあえず２番目に簡単だと思う．

最後に東端の蒲生田岬（駐車場）．

夜の９時を過ぎて真っ暗な状況で到着．r36→R11→高松自動車道→R55→r26→r200とかでアプローチ．とりあえず四端の中で最も行きにくい場所だった．例により最後の10キロが……　二輪とのすれ違いもできないような狭い場所がチラホラあって，しかもちょっと長い上にクネクネしてて先が読めないところがあったり．対向車来ませんようにとか祈りながら進んだ．まあ，幸いにして夜遅かったので対向車ゼロだったけど．つか，次にここに来るなら２輪だな．

ちなみに灯台は工事中だとかで，長い階段を登って灯台に行ってみたのだけど防音シート？で囲われててよく見えなかった．階段から灯台を挟んで反対側の斜面（木道）を下ると，振り出しに戻る．

閑話休題．

とりあえず四国の四端は１日あれば回れることが確かめられた．夏なら日のあるうちに全部を回れるかもしれない．

不要になったサーバとかを廃棄手続きのためにちょっと移動したら，手が真っ黒．服も真っ黒．

つーかこのホコリはどこから入り込んだんだか．室内においてあったのにあんなに汚くなるとか訳わからん．

閑話休題．

空港も飛行機も混んでるなぁ．明日から連休だからか？

とりあえず保険証は山登り装備の中に入ってた．そういや富士山に持ってった後にいつもの場所に戻した記憶がない．アホだ．

閑話休題．

今日も今日とて探しもの．色々とめんどくさい．つか，備品管理シールを重たい物体の底面に貼ったのは何処のどいつだ？

閑話休題．

ワイン鍋ってググると結構引っかかるのね．安全なレシピが手に入りそうで一安心．

カード型に切り替わるそうで，事務で古いのと交換してねと連絡が来たのだけど……　夏のはじめに病院に行った時に使ったことは覚えているがそのあとにどこへやったかわからない．

基本的に普段は身に着けていたのだけど，海外出張で無くすと困るからとどこかに仕舞ったような？　それでいて何処にあるかわからないとか本末転倒．ゴタゴタしてて変なところに入り込んだかなぁ．

なんとなく色々と面倒な気配．

うん，まあ，１週間前から分かっていたことだけど．どうも中途半端な状態から回復するってのが無理らしく一度くたばってからでないと回復出来ないらしい．

週末に乗る飛行機が怖い．

閑話休題．

とりあえず蜜柑を箱買い．

トヨタレンタリースで借りて400キロほど高速と街中と山道と細い路地とを走ってきた．

感想：ハイブリッドシステムインジケーターが気になりすぎてメリハリのある運転ができない．

ちゃんと加速しようと思うとすぐに赤いパワーゾーンに突っ込むし．つか，山道のぼれない．平地でもまったりすぎる……　まあ，そのおかげか燃費は 25.4km/L とかで CB400SF よか低燃費なのはすごいのだけど．あのインジケーターにどの程度支配されるべきなのかがよく分からん．

ちなみにインジケーターを気にせずアクセル踏み込めばちゃんと加速してくれる．燃費がどうなるかは知らんけど．

あとは後ろが見にくい……　バックモニター必須？

閑話休題．

4輪ペーパードライバー歴10年超えでもぶっつけ本番で大丈夫なことが判明．最初の駐車で中心から右に10cmくらいずれてたのはご愛嬌．

車だと，外気温四捨五入で0度の山に行っても寒くないし，荷物たくさん持っていけるし，途中で休憩（睡眠）できるし，こけないし，メリットが沢山．デメリットは高速を走るのがつまらないことと路地からの脱出が面倒なことか？

うーん……　惰性？

寒いのに暖房故障中で研究室が寒い．じっと集中して作業していると，気づけば手が白くなっている程度に寒い．マジでこたつがほしい．

とりあえず１２月まで直らないらしいので暖房が入る前に絶対に風邪をひくと思われる．

寝る前に一仕事終えるかとか思って取り掛かったら夜が明けていたでござる．というか昼前？

まだ微妙に時差ぼけてるのかもしれない．

三井住友も楽天も半年以上前の明細をWEBサービスから取得できるのに，UFJというかMUFGカードのWEBサービスでは２ヶ月前までしか取れない．「WEB明細サービス」というのを使っていても，毎月の紙面の明細が無くなる＆メールでWEBの明細を見ろと連絡が来るだけで，オンラインで取得できる情報の範囲はサービスを申し込んでない場合と同じ過去２ヶ月のみ．この事実はサービスの説明ページに書いてあることで前から知っていたことなのだけど，いざ過去の明細が必要になってみると僅か２ヶ月前までってのは（他社と比べて）サービス悪いなと思う．名が体を表してない（「明細確認メール通知サービス」ってんなら名は体を表しているが）．

ということで，過去の明細の再発行を電話で依頼．カード番号の確認やら生年月日や住所の確認やらを口頭で行わなきゃならん上に，発行まで１週間から１０日かかるのだとか．いろいろ面倒．

まあ，毎月ちゃんと明細をダウンロードしにいけばいいだけの話なのかも知れないけれど．

閑話休題．

キャッシュカードの再発行手続きに行ってきた．でもお届けは郵送で１週間とかかかるらしい orz　

緊急で処理しなければならないことを片付けて一日終わった……

今日が特に気温が高いってのもあるけれど，暑い……

そして手持ちの現金が少ない……　キャッシュカードを取り出したら割れてた……

とりあえず修学旅行に巻き込まれてチェックインにも時間を食う始末．駅でも５分遅れで電車を逃し２時間足止めとか．

色々とタイミングが悪い．

シンクとかレンジとかの掃除は楽に終わったんだけど，電気コンロ上面のガラスプレートを磨き上げるのに2時間半かかった．汚れの主な原因はフライパン：フライパン本体と縁が別パーツになっていて隙間がある → その隙間に歴代の油汚れが貯まっている → コンロにかけると熱で微妙に溶けて外側に垂れる → コンロのプレートに焼き付く → 根性入れないと落ちない．

この掃除をしておかないとキッチン掃除代15ユーロを取られるのだけど，労力的に掃除しなかったほうがお得だった気がする．まあいいか．

閑話休題．

そして気づけば右腕が筋肉痛．

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

閑話休題．

広いセミナー室に二人ほぼ会話なしで６時間ぶっ続けて証明を書き続けるとかいうことをしても敵は依然として大きいまま．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 の排熱が熱すぎるんだけど大丈夫かなぁ．

「Notification: Re-validate your email」とかいうタイトルでスパム判定もされずに下記の内容のメールが届いた．パスワード送れ系の詐欺メールは初めて受信した．

To increase your storage capacity and the functions, you are required to
reply to this mail and enter your Login ID and Password in the space
provided below due to the fact that we are about to carry out maintenance
and increment of storage capacity on our web-mail services/account within
the next 72 hours.
nbsp;
Failure to do this within 72hours will immediately render your email
account deactivated from our database.
nbsp;
FULL NAME:
E-MAIL ADDRESS:
USERNAME:
PASSWORD:
CONFIRM PASSWORD:
nbsp;
Your Account can also be verified via our Web-mail Link before the
information are sent.

送り主は「hogehoge.ac.jp E-mail Services <acct.auth@ hogehoge.ac.jp>」とかなってるのに，送り元IPはトルコ．ヘッダを見みたらトルコの大学か何かの誰かのアカウントから送られてるようなので乗っ取られたのかね．

つか，平文でパスワード書くのに confirm password のフィールドは必要なのか？

閑話休題．

何となく最近銀行とかのログイン画面のところに「うちのページでは乱数表を全入力させるとかないから気をつけて！」とかあるのが印象に残ってるのだけど，オンラインバンキングをターゲットにしたトロイの木馬とか流行ってるのか？

閑話休題．

他のプログラムに寄生して頑張るコンピュータウイルスって未だいるのかね？　○○日に発病するまで潜伏してるとか，寄生してもファイルサイズ増やさないように巧妙にできてるとか，自己複製を頑張るとか，昔のウイルスは面白みがあった気がするのだけど……　最近ウイルスと呼ばれいている悪意あるソフトウェアは技術的にもやってる事的にもつまらん気がする．ただの詐欺ツールだったりするのだから，ウイルス以外の名前で読んでほしい．

何となく低めの位置の雲の動きが速い時が多いようなきがするのだけど，山とかがない平坦な土地だからなのか？　季節的なものなのか？　日本だとそんなに頻繁に見ない気がするのだけど．よくわからん．

とりあえず天気の悪い週末が多い気がするぞ．

証明というか項というか，その構成途中に展開できないものを使ってしまうと Eval で評価して動作確認ができなくなる．んで，どの場所が展開不能なのか探り当ててそれを使わない方向で証明を書きなおし……　とかいう作業がちらほら．XX_dec 系のは動くプログラムとして使いたいけど直接プログラム書くのが面倒だから証明しちゃえとかやるとこうなる．

折衷案としては危なそうな部分は手で書いておいて細かい部分を個々に証明して埋めるってのかね．

必要最低ラインまで突貫工事で直し終えたら締切伸びた．まあ，時間に余裕が出来たことは良いことだ．……あと２日早く宣言して欲しかったなぁ．

さて，これで実装を覗く時間が出来たのでチェックを入れよう．