2002-04-10
λ. 「なんで、7日の分を書かないィ？」と言われてしまったので、7日の日記を補完。
せっかくカメラを持っていったのだから、みんなで写真を撮れば良かった。
λ. 圏論
相変わらず Map object で苦戦中。やはり、学期が始まると思うように時間がとれない。早く、Toposeやりたいのに。
2004-04-10
λ. John Hughes, "Generalising Monads to Arrows"
を読んだ。
本筋とは関係ないんだが、「data (Read x) => T x = ...」というようにデータ型を定義しても、型「T a」からaがReadのインスタンスだということを推論してくれないのは、僕もずっと不満に思ってた。(Restricted Datatypes in Haskell を参照)
[2005-03-27 追記] 圏論が何故プログラミングに役立つかということについての説明が良かったので、以下に引用しておく。
Some might find it surprising that something so abstract as category theory should turn out to be useful for something so concrete as programming. After all, category theory is, in a sense, so abstract as to be rather unsatisfying: it is `all definitions and no theorems', almost everything turns out to be a category if you look at it long enough, to say something is a category is actually to say very little about it. The same is true of most categorical concepts: they have very many possible instantiations, and so to say that something is, for example, a monad, is to say very little. This extreme generality is one reason why it is hard for the beginner to develop good intuitions about category theory, but it is hardly surprising: category theory was, after all, developed to be a `theory of everything', a framework into which very many different mathematical structures would fit. But why should a theory so abstract be of any use for programming?
The answer is simple: as computer scientists, we value abstraction! When we design the interface to a software component, we want it to reveal as little as possible about the implementation. We want to be able to replace the implementation with many alternatives, many other `instances' of the same `concept'. When we design a generic interface to many program libraries, it is even more important that the interface we choose have a wide variety of implementations. It is the very generality of the monad concept which we value so highly, it is because category theory is so abstract that its concepts are so useful for programming.
λ. 借りた本
- 『なぜ人はニセ科学を信じるのか—UFO、カルト、心霊、超能力のウソ』
- マイクル・シャーマー(Michael Shermer) [著], 岡田 靖史 [訳]
- 『よるねこ』
- 姫野 カオルコ [著]
- 小説すばる 2003年11月号
- -
2005-04-10
λ. ハムナプトラ２／黄金のピラミッド
イムホテップたん、哀れ。
λ. 横田基地：空自司令部を移転 日米政府、共同使用で合意
首都圏上空の航空管制権が米軍から返還されるという部分がまず目を引いた。首都圏上空の航空管制権を米軍が持っているという事実はしばしば「日本は独立国ではなく米国の属国」という主張の根拠の一つとして使われていたのを思い出す。この返還は、そういった主張をしていた人たちにとってはシンボリックな意味があるのだろうけれど、それ以外に何か実際の変化があるのだろうか。
そして、この移転は米軍再編の流れの中でどう位置づけされて、そしてそれは日本や極東にとってどういう意味を持つのだろう? 僕はこうしたニュースに接しても、それが軍事的にどういった意味を持つかサッパリ分からなくて、いつも困ってしまうのだ。せめて、ニュースくらいは理解したいなぁ、と思う。そういった軍事に関する教養みたいなのってどうやって学んだら良いのだろう。SFCの授業でそういったのを学べる授業ってないのかなぁ……
2008-04-10
λ. スライスがCCCのときのプルバックの右随伴
メモ。
圏Cの全てのスライスがCCCであるとき、C上の射 F: A→B からプルバックによって定義される関手 F*: C/B→C/A が右随伴 ∏F: C/A→C/B を持つことを示す。
p∈|C/A| とすると、pはCにおける dom(p)→Aという射で、C/Bの(F∘p)→Fという射でもある。
![\xymatrix{ \mathrm{dom}(p) \ar[rr]^{p} \ar[dr]_{F\circ p} & & A \ar[dl]^{F} \\ & B }](tex/7553ef7d748eff57f107903651f58c28.png "\xymatrix{ \mathrm{dom}(p) \ar[rr]^{p} \ar[dr]_{F\circ p} & & A \ar[dl]^{F} \\ & B }")
また、F∈|C/B| で C/B はCCCなので (-)F : C/B → C/B という関手が出来、これを適用すると pF : (F∘p)F → FF が得られる。 そこで、これと curry(π2) : 1 → FF とのプルバックで ∏F(p)∈|C/B| を定義する。 (C/B にプルバックが存在することは、この間の「スライスのスライスはスライス」から言える)
![\xymatrix{ \prod_F(p) \ar@{}[dr]|{\text{pb}} \ar[d] \ar[r] & (F\circ p)^F \ar[d]^{p^F} \\ 1 \ar[r]_{\mathrm{curry}(\pi_2)} & F^F }](tex/7c94a62e1cab8b2f5495183cfe4f1c4b.png "\xymatrix{ \prod_F(p) \ar@{}[dr]|{\text{pb}} \ar[d] \ar[r] & (F\circ p)^F \ar[d]^{p^F} \\ 1 \ar[r]_{\mathrm{curry}(\pi_2)} & F^F }")
そうすると、以下が自然な対応になる。
- X→∏F(p) in C/B
- f : X→(F∘p)F in C/B such that pF∘f = curry(π2)∘!
- g : X×F→(F∘p) in C/B such that p∘g = π2
- g : (F∘F*X)→(F∘p) in C/B such that p∘g = F*X
- g : F*X→p in C/A
2009-04-10
λ. TLUG
Tokyo Linux Users Group (TLUG) / 2009 April Nomikai に参加してきた。
ポーケンを持っていったが……
Quizletというサイトを教えてもらった。
ヒューガルデン飲んだ。
