比較的暖かい日。起床は7時15分、出勤してコード書き。最終日だけあってさすがに疲労の色が濃い。様相論理のsatisfactionを定義すると、terminateしないことが明らかに。進捗報告で意見を募ると、どうやらsubstitutionの処理が原因らしい。今後の課題だ。ほ…

起床は7時15分、眠い。出勤してコードスプリントの続き、昨日の問題点の修正。他に税金関係の書類を提出。 本日はエクスカーション、11時半に出発。参加者は8人（夕食時にもう一名が合流）、灘の酒蔵へ行く。 昼食を食べてから酒蔵を見学、それから試飲をす…

起床は7時15分、朝方はとても寒い。紅葉が急速に進んでいる。 9時になんとか到着、コードスプリントの続き。Ktさんの助けも借りて、変数の処理法と意味論の修正で大きな前進・・・と思ったのだが、夕方発表するとスウェーデン人コンビから盛大に突っ込まれる…

起床は7時、出勤してコードスプリント。様相論理システムの第一バージョンが完成、昼のミーティングで一部発表する。いろいろ突っ込まれる、要改善。 午後は講演会、H氏の話（項書き換え系におけるTerminasionを多項式によってinterpretationする）は面白か…

本日Ktさんから教えていただいた話、備忘のため。

9時に職場に集合。スウェーデンからのAgda開発チーム3人（タフで頭の回転が速い）を加え、合計10人程度で一週間ひたすらAgda2のコードを書き続ける。会議室にこもって一日中コーディングなんて、スーパーハカーにでもなった気分。 意見交換や成果紹介も重要…

起床は7時、眠い。慌てて出勤。急行が蛍池に止まらないことを知らず乗り過ごして、結局5分遅刻する。 20時に退所、21時半に帰宅。夕食は牡蠣クリームシチューとマカロニ。

"Mathematics in Philosophy" pp.221-251. 新幹線内で読了・・・しかし難しい。もう一回読むことに決定。

論文の改訂が進んでいないとなじられる夢を見る。起床は11時半。実家は木造で、屋内が外よりも寒い。昼食は手巻き寿司。 実家の近所は秋の気配。もみじが赤くなってきた。 16時に東京駅へ行くも、3連休の最終日のため当然新幹線の指定はとれず、結局自由席で…

起床は11時半、乾燥していて喉が痛い。実家で一日静養。西荻窪の古本屋に行き、その後夕食、両親と鰻屋に行く。CATVで「バスカビル家の犬」（BBC／2002年版）を見て、26時に寝る。

起床は8時、安宿なのでうるさく、よく眠れず。慌てて大学へ。研究集会二日目、カリー化の話が印象に残った。ほかに自作証明系やフレーゲの話まで。面白い話が多いが、二日目なので参加者の疲労度が濃い。 大学のプレゼン室、天井の蛍光灯がデジタル数字の8の…

ホテルから更新。 起床は7時、結局５時間睡眠。あわてて空港へ行き、8時55分の便で羽田に向かう。機内で爆睡。モノレール、山手線、つくばエキスプレス経由でつくばへ。定理証明系に関する研究集会に出席する。面白い話が多い。 今回はテーマ（バランスがと…

本日よりつくばに出張し、その後実家により、関西には日曜日に帰ります。したがって、次回更新は遅ければ日曜日となる予定です。ご了承ください。

18:30-21:00、参加は三人。 Ted Siderの"Reductive Theory of Modality"を読むはずだったが、今回はK氏が、論文のネタとして考えている話と、David Lewisの謎の論証について話をする。おもしろかったが、ここで紹介するわけにはいかないので略（後者だけでも…

本日Ktさんに聞いてわかったことを、備忘のためにメモ。Agda 2 でデータ型からデータ型 への関数を定義するとき、変数の束縛に関して、思いもよらないことがおこる（昨日はバグはこのせい）。 Aのデータ型は A : Nat -> A g : (n : Nat) -> ... の形をしてお…

だんだん寒くなる。起床は9時、出勤してコード書き。様相述語論理の部分で 原始述語と and の場合の処理が完了。Not の処理で型があわず、悩む。打ち合わせ後、前勤務校の源泉徴収票を電話で送ってもらうように手配してから、17時に退所。 帰宅は21時半。夕…

午前はよく晴れ、暖かい。しかし日が暮れるととても寒い。 起床は9時、最近この時間が標準になってしまった。出勤してコード書き。型チェックに何度か失敗し、その度にKtさんに泣きつく。とりあえず、やっと、暫定的に述語論理はパスするが、今度は様相論理…

朝は暖かいが、日が暮れると急に寒くなる。画像は朝の風景。朝の光が海に反射する。 起床は9時、遅め。郵便局に寄ってから出勤。コード書き、いろいろ難航する。やはり任意の自然数nについて、コンピューター上でn変数述語を用意して述語論理を展開するのは…

昨日は水曜日読書会のまとめ記事、本日は上記書類に予想外に手間取ってしまったため、「ラッセルのパラドックス」の更新は今週はお休みさせていただきます。申し訳ありませんが、お気長にお待ちいただければ幸いです。

暖かい日。起床は12時半、よく寝た。読書と論文読み。夕食は18時、貰い物のカニのトマトソースパスタ。 カニなんて、年に何回食べられるのやら。 食後は某書類。内容はともかく、Mac上で扱うワードやエクセルとプリンターの関係でひどく苦労する。25時半まで…

読書会の記事と、木曜日の談話会の記事を追加しました。ご意見をいただければ幸いです。

よく晴れた暖かい日。起床は11時。洗濯と掃除をする。先週は夫婦そろって出張だったので、二週間分たまっている。13時にはCも実家から帰ってくる。掃除の続きと家具の配達。 夕方、Cと外出。三宮で本屋とデパートに行き、ハンバーグを食べて帰る。

急に寒くなる。起床は9時、出勤してコード書き、噂は確認がとれず。午前中の会議は機器不良のため中止、午後はH氏と認証に関して議論。夕方から某プロジェクトの打ち上げ。24時に帰宅、27時に寝る。

物理ではシミュレーションはもはや不可欠な道具だが、シミュレーションに関して 定量的な議論はできるが、定性的な議論はできない モデルの妥当性を問うことが難しい（シミュレーションが変な数字を出してきて初めて前提のおかしさに気づく） という問題があ…

今日もよく晴れる。起床は9時。出勤してコード書き。現在悩んでいる問題は、実は既にOさんの手で実装されていたらしい、という噂を聞く。ついでに、来週末もまた出張となった。午後は全体会議と談話会、19時に帰宅しようとしたところちょうど飲んでいたグル…

意気消沈すると、少し感傷的になり、ちょっとしたことで涙もろくなることもある。 先週末、東京への出発の直前、変なメールを受け取った。本文は空白、添付はpdfファイルが一つだけ。SPAMかと思ったが、帰ってきた後ファイルを開いてみた。すると「あなたの…

19時より22時まで。参加者3人。p.18第2段落より最後まで。 パットナムのトリック K氏の指摘で議論が始まる。p.19の第一パラグラフ-第二パラグラフの重要な点でパトナムは叙述トリックを使っている。 第一パラグラフでは、集合論のパラドックスの話で、ラッセ…

よく晴れた、暖かい日。起床は9時、二日続けて遅め。 出勤してコード書きの続き。打ち合わせで失敗を報告、意気消沈する。早めに退所、読書会へ。 帰宅は22時半、夕食はマカロニ入りトマトシチュー、美味。

これまで誤解していたが、Agda2のdata typeの型の定義で、 (n : Nat) -> TermSeq n -> Set みたいな定義はよくて（ちなみに TermSeq nは長さがnのTermの列）、 (n : Nat) -> Term -> Pred (n-1) （ただし Pred 0 = Set） みたいな定義は不可能だ ということ…

起床は9時、少し遅め。出勤してコード書き。この件で時間を取られ、メールを書いたりしなければならなかったのに結局何もできず。気がついたら20時、慌てて退所（帰宅は22時）。Cも東京から帰ってきた。