2007-06-01 [長年日記]
λ. 『ピタゴラ装置DVDブック』
今更だけど、ピタゴラ装置DVDブックの1巻・2巻を観た。本当はもっと早く見ようと思ってたのだけど、大分にはDVDドライブは結局持っていかなかったので、いままで観れなかったのだった。
ピタゴラスイッチの番組自体はあまり見たことがなかったのだけど、それでも十分に楽しめる。テンポ良く計算された動きをするビー球を追いかけるのは単純に気持ちよいし、それに装置のつくりがとても丁寧で観ていて楽しい。
2007-06-02 [長年日記]
λ. 第4回東京理科大学ピアノの会OB会演奏会
![[グランドピアノ(ベーゼンドルファー)]](./images/20070602_0.jpg)
弟が演奏するので、第4回東京理科大学ピアノの会OB会演奏会というものに行ってきた。何か名前が長いよ、「会」という字が3回も使われているし(笑
演奏していた曲 (2008-06-16 追記)
演奏されていた曲を ナクソス・ミュージック・ライブラリ(Naxos Music Library, NML) で探してみた。
- 雪のワルツ / Rei
- 夢想 / ドビュッシー
- ピアノソナタ第23番「熱情」Op.57より第3楽章 / ベートーヴェン
- バラード第2番Op.38 / ショパン
- ソナチエ 全楽章 / ラヴェル
- Night And Day / Cole Porter
- 愛の夢 第3番 / リスト
- エチュードOp.10-12「革命」 / ショパン
- エチュードOp.25-1「エアリアンハープ」 / ショパン
- 舟歌 / ショパン
- ラプソディ第2番 ト短調Op.79-2 / ブラームス
- 夜のバスパールより「水の精(オンディーヌ)」 ピアノソナタ第10番K.330 第2楽章 / モーツァルト
λ. SMCC
電車で「SMCCローンカード エブリ誕生」という広告を見て一瞬？？？となった。SMCCは「Symmetric Monoidal Closed Category」じゃなくて「Sumitomo Mitsui Card Co.」とかか。
2007-06-04 [長年日記]
λ. LL魂のチケット購入
Lightweight Language Spirit のチケットを購入。
セッション内容を見ると今年の「キミならどう書く」のお題は「プレゼンソフトを作る」か。UIのライブラリが充実してない言語だと大変かもね。
2007-06-06 [長年日記]
λ. CCC と *-autonomy
先日のIntroducing categories to the practicing physicistに以下のようにあったが、これはどう示すのだろう?
Proposition. A symmetric monoidal category which is both cartesian closed and *-autonomous can only be a preordered set.
まず、hom(A,B) ≅ hom(1,A⇒B) ≅ hom((A⇒B)*, 1*) ≅ hom((A⇒B)*, 0) 。 一方、CCCは分配的な圏なので 0≅0×0 であり、hom(A,B) ≅ hom((A⇒B)*, 0) ≅ hom((A⇒B)*, 0×0) ≅ hom((A⇒B)*, 0) × hom((A⇒B)*, 0) ≅ hom(A,B) × hom(A,B) となる。 ここから、hom(A,B) は空集合か一点集合か無限集合であることがわかる。 あとは無限集合でないことを言えばよいのだけど、これをどう示したらよいかわからない。
【追記】 もっと単純な話だった。 もし、f: X→0 が存在すれば、 <id, f>: X→X×0 と p: X×0→X が inverse になっている。 p ∘ <id, f> = id は明らかで、 <id, f> ∘ p = id は X×0 ≅ 0 が始対象であることから言える。 なので、X ≅ X×0 ≅ 0 。 したがって、hom(A,B) ≅ hom((A⇒B)*, 0) は空集合か一点集合。
【追記】 ところで、A⇒0 を ¬A と書くことにすると、これは CCC に A≅¬¬A を加えると縮退してしまうということを言っていていて、古典論理に対応する圏を作ることの難しさを示している。 そういえば、古典論理に対応する圏を作ることが難しいことは、檜山さんの「論理とはなにか？ (4:完) -- 論理から圏へ」のところでも言及されていた。
λ. 『λに歯がない』 森 博嗣
を読んだ。
Gシリーズは正直微妙だと思ってたけど、今回のは結構好みの話だった。
この傾向が続くといいなぁ。
2007-06-07 [長年日記]
λ. 東方弾幕風を使って「もってけ！セーラーふく」を弾幕で表現
制服「もってけ！セーラーふく」。 ちょっwww 元ネタを知らないのだが、これは吹いた。
2007-06-08 [長年日記]
λ. サンタクロース問題
最近、コードを全然書いていなかったのでリハビリのつもりでやってみた。 とりあえず、Concurrent Haskell + STM で安直に。 出力はかなり手を抜いていて、複数のスレッドの出力が混ざったりと散々w
module Main where
import Control.Monad
import Control.Concurrent
import Control.Concurrent.STM
import System.Random
import System.IO
main :: IO ()
main =
do hSetBuffering stdout LineBuffering
reindeerCh <- newTChanIO
elfCh <- newTChanIO
mapM_ (forkA reindeerCh) ["Reindeer("++show n++")" | n <- [1..9]]
mapM_ (forkA elfCh) ["Elf("++[c]++")" | c <- ['A'..'J']]
forkIO $ sequence_ $ repeat $ join $ atomically $ msum $
[ do xs <- readN 9 reindeerCh
return $ do putStrLn "Santa Claus goes with reindeers."
randomWait
mapM_ (flip putMVar ()) xs
, do xs <- readN 3 elfCh
return $ do putStrLn "Santa Claus solves elve's problem."
randomWait
mapM_ (flip putMVar ()) xs
]
getChar
return ()
forkA :: TChan (MVar ()) -> String -> IO ThreadId
forkA ch s =
do v <- newEmptyMVar
forkIO $ sequence_ $ repeat $
do randomWait
putStrLn (s ++ " comes.")
atomically $ writeTChan ch v
takeMVar v
putStrLn (s ++ " goes away.")
randomWait :: IO ()
randomWait = randomRIO (500000, 2000000) >>= threadDelay
readN :: Int -> TChan a -> STM [a]
readN n = sequence . replicate n . readTChan
【追記】 らくがきえんじん(2007-06-09) でsyd_sydさんがこのコードについて解説してくださっているので、こちらもどうぞ。
λ. 『位相と論理』
先日 Topology via Logic も一応読み終わったし、似たようなタイトルということで『位相と論理 (日評数学選書)(田中 俊一)』に手を出してみる。 今日は、第一章「順序と束」を読んだ。環論についてよく知らなかったので、ブール代数のイデアルとブール環のイデアルの対応を丁寧に追っていたら、思ったよりも手間取ってしまった。
2007-06-10 [長年日記]
λ. RubyKaigi 2007 二日目
(後で書く)
それから、終わってから気付いたのだけど、例のRuby-GNOME2のGCの問題の話でRejectKaigiに申し込めば良かったと思った。最近Rubyに触っていなかったのですっかり忘れてたよ。後の祭り。もう意味はないのだけど、気まぐれにちょっとスライドを作ってみた。ruby-gnome2-gc.ppt
λ. 『位相と論理』 第三章「構造とモデル」
RubyKaigi の行き帰りの電車の中で、第三章「構造とモデル」 を読んだ。 あれ? 基本写像の定義が抜けてる?
ψ たけを [おー、『位相と論理』やってるのですか。自分は3章で止まってるので、日本に帰ったら教えてね。]
ψ さかい [りょーかい。 実は今4章でつまってたりしますが、まあなんとかなるでしょう(^^;]
ψ kou [そうか、こうなっていたんですか。 GtkButtonがdestroyされたらGClosureが死ぬので、そのタイミン..]
ψ さかい [ちょっwww # ちなみに、私はcountとかの辺りが良くわかってなかったり……]
ψ むとう [なんともタイムリーなネタですね。 やはり図にすると頭の中がすっきり整理できますね。 勉強になりました（笑）。]
ψ さかい [いやぁ、直後に http://sourceforge.net/mailarchive/forum.php?threa..]
ψ タナカコウイチロウ [お久しぶりです。 『位相と論理』についてですが、酒井サン、たけをサンお二人の情報交換の場があるときには、私を末席にで..]
ψ さかい [お久しぶりです。 情報交換の場……たけをさんが天竺から帰ってきてからの圏論勉強会とかになるのかな。]
2007-06-12 [長年日記]
λ. 『位相と論理』 第四章「ブール代数の表現定理」
『Topology via Logic』とこの本とでは、Stone空間の定義が異なっている。もちろん同値な定義ではあるんだけど、流儀の違いが少し面白いと思った。 『Topology via Logic』では「スペクトラル*1な位相空間でコンパクト開集合がブール代数をなすもの」という定義なのに対して、 この本では「コンパクトなハウスドルフ空間Xで、clop(X)が開集合の基になるもの」という定義をしている。
p.62 の Xa,b が閉部分集合になるのが何でだか良くわからない。
*1 コヒーレントという呼び方が一般的なようだが、Topology via Logic ではジラールのコヒーレントスペースとの混同を避けるためスペクトラルという言葉を使っている
2007-06-17 [長年日記]
λ. 『チェーザレ・ボルジアあるいは優雅なる冷酷』 by 塩野七生
先日『チェーザレ — 破壊の創造者』を読んで、チェーザレ・ボルジア(Cesare Borgia)についてもっと知ってみたくなって読んだ。時代を駆け抜けた英雄という感じだな。活躍が華々しい分だけ、その後の没落していく様には泣けるものがある。
2007-06-21 [長年日記]
λ. g_type_is_a()は推移的でない
今日、初めて気付いたのだけど、g_type_is_a()は推移的(transitive)ではないのだな。
例えば、g_type_is_a(GTK_ENTRY, GTK_EDITABLE) かつ g_type_is_a(GTK_EDITABLE, G_TYPE_INTERFACE) であるにも関わらず、g_type_is_a(GTK_ENTRY, G_TYPE_INTERFACE) ではない。
これは「GTK_ENTRY は GTK_EDITABLE インターフェースを実装した型である」という is-subtype-of 関係と、「GTK_EDITABLE は基本型 G_TYPE_INTERFACE に属する」という一種の is-instance-of 関係の、二つの異なる概念を同じ述語で表現してしまっているためだろう。
気持悪いよ……
Ruby-GNOME2ではgtkの型をRubyのClass/Moduleにマッピングして、g_type_is_a() が Module#<= に対応するようにしていたのだけど、Module#<= は当然推移的なので、Gtk::Entry <= GLib::Interface も成り立ってしまっている。
しかし、これは気持悪いので、Gtk::Editable のような個々のインターフェースに GLib::Interface をincludeするのはやめるべきかな。
2007-06-22 [長年日記]
λ. “Coroutines in Lua” by Ana Lúcia de Moura, Noemi Rodriguez and Roberto Ierusalimschy
遠藤さんの[ruby-dev:30986]を読んで、読んでみた。
コルーチンのモデルには、全てのコルーチンが対等に呼び出しあう対称コルーチンと、親子関係があって子は親に制御を返すことしか出来ない非対称コルーチンがある。 対称コルーチンと非対称コルーチンの表現力は相互に比較不可能と言われているけど、実は同じらしい。へぇ(3)。しかし、非対称コルーチンの方が単純さや実装のポータビリティの点で優れているので、Luaでは非対称コルーチンのみをサポートしていると。
確かに操作的意味論は単純だし、これを読んでるとなんだか「RubyのFiberもLuaと同じようにすれば良いのに」とか思えてきてしまう。洗脳されてしまった。
あと、対称コルーチンと非対称コルーチンの関係が継続と部分継続の関係に似ているという話は面白かった。ただ、非対称コルーチンの場合にも部分継続と同様の点が少し気になる。具体的には、部分継続の場合の「どこまで切り取るか」という点に対応して、yieldでどのresumeに制御を移すかという点。この操作的意味論だとyieldで制御が渡る先はダイナミックスコープで決まっているけど、それで本当に十分? 部分継続の方では議論が収束気味らしいので、こっちでも結論は出てるのかも知れないけどさ。
2007-06-26 [長年日記]
λ. Coq の extraction
<URL:http://d.hatena.ne.jp/syd_syd/20070622#p1> と <URL:http://www.eva-01.jp/d/?date=20070623#p03> あたりを読んで、なるほどと思った。 Coqではextractionをそういう風に使うのね。 AgdaだとそもそもSetとPropの区別が無いから、extractionのようなことをあまり意識したことがなかった(Agdaで書くと下みたいになっちゃうし*1)。考え方の違いが面白い。
Decidable :: Set -> Set Decidable P = P `Or` (Not P) lemma :: (C::Context) -> (e::Expr) -> (t::Type) -> Decidable (C |- e : t)) lemma = ... typeCheck :: (C::Context) -> (e::Expr) -> (t::Type) -> Bool typeCheck C e t = case lemma C e t of (inl x) -> true (inr y) -> false
*1 表記はちょっと誤魔化してるけど
![[たろいもプリン]](./images/20070627_0.jpg)
