2002-05-21
λ. 「ヘルシング」と「大同人物語」の作者が同一人物だと知ってショックを受けている今日このごろ、皆さんどのようにお過ごしでしょうか?
λ. 酒井大明神
私は「酒井大明神」らしい。大明神と権現さまはどっちが偉いのかな?
λ. Coalgebra に基づく有限オートマトン理論の再構成(概要)
を眺めてみるが……む、難い。
λ. プログラミング言語論
言語の評価が、Javaに近い言語とそれ以外でダブルスタンダードになっているような気がするのは気のせい?
λ. 情報数学Ⅱ
わけわからなくなってきた。ちゃんとした確率論の教科書を読まなくちゃついていけなさそう……
λ. クリスチャン
「例外がきたら、みんな神様にthrowすればよい」と某氏が言っておりました。もちろん冗談でですよ。
λ. FreePascal
{$packrecords C}を指定すると列挙型もCと同じサイズになるみたい
λ. Parted-1.6.0
のソースを見た。Partedのソースを見るのは久しぶり。PedGeometryがPedDiskへのポインタではなくちゃんとPedDeviceへのポインタを持つようになってる。
autoconf 2.50 以上が必要なのか。どうせなので Asumi を入れるか。
2006-05-21
λ. 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
∑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になるのがどうしてなのか、わからない。
2007-05-21
λ. 「週末」
「一週間」の終わりが近くなると、どうしても「早く仕事が終わらないかなぁ」と思ってしまい、時間が長く感じられる。 実際は今日は見学等があったので、クリーンルーム内にいる時間は短かったんだけどね。
そんなわけで体力的には余裕があったので、夜にフィットネスルームでエアロバイクをこいできた。 運動不足解消コースとか書いてあったコースで、心拍数120を目標に20分間。 107.5kcalの消費。
エアロバイクは、自分にどれだけの負荷がかかっているかとかが、目に見える形でわかるので、分かりやすくてよいな。ウェイトトレーニングはどれくらいの負荷をかければよいのか、私のような素人には分かりにくいよ。
明日明後日は休日なので別府に行ってくる予定。