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時半。夕…