日々の流転

λ. OMG

OMG(Object Management Group)の名前は、「ああ、女神さま」(Oh My Goddess!)からきているらしいですよ(嘘)。

λ. compactness

compactness わかんねー

λ. ITスキル標準人材育成研修

PC組み立ててDebianインストールしますた。PCを組み立てるのは初めてだったので、結構ドキドキ。でも、難しいなぁ。あと、講義の方でも、バスの仕組みとか全然知らなかったので、ちょっぴりカンドー。

• プラットフォーム講義・実習資料

λ. 昼食

KUA`AINA

λ. Any endo-functor on the class of all classes is set-based. (J. Adámek, S. Milius, J.Velebil: On coalgebra based on classes)

以前に先生に聞いた時には「ふーん」と思ってたけど、考えてみると、なかなか驚くべき結果だよなぁ。そうか、そうだったのか。

λ. 何か

えーっと……、外部にpingを普通に飛ばすだけでアタックだと言われるなんて、思いもよらなかったよ。はぁ (ため息)

λ. 昼食

「角で」で。

λ. 東方妖々夢

久しぶりにプレイ。魔理沙でようやくクリア。

• 魔理沙(魔符) / 547360300点
• 魔理沙(恋符) / 509924800点

これでノーマルは一応全員ノーコンテニュークリアしたわけだし、しばらく妖々夢は封印の予定。

……と思ったが、その前にExtraを一回だけプレイ。むずい。でも、最初のプレイでボスまでたどり着けたことを考えると、やっぱ紅魔郷よりはだいぶ簡単かな。

λ. RHG 読書会 reloaded

今度は参加してみたいなぁ。でも、今からでも参加できるのかしら。

λ. 昼食

KUA`AINA

λ. 打ち上げ＠花のれん

• 有名な○○書店の隣らしい
• 頼人さんはネタを引っ張る
• 「タッチ」のあの兄弟はフェイルオーバクラスタだったらしい
• みんな「あいのり」が好きだなぁ
• SAINT2004 はおいしいらしい

λ. 東方妖々夢

ITSSも終わったし封印解除(早っ)。というわけで、Extraに挑戦してみる。が、「狐狗狸さんの契約」であえなく撃沈。やっぱ、中村さんや伏屋さんみたいにはいかないなぁ。

λ. 東方妖々夢Extraクリア

Extraクリア。でも、Phantasmはまだプレイできないや、残念。

λ. Ruby-GNOME2-0.7.0

リリースされたので、msvcrt用とcygwin用のパッケージを更新。両方ともruby-1.8用のみ。

λ. 咲夜(時)でもExtraクリア

咲夜(時)でもExtraクリア。が、まだPhantasmはプレイできない。やっぱ、スペルカードを集めなくちゃいかんのかと思い、かといってHardやLunaticのを集めるのはダルイので、安易にEasyで集めたらPhantasmが出た。しかし、Easyの方がNormalよりも得点が高くなってしまったのはビックリ。それは流石に悔しいのでNormalでも久しぶりにプレイ。そしたら、後半集中力が切れて6面で8機も失ってしまう。得点も7億にも届かなかったし、当然Easyよりも低い。……笑え。

λ. バイト

PNGファイルの容量を削るためにpngdietというツールを紹介されていたのだけど、使い勝手が良くなかった(チャンクを削る事しか出来ないみたいだし、一括処理も出来ないみたい)ので、結局pngrewriteとpngcrushを使った。

λ. 成績

成績がきた。今期は悲観していたのだけど思ってたよりは良かった。Bが一つ、Dが一つ。

λ. バイト

0xシリーズと5xシリーズの両方に対応するためにプリプロセッサを使って条件コンパイル……というところまではいいのだけど、紹介されたのはJavaPP。cppの中途半端なサブセットを使ってもなぁ、と思いcppを使う。

そういえば、Java用のプリプロセッサといえば、EPP なんかは結構面白そう。

λ. SLACS 2003

に行ってきた。池上さんにも久しぶりに会えたし、興味深い話も沢山聴けて、とても楽しかった。だけど、ついていけない話も多くて結構悔しい。懇親会にも参加してきた。

λ. Modal logics for coalgebras -- A Survey, 蓮尾 一郎 (東工大)

そういえば、これまで bisimilarity と behavioral equivalence は同じだと思い込んでいて少し恥ずかしかった。本当は、bisimilarity の方が一般には強い条件で、関手Tがweak pullback を保存するならば同値になるのか。

• Technical Report

λ. Regular category の中の非決定性オートマトン, 池上 大介 (産総研/CREST)

最初は割と簡単かなと思っていたら、いつの間にか付いていけなくなっていた。気になっていた話の一つだったので悔しい。Adámek らのアプローチ(cf Automata and Algebras in Categories)の特殊な場合になってるらしい。

λ. 抽象解釈にみられる圏論的構成について, 西澤 弘毅 (東大/産総研)

抽象解釈(abstract interpretation)って名前はよく聞くけどどういうものか知らなかったので、その辺りが良くわかって嬉しかった。今回聴いた発表のなかでちゃんと理解できたのはこれだけかも。

λ. 明示的代入計算の強正規化性の証明について, 桜井貴文 (千葉大)

.

λ. 様相μ計算の完全性について, 鹿島 亮 (東工大)

様相μ計算というのは、様相命題論理の体系に不動点演算子を加えたもの……なのかな。そういう事は全然考えたことが無かったので新鮮に感じた。よくは分からなかったけど。

λ. Announcement of Typed Lambda Calculus and Applications, 長谷川真人 (京大)

国際学会 "Typed Lambda Calculus and Applications" のアナウンス。2005年奈良。typed lambda calculus というタイトルだけど、untypedでも、λ以外でも実は良いらしい。来年の10月くらいが論文の締め切りで、長さ的には15ページ程度らしい。

それから、

Fourth ACM-SIGPLAN Continuation Workshop (CW'04)

deadlineは10/1。

Category Theory in Computer Science (CTCS 2004)

コペンハーゲン。カテゴリの「カ」の字でも入ってればOKらしい (笑)

なんてのもあるそう。

それから、線形論理では「A = (A -o ⊥) -o ⊥」「!A = (A → ⊥) -o ⊥」「?A = (A -o ⊥) → ⊥」が成り立っていて、前者の二つに関しては「A = ∀X. (A -o X) -o X」「!A = ∀X. (A → X) -o X」も言えるのに、最後のだけは「?A = ∀X. (A -o X) → X」ではなく「A = ∀X. (A -o X) → X」になるのは何故か、といった話もしていた。

λ. Flow Analytic Type System for Compiler Optimizations , 松野裕(東大)

.

λ. NP完全問題を解く決定性アルゴリズムについて, 久馬栄道 (愛知学院大)

.

λ. On Sufficient Conditions And Partial Analysis for Secure Cryptographic Protocols, Masao Mori (九大)

.

λ. AMG

AcronymFinderでAMGを検索すると、「Aa! Megami Sama! (anime)」がトップにくる。「Ah! My Goddess」ではなく「Aa! Megami Sama!」がdefinitionとして載っていることに少し驚く。

λ. SLACS 2003

今日も行ってきた。発表を聞いていたら、僕も研究しなくちゃなぁという気がしてきた。

λ. 外延的π計算

へぇ、λ計算をπ計算に埋め込めるのか。

λ. 情報と依存関係の論理, 小林 聡(京産大)

竹内君とか、結構興味がありそう。内容そのものも面白かったけど、論理体系を作っていく過程みたいなのが面白かった。

λ. The double-negation and ?! translations of classical logic, 白旗 優 (慶應大)

.

λ. 等式の対応関係について, 西原 秀明 (産総研/CREST)

.

λ. 学校

帰りに学校によって、幾つか雑用を済ませてくる。久しぶりの学校は何やら工事か何かをしていた。あ、ITSSの謝金申請書を提出してくるの忘れた。

λ. 読書

『夢使い 5』

植芝 理一 [著]

λ. Scott位相, Compactness

Scott位相の開集合の条件に「inaccessible by directed join 」があるって事は、例えば、半順序集合 (N∪{∞}, ≦) 上のScott位相を考えると、{∞}は含まれないって事かな。……なるほど、なるほど。

Compactnessまだ分からん。池上さんも「普通に勉強していても詰まるところ」と言っていたので、気長に行こっと……

λ. Re: NP完全問題を解く決定性アルゴリズムについて

私は計算量問題とかにはど素人なので、以下は眉につばを沢山つけて読んでくださいませ。(間違っていたら遠慮せずに突っ込んでもらえると嬉しいです)

まず、構成的数学というのは、直観主義論理に基づいた数学で、要するに証明に背理法*1を使わない世界です。背理法を使えないので、何かが存在することを証明するにも、存在しないことを仮定して矛盾を導いてもダメで、具体的にその何かを構成しないといけないわけです。例えば、ブール式の充足可能性問題(SAT)を解く場合でも、具体的な割り当てを構成する必要があります。つまり、充足可能かという情報だけでなく、実際の割り当てという「それ以上」の情報が必ず分かってしまいます。

そこで、yes/noの答えはP(違ったかも)で求まるけど、そこから「それ以上」の情報を計算するにはより大きな計算量を必要とする、そういう問題とそれを解くアルゴリズムを無理やり捻り出してみて、それを分析中。……というような話だった思います。まだ完成した話ではないそうです。

λ. おでかけ

友人たちと秋葉原と神保町へ。自分から秋葉原に行くなんて、失ってはいけないものを失ってしまったような気もするが、気にしない事にする。それから、秋葉原から神保町まで歩こうとして迷ってしまった。

λ. 読書

『グリーン・マイル (1) -- ふたりの少女の死』

スティーヴン キング (Stephen King) [著], 白石 朗 [訳]

λ. アンテナ

たまてばこは、僕の好みじゃない部分が結構あるので、そろそろ捨てたい。五月雨にしようか、それとも自分で書こうか……

λ. いろんな事が思うようにいかない。ちょっと疲れた。

λ. Re: 続・NP完全問題を解く決定性アルゴリズムについて

なるほど。勉強になります。先日の駄文を書いた甲斐がありました (^^;)

λ. 陸軍航空隊

知り合いの某氏(バレバレですが)が作ったゲーム「陸軍航空隊」を遊んでみる。なかなか難しい。「マレー敵飛行場強襲」のミッションが難しかった。

λ. Comonad (2)

先日読んだ "Codata and Comonads in Haskell" のコードは本当に動くのかと思って、Hugsで試してみる。echoは確かに動くのだけど、自分で

stdPutString :: String -> OI () -> ()
stdPutString [] t = coeval (t .>> ())
stdPutString (x:xs) t = coeval (t .>> x =>>
                                stdPutChar =>>
                                stdPutString xs)

とか定義して、「stdPutString "hogehoge" stdOI」とかやっても、何も出力されない。何がまずいのだろう。

λ. GUNSLINGER GIRL アニメ化

楽しみ。

λ. バイト

7-zipで圧縮しなおすと、jarファイルがちょっぴり小さくなるそうだ。サイズを小さくするために出来るのは、あとはクラスファイルのObfuscationくらいかなぁ……。とりあえず、幾つかツールをメモ。後で比較してみよう。

• RetroGuard
• DonQuixote
• jarg - Java Archive Grinder

λ. 影鷹 - 縦書きブラウザ

影鷹（かげたか）は HTML を縦書きに表示するためのソフトです。最終的には Intenet Explorer や Mozilla などのようなブラウザを目指していますが、今はまだ普通の HTML（Javascript などを使っていない）を表示するのがやっとの状態です。

メモ。

λ. Experimental GLib TreeModel interface

gobjectのインターフェースをRubyで実装するための、Geoff Youngs さんの実験的なコード。この辺りは色々と難しい問題が山積みなので、あまり手を出したくなかったのだけど、そうも言ってられなくなってきたなぁ。

λ. g_signal_override_class_closure()

それで思い出したのは、g_signal_override_class_closure()とg_signal_chain_from_overridden()。こいつらをRubyから使えるようにすれば、シグナルのデフォルトハンドラーに関しては、Cレベルでゴチャゴチャやらなくても済むようになるはず。

素直に実装すれば

class MyButton < Gtk::Button
  register_type("MyButton")
 
  signal_override("clicked"){|instance, *args|
    puts "#{instance.inspect}.clicked"
    instance.signal_chain_from_overridden(*args)
  }
end

のように使う事になると思うのだけど、出来ればdefine_methodのようにinstanceのコンテキストでブロックを実行するようにして、

class MyButton < Gtk::Button
  register_type("MyButton")
 
  signal_override("clicked"){|*args|
    puts "#{self.inspect}.clicked"
    signal_chain_from_overridden(*args)
  }
end

と書けるようにしたいところだ。やり方が分からないけど (^^;)

λ. モズグズ様立体化

なんとなくchikoさんへ。

λ. Javaバイトコード処理系の作り方, 首藤 一幸

を読んだ。だいありー(2003-09-17)より。

λ. Phantasm初クリア

Phantasm初クリア。使ったのは咲夜(時符)。「人間と妖怪の境界」から先が全然だめ。ボムの多い咲夜を使っててよかった (^^;

λ. 借りた本

『グリーン・マイル (2) -- 死刑囚と鼠』

スティーヴン キング (Stephen King) [著], 白石 朗 [訳]

『数学の不思議な旅 — ピュタゴラスの定理から超数学まで』

A.K. デュードニー (A.K. Dewdney) [著], 好田 順治, 小野木 明恵 [訳]

小説すばる 2002年10月号

-

λ. 買った本

月刊「現代」 10月号

-

λ. モーニング娘

どうでもいいけど、最近加護ちゃんかわいいですね。
あの辺の年齢はどんどん化けるので、将来が楽しみです
同様の理由で、辻ちゃんにも期待
新規加入した娘。は正直わからんし、どーでもよいです

そんな直江先生は、辻加護判別ゲームなど余裕に違いない。(とか書いてみる)

λ. signal_connect("destroy"){}

「ruby -rgtk2 -e 'Gtk.init; Gtk::Button.new.signal_connect("destroy"){} '」で落ちる問題、とりあえず解決。原因は前から分かっていて、

1. Rubyの終了処理開始
2. Ruby側のオブジェクトが開放される
3. glib/gtk側のオブジェクトがunrefされる
4. glib/gtk側のオブジェクトのリファレンスカウンタが0になる
5. destroyシグナルが発生して、signal_connectのブロックを呼ぼうとする
6. しかし、Ruby側はすでに通常の実行状態ではないので、正しく呼べない
7. Segmentation Fault

という事が起こっていた。

Rubyが終了処理に入っていたらブロックを呼ばない事にすれば良いのだけど、「Rubyが終了処理に入っている」事をどうやって知れば良いかで数日悩んでいた。で、今日ふとrb_set_end_proc()で登録した関数内でフラグを立てればいいということに気が付いたので、解決。

この件についてはもっと対処が必要な気もするけど、落ちることだけはなくなるはずなので、残りは後回しでいいや。

λ. Relator

Functorの概念を使っているプログラミング言語は多いけど、Relatorの概念を使っている言語はあるか? (高階の論理型言語とか?)

λ. 読書

『天国に涙はいらない 9 - ふんどし汁繁盛記』

佐藤ケイ[著] さがのあおい[イラスト]

λ. 親知らず

親知らずを抜歯。多少痛む。

λ. pcl-cvs

cvsコマンドを直接使うのが馬鹿らしくなったので、pcl-cvsを使ってみる。しかし、MeadowからCygwinのsshにパスフレーズを渡すことは出来ないみたい(MeadowがCygwinのptyを扱えないのはまぁ当然だよね)。ssh-agentを使えば良いみたいだけど、どうせなのでwin-ssh-askpassというのを使ってみる。なかなか便利。

λ. 分類と情報射のなす圏のexponential (PDF)

そのままじゃ存在しないよね。忘れないうちにメモしておく。

[2005-03-27 追記] distributive category でないことを示しすことによって間接的に証明した方がスマートだと思う。

λ. 親知らず

消毒してもらってくる。もう痛みはほとんど無い。

λ. RHG読書会 Reloaded

市ヶ谷駅から間違えて反対側へ行ってしまい、靖国神社まで行ってしまった。どうせなら参拝していこうかとも思ったけど、すでに時間が過ぎていたので、急いで引き返す。地図を印刷していけばよかった。

これまで雲の上と思ってた人たちに会うことが出来て、ちょー感激。

λ. g_signal_override_class_closure() その2

メモ

• Chaining Class Closures (gtk-devel-list)

λ. 萩野研現代史

κ208では易姓革命が起こり、kunoがjnから王位を簒奪した模様。κ208の暗黒面を統べていたkunoの政権には反感を持つものも多いようだが、今のところ表立った反対運動などは起こっていない。これに対してkunoは早期に改革及び粛清を行い、体制の不安要因を取り除くことを目指すようである。なお、権力闘争に敗れたjnはMAGに放逐されるとの事である。また、今後のkuno新政権の運営手腕には一層の期待が集まるが、卒業をひかえたkunoは所詮レイムダックに過ぎないとの一部の観測もあり、水面下の権力争いはますます激しさを増しているようである。

• 王者の証である聖杯を手に笑顔を浮かべるkuno:
  
• 聖杯の拡大写真:
  

λ. Compact-Open Topology

メモ。

λ. g_signal_override_class_closure() その3

ちょっと閃いたので、

class MyButton < Gtk::Button
  register_type("MyButton")
 
  signal_override("clicked"){|instance, *args|
    puts "#{instance.inspect}.clicked"
    instance.signal_chain_from_overridden(*args)
  }
end

と書くかわりに、

class MyButton < Gtk::Button
  register_type("MyButton")
 
  def do_clicked(*args)
    puts "nil.clicked"
    super
  end
end

と書けるようにしてみる。実装は、method_addedを使ってメソッド定義を検出してsignal_overrideを呼び、後は例によってモジュールをincludeすることでsuperを横取りしてsignal_chain_from_overriddenを呼ぶようにしています。

「do_シグナル名」というメソッド名は、特別な意味を持たせるにはちょっと一般的過ぎる名前なので、名前は変えたほうがいいと思うけど、それ以外は結構いい感じだ。

λ. Excite エキサイト : サーチストリーム＞サーチストリーム

笹田さんの「だいありー未満」(2003-09-22)で知って、試してみたら、以下のようなエラーが大量に発生して、何も表示されなかった。駄目な単語を見たかったのに、残念。

java.lang.NullPointerException
        at excite.voyeur.Voyeur.paint(Voyeur.java:174)
        at excite.voyeur.Voyeur.update(Voyeur.java:215)
        at sun.awt.RepaintArea.paint(RepaintArea.java:169)
        at sun.awt.windows.WComponentPeer.handleEvent(WComponentPeer.java:260)
        at java.awt.Component.dispatchEventImpl(Component.java:3699)
        at java.awt.Container.dispatchEventImpl(Container.java:1623)
        at java.awt.Component.dispatchEvent(Component.java:3480)
        at java.awt.EventQueue.dispatchEvent(EventQueue.java:450)
        at java.awt.EventDispatchThread.pumpOneEventForHierarchy(EventDispatchThread.java:197)
        at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:150)
        at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:144)
        at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:136)
        at java.awt.EventDispatchThread.run(EventDispatchThread.java:99)

λ. Design and Implementation of Object Oriented Virtual Machines

メモ。

λ. アドバイス

世の中に、役に立たないアドバイスのなんと多いことか。アドバイスすること自体が目的になってるとしか思えない。

λ. Haskellスレ

Haskellスレからリンクがはられているのを見て驚く。圏論を紹介したいのなら、私の恥ずかしい発表資料ではなく、もっとマシな資料を参照したほうがよいと思う。まぁ、どうでもよいけど。

λ. 女の勘

結局S女史の予想通りだったって事なのかな。女の勘、恐るべし。

λ. 授業

今日から秋学期の授業が開始。夏休み中全然会わなかったような知り合いにも久しぶりに会う。変わっている人もいれば、そうでない人も。

λ. 誕生日

ちなみに明日は私の誕生日。

λ. 西岡研

暇だったので覗いてみることに。符号理論がテーマで代数の入門から。

シラバスには

とっつきにくい代数系ではあるが、近年の計算機の発達のおかげで、大変な計算も記号的に処理され、瞬時に結果が得られるようになってきた。このため、学習する手法もすこし変わってきつつある。

と書いてあったので、Computer Algebra Systems をバリバリ使って学習/研究することを期待してみる。

λ. "Topology via Logic" を輪講することに

今期は"Topology via Logic"を輪講することになった、……というかした。やるぞー

λ. Otter: An Automated Deduction System

Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP.

Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry.

メモ。paramodulationって何?

【2006-06-29追記】 萩谷先生の「命題論理の演繹体系」という講義録にparamodulationの解説がある。

λ. ACL

についてちょっと調べてみる。

• Solaris における File ACL (Access Control List)の設定方法

λ. 夕食

水龍。

λ. 誕生日

というわけで今日は誕生日でした。本当に色々な人に祝ってもらえて、とても嬉しかったです。どうもありがとうございます。

川井君にアイスクリームをおごってもらった。

それから、Zinniaさんにねういちさんという方と同じ誕生日だと教えてもらいました。これまで不思議と同じ誕生日の人に会ったことがなかったので、ちょっと嬉しい。それに、この方のTODOには「rubyの勉強」「卒研」「親知らずを抜く」といったキーワードが並んでいて、何だか親近感を感じるのでした (^^;

λ. Zukachan Index - The Five Star Stories

.

λ. 疲れたよ。

λ. 借りた本

『グリーン・マイル(3) - コーフィの手』

スティーヴン キング (Stephen King) [著], 白石 朗 [訳]

『ハンニバル (上)』

トマス ハリス (Thomas Harris) [著], 高見 浩 [訳]

λ. readFile / writeFile

readFileとwriteFileを使ってファイルを書き直すようなコード(ちょー単純化すると以下のような感じ)を書いたら、期待通りに動かなかった。理由は理解できるのだけど、これはちょっと切ないぞ。

main =
    do s <- readFile "test.txt"
       writeFile "test.txt" (s ++ "hogehoge\n")

λ. 踊る大捜査線 The Movie 2

takotセソセイにフジサワ中央の夕方が安いと教えてもらったので、せっかくだから家族で見に行ってきた。これでようやく元ネタがわかったYO。で、面白かったとは思うけど、リピーター続出ってのはちょっと信じられんな。