2002-01-26
λ. なんだか楽しげな夢を見たような気がする。
λ. 借りた本
- 魔術士オーフェン・無謀編12 『そのまま穴でも掘っていろ!』
-
秋田禎信 [著]草河遊也 [イラスト] - 『君主論』
- マキアヴェリ(Niccolò Machiavelli)[著]
池田廉 [訳] - chikoさんにマキャヴェリを勧められたので
- 『始動! ネットビジネス - サイバー経済の舞台裏』
- 日本経済新聞社[編]
- 『夜明けのブギーポップ』
- 上遠野浩平[著] 緒方剛志[イラスト]
- 『つい買いたくなる売り場のつくり方』
- 小暮衣里[著]
λ. Open BeOS
OpenBeOS is a project dedicated to the re-creation, followed by the extension, of the BeOS.
Individual servers and APIs (known as kits) are being re-written from scratch by an enthusiastic team of volunteers who want to continue the revolution started by Be Inc. The kernel is being based on NewOS, a microkernel written by a former Be engineer, and adapted by a dedicated team of hard core programmers.
λ. チェルノブイリの少年たち
小学校のころ読んだ「チェルノブイリの少年たち」が広瀬隆の本だったと最近たまたま知って、衝撃をうけた。
λ. 9.11 アメリカに報復する資格はない!
チョムスキー(Noam Chomsky)がこういう本を出していたとは知らなかった。
原著はAmazonから五ドルでダウンロードできるそうです。(黒木のなんでも掲示板3より)
それから、補遺 (同じく、黒木のなんでも掲示板3より)
2003-01-26
λ. readline
でreadlineでコンテキストセンシティブな補完を実装するにはどうしたら良いのだろうと悩んでいたら、Enhanced Readline? というRCRがあった。
2005-01-26
λ. Strongly typed heterogeneous collections, Oleg Kiselyov, Ralf Lämmel, and Keean Schupke
を読んだ。主題についても面白いが、型クラスを拡張機能を含めて本格的に使う場合の Tips を学ぶにも良いと思う。
λ. Haskell's overlooked object system, Oleg Kiselyov, Ralf Lämmel, and Keean Schupke
を読んだ。
2006-01-26
λ. Infinite Objects in Type Theory. Thierry Coquand.
を読んだ。 guarded induction についての多分最初の論文。
どうでも良いけど、表記が少し珍しい気がする。 普通「f : (N -> P) -> P」と書くところを「f : ((N)P)P」と書き、「λx.u」と書くところを「[x]u」と書いている。
【2007-09-11追記】 「[x]u」は「自由変数としてxを含む項u」という意味だろうし、「((N)P)P」についても同様だろう。 なので、上記部分は私の勘違いだろうと思う。
Quotation
In order to establish that a proposition φ follows from other propositions φ1,...,φq, it is enough to build a proof term e for it, using not only natural deduction, case analysis, and already proven lemmas, but also using the proposition we want to prove recursively, provided such a recursive call is guarded by introduction rules. We call this proof principle the “guarded induction principle”.
sec. 2.8 より。 Guarded Induction on Final Coalgebras で引用されていたのと同じところを引用するのは、ちょっと癪だけど。
分からなかった点など
- impredicative proof of Tarski's fixed point theorem.
- Tarskiの不動点定理について良く知らないことに気づいた。どの辺りがimpredicativeなんだろう... <URL:http://www.hss.caltech.edu/~fede/wp/pf-tarski4.pdf> とかは関係ある?
- strong positivity
- P.Dybjer. Inductive Families. を参照。
2008-01-26
2009-01-26
λ. 『社長になる人のための経理の本』 by 岩田 康成
読了。昔、「企業会計論」という授業で勉強したこと(の一部)のよい復習になった。
授業では、やっぱり原理・原則から入っていく面がどうしてもあるけど、この本ではそうではなくて経営者の視点に特化していて、しかも登場人物がセミナーを受講して議論しているという形式が、非常にわかりやすかった。
ただ、この本は1996年に出版されたものにその後の経理・会計をめぐる動きを付け加えて2001年に出版されているのだけど、最後の「8. 会計ビッグバンを学ぶ」以外でキャッシュフロー計算書に触れられていない点など、今からすると少し古い印象を受ける部分もある。
