2002-03-16
λ. 38.9℃。某クリニックのお世話になった。若くて有能そうな先生だという印象を受けた。
λ. Ruby 1.6.7
いつのまにかCNSのRubyが1.6.7になってた。
λ. 圏論
オートマトンの圏。あとちょっとでモナドも出てくる。でも、monad じゃなくて monoid って名前になってるのは何故だろう。monoidって identity element を持つ半群じゃなかったっけ?
[追記] monadとmonoidは別物なので注意。
λ. Re: Ruby/GTK vs GTK-2.0
そっか、GTK-2.0ではgdkcursors.hは無くなっちゃったのか。僕のところでビルド出来てしまっていたのは、1.3の時にインストールしたファイルが残っていたからのようです。
2003-03-16
λ. ruby-1.8.0-preview2
AtheOSのRubyのパッケージ 無いと思ったらあったのね。でも、これ拡張ライブラリのダイナミックローディングが出来ないそうだ。それもなんかなぁと思いRubyのCVS版を見ると、configure.inにatheosという文字があったので1.8.0-preview2を試したら、ソース無修整でコンパイル/実行できた。ダイナミックローディングもバッチリでした。
ただ、config.guessとconfig.subが古すぎてatheosを認識してくれないので、これを新しいものに入れ替えるのと、あと現在のatheosはtruncateが未実装で常に失敗するので、インストール時にはinstrubyを編集してインストールした。
どうせなのでバイナリを置いておこう。ruby-1.8.0-preview2.bin.1.tar.bz2
λ. 007 - Die Another Day
家族で見てきた。それなりに楽しめたけど、ストーリィはいまいち。
λ. winBe - The BeOS API on Win32
とよしまさんのWinBeとは別物。ちょっと紛らわしい。
λ. Ruby-GNOME2 Document sites
くぅるだ。さすがむとうさん。(Rubyにまつわるえとせとら日記(2003-03-17)より)
2005-03-16
λ. モナディックシューティング Shu-thing
純粋関数型雑記帳(2005-03-15) と think physically about computation. think computationally about physics. (2005-03-15) より。おー、すげー。
数回プレイして一応クリア出来た。ステージ半ばの7-Way弾を撃ってくる敵が出てくる辺りが一番難しかった。それから、ボスのヤ○○に笑いますた。
λ. 島根県議会、「竹島の日」条例を可決
島根県議会GJ
細田重雄県議の「日韓友好は大切だが、日本の立場や主張を鮮明にする必要がある。国民に竹島問題が広く認識されるよう期待する」という言葉には全く同感。
それから、「竹島の韓国領有権を主張する団体「独島郷友会」の会長で、同県議会を訪れていた韓国の崔在翼ソウル市議が議会棟の玄関付近でカッターナイフを取り出し、近くにいた警察官らに取り押さえられた」というのに驚いた。仮にも公職にあるものが一体何をしてるんだか。
- 基礎知識
-
- 外務省 : 竹島問題
- 日本側の主張
- All About : 竹島問題の基礎知識
- とてもわかりやすくまとまってる
- 『竹島は日韓どちらのものか』, 下條 正男
- より詳しい歴史的経緯を知りたい場合にお勧め
λ. Jan Johannsen's cute title collection
cuteな論文タイトルのコレクション。
ψ やいざわ [竹島に海上保安庁のドックでも作っちゃえばいいのに・・・と思うのはおいらぐらいっすか? # なんか政府のやる気があんま..]
ψ さかい [ドック作るには竹島を不法占拠してる韓国を排除しないと無理ですってば。 > # なんか政府のやる気があんまり感じられ..]
ψ さかい [まあ、北朝鮮問題がある今は韓国との関係をこじらせたくないという政府の立場も、それはそれで理解できるんですけどね。 い..]
ψ やいざわ [いいことを思いついた! 獨立国家「竹島」(コラ]
ψ たけしま [ ＼ │ ／ ／￣＼ ／￣￣￣￣￣￣￣￣￣ ..]
ψ さかい [先生! 元ネタがわかりません! > 獨立国家「竹島」 ひょっとして、日本と国交を結んだりとか、北極海を抜け国連総会が..]
ψ やいざわ [いや，まぁネーミング的元ネタはそれだけども，「いっそ竹島なんぞなけりゃ面倒が無いのに」という皮肉です，はい． # 「..]
ψ さかい [じゃあ、竹島なんて爆破しませう(笑 http://www.f7.dion.ne.jp/~moorend/news/2..]
ψ K [ ＼ │ ／ （ ヽ ／￣..]
ψ さかい [また、しょーもないAAを……]
2006-03-16
λ. Workshop on Linear Logic, Proof Theory and Computer Science (with Lecture Series by Jean-Yves Girard)
に行ってきた。 syd_sydさんやいろんな人にお会いできた。
疲れた。
Jean-Yves Girard (Marseille, IML), “Evolutions of Proof Theory Part I”
生の Jean-Yves Girald にワクワクドキドキ。
- internal と external がなんか良くわからなかった。
- Quantum coherent space とか Hilbert space とか色々わけわからん
昼食
初(UBU)
Naoki Kobayashi (Tohoku University), “Linearity and Order in Type Systems for Programming Languages”
わかりやすい。
- f: File(R)
- read once
- f: File(C)
- close once
- f: !File(R)
- read arbitary times
- f: !File(R); File(C)
- 任意の回数読まれた後に閉じられる
XMLの処理の話を以前にちょっと聞いたときには、Lazyな関数型言語でパースも木の変換も全部lazyにやればいいじゃんと思ったものだが、あるマナーに沿ってトラバースしていることを保障する型システムは非常に面白いと感じた。
- Ordered linear channel types
- Orderdd linear resouce types
- Ordered lineer tree types
Martin Berger (Queen Mary, Univ of London), “Process Calculi and Interaction Types”
Aliasing があると、古典的なホーア論理の syntactic substitution に基づいた規則はうまくいかない。事前条件を詳細化する。例えば「 {(x≠y ∧ !x=7) ∨ (x=y ∧ !y=6)} y := !y + 1 {!x = 7}」。
Sylvain Salvati (NII), “Type systems for syntax”
Montague の話とか出てきてちょっと嬉しかった(ぉぃ
2007-03-16
λ. ロッサーの不完全性定理
かがみさんの「ロッサーの不完全性定理」と通りすがりさんのコメントで情報としては十分過ぎるけど、ちょっと考えたこともあるので一応メモ。
ロッサー文
prove´(x,[A]) := prove(x,[A]) ∧ (∀y≦x. ¬prove(y,[¬A])) として、 T ⊢ R≡¬∃x. prove´(x,[R]) を満たす論理式Rをロッサー文という。 T ⊢ R≡(∀x. prove(x,[R]) → ∃y≦x. prove(y,[¬R])) なので、通りすがりさんが書いているように、Rの直観的な意味は「この命題の証明が存在すれば、この命題の否定のより簡単な証明が存在する」となる。
補題1: T ⊢ A ならば ∃x. prove´(x,[A])
T ⊢ A と仮定する。
- その証明図πが存在し T ⊢ prove([π],[A])。
- Tの無矛盾性より T ⊬ ¬A であり、任意の x≦[π] について T ⊢ ¬prove(x,[¬A]) 。したがって、 T ⊢ ¬prove(0,[¬A])∧¬prove(1,[¬A])∧…∧¬prove([π],[¬A]) であり T ⊢ ∀x≦[π]. ¬prove(x,[¬A]) 。
したがって、T ⊢ ∃x. prove´(x, [A])
T ⊬ R
T ⊢ R と仮定する。
- 補題1より T ⊢ ∃x. prove´(x, [R])
- 一方、T ⊢ R≡¬∃x. prove´(x,[R]) より T ⊢ ¬∃x. prove´(x,[R]) 。
これは矛盾なので、背理法より T ⊬ R 。
補題2: ある定数nについて T ⊢ ∃x≦n. prove(x, [A]) ならば T ⊢ A
T ⊬ A と仮定し、nを任意の定数とする。 任意のx≦nについて T ⊢ ¬prove(x,[A]) であるので T ⊢ ¬prove(0,[A])∧¬prove(1,[A])∧…∧¬prove(n,[A]) で T ⊢ ∀x≦n. ¬prove(x,[A]) 。 すなわち T ⊢ ¬∃x≦n. prove(x,[A]) で、Tの無矛盾性より T ⊬ ∃x≦n. prove(x,[A]) 。
T ⊬ ¬R
T ⊢ ¬R だと仮定する。
- その証明図πが存在して T ⊢ prove([π], [¬R])
- 一方、T ⊢ R≡¬∃y. prove´(y,[R]) より T ⊢ ∃y. prove(y,[R]) ∧ ∀z≦y. ¬prove(z,[¬R])
ここから T ⊢ ∃y. prove(y,[R]) ∧ ¬([π]≦y) で、簡単な定理を適用すると T ⊢ ∃y<[π]. prove(y,[R]) が得られ、補題2より T ⊢ R 。 これはTの無矛盾性に矛盾するので、背理法より T ⊬ R 。
考察
巧妙なのは、「T ⊢ ∃x. prove(x,[A]) ならば T ⊢ A」にはω無矛盾性が必要なのに対して、補題2の「ある n について T ⊢ ∃x≦n. prove(x,[A]) ならば T ⊢ A」には無矛盾性で十分なこと。そして、それが利用できるように論理式Rを構成した点か。ゲーデルのアイディアに比較すれば技術的な微調整に過ぎないかもしれないけど、こういうのも好きだし感心。
算術的階層との関連で考えると、 ∃x. prove(x,y) は Σ1 であって Δ1 ではないのに対して、 ∃x≦n. prove(x,y) は Δ1 というのが効いているのだろうと思う。
次は「クライゼルの注意」について考えるか。
λ. 堀江被告に実刑2年6月「一般投資家欺いた」
有罪自体はそこまで意外ではないけど、実刑になったのは意外。 証取法で実刑なんて結構珍しいのでは。
それと、「堀江被告、即金2億円で再保釈 保証金は5億円」を見て思ったのだが、保釈金って法定利息が付いたりするのだろうか? ……どうやら付かないらしい。供託金には利息がつく*1のに保釈金には付かないというのは少し気持ち悪い気がする。
*1 供託法第3条「供託金ニハ法務省令ノ定ムル所ニ依リ利息ヲ付スルコトヲ要ス」
2008-03-16
λ. 花粉症?
ここ一週間くらい目が痒い＆鼻水出まくりで、認めたくないけどこれは花粉症なんだろうなぁ。一昨年はちょっと痒いくらいで、去年は特に症状はなかったのだが、今年はついにという感じ。 何か悔しいので昨年までと違う何かが原因なんじゃないかと考えてみたら、今年は中国製(?)のヒマワリの種を貪っていることがあった。ひょっとして……まあ濡れ衣だろうけど。
![[ヒマワリの種のパッケージ]](./images/20080316_0.jpg)
![[ヒマワリの種]](./images/20080316_1.jpg)
2009-03-16
λ. 部分継続でDelegateMap
ku-ma-meさんの map が面倒なので DelegateMap を読んで、なんか部分継続(delimited continuation, 限定継続)っぽいなと思ったので、shift/resetで書いてみた。 (shift/reset自体の実装については、call/ccによるshift/resetの表現 - ヒビルテ(2003-05-03) や まめめも(2008-04-17) を参照のこと)
module Enumerable
def dmap2
# Object.__fcall__(:shift) {|k| map {|e| k[e] } }
Object.__send__(:shift) {|k| map {|e| k[e] } }
end
end
p reset { 1 + [1, 2, 3].dmap2 }
#=> [2,3,4]
p reset { 1 + [[1,2], [2,3], [3,4]].dmap2.dmap2 }
#=> [[2, 3], [3, 4], [4, 5]]
まあ、自然言語の「任意の」とかの量化子はまさにこんな感じなので、当たり前といえば当たり前な感じだけど。 参考: “Continuations in Natural Language” by Chris Barker - ヒビルテ (2008-03-13)
