日々の流転

λ. お昼

しまった!! 今日はお弁当を持ってきていたのに学食を食べてしまった。お茶があるから食堂で食おうとか思ったのが何とかのつき…とでも言おうか。繊維たくさんピラフとチキンドラム。

λ. ゆっけがKondaraだなんて意外だなぁ。

λ. ペイオフ再延期は無し

再延期は小泉内閣の存在意義を否定するようなものではあるのだけれど、それにしてもこれは残念。小泉内閣にまた失望。

λ. ruby-iconv-0.4.4

これまで存在は知っていても使ったことは無かったので、なかださんにツッコミを貰ったついでに試してみる。…うん、メモリの管理を考えなくても良いだけでこんなに扱いやすくなるとは!

で、速攻で地雷を踏んでしまったのでパッチ。

--- iconv-0.4.4/iconv.c.orig	Mon Feb  5 07:56:10 2001
+++ iconv-0.4.4/iconv.c	Thu Nov 15 22:22:52 2001
@@ -209,6 +209,7 @@
     }
     rb_ivar_set(error, rb_success, success);
     rb_ivar_set(error, rb_failed, failed);
+    return error;
 }
 
 static VALUE

λ. 買った本

「そして二人だけになった - Until Death Do Us Part」

森博嗣[著]

λ. おぉ、Zinniaさんのとこでもこないだのスタックの話と似たような話題が。なるほどobjdumpってこういう目的にも使えるのですね。参考になります。

λ. 言語の意味論

これでモンタギュー意味論もようやくおしまい。次回からは状況意味論へ。全然知らない領域なので楽しみ。

λ. 東方紅魔郷

ノーコンテニューで5面ボスまで到達。

λ. Lawvereの不動点定理について発表

Lawvereの不動点定理について発表。カントールの対角線論法との関係と、不完全性定理との関係について説明した。原さんの Y Combinator の導出方法も準備でしてたのだけど時間切れ。発表しないのももったいないので次回発表しよう。

λ. 夕食

片山さんとデニーズへ。そこで某氏らと遭遇。

λ. Light of the Earth 東方紅魔郷コーナー

スペルカードリスト等あり。

λ. るびま 0003号

きたー。

λ. Concurrent Haskell と FFI

次のようなプログラムをGHCでコンパイルして実行するとプロセスが暴走するっぽい(Windows版とLinux版のGHC 6.2.1 で確認)。原因は良くわからないが、Concurrent Haskell と FFI の組み合わせには気をつけようと思った。

import Control.Concurrent
import Foreign

foreign import ccall foo :: FunPtr (IO ()) -> IO ()
foreign import ccall "wrapper" mkCallback :: IO () -> IO (FunPtr (IO ()))

main :: IO ()
main =
    do mvar <- newEmptyMVar
       callback <- mkCallback $ mapM_ (putMVar mvar) [0..2]
       forkIO $ foo callback
       takeMVar mvar
       return ()

---

void foo(void (*bar)(void))
{
    bar();
}

まだ良く理解してないのだけど、ひょっとして次のようなことが起こっている?　fooを実行するOSスレッドA(Worker Threadではない)は mapM_ (putMVar mvar) [0..] を実行するためのCHスレッドαを生成し、その終了を待つために眠る。その間に別のOSスレッド(Worker Thread)によってメインのCHスレッドの処理が進んで終了し、他の全てのCHスレッドも殺されてしまう。αに先に死なれてしまったAが変なことになってる?

λ. 紅葉＠SFC (2)

λ. 『隣の家の少女』　ジャック・ケッチャム(Jack Ketchum)

を読んだ。

λ. UNIQLOCK

今更ながらUNIQLOCKにはまる。 これはいいなぁ。かわいいなぁ。

λ. “Seven trees in one” by Andreas Blass

Following a remark of Lawvere, we explicitly exhibit a particularly elementary bijection between the set T of finite binary trees and the set T⁷ of seven-tuples of such trees. “Particularly elementary” means that the application of the bijection to a seven-tuple of trees involves case distinctions only down to a fixed depth (namely four) in the given seven-tuple. We clarify how this and similar bijections are related to the free commutative semiring on one generator X subject to X = 1 + X². Finally, our main theorem is that the existence of particularly elementary bijections can be deduced from the provable existence, in intuitionistic type theory, of any bijections at all.

Seven Trees やっと解けた - ヒビルテ(2008-10-28) のツッコミと、Seven Trees：最後のヒント＋もっと面白い話 - 檜山正幸のキマイラ飼育記 から。 例の Seven Trees を詳しく扱った論文で、多項式P(X)とQ(X)に関して以下が同値だという話。

1. Tを二分木の集合としたときに、P(T)とQ(T)の間に very explicit な全単射が存在する (combinatorial equivalence)
2. 半環 N[X]/(X=1+X²) でP(X)=Q(X) が 成り立つ (algebraic equivalence)
3. P(T) と Q(T) の間の全単射の存在を構成的に証明できる

t=1+t² の複素数解 t = (1 + i√3)/2 の性質に関しては、P(t)を多項式P(X)の“Euler characteristic”と呼んでいて、それとP(ℵ₀)を{0, 有限, 無限}の3値で解釈した「次元」とをあわせたものが、jointly injective だと言っている。つまり、両方とも等しければ P(X)=Q(X) 。

例えば、P(X)=X⁷ と Q(X)=X の場合には、P(t)=Q(t)=t でかつ P(ℵ₀)=Q(ℵ₀)=ℵ₀ なので、P(X)=Q(X) 。 一方で、P(X)=X⁶ と Q(X)=1 の場合には、P(t)=Q(t)=1 だけど、P(ℵ₀)=ℵ₀≠1=Q(ℵ₀) なので、P(X)≠Q(X) 。

最後の構成的集合論の話は面白そうだけど難しいね。一応グロタンディークトポスとか定義は調べて分かったけど、分類トポスやらグロタンディーク位相での強制法やらの話で挫折。

• <URL:http://dx.doi.org/10.1016/0022-4049(95)00098-H>
• <URL:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.8517>

λ. 第五十八回圏論勉強会

今日は圏論勉強会。

今回は P. Selinger, “A survey of graphical languages for monoidal categories”の 5 Traced categories の残り。 Example 5.21 の symmetrical traced category だけど compact closed でない例が面白かった。