2002-03-07
λ. おぉ、Rubyはシャア専用言語だったのかぁー!! ってのは置いておいて、この日記を見てカテゴリー論に興味を持たれるとは思いませんでした。嬉しいです。
インタプリタのソースはRubyとSWI Prologをちょこっと読んだことがあるだけなので、インタプリタのソースの面白さってのは良く分からないけど、Scheme系の方が面白いなら、そのうち何か読んでみよっかな。
あ、そうそう。プロセス、イベントループ、スレッドをなくした並列GUIイベントドリブンなプログラム開発が可能な言語、期待しています。
λ. 論文読み会
ちょっと都合が悪くなって行けなかった。興味のあるテーマだっただけに残念。
- A toolkit for user-level file systems.
In Proceedings of the 2001 USENIX Technical Conference. June, 2001.
David Mazieres.
λ. A first introductin to categories
ちょっとだけ読み進んだ。明日はBrouwer's theorems。要は不動点定理?
λ. 日本国債
ETV2002の「どうする借金大国 〜 ふくれあがる国債 〜」を見た。木村剛が出てきた時点で内容は予想がついたんだけど、暇だったので見てしまった。
で、結構笑えたのが「個人金融資産の1400兆円に比べて、国債/地方債の690兆なんて、たったの半分じゃないか」という議論に対する木村の反論。
彼は「この議論はちょっとおかしい。社員がいくら金融資産を持ったって、借金を大量に抱え込んでいる会社に投資/融資が集まるわけがない。社員の持っている金融資産と会社の返済能力は別だ」というような主張をした。
……が、「ちょっとおかしい」のはお前の頭の方じゃ。考えるまでもなく、私企業と違って政府には徴税権と通貨発行権がある。この議論でこの違いを無視するなんて、あまりにも粗雑だ。
2007-03-07
λ. 健康診断
内定先の健康診断に行ってきた。
λ. ⊤⊤-closed relations and admissibility by Martín Abadi
一ヶ月前にKeisukeNakanoさんに紹介してもらったのをようやく読んだ。
メモ
Theorem 2 の証明の前半では
R⊇{(a,b)∈A×B | a ![\[\preceq_R\]](tex/5730a5e8b4d373a0bca1725ba5f8d8ba.png "\[\preceq_R\]")
b ∧ b a}
だけ示して
R⊆{(a,b)∈A×B | a b ∧ b a}
は示していないが、後者は R ⊆ と R-1⊆ より自明。
Theorem 2 の証明の後半では R が TT-closed であることを示すのに、¬(a R b) ⇒ ¬(a RTT b) を示しているが、a RTT b ⇒ a R b を示すようにした方が全体の流れが分かりやすくなると思った。
Corollary 3 の「It follows that: a R b ≡ a b ∧ b a」の部分は以下から言える。
- ⊆
![\[\preceq\]](tex/be7b8d1c9c6a0368e7d464ac90e2cae8.png "\[\preceq\]")
より、a b ∧ b a ⇒ a b ∧ b a ⇔ a R b - R ⊆ と R-1 ⊆ より、a R b ⇒ a b ∧ b a
λ. 今日の英語: Don't count on anyone except yourself.
「誰にも頼るな」という意味。
