andante

お昼から仕事。問題解決密度は高かったけど問題が多かったのであまり進みませんでした。うーむ。
画像のダウンロードの進捗管理にNSProgressを使ったのだけどまあまあ便利。複数のProgressを束ねて一つにできるのとかもよいですね。ただKVOで監視というのはちょっとどうか。Swift時代にそぐわないのではないか（とはいえ他にやりようもない）。

あとまたCoreDataとニラメッコしていました。エンティティを継承できるのはいいんだけど、FetchRequestがそれに追いついてないような感じがある。たとえばShapeエンティティを継承してCircleとTriangleを作ったときに、「Triangleまたは半径がrのCircle」みたいなPredicateはどう書けばいいのかよくわからない。具体的にはkeyPathにradiusを指定したところで失敗する（Triangleにはradiusがないから）。ううむ。

そういえば、ふと気になったので今のプロジェクトで書いたコードの量を数えさせてみたところ6400行くらいということでした。一ヶ月半くらい？でこれは多いのか少ないのかよくわからない。こんなに書いた実感もないのだけど。まあでもまあまあがんばったのかしらね。
全部自分でやると、全部自分でできるのでいろいろなしがらみに流されることなく考えられるのでよいのだけど、全部自分でやらなきゃいけないのでとってもしんどい。なにげに規模の大きいアプリだと思うし。いい経験だと思うけど、明らかに力不足っぽいところもある。はー、がんばろ。

はー、今週はなんかほんとうに飛ぶように過ぎてしまった気がします。土日もmac借りて帰って作業しようかなー。問題の数はだいぶ減ったはずで、あとはWebAPIとの繋ぎの部分を書くだけ、みたいなイメージなんだけど……。

どうも昨日くらいからまた消化器系の調子が良くないです。すごいもたれる。ウー。

お昼から仕事。またモデルにいろいろと手を入れたけどなんとかまとまってくれました。明日にはこのあたりは完成させてメイン機能に移れそう。
FetchedResultsControllerが八面六臂の活躍を見せています。便利だな、これ。いろいろと関心事が分離できるし。

デザインの思想についてちょっとおしゃべりをしました。僕は自分のことをどちらかというとミニマリストだと思っているのだけど（実際にはそもそもどこかにカテゴライズされるほどの思想がない、という点はサテオキ）、それって単に僕が複雑さをうまく扱う技術も心的リソースもないからなんだよな、とか思います。でも、僕以外の多数派の人々もそういう状態（心的リソースが足らない）なのだとしたら、それに従うことは正解と呼んでもいいような気がする。

h.b. > κ.

ついに四半世紀を生きてしまいました。四捨五入すると30です。うわっ。うわっっ。

誕生日というとどうしても内面的な節目になるし、まあ昨日の手続きのこととかもあって、この一年をちょっと総括しようかな、なんて気分になるのだけど、眠いので考えていません。
この一年、健康状態がどんどん悪化してしまったし、精神的にもなんだかいろいろなことが億劫になってしまった感じがあります。人付き合いとかそういうことのコストが。それに加えて自分自身の人格への失望や諦めが支配的になってしまって、僕はもはや他人とまっとうな人間関係を構築することなどできないしすべきでないし望むべきでもないのだ、みたいな確信めいた想いが強くなってしまった。なにもかもが面倒にしか思えないし振る舞えないのに、僕はたしかに寄り添う他者を必要としている（ほんとうに？）。なんなんだこいつは。
僕は誰かに側にいて精神を支えてほしいと思ったりするけれど、そのような関係を維持するリソースが自分には（あるとはもはや思え）ないし、そうでないように振る舞うこともできるとは思えないし、そういった相手にとって自分が魅力的であることができるとも思えないし、そういった相手がいたところで自分がほんとうに救われるとももはやあまり思えないし、そもそもそういう相手を探しに行こうとももう思えなくなっている。こういうことを考えていると、ほんとうに心の底から死んでしまいたくなる。というよりも生きるのが嫌になる。幸福になれないってわかっている人生をあと何十年も続けて、挙句みじめに他人を呪いながら死んでゆく。そんなのはとても耐えられない。頭ではそうわかっているのに、僕は死ぬこともできずにいる。仕方がない、意志決定のスコアの中で、こんな遠未来の要因に割り振られている重みなんて、きっと微々たるものなのだ。ただ遠くにあるというだけの理由で。どんなに遠くたって、それは確実に訪れるというのに。

精神と身体の健康がほしい。精神はじつは比較的充実した感じだと思っているけれど、健康的とは言えない（でも僕の精神が健康的だったことなんてあっただろうか。あったような気がする、でもそれは縋る他者がいたというだけではないのか？）。身体的には絶望的だ。運動をしなくてはいけないのだけど。

仕事は多少順調。ちょっと具合が悪かったけれど、なんとか懸念事項に目処が立った。あとはなにもかもが理想的に協働してくれればいいのだけど。

「（Ｐが）有り得る」という表現を素朴に否定した「あり得ない」は、「Ｐである可能性がない」になってしまうのだが、「Ｐでない可能性がある」を短く表現するにはどうすればいいのだろう。ここで様相論理の記法を借りると、これは「♢￢P」と書くことができて、さらに♢だか□だかの定義から「￢□￢￢P」になり、二重否定を除去して「￢□P」を得る。つまり必然性を短く言うことができればその否定で表せることになるだろう（注意しなければ□￢Pの意味になってしまうが）。
そこまでは考えたのだがそういう言いかたはよくわからなかった。古文には確述助動詞というものがあって云々とか思ったけど、作ってみて「ありなず」みたいな文字列ができたのでこれは違うと思う（そもそも語用論の前に統語論として怪しい）。というか、必然性という概念はただの断言とは趣を異にするはずで（だってそれは可能の否定という形で導入されるものだから）、対応する日本語はないのかもしれない。「あらざり得る」の方向は当然ありえる。「ない」が動詞だったらそれで済む話なのだが、あからさまに動きでもありようでもないものをどうしろと、とは思う。

そういえばF#をインストールしました。まだ触っていませんが。

昨晩は早めに眠ったはずなのですが、二時半ごろに目が覚めてしまってそれからずっと眠れませんでした。主観的には朝までほとんどずっと起きていたのだけど、アプリの推定によれば三時間くらいは眠っていたようです。ぜんぜんそんな感じしなかったけどな……。

ちょっと早めに起きて大学院の奨学金事務所にゆきました。ついでに学生証も返しました。これでもう当分はあそこに行くこともないでしょう。手続き自体はだいぶ前に終わっているけれど、なんだかすこしセンチメンタルっぽくなります。そうでもないか。ふーむ。

結局、僕は大学院に進学してもなにひとついいことがなかったなあ、と今は思います。なんだったんだろう、あれは。ちゃんと自分の進路について考えることがついにできなかった、ということが問題だったのだとは思います。あるいは、潔く学部で就職してしまえばよかったのか（そして結局そうなったわけですが）。でも就職活動なんてできなかった。こういったところは僕の欠陥が強く現れている。そしてそれを僕はどうもしなかった。いや、それはあまりにも僕の一部をなしているのではないかという恐れ。

飽きたので内省っぽい話はやめにします。19音平均律の音楽をネットで探して聴いています。

ところで仕事はめっちゃ寝不足だったのでしんどかったです。寝不足というかリズムが狂っている感じ。はー。
スケジュールがちょっと厳しそうになってきた。あとちょっと難しい問題。明日元気だったら解決できるといい。

日記書いてみて思ったけどやっぱり寝不足なのか思考がぜんぜんできません。ふらふらしている。今夜こそちゃんとねむりたい。ねむれないのは怖い。

特になにもしていません。OCamlをインストールしてぽちぽち触ったりしましたが、いまのところHaskellのがかっこいいなあと感じます。なんだってリストはセミコロン区切りなんだ、とか。IntとFloatとで演算子が違うのは、まあ一理なくもないかなーと思うけれど。（でもそもそもIntとFloatが別の型なのってそりゃ計算機側からすればそうでしょうけどって感じはするのよね。いや、精度の差もあるからやっぱりそれはそれで妥当なのか？）

そういえば、退学に伴う奨学金関係の手続きをしていないことを思い出したので、明日ちょっと行こうと思います。はー、はー。

自由よりも公共の利益が優先されるという状況は、それは自由が認められているのではなく、「役に立つから利用されている」のである。

昨夜からずっと本を読んでいます。そういえば「論理学をつくる」を読みおわりました。二階の言語！でもコンパクト性も完全性もないらしいです。えー。
ところで一階二階と来たらじゃあ三階はどうなんですかと思うのは自然だと思うのですが、"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でディレイを表現したのだけど、大丈夫なのかしらこれ。

ところで仕事はほんとうにつらかったです。夕方くらいが特に。うーん、やる気スイッチが押されるタイミングをちゃんと制御しないとなー。

髪が乾いたら眠ります。それまでは「論理学をつくる」。

昨日話していて思ったけど、僕は大学でもっと違ったサークルに入ればよかったのだろうか。僕のいたところは凄いひとが勝手に凄いことやってるみたいな感じっぽくてあんまり指導的立場の人とかいなかったから（毎週集まっておしゃべりしてラーメン食べてた印象しかない）、僕みたいな受け身の人間にとってはあまりいいことなかったのかも。うーん、でもなんかそんなに積極的になにかやりたい、なんて思ってなかったし、仕方ないのかも。
どうせならもっと大学生っぽいことをすればよかった、とすこし思います。弓道とか（そんなに大学生っぽいか？）。大学時代○○やってたんですよ～、みたいな話、僕にはなにも話すことがないな、と思うとすこしさびしい。大学時代なにやってたっけ。勉強はちょっとはしたけど、いま思うとぜんぜんしてなかったよな。うーむ。

お昼に起きて大富豪をするオフにゆきました。四時間半ほどずっと大富豪をして、大富豪には強い弱いの差がちゃんとあることと、僕はどうやらものすごく弱いらしいことがわかりました（圧倒的に独り負けしたのです）。なんだそれ、がっかりだ！学びをシェアします！
とはいえ楽しかったのですけども。今度やるときはもうちょっと戦術をちゃんと考えたい（考えない）。

その後はご飯を食べて喫茶店でだらだら話をしました。なんかこういうオフ会然としたオフ会ってかなりひさびさのような気がする。深井さんとかとだとなんかいつものメンバ感あるし。

さて、なんか早く帰ってきたら仕事でもしようかと思っていたけど今夜はもう無理ですね。うーん、画面遷移エフェクト。

めも：意味論の側から作った真理概念と、構文論の側から作った真理概念（これは構文論的には真理とは呼ばれないけれど）とがうまく整合するかというのはまったく自明なことではないし、実際に公理系をテキトーに作るとだめなんだけど、それがぴったりと覆い被さるというのが、公理系が健全だったり完全だったりするということ、のようだ。たとえば、日常用語を使った雑な推論（たとえば「逆にアリだよね～」みたいな）では、用いられている公理系（特に推論規則）が健全ではないために、トートロジーではないものが出てきてしまう、ということなのだろう。だから、どういった推論が健全な公理系を作るかについて調べておくことは重要だ。