昨夜からずっと本を読んでいます。そういえば「論理学をつくる」を読みおわりました。二階の言語！でもコンパクト性も完全性もないらしいです。えー。
ところで一階二階と来たらじゃあ三階はどうなんですかと思うのは自然だと思うのですが、"third-order logic also quantifies over sets of sets"みたいな記述があったけどピンときません。たとえば述語の述語を量化できる、とかでしょうか。述語の述語って？
あとは「仁義なきキリスト教史」を読みました。宗教にまつわる概念を全部ヤクザの話にする話。メチャおもしろかったけど、べつにキリスト教史の知識が深まった感じではないです（当然ではある）。このあたりの話、アウトラインくらいはちゃんと知っておきたいんだけどねー。世界史も勉強しようかしら。ただああいういろんなひとが同時並行していろんなことをやっているお話、たぶん苦手なのよね。しかもみんなそれぞれ違う目的を持っているのに相互作用するから。これがプログラミングだったら専用のキュー作って他とは相互作用しないようにするんだけど……。
お昼から仕事。エフェクトをごにょごにょ。説得力あるアニメイションの作りかたみたいなの、ちょっとずつ道具が集まってきたけど、まださっぱりわからない。こういうのの専門家に弟子入りしたい思いがある。
あと結局CollectionViewのself-sizing cellsは壊れているのでしょうか。なんかAutoLayout絡みの警告がガンガン出るのはいいとしても、estimatedSizeの分しかセルが配置されてない？っぽいし、配置されたセルも位置が変だし、だめっぽい。はー、TableViewのほうはそんなことないのかしら。がっかりです。
クリプキは17歳の高校生で様相論理の意味論を完成したそうです。高校生って。プラネタリウムじゃないんだから。（高校生くらいが部活動で作りそうだな～という意図です）
導入する公理の種類が適用可能なフレームの構造と対応するなんて、なんてステキなんでしょう、と思いました。でも、このフレームって概念、直感的な「可能世界」みたいな概念をあんまり反映はしていない気がする。これは僕の知っているものじゃない。じゃあいったい何なんだ。
まあ、古典命題論理がそうであった（たとえば「→」とか）ように、これもそういう模型でしかない、のではあるけれど。公理系がいろいろあるのもそういう事情を反映していそう。たまたま用語が日常語に由来しているというだけで、これはまったく別の記述力を持っていると考えるべき。「◇□Ｐ→□Ｐ」とかちょっと戸惑うし。「（Ｐは必然的である）可能性がある ならば Ｐは必然的である」？？そんなことあるめえよ。僕が勘違いしているのか？
論理学って、要するにある構文の持つ構造を調べたり、それがどういう意味論とぴったり重なるかを調べたりする、みたいな学問なのかしらね、と思いました。たとえば時相論理というやつがあって、これはシステムの検証なんかで依存関係を記述する方法として利用されているらしいのだけど、つまり、ある文法で書ける文字列全体の構造、曖昧さや矛盾が生じないこと、そしてそれに対して適切な意味をつねに与えることができること、なんかを論理学がきちんと調べて保証する、みたいな話なのかな、みたいな。ぜんぜん調べないで言ってますけど。
お昼から仕事。昨夜はまあまあ普通の時間に眠ったはずなのだけど朝がつらかったです。なんでだろ。はー。
仕事はまあまあ。SwiftはKVCに完全には対応していない？のかCoreAnimationでゴニョゴニョするのがうまくゆかなくて難儀しました。とりあえず使えそうなものにはなったけれど、正解とは言えなさそうな感じです。というかCoreAnimation難しい。
あと上長と評価面談をしました。androidとかもちゃんとやったほうが将来性はあるんじゃないかなーとかそういう話をしました。まあ世界的なシェア的にはそうよね。一方で、リッチなものを作ろうとか、ちゃんと有料／課金アプリでお金を稼ごうという戦術ならばiPhoneのが客層的に合ってるのかも、とかも。僕にはよくわからないけれど。androidなー、ただちゃんと戦えるレベルまで習得するのにどれだけかかるかって話と、二兎を追い続けることのコストを考えるとなーとか。サーバ・サイドという手もある。
そういえば上長に「コミュニケイション能力は普通にある」と言われてびっくりしました。まあ、そう言われてみると、必要な場面でちゃんと説明をしたり確認をとったり、みたいなことは普通くらいにはできているのでしょう。僕としてはあんまり自然にできているとは思わないけれど、無難にできているならなによりです。でも人見知りがひどくってねえ。
あと、もっと根本的なところで他人とうまくやってゆく能力が低いと感じてもいますが、まあ会社ではべつにそんな能力いらないしな。ただ孤独ってだけで。
さて、明日は金曜日なのでそれが終わったら土日です。うーん、火曜日が休みってのはあんまりいいことがない気がする。月曜日が二度来たみたいな気分になるもんな。そのあと三日で休みなのはいいけどさ。
昨晩は寝る前にちょっとだけ仕事するかーと思ったのだけど予想外に時間が掛かってしまって六時前くらいまで起きていました。はー、そういうことすると翌日ほんとうにつらいから（これは最近そうなってきた感じがするので加齢を感じます）よしなよって言ってくれるお姉ちゃんが必要（？）
やりたかったことはできたのでよかったのだけど、どうもUIViewのスナップショットを何度も撮るとCAMediaCurrentTimeがドンドン遅れてゆくらしい？バグ？っぽい？ものを踏みました。なんだこれ。afterScreenUpdateをfalseにすると起こらないんだけど。これのせいでCAAnimationにディレイをかける定石通りのコードがドンドン遅れてゆくことになってしまって難儀しました。仕方がないのでdispatch_afterでディレイを表現したのだけど、大丈夫なのかしらこれ。
ところで仕事はほんとうにつらかったです。夕方くらいが特に。うーん、やる気スイッチが押されるタイミングをちゃんと制御しないとなー。
髪が乾いたら眠ります。それまでは「論理学をつくる」。
昨日話していて思ったけど、僕は大学でもっと違ったサークルに入ればよかったのだろうか。僕のいたところは凄いひとが勝手に凄いことやってるみたいな感じっぽくてあんまり指導的立場の人とかいなかったから（毎週集まっておしゃべりしてラーメン食べてた印象しかない）、僕みたいな受け身の人間にとってはあまりいいことなかったのかも。うーん、でもなんかそんなに積極的になにかやりたい、なんて思ってなかったし、仕方ないのかも。
どうせならもっと大学生っぽいことをすればよかった、とすこし思います。弓道とか（そんなに大学生っぽいか？）。大学時代○○やってたんですよ～、みたいな話、僕にはなにも話すことがないな、と思うとすこしさびしい。大学時代なにやってたっけ。勉強はちょっとはしたけど、いま思うとぜんぜんしてなかったよな。うーむ。
お昼に起きて大富豪をするオフにゆきました。四時間半ほどずっと大富豪をして、大富豪には強い弱いの差がちゃんとあることと、僕はどうやらものすごく弱いらしいことがわかりました（圧倒的に独り負けしたのです）。なんだそれ、がっかりだ！学びをシェアします！
とはいえ楽しかったのですけども。今度やるときはもうちょっと戦術をちゃんと考えたい（考えない）。
その後はご飯を食べて喫茶店でだらだら話をしました。なんかこういうオフ会然としたオフ会ってかなりひさびさのような気がする。深井さんとかとだとなんかいつものメンバ感あるし。
さて、なんか早く帰ってきたら仕事でもしようかと思っていたけど今夜はもう無理ですね。うーん、画面遷移エフェクト。
めも：意味論の側から作った真理概念と、構文論の側から作った真理概念（これは構文論的には真理とは呼ばれないけれど）とがうまく整合するかというのはまったく自明なことではないし、実際に公理系をテキトーに作るとだめなんだけど、それがぴったりと覆い被さるというのが、公理系が健全だったり完全だったりするということ、のようだ。たとえば、日常用語を使った雑な推論（たとえば「逆にアリだよね～」みたいな）では、用いられている公理系（特に推論規則）が健全ではないために、トートロジーではないものが出てきてしまう、ということなのだろう。だから、どういった推論が健全な公理系を作るかについて調べておくことは重要だ。
お昼から仕事。UIをごにょごにょ。CollectionViewのセルをtransformで調整するのは比較的うまく動いてくれました。これでセルのサイズが変化しても間隔を比較的一定に保ってくれる（しかもレイアウトを変えずに）。一次近似？でもだいぶうまく動いてくれたので高次の補正項はとりあえず要らなさそうです。やったね。
あとは会社のいろんな人に紙芝居を触ってもらって意見を聞きました。コンセプトの伝わりづらさはすでにわかっていたけど、だいぶ具体的な欠陥が見えてきたかも。ただこっからどのくらい方針転換できるのかなーとは。
よいアプリを作るのはむつかしいですね。特にこんなふうに最終的な目標が遠い場所にあるときには。（たとえばTwitterクライアントを作る、とかだったらTwitterが使えることが目標だってみんなわかってるから悩むことなんてほとんどないし、ちょっとくらい変化球を出してもユーザはそれをどう使えばいいのかうまく考えてくれると思われる）
さて、明日はオフ会です。ひさしぶりのような気がするけどそうでもないのか。
「論理学をつくる」第II部まで読みました。なるほど、ここまでは真理値割り当てやモデルとアサインメントを使って式の集合に意味を与えて妥当性を判断するということをしていたけど、そんなことしなくても純粋に構文規則だけで論証することもできるよね、というのが昔大学で教わった自然演繹なのね。大学の記号論理学は自然演繹ばかりやっていたっけ。
そういえば朝起きたらATOK for iOSが出ていたので寝ぼけ眼で入れました。四年越しの悲願叶ったりということで大喜びだったのだけど、現時点ではちょっと微妙です。互換モードのアプリでレイアウトが崩れるのは単なる不具合なのでもう修正版が申請されてることと思いますが（知らないけど）、未確定文字列がキーボード内にしか出せないのはOSの制限らしい？のでしばらくは直らなさそう。それは慣れるまではつらそうだし慣れられるかどうかもまったく非自明だなと思います。うーむ。
というか、僕がほしいのはキーボードじゃなくてIMEなんだけど、appleさんはそのあたりどうお考えなのかしら。標準の日本語変換はほんとうに悲惨なのだけど。
起きてぼんやりしてたらiPhone6が届きました。うーん、やっぱり大きいや。文字入力はちょっと慣れたらできるようになったけど。ここからどんな感じで手に馴染んでゆくのだろうか。
「今回は新しいユーザ体験がない」みたいな批判をけっこう目にするけど、僕はそんなものなくても数字上のスペックが良くなってくれればぜんぜん満足だし、もしそんなもののために大型化したのだったらほんと勘弁してくれとは思う。でもこういうのっておじいさんって感じだな。どんどんおじいさんになってゆくよ。
ひとしきり遊んだあとは電器屋に行ってケースとフィルムを買いました。ケースはいつもそうしているようにシリコン（シリコーン？）のふにょんふにょんしたやつにしたのだけど、これ系ってもしかしてあまり人気がないのかしら。並んでいるものはどれも硬かったり大きかったりで、探すのに苦労しました。このシリーズ一つしかなかったんじゃないかな。まあ、満足できるものだったのでよかった。
あと保護フィルム。保護というよりは指の滑りがよくなることを期待してのことですが。BUFFALOが出してるやつが、特製アプリで画面に目印を出して位置合わせを簡単にする仕組みになっていて、なるほど画期的だと思ってそれにしました。貼ってみたらたしかに位置合わせがとても簡単でよかったのだけど、大きさが液晶領域ギリギリなせいで、斜めから見ると境界の線が見えるし、パンジェスチャで指が引っかかります。うーん、それはちょっと微妙だな。しばらく使って慣れればいいのだけど。
明日は仕事。UI微調整。あとそろそろiPhone6/6+でのテストをしておきたいかな。
明後日は休み？らしいけど大富豪で遊ぶオフ会に参加します。お酒の飲める店でトランプゲーム、それはポーカーじゃないのか。ポーカーのルール知らないけど。じゃあこの知識はなんなんだ？ん？
昨晩ふと思い立って「ゲージ場の量子論」を読み始めました。買うだけ買って最初３ページくらい読んでほったらかしてたやつです。いきなり難しい。リー代数の言葉、昔々にちょっとだけ勉強したはずなのですが当然頭からすっかり流失しており厳しい。でもずっと昔このあたりのことを勉強したとき（学部四年かな）よりはいろいろの気分がわかった気がする。要するに場がローレンツ変換に対して線型変換を受けることを要請するならばその変換行列はローレンツ群のＮ次元表現になって、そのあり得る姿は表現論から導かれ、とにかく二種類の角運動量代数と関係づけられて、ここからまず二種類の２成分スピノル場が現れる。これらの量を適切に合成するとスカラー場とベクトル場が現れる。もっと高次元の場についてもスピノルとベクトルの合成だと思うことができる。
んだけど、μνで書かれる0123添字が空間の次元４に対応するのかベクトル場の次元４に対応するのか（無論ベクトル場は空間の次元数と一致するからベクトルと呼ばれるわけだけど、いま扱っている議論はベクトル場だから0123なのかスピノル場であっても空間の次元によって0123なのか、というところがよくわからなくなる）こんがらがってしまうことがときどきあって難儀しました。まあ、そこまで拘る必要のあるところでもないかもしれないけれど。
そういえば「論理学をつくる」も読んでいます。述語論理のセマンティクスとか。
朝起きるとSoftbankからiPhone6の本申し込みの案内が来ていたので申し込みました。到着は21日ごろのようです。ちょっと遅くないかね。
お昼から仕事。会社には検証用のiPhone6/6+が届いたので触ったり。やっぱり6+は大きすぎると思ったけど、6も想像していたほど手に馴染まなくて、そんなら潔く片手持ちなんか諦めて6+にしたらよかったじゃない、と思った。そういう賭けになることはわかっていたけれど。
まあでも、文字入力については6でもちょっと慣れれば片手でできそうなので、よかったと思っておきます。ふうむ。
UICollectionViewFlowLayoutのセルのサイズをスクロール位置に応じて変動させるのってどうやればいいんでしょうね。Transformでスケール変えるだけだと隙間が開いたり閉じたりして見栄え悪いので、レイアウト自体やりなおさないとだめだと思うのだけど。ここにさらにUIKit Dynamicsでばいんばいん動く効果もあるから、レイアウトだけ変えてもBehaviorのアンカーを移さなくちゃいけないし。となるとBehaviorの再利用も必要になるのか？それは一日仕事になりそうだ……
あとはまあTransformでスケールだけじゃなくて位置もちょっとずらしてやれば、上下との隙間が等しくなって見栄えは向上するだろうか、とかも。当たり判定とかそれで大丈夫なんだっけ。
まあ拘るのは後でしょうけど。
「ブラインドサイト」読みました。いろいろのアイデアはとてもおもしろかったけど、全体としてはそれほど、な感じ。あと巻末の参考文献がとてもおもしろかった。
自分より自分の無意識のほうが頭がいい、みたいなのはだいぶ前から思っていて、たとえば自分で考えたことより口が勝手にしゃべったようなことのほうが気が利いてておもしろい、みたいなことがよくあるのだけど、でもそれじゃいけなくて、制御できなきゃ道具として三流だよな、とも思う。無意識に染みついた反射だけでは動機が不足している。それも人類の進化が足りてないのかもしれないけど。
追記：いやいや、その「制御」ってのがそもそも遅れてるわけだ。だから批判はもう片方の「反射だけでは動機が足らない」だけになる。もっとも、それが生存に役に立ったかは別問題だし、淘汰される可能性だってぜんぜんあっただろう。すべての生物種は「まだ淘汰されていない」にすぎない、という指摘はその通りだと思う（だから現在の生物を自然淘汰で説明する議論にはちょっと抵抗がある）。
ただ、ひとつの生物種が宇宙に進出しようと思うほどこの世界の淘汰圧？は強くない、あるいはそれには時間が掛かりすぎるのではないかと思う。向こう側から侵略されない限り、重力に逆らって播種する進化は起こらないのではないかな。そしてそれを（おそらく無駄に）可能にしたのは人類の持ってるこれなんじゃないだろうか。
書き忘れ：無意識の計算が幻覚という形で意識に割り込んでくる、というのは「探偵という病気」のアイデアよね。これの話ここでしてないかもしれないけど。
にゃーにゃーねこにゃー。
お昼から仕事。ちょっと会議多め。デザイナさんとの打ち合わせで全体的なインタラクションの雰囲気を相談させてもらったりしました。アニメイションはまず作ってナンボという話だと思うのだけど、手軽にアニメイションを作る技術がないのでできません（習得している余裕もないし）。そういうのを試作する専門職みたいなのがあってもいいのかなと思いました。
あと社内の人にプロトタイプ紙芝居を見せて反応を見たり。画面がシンプルなせいでコンセプトが伝わりづらいです。そこはUIがもっと雰囲気作って誘導してやらないといけないのかなーとか。あとフロー自体の見直しとか。スケジュールがまた延びそうだ。
あとはAPI叩いたりしていました。責任をモデルのほうに分散させようかなともちょっと思ったけど、いまいち完成予想図が見えてこないので結局当座はマネジャに集約する感じにしました。これこのまま固定されるんだろうなーと思いつつ。まあその方がいいならそれでいいんだけど。
そういえばiOS8が来ましたね。僕は結局まだアップデートしていません。iPhone6がもうすぐ手に入るし、一度上げると戻せない（もしかしたら会社に検証端末として売るかもしれないし、そしたらiOS7のがありがたがられる可能性がある）のでちょっと慎重に。
iPhone6/6+も会社の検証用はAppleStoreから発送されたらしく明日には届きそうですが、僕が個人的にSoftbankで予約したものはどうなったのかしら。いまのところ連絡ないけれど。