日々の流転

λ. 「ヘルシング」と「大同人物語」の作者が同一人物だと知ってショックを受けている今日このごろ、皆さんどのようにお過ごしでしょうか?

λ. 酒井大明神

私は「酒井大明神」らしい。大明神と権現さまはどっちが偉いのかな?

λ. Coalgebra に基づく有限オートマトン理論の再構成(概要)

を眺めてみるが……む、難い。

λ. プログラミング言語論

言語の評価が、Javaに近い言語とそれ以外でダブルスタンダードになっているような気がするのは気のせい?

λ. 情報数学Ⅱ

わけわからなくなってきた。ちゃんとした確率論の教科書を読まなくちゃついていけなさそう……

λ. 萩野先生と一緒に歩くUFO

萩野先生と一緒に歩くUFOが……*1

λ. クリスチャン

「例外がきたら、みんな神様にthrowすればよい」と某氏が言っておりました。もちろん冗談でですよ。

λ. FreePascal

{$packrecords C}を指定すると列挙型もCと同じサイズになるみたい

λ. Parted-1.6.0

のソースを見た。Partedのソースを見るのは久しぶり。PedGeometryがPedDiskへのポインタではなくちゃんとPedDeviceへのポインタを持つようになってる。

autoconf 2.50 以上が必要なのか。どうせなので Asumi を入れるか。

λ. 『計算機プログラムの構造と解釈』 第二版. Harold Abelson, Jerry Sussman, Julie Sussman [著] 和田英一[訳]

有野さんと高林さんがSICPについて書いているのをみて、読んでみたくなった。とは言っても全文をオンラインで読むほどの気力も無いので、借りてみた。

λ. 自分の関数名を取得する方法

C 言語の研修より。C言語で自分の関数名を取得する方法は __func__ かな。自身の関数ポインタを取得する方法はちょっと知らない。

λ. Extensible datatypes. Andres Löh

を読んだ。

λ. Inductive Types for Free

を読んだ。

• Containerは存在自体は知っていたが、嬉しさがようやく理解できた
• strictly positive の定義は?
  • 【追記】 下の Representing Nested Inductive Types using W-types の方に書いてあった。
• LCCC = locally cartesian closed category
• Representation Theorem 面白い
• Martin-Löf category = LCCC + W-types
• 「M-types can be constructed from W-types」というのはどうやるのだろう?

λ. Representing Nested Inductive Types using W-types

• <URL:http://www.cs.nott.ac.uk/~txa/publ/icalp04.pdf>
• <URL:http://www.cs.nott.ac.uk/~txa/publ/>

∑_A: C/A → C が π_B^*: C/A → C/∑_AB の左随伴というのは何を言っている?

coproduct が disjoint であるときに、A+B ⊢ C ⟼ (A ⊦ κ^* C, B ⊢ κ'^* C) で定義されている関手 C/A+B → (C/A)×C/B がequivalenceになるのがどうしてなのか、わからない。

λ. 「週末」

「一週間」の終わりが近くなると、どうしても「早く仕事が終わらないかなぁ」と思ってしまい、時間が長く感じられる。 実際は今日は見学等があったので、クリーンルーム内にいる時間は短かったんだけどね。

そんなわけで体力的には余裕があったので、夜にフィットネスルームでエアロバイクをこいできた。 運動不足解消コースとか書いてあったコースで、心拍数120を目標に20分間。 107.5kcalの消費。

エアロバイクは、自分にどれだけの負荷がかかっているかとかが、目に見える形でわかるので、分かりやすくてよいな。ウェイトトレーニングはどれくらいの負荷をかければよいのか、私のような素人には分かりにくいよ。

明日明後日は休日なので別府に行ってくる予定。

λ. 『無理なく続けられる 年収10倍アップ勉強法』 by 勝間 和代

を読んだ。 (後で書く)