日々の流転

λ. あぁぁぁぁ。時間を無駄にしすぎ。

λ. 正規表現

気晴らしにRubyで正規表現(?)のエンジンを書いてみた。どうせなので文字列じゃなくてEnumerableを対象にすることにする。

NFAからDFAへの変換時に、馬鹿正直に巾集合オートマトンを作ってるせいか、かなり遅いなぁ。ただ、Prolog版よりRuby版の方が速かったのには驚いた。あとは、bisimilarな状態が複数出来てしまう事があるのがヤな感じ。bisimulationで割った商集合を状態集合とするオートマトンを作れば良いんだけど、具体的にはどうやるんだっけなぁ? 確かcoalgebraで変数を…… まあ気が向いたら実装してみるか。

a = Object.new
re = SRegexp.new(SRegexp.concat(SRegexp.star(SRegexp.concat(0, 1)), a))
re.accept? [0,1,0,1,a] #=> true

λ. ERE

先日、第一回の試験が行われたERE(経済学検定試験)というのがあるそうだ。

λ. Re: druby vs リモートでの例外

その例だとURIがDRb.primary_serverと一致して、リモート呼び出しでなくなってしまうと思います。再現例としてはこんな感じかと。

require 'drb'
DRb.start_service(nil, nil)
DRbObject.new(nil, DRb::DRbServer.new(nil,
  lambda{raise RuntimeError.new.extend(DRbUndumped)}).uri).call
#=>
# drb/drb.rb:239:in `raise': exception class/object expected (TypeError)
#         from drb/drb.rb:239:in `method_missing'
#         from hoge.rb:3

λ. 携帯電話

やっぱ慣れないものを使うのは難しいなぁ。ビデオの予約も出来ない酒井に、果たして明日はあるのか!?

λ. け・い・ぞ・く

トップレベルはread-evalのループだから、引数無し手続きの呼び出しと、その手続きのbodyをトップレベルに書いたものは、継続とか関係する場合は振る舞いが異なるのね…… (guileの場合。処理系依存かも)

自分は継続を誤解してるんじゃないかと、すっかり不安になって、ぐぐってしまったよ。てへっ。

λ. 1.8 のRuby binaries と setup.exe

cygwinのsetup.exeって、同じホストの複数のディレクトリを指定できないみたい。しかも既に追加したURLを削除するUIが無いので、とりあえず/etc/setup/last-mirrorを書き換えて、ようやく1.8用のRuby binariesをインストールできた。

λ. 昼寝

してたら、寝過ごして、約束をすっぽかしてしまった。欝だ。

λ. gtk2 on cygwin

GImageViewを使っていて、他のWindowsアプリケーションからファイルをドラッグ出来ないのに気付いておかしいなぁと思って調べてみる。

• gdkdnd-win32.cでファイル名をWin32形式のままg_filename_to_uri()に引き渡しているので、先にファイル名をPOSIX形式に変換するようにした。
• GImageViewは file:/usr/share/pixmaps/gimv.png という形式しか認識しないので、g_filename_to_uri()が作る file:///usr/share/pixmaps/gimv.png のような形式も認識できるように修正。(本来は後者の形式の方が正しかったような記憶が……)
• gdk-win32はGtkSelectionDataにtext/uri-listを入れる際にデータをNUL-terminateしないが、GImageViewはNUL-terminateされている事を期待している。lengthを同時に受け取るのだからNULは要らないだろと思い、GImageViewの方を修正

というわけで手元ではDnD出来るようになったので、GImageViewのパッチとバイナリを追加。ただ、gtk+の方のパッケージをまだ更新していないので、このGImageViewのパッケージを入れるだけではDnDは出来ないかもしれません。

λ. runghc

CVS版のGHCにはrunghcコマンドが含まれていて、runhugsコマンドと同じように使える。ちと起動が遅いけれど、Haskellのパッケージのセットアップ/インストール用のスクリプトをHaskell自身で書いたりするのに便利そうだ。

% cat hello.lhs
#!/usr/bin/env runghc
> main :: IO ()
> main = putStrLn "Hello World"
% ./hello.lhs
Hello World

λ. ANNOUNCE: GHC version 6.4

キタ━━━━(゜∀゜)━━━━ッ!!

過去の日記

• GADT (Generalized Algebraic Data Types)
  • ghc の新しい機能 Generalized Algebraic Data Types (GADT)
  • AVL木でGADTを試してみる
  • AVL木でGADTを試してみる (2)
• STM (Software Transaction Memory)
  • Composable memory transactions
• ライブラリ
  • GHC 6.4 のライブラリ
• その他
  • (GHCiの:infoコマンドで)インスタンスの列挙

明示的にforallで束縛した型変数を scoped type variable として使えるようになったのは、STモナドを使うときなんかに、地味に便利そうだ。これまでそういうときには不自然なコーディングを強いられてきたからなぁ。

λ. 不完全性定理に関して混乱中 (2)

不完全性定理に関して混乱中の続き。 かがみさんの「モデルでの真偽」というエントリを読んで、考えてみる。

第二不完全性定理の証明では第一不完全性定理の算術化が必要なので、第一不完全性定理で使う概念は、ω無矛盾性を含めて全て算術化可能なのではないかと思います*1。 Tのω無矛盾性は「任意のnについて T ⊢ P(n) ならば T ⊬ ∃x. ¬P(x)」だから、 provable(x) := ∃y. prove(y,x) と定義すると、 ωCon(T) := ∀[P]. (∀n. provable([P(n)])) → ¬provable([∃x. ¬P(x)]) のような感じで算術化可能なはず(表記は少し誤魔化してるけど)。

そうすると、私の知りたかったことは、大体「M ⊧ T∪{¬G} のとき M ⊧ ¬ωCon(T) や M ⊧ provable([¬ωCon(T)]) は成り立つのか?」になるのかな……

まず、M ⊧ ¬ωCon(T) について考えてみる。 T ⊢ Con(T)→¬provable([G]) と T ⊢ G≡¬provable([G]) から T ⊢ Con(T)→G 。 対偶をとって T ⊢ ¬G→¬Con(T) で、したがって T∪{¬G} ⊢ ¬Con(T) 。 完全性定理から T∪{¬G} の任意のモデルMで M ⊧ ¬Con(T) 。 M ⊧ ¬ωCon(T) だけでなく M ⊧ ¬Con(T) まで成り立つのだな(考えてみればあたりまえだけど)。

次に、M ⊧ provable([¬Con(T)]) について考えてみる。 T∪{¬G} ⊢ ¬Con(T) ということは任意の論理式Aについて T∪{¬G} ⊢ provable([A]) であり、従って T∪{¬G} ⊢ provable([¬Con(T)]) 。ということは、M ⊧ provable([¬Con(T)]) も言える。

結論。Mの中で形式化したTは矛盾している。 そして、矛盾してしまったのは、超自然数に対応する証明図がある分、証明能力が強くなっているため。 疑問は解けたが、なんだか少し不思議な感じがするなぁ。

λ. 世界一の債権国、日本に味方はいない

<URL:http://www.h-yamaguchi.net/2007/03/post_3683.html> より。 後で読む。

λ. 民主党的には低金利政策は悪なのか?

週末にTVを見ていたら、自民党が時期日銀総裁に推している現副総裁の武藤氏について、民主党の鳩山由紀夫幹事長が「低金利で国民に多くの損害を与えた責任」を反対の理由に挙げていて眩暈が。 そのときは聞き間違いかと思ったが、民主党の「日銀「武藤総裁」に不同意　役員会で党議決定」という記事にも「バブル経済、超低金利政策に対する反省がみられない」とかあるし……

不況時の金融緩和自体は当たり前だし、当時利上げなんかしていたら景気が更に悪化して国民に大きな損害を与えたことは疑いないと思うんだが、民主党は一体何を言ってるんだ!?　意味が分からない……

【2008-03-17 追記】 低金利と財政政策、金融政策 - lethevert is a programmer (2008-03-13) で言及されていた。 一応補足しておくと、財政政策に言及していないのは「金融政策は財政政策よりも有効」と考えているからではなく、財政政策に関わりなく、また金融政策に限界があるにしても、金利を低水準に抑えるのは当然の政策だからです。

【2008-03-18 追記】 この件に関して民主党の言っていることのデタラメさについては、現在の民主党に政権担当能力はないね - svnseeds' ghoti! (2008-03-11) が良くまとまっている。

【2008-03-25 追記】 泥酔論説委員の日経の読み方(2008-03-19)で知ったのだけど、民主党「次の内閣」は2003/01/29時点の「当面のマクロ金融政策について」では、量的緩和などの政策を継続・強化することを主張していた。

λ. 圏論の講義をYouTubeで

YouTube - TheCatsters's Playlists に圏論の講義のビデオがたくさん。自然変換、モナド、随伴、Hopf代数、etc.,　講義をしているのは高次元圏論の研究者の Eugenia Cheng 女史という方らしい。素晴らしい!　 wrong, rogue and log : モナドの講義をYoutubeで より。