2002-03-09
λ. Win32でスペースを含むパスにスクリプトのプラグインを置けない?
実際にプラグインのプロセスを作るのはxspawnvという関数なんだけど、ここで呼ばれている_spawnlpは、引数に空白が含まれていても、連結する際にクォートしてくれないようなのだ。この辺りは関数を呼ぶ側の責任なんだろうか?
2003-03-09
λ. gtkengine and librsvg
gtk2 on cygwin に gtkengineとlibrsvgのパッチを追加。バイナリを公開していないのは、これ以上手を広げるなら、win32版とx11版の共存について考察した方がよさそうだから。
GImageViewは一部に需要がありそうなので、もう少しがんばってみる。……プラグインのDLL化を一応なんとかした。 exeファイルからシンボルをエクスポートする方法をすっかり忘れていて随分はまってしまった。他のプラットフォームみたいに「gcc -Wl,--export-dynamic -o test.exe 」だけで済めばどんなに良いか…… (「binutilsでもhackすればぁ?」クレヨンしんちゃん風に) とりあえず、設定画面のスクリーンショットと作業中のパッチ。
λ. 有野さん
λ. 1.8のRuby Binaries
キタ━━━━━━(゜∀゜)━━━━━━ !!
しかし、うーん、ruby-gnome2-devel-jaでこんな不用意な発言しなけりゃ良かったかも(笑)。
> ＃あれ？1.8.x対応は？(^^;) (1.8用の)バイナリの公開は、わたなべさんの Ruby Binaries あたりで 1.8のバイナリが公開されてからでいいかなと思ってます。
2004-03-09
λ. 借りた本
- 『アリソン』
- 時雨沢 恵一 [著]
- 『「無限」に魅入られた天才数学者たち』
- アミール・D・アクゼル(Amir D. Aczel)[著], 青木 薫 [訳]
- 小説すばる 2003年9月号
- -
- 『クリスティーン 下』
- スティーヴン キング (Stephen King) [著], 深町 眞理子 [訳]
- 『経済記事を読みこなす基礎知識』
- 原田 泰 [著]
2005-03-09
λ. インスタンスの列挙
[Haskell-cafe] Is it possible to print out types of instances in scope で知ったのだが、新しいGHCiの:infoコマンドは、型クラスの名前を与えるとインスタンスのリストを表示してくれるし、型の名前を与えると属しているクラスのリストを表示してくれる。Hugsには前からあったので、GHCiでも使えるようになって嬉しい。
λ. 構成的な関数からなる圏
よく出てくるのは
- PER
- ω-Set
- effective topos
くらいか。どれもあまり知らないや。
- キーワード
-
- Kleene の実現可能性解釈 (realizability interpretation)
- 実現可能性宇宙 (realizability universe)
- 総合的領域理論 (Synthetic Domain Theory)
λ. Extensional PERs, Peter J. Freyd, P. Mulry, Giuseppe Rosolini, D. Scott
を読んだ。
2007-03-09
λ. 女性誌がモテに使える5つの理由
研究室の某氏の机の上には時々女性誌が置いてあるのだが、あれにはこんなメリットがあったのだな、と思った。
λ. 不完全性定理に関して混乱中
Tを(第一)不完全性定理が適用可能なセオリー、GをTでのゲーデル文とする。 すなわち、T ⊢ G≡¬(∃x. prove(x,[G])) で、また T ⊢ prove(p,a) は「aはある論理式Aのゲーデルコーディングであり、pは T⊢A のある証明図πのゲーデルコーディングである」ことと同値であるとする。
Tがω無矛盾ならば、Tでは G も ¬G も証明できない。 ということは、Tがω無矛盾なら T∪{G} も T∪{¬G} も無矛盾なわけで、それぞれモデルが存在する。 前者のモデルでは「G は真だけど証明できない」ということになり、Gの「自分は証明できない」という直観的な意味にマッチしていて、なんとなく理解出来る気がする。
しかし、後者のモデルは直観的にはどう理解すればよいのだろうか? このモデルでは ¬G が真であり、したがって ∃x. prove(x,[G]) も真である。 この x はモデルの外から見れば当然 T ⊢ G の証明図を表してはいないが、モデルの中からみれば T ⊢ G の証明図を表しているのだろうか? もしそうだとすると、このモデルの中からはTがω矛盾しているように見えるのか?
多分、非常に基本的かつ簡単なことだと思うのだが、混乱中。 情けない……
λ. SFCから都政へ挑戦! 浅野史郎教授が都知事選に出馬表明
浅野史郎氏ってSFCの教授だったのか。知らなかった。 しかし、 小熊さんの意見 や 泥酔論説委員の日経の読み方(2007-03-04) を読むと、あんま都知事にはなって欲しくないなぁと思う。 私は東京都民じゃないから、都知事選には投票できないけどさ。
ψ 竹内 [「Gが証明できない」仕組みと「¬Gが証明できない」仕組みが違うのでは。 Gって∀xF(x)の形で、「個々の具体的な整..]
ψ 竹内 [ごめんなさい。以下は間違い。 「ω矛盾しているなら、矛盾している」 これは言えませんでした。 ところで酒井君、学校..]
ψ さかい [T∪{¬G} はω矛盾ではあるけど矛盾はしていないので、モデルを作るのに問題はないはず。 # 同様に考えると T∪{..]
ψ 佐野 [http://itc.sfc.keio.ac.jp/pukiwiki/index.php?%C2%B4%B6%C8%..]
ψ alpha [女性誌読んでもモテにはつながりません。あと CanCam とかはリスク分散（？）のために彼氏は常に 2 〜 3 人は..]
ψ 竹内 [考えているのは、矛盾はしてないがω矛盾している モデルっすね。勘違いしてて何も解決してませんでした。 以下、少し調べ..]
ψ さかい [＞佐野さん やっぱ電子ジャーナルとかは使えないのね。 仕方ないのだろうけど、やっぱ1万円分の価値はないねぇ。 ＞a..]
ψ たけを [電子ジャーナルは、酒井さんの内定先で契約しているところなら、会社経由で使えますよ。SFCのよりは圧倒的に少ないだろう..]
ψ 通りすがり [昔廣瀬健先生に習った記憶では T∪{¬G}はω矛盾な理論の例です。 つまり、Ｇの"証明"はノン・スタンダードなもので..]
ψ さかい [＞たけおさん おお、会社経由で使えるんですね。それは良かったです。 図書館の利用カードはいつでも手続き出来るようなの..]
ψ 某氏 [当然じゃないか！ サーベイ重要！]
2008-03-09
λ. 第三十八回圏論勉強会
今日は圏論勉強会。
The Haskell Programmer's Guide to the IO Monad — Don't Panic を読む二回目で、今回は関手と自然変換の部分を読んだ。次回はモナド。
ちなみに、圏論勉強会の会場はびぎねっとさまに貸していただいています。いつもありがとうございます。
λ. ライフカードPresents 真冬のホラーゲームキャンペーン
先日ライフカードを作ったときにやっていた「真冬のホラーゲームキャンペーン」というキャンペーンのVISAギフトカード3,000円が届いていた。わーい。
