日々の流転

λ. 帰りに泳いできた

また帰りに泳いできた。1kmを30分弱で。

λ. Amazonクレジットカード終了

Amazon^®クレジットカード サービス終了のご案内

まじですかー。 20070503#p03に作ってからまだ一年半もたってないのに……。 これまでAmazonクレジットカードをメインで使っていたので、どこに乗り換えたらよいか悩む。

λ. 内積と随伴に関する性質いくつか

量子情報以前に、線形代数の基礎と格闘中。

x = y ⇔ ∀z. 〈x,z〉=〈y,z〉 ⇔ ∀z. 〈z,x〉=〈z,y〉

x = y ⇒ ∀z. 〈x,z〉=〈y,z〉 と x = y ⇒ ∀z. 〈z,x〉=〈z,y〉 は明らか。

一方 x≠y とすると、z = x - y ≠ 0 とおいて、

• 〈x,z〉 - 〈y,z〉 = 〈x-y,z〉 = 〈z,z〉 > 0
• 〈z,x〉 - 〈z,y〉 = 〈z,x-y〉 = 〈z,z〉 > 0

なので、〈x,z〉 ≠ 〈y,z〉 かつ 〈z,x〉 ≠ 〈z,y〉 。

これは、米田埋め込み(Yoneda embedding)についての性質 A≅B ⇔ hom(A,-)≅hom(B,-) ⇔ hom(-,A)≅hom(-,B) にちょっと似ているな。

随伴 A^† の一意性

B,Cが共にAの随伴だとすると、任意の x, y について 〈Bx,y〉=〈x,Ay〉=〈Cx,y〉なので B = C 。よって、随伴 A^† は存在すれば一意。

A^††=A

〈Ax,y〉 = 〈y,Ax〉^* = 〈A^†y,x〉^* = 〈x,A^†y〉 より、A^††=A

(AB)^† = B^†A^†

〈x,ABy〉 = 〈A^†x,By〉 = 〈B^†A^†x, y〉 より、(AB)^† = B^†A^†

λ. 状態ベクトルと統計演算子

考えたことメモ。

線形写像 A : H→H は以下の条件を満たすとき統計演算子(statistical operator)と呼ぶ。

有界線形(bounded linear)

ある c が存在して、任意の x∈H について ‖Ax‖ ≦ c‖x‖

正値(positive)

有界線形でかつ任意の x∈H について 〈x, Ax〉 ≧ 0

自己随伴(self adjoint)

A^† = A

トレースクラス(trace class)

tr A ≡ ∑_k 〈Av_k, v_k〉 が任意の正規直交基底 {v_k} について絶対収束する(absolutiely convergent)。

量子力学では H を可分なヒルベルト空間として、統計演算子 H→H を系 H の状態と定義するそうだ。

状態ベクトル u∈H に対して、ρ : H→H を ρx = 〈u, x〉u と定義すると、ρはちゃんと統計演算子になっている?

線形性

• ρ(x+y) = 〈u, x+y〉u = (〈u, x〉 + 〈u, y〉)u = 〈u, x〉u + 〈u, y〉u = ρx + ρy
• ρ(ax) = 〈u, ax〉u = a〈u, x〉u = aρx

有界線形

‖ρx‖ = ‖〈u, x〉u‖ = |〈u, x〉|‖u‖ ≦ ‖u‖‖x‖‖u‖ = ‖u‖²‖x‖ 。

正値性

〈x, ρx〉 = 〈x, 〈u, x〉u〉 = 〈u, x〉〈x, u〉 = 〈u, x〉〈u, x〉^* = |〈u, x〉|²

自己随伴

〈x, ρy〉 = 〈x, 〈u, y〉u〉 = 〈u, y〉〈x, u〉 = 〈x, u〉〈u, y〉 = 〈u, x〉^*〈u, y〉 = 〈〈u, x〉u, y〉 = 〈ρx, y〉 より ρ^† = ρ

エルミート内積を双線形だと思い込んでいて、計算が合わないことに一週間くらい悩んでしまったorz　実際は一方の引数に関して線形で、他方の引数に関しては反線形。

あと、一般に正値な有界線形写像は自己随伴になっているのだけど、それはまた別に書く。

トレースクラス

tr ρ = ∑_k 〈ρv_k, v_k〉 = ∑_k 〈〈u, v_k〉u, v_k〉 = ∑_k 〈u, v_k〉^*〈u, v_k〉 = ∑_k|〈u, v_k〉|²

これが収束するのは有限次元だと自明だけど、無限次元だとどうやって示すんだろう?

【2008-10-06 追記】 無限次元であっても、ベクトル u は基底の有限個の要素の線形和で書くことが出来るということを教えてもらった。 そうすると、|〈u, v_k〉| は有限個を除いて全て 0 になるため、やっぱり収束する。

λ. 正値な有界線形写像は自己随伴

メモ。

任意の x について 〈x, Ax〉 が実数とする。 このときAが自己随伴であることを示す。

〈x+y, A(x+y)〉 = 〈x, Ax〉 + 〈x, Ay〉 + 〈y, Ax〉 + 〈y, Ay〉 の虚部を考えると、〈x+y, A(x+y)〉, 〈x, Ax〉, 〈y, Ay〉 は実数なので、0 = Im〈x, Ay〉 + Im〈y, Ax〉 となり、Im〈Ax, y〉 = Im〈x, Ay〉 となる。

同様に 〈x+iy, A(x+iy)〉i = 〈x, Ax〉i + 〈x, Aiy〉i + 〈iy, Ax〉i + 〈iy, Aiy〉i = 〈x, Ax〉i - 〈x, Ay〉 + 〈y, Ax〉 + 〈y, Ay〉i の実部を考えると、〈x+iy, A(x+iy)〉i, 〈x, Ax〉i, 〈y, Ay〉i は純虚数なので、0 = -Re〈x, Ay〉 + Re〈y, Ax〉 となり、Re〈x, Ay〉 = Re〈Ax, y〉 となる。

よって〈Ax, y〉 = 〈x, Ay〉 なので、A^† = A 。

λ. 第8回 RHGの逆襲

以下個人的なメモ。シグナル周りとスタックの構造に関する辺りとかは聞いてても良く分からなかったので、特にその辺りは変なこと書いてるかも。

リリース計画等

• 1.9.0-5
  • 9/25予定だったのが10/3に
  • make test 通らない www
  • ちょっと残念
  • リリースだって言っているのに、make test が通らないコミットをした人が……
  • この期に及んで仕様を変えたいという意見が……ことによると1.9.1は1月にずれ込むかも
  • 熱心な人は試してみてっ
• 昨日、幾つかのプラットフォームのサポートのコードを削った
  • 削ったもの
    • VMS : がんばると言っている人はいるので復活するかも
    • human68k
    • DJGPP (MS-DOS)
    • WinCE : 力作だったので残念
    • Classic MacOS
  • 削らなかったもの
    • OS/2
    • bcc32
    • BeOS
• 1.9.1 preview 1 (10/25予定)
  • 仕様フリーズ、この仕様で完成度を高めて1.9.1リリース
  • 何か言いたい人はここまでに
  • ABI fix
    • 大きいのは構造体のレイアウト
    • 1.9.x まで保たれるかは不明
    • 当初は保つ予定だったが、どう考えても無理ということがわかってきた。MVMとか
    • MVMはRubyとは別物にするかも (sasada)
    • やっぱり欲しい (yugui)
• 1.9.1 preview 2 (11/25予定)
• 1.9.1 (12/20予定)

install directory

• 1.8だと/usr/lib/ruby/1.8だった
• 今は /usr/lib/ruby/1.9.0
• 将来も .../1.9.1 に入れたほうがいいか?
• 1.9.1という名前で勝手に既成事実化して文句が出なければ良いかも。
• gtkだとABIが保たれるうちは古い名前で。
• シンボリックリンクを貼る? 両方見る?
• バージョン情報を拡張ライブラリに埋め込んで判断?
• dlsymとかでシンボルをみて判断?
• ABIが変わったら、そもそも拡張ライブラリからlibrubyのシンボルの参照を解決できなくてdlopen相当が出来ない可能性があるので、ロードしてdlsymとかで調べるというのは今の枠組みだと良くないのでは?

instruction sequence

• よくバイトコードといっているやつ
• 他と一緒なのはいやだったのでバイトコードにはしなかった
• バイトコードは通常一命令1バイトで出来るだけ小さく詰め込もうとしてるが、YARVでは1バイトにこだわらずワード(ポインタのサイズ)に。

バイトコード出力

やらなくちゃいけないこと:

• require/load出来るようにする
• 開始時に指定できるようにする

問題:

• 互換性
  • まだまだバイトコードを変えたいと思っている
  • バージョン限定で構わない (yugui)
• 安全性
  • 今のyarvにはverifierがないので、バイトコードをいじると簡単にSEGV。JAVAだとverifierがあるので大丈夫。
  • 責任をどう転嫁するか?
    1. verifierを作る
       • 大体わかってるけど、まじめに考えてないので自信がない。
       • ちゃんと考えて入れようとしたら1.9のリリースは遅れるだろう。
    2. 自己責任
  • c.f. 遠藤さんの作ったverifier
    • YARV のバイトコードベリファイアを作ってみた - まめめも(2008-05-23)
    • YARV のバイトコードベリファイアを作ってみた の続き - まめめも(2008-05-24)

いれちゃったら?

• ビジネスのニーズとしては、ソースを隠した気分になりたいというのがある。
• 出力する仕組みは入ってる
• ロードする側は作ったんだけど、Rubyから使う手段は削ってある (iseq_load)
• これを使って御社のエンタープライズソリューション(ry
• evil-ruby : yuguiさんが作っている邪悪なruby?

本当に難読化可能?

• 難読化は夢で、夢を買いたい人がいる。お金はあるけど、頭の悪い人。
• 契約で縛るときに意味がある。偶然見たりgrepで引っかかったりしないことが重要。なぜわざわざ見たのか? と主張できる。

ファイル構成とか

• ヘッダ /include/ruby/*
  • インストールされる。これまで ruby.hだったのが ruby/ruby.h になった。node.h は ruby/1.9.1/node.h にインストールするというのもありでは?
• パーサとか : parse.y, lex.c.*, …
• コンパイラ : compile.c, iseq.c, …
• VM
  • vm.c
  • vm_*.c/h
  • vm_core.h
    • このなかに大事なVMの構造体とかがはいってる。これを見たら大体VMの構造がわかる。coreというファイル名はやめろという苦情あり。(rm *core* とかするひと)
    • vm_core.hは宇宙が滅んでもインストールされないのか? ⇒ 1.9.1というディレクトリがあったら入れてもいいと思う。1.9.1内では変えないだろうし。
• *.def が増えている ==コード生成⇒ *.inc
  • insns.def
  • defsというディレクトリを作ったのでそっちに移しませんか?(yugui) ⇒ grep出来ないので嫌(sasada)
• いろいろ : main.c, ruby.c
• eval.c
  • 1.8では1万行くらいあったのをeval*に分割、vm*, proc.c に移動などして、骨抜きにした。
• 組み込みライブラリとか: array.c, hash.c, string.c, encoding.c, transcode.c, complex.c, rational.c, …

Pythonだともっと厳密に分けられている

• 分けたほうがいいとも思うけど、signal.cとかどこ? というのは悩ましい。
• ディレクトリ間で相互依存してると何かまずいの? (sakai) ⇒ 気分とか(sasada)

prelude.rb

• 名前はhaskell由来
• 10階にいる髪の長い人が悪用して……
• 先にバイトコードorCにコンパイルしておきたい。そうすれば速くできるかなぁ。

VM (1)

• VMの教科書はコンパイラとバーチャルマシン (IT Text)(今城 哲二/岩沢 京子/千葉 雄司/布広 永示)という本はある。

• 例外処理をポータブルにやるにはどうやるか?

  1. setjmp/longjmp法
  2. 二返戻値法
  3. テーブル引き (JVMの方法)

  YARVではsetjm;/longjmpとテーブル引きを併用。rubyで完結する場合にはテーブル引き。Cの部分をはさむ場合にはsetjmp/longjmpを使う。

• direct threaded code : 省略。詳しく読みたい人は YARV Maniacs 【第 3 回】 命令ディスパッチの高速化 等を参照。
• 命令融合
  • 9? 年にこうやったらいいよ、という提案があったのでそれに乗っかった。
  • opt_insn_unif.def に書いておくと融合。
  • こういうことをやりたかったのでdefからコード生成する変換機を作った。
• オペランド融合
  • opt_operand.def
• 命令融合とオペランド融合とで組み合わせが爆発
  • 今のYARVでは全部出力 七十何命令から命令から二百何十命令になる。コンパイルが遅くなる。コードが大きくなる。
  • 今は両方ともオフにしている (vm_opts.hにオプションがあり)
• この仕組みがあるので、YARVではgeneralな命令しか用意していない
• 近々に早くしたい人はこれを使うといいかも。JITとか入ったら意味無くなるけど。
• コンパイルオプションで制御できる。
• オフにした状態でも、1.8と1.9で active support のパース・コンパイルにかかる時間が、 違いがわかるぐらい違う
• VM屋さんにとっては拘っているところ
• 命令融合があると、命令の番号が変わっちゃう
• 処理の流れ
  • オペランド融合は生成しながら変換
  • 命令融合は生成後に探索して変換
• notはピープホール変換しちゃまずい? メソッド呼び出しににコンパイルされているので大丈夫っぽい。

VM (2)

• vm_opts.h でオプションを設定。SUPPORT_JOKEでgotoが使えるようになる。
• builtin_expect
  • 分岐予測のヒント
  • VCにはたぶんない ... 残念
  • エラー処理とかに使う
  • if (LIKELY(x)) { ... } else { ... }
  • Intel系では最初にくる側の分岐をデフォルトで分岐予測するので、エラー処理が後にくる効かない
  • エラー処理が最初にくるときに if (UNLIKELY(x)) { ... } else { ... } にすると効く
• intel compiler にしたら速くならないの?
  • なる……けど、コンパイル出来なかった。
  • 二段階のコンパイルがintel compiler の想定している使い方でなくて、相性が悪いっぽい。

• instruction sequence の種類
  • top
  • method (def ... end)
  • class (class ... end)
  • block ({ ... })
• メソッドの引数とか、topだと意味無いけど、どの種類でも持っている。
• 引数情報
  • 1.9 から post argument を入れる話が出てきたりして大変だった。
  • メソッドが呼ばれるごとにarg_*をチェック。Rubyが遅いひとつの要因。
• stack_max
  • stack size は argument は含まれない?
  • pushの数を数えて、popは数えてないので、大き目の値がはいってる
• block inlining を試みた残骸
  • メソッドの定義とブロックの定義を持ってきて、というのがひとつの方法だけど、rubyだと意味を保ったままインライン化するのが難しい(面倒)。evalとかbindingとか。breakしたときとか。
  • bindingはあまり出てこないので、binding を予約語にして検出する手はある。
  • 再定義されたときにフラッシュしなくちゃいけない。
  • スタックトレースでメソッドが現れなくなる。けど、sendの最適化が入っていて、obj.send(:foo) で、sendがスタックとレースに出なくなったという前例はあるので、許されやすいかも。

VM (3)

• struct rb_vm_struct
• GVLを明示的に手放す方法 BLOCKING_REGION
• そういうスレッドをとめるには?
  • pythonではサポートされていない
  • yarvでは待ちを解除するときに呼んでほしい関数を指定して貰ってそれを呼ぶ。たとえば read だったら signal 。
  • signal で安全にとめるのはすごく難しい。ロックを手放してからreadに入る前にシグナルが飛んでくると取りこぼしてしまう。readの前にflag sense する方法は、flag sense してから read する前に 飛んでくる可能性があるので何も解決しない。結局、解除されるまで何回も送る方法をとっている。髪の毛の長い人に「これは怖い」と言われて実装。
  • windows だったらシグナルオブジェクトと一緒に指定できて素晴らしいけどstdioには使えない(?)。今の1.9ではusaさんがそれを使うようにしてくれて、止まるようになった。
• VMはスレッドの集合を持っている
• src_encoding_index : これ知らなかった
• control frame いわゆる method frame : これを指すのがcfp
• 割り込みが実行される可能性のある幾つかのパターン
  • Thread#kill
  • シグナルハンドラ (シグナルはメインスレッドに届く)
• Cメソッドを実行中に割り込みが発生すると不味いことになるので、割り込みしていいかとかを interrupt_flag とかで管理。スレッド移す際にGVLを手放す前に...
• 1.9からは set_trace_func をスレッドローカルに出来るように拡張されてる。
• 1.8ではCHECK_INTSでシグナルをチェックしていた。1.9ではRUBY_VM_CHECK_INTSと名前が少し長くなった。UNLIKELYがこのマクロのなかにはいっている。スレッド切り替えも契機にもなっている。
• set timer interrupt
• rubyのスレッドの他に timer thread がいて、定期的に polling、時間がきたら「お前ちょっと自重しろよ」と...
• Thread#kill は pthread_kill で実装している
  • 直接送る?
  • SIGVTALRMでpthread_kill
  • null signal handler を登録しておいて……
  • read とかは EINTER で帰る、帰ったところの CHECK_INTS でチェック

• Procに必要なデータをスタックからヒープに移す部分など、なんで今動いてるのか分からない。
• ここらへんのコードはあまり見ないほうが良い。
  • デバッグしてもらえると助かる。
  • 説明するのが面倒でD論とかでも詳細は省いている。(こういう構造体を使っている。以上。)
  • 1.8の方がひどいと思うので、それよりはまし。
• なんでスタックをひとつにまとめないのか?
  • まとめようとして挫折。
  • メモリのローカリティ的には良くないので頭痛い。
  • 工夫: 二つのスタックを両側から伸ばしてる

その他

• パーサーのどのあたりがVMと相容れず変更する必要があったのか
• MVMはシグナルとか大変
• vm.cとvm_insnhelper.[ch]はほんとに使い分けられているの?
• スコープの管理
  • レキシカルという原則があるのに、それを破壊する悪魔module_eval
  • レキシカルなのにClass.dup すると、違うクラスがはいってるってどうよ。

今後の予定

二次会

• 形式的意味論 ⇔ 民主的意味論
• FFTによる多倍長整数の乗算

関連

• RHGの逆襲 - soutaroにっき(2008-10-05)
• RHG の逆襲 第8回 - PB memo (2008-10-05)
• 第８回RHGの逆襲に参加してきました - プログラマーに憧れるSEの日記 (2008-10-05)

λ. ザリスキー位相

先日、プログラミング言語の方のschemeの話をしていたら、schemeつながりで代数幾何のスキーム(scheme, 概型)の話になり、そこからザリスキー位相の話が出てきた。 そういえば、ザリスキー位相というか Zariski spectrum の話は Topology via Logic の第12章 Spectra of rings でちょっと読んだことがあるな。 この章はおまけ的な章だったので、あまりまじめに読んではいなかったけど、Zariski spectrum って代数幾何で使うような概念だったのか。 代数幾何って魑魅魍魎の世界だと思い込んでいたので、そんなのが自分の知識の中に迷い込んでいたことに、ちょっとビックリだ。

ただ、Topology via Logic ではスペクトルは束のような代数に対して定義されるものだった。なので、環の Zariski spectrum も環のイデアル全体のなすquantaleを考えて、そのquantale上普遍的なフレームに対応するlocaleとして定義していた。そして、その後にこのlocaleの点が元の環の素イデアルに対応していることを示すという流れになっていた。

それに対して今回聞いた話だと、環のスペクトルを素イデアルの全体の集合として直接定義して、後から位相を入れようとしていた。

前者が位相ありきの考え方なのに対して後者は点ありきの考え方で、対照性が際立っていて面白い。

λ. 12.2 Quantales and the Zariski spectrum

読んでいて分かりにくかった点についてメモ。

Theorem 12.2.7 (i)

←: b^r = 1 or b modulo frames なのは、Proposition 12.2.2 より乗算が冪等だから。

→: Fが乗算を保存するのは、(∃r. b^r≦x)∧(∃r. b^r≦y) ⇒ (∃r. b^r≦xy) が乗算の単調性より成り立ち、この逆向きは 1 が最大元であることと単調性から xy≦x1=x と xy≦1y=y が成り立つことから言える。

Theorem 12.2.7 (ii)

→: Aはcoherentなquantaleなので、a∈A はコンパクトな要素からなる集合 S を用いて a = ⋁^↑S と表すことが出来て、[a] = [⋁^↑S] = ⋁^↑{[c] | c∈S} 。[a] はコンパクトなので、ある a´∈S について [a] ≦ [a´] 。一方で当然 [a´]≦[a] なので [a]=[a'] で、あるコンパクトな要素 a´ が存在して a≡a´ であることが示せた。

←: bがコンパクトな要素として、[b] ≦ [⋁^↑S] だとする。 (i)から b^r≦⋁^↑S 。 A は coherent なので b^r もコンパクトで、ある c∈S について b^r≦c 。よって (i) より [b]≦[c] 。

Theorem 12.2.7 (iii)

A/≡_Fr が coherent であることを示すために、Theorem 9.2.2 (iii) で同値であることが示されている条件のうち、finite meet が要素のコンパクト性を保つことを示す。 [a_i]がコンパクトだとする。 (ii) より 各 a_i に対して、コンパクトな c_i が存在して、[a_i]=[c_i] 。 よって、⋀[a_i] = ⋀[c_i] = [∏c_i] 。 coherent であることから ∏c_i はコンパクトで、(ii)より [∏c_i] = ⋀[a_i] もコンパクト。

Theorem 12.2.8

イデアルが有限生成されていることと、quantaleの要素としてコンパクトであることとが同値であることを理解するのに手間取ってしまった。

I が a₁, …, a_n ∈ R から生成されるイデアルだとする。 イデアルの集合 {I_j}_j∈J に対して I⊆⋁_j∈JI_j とすると、a_i∈I⊆⋁_j∈JI_j はjoinの定義より有限個の b_j∈I_j の和で書ける。 よって、a_i は有限個の I_j のjoinの要素になっている。 同様に、{a₁, …, a_n} も有限個の I_j のjoinの部分集合になっているので、{a₁, …, a_n} から生成されるイデアルである I も有限個の I_j のjoinの部分集合になっている。

逆に、Iがコンパクトだとすると、I = ⋁{Ra | a∈I} で、コンパクト性からある有限集合 S⊆I について I = ⋁{Ra | a∈S} で、有限集合Sから生成されるイデアルになっている。

λ. Thinkpadのキーボード交換

Thinkpadのキーボードからキーが取れてしまったので、3日にサポートに電話して交換用部品を送ってもらった。キーボードの部品ってこんな風になってるのね。 交換は Lenovo キーボード取り外し/取り付け手順 - ThinkPad X60/s, X61/s, X60 Tablet, X61 Tablet - Japan に書いてある通りで、とても簡単だった。

本体に同梱されていた紙に書いてあったサポートセンターの電話番号がずいぶん前に変更された古い番号だったのには呆れたけど、届くのも早いし交換が簡単だったので好印象。

λ. 個人向け国債、10月販売額が半減　金融不安で需要が減退

「質への逃避」で国債需要は増しているかと思ったら、個人向けでは逆に減ってるのね。ちょっと意外。

λ. 帰りに泳いできた

今日も帰りに泳いできた。いつものように1kmを30分弱で。

λ. “&” by Christopher J. Mulvey

Quantale - Algebraic Toplogy: A guide to literature に「Quantale とは quantum locale という意味らしい」と書かれていて、Quantaleの語源が気になった。Topology via Logic によると、Quantale という言葉が導入されたのは C.J.Mulveyによる以下の文献らしい*1。

Christopher J. Mulvey, “&”, pp.99-104 in Supplemento ai Rendiconti del Circolo Matematico di Palermo, Serie II no. 12, 1986

This note summarises three intertwining observations, concerned with non-commutative C*-algebras, with constructive foundations for quantum mechanics, and with non-commutative logics, made at the Category Meeting at Oberwolfach in September, 1983

quantaleの名前の由来は書いてなかったものの、量子論理のようなものが念頭にあったのは確かなようで、quantum locale というのは確かにありそうだと思った。

ただ、私はC*-環(C*-algebras)が分かってないので、この論文のメインの部分はぜんぜん分からず、残念……

λ. お菓子補充

λ. 最近、愕然としたこと

自分が最近何ら面白いことを出来ていないことに気づいて愕然とした(仕事はともかくプライベートで)。 特に、自分の作品と呼べるようなものが殆ど何も無いんだよな。 論文の感想なんかだらだら書いてる場合じゃなくて、もっと創造的なアウトプットをしなくちゃ……

λ. Derivatives of Regular Expressions by Janusz Brzozowski

積読論文消化。 文字列の集合 R と有限の文字列 s に対して、R の s による微分を D_s := {t | st ∈ R} と定義する。正規表現の微分は正規表現になっていて、かつ正規表現を微分していって得られる正規表現は(等価なものを除けば)有限個で、それらを状態とする決定性有限状態オートマトンを正規表現から直接作ることが出来る。

関連

• Derivatives of Regular Expressions | Lambda the Ultimate

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

今日は圏論勉強会 だった。

今回は、6節 Planar Geometry of Interaction and the Temperley-Lieb Algebra からで、6.4節 The Temperley-Lieb Category の冒頭部分までを読んだ。 今回のメインは、ダイアグラムや平面性の数学的な定義で、これが非常に巧妙で感心した。 あと、involutionの訳語は「対合」らしい。

余談になるけど、線形写像の圏を考えるとnameは線形写像の行列表現、という檜山さんの話が面白かった。 私の理解を書く。 まず、A→B ⇔ I→B^A ⇔ I→A^*⊗B なので、線形写像 f : A→B は A^*⊗B の要素とみなすことが出来る。 ここで、Aの基底を{a_i}_i, Bの基底を{b_j}_jとすると、A^*⊗B は {a_i^*⊗b_j}_i,j を基底とする空間なので、A^*⊗B の要素はこの基底の線型結合で表すことが出来、そのときの a_i^*⊗b_j の係数を行列のj行i列目とすることで、行列として表すことが出来る。 また、ディラック記法を使うと a_i^*⊗b_j は |b_j〉〈a_i| という ket-bra で書くことが出来、やっぱりちゃんと対応している。

二次会で少し口にした「短時間ならエントロピーが減少し得る」という話は、Decoding the Universe の p.51 で紹介されていた、Experimental Demonstration of Violations of the Second Law of Thermodynamics for Small Systems and Short Time Scales. G. M. Wang, E. M. Sevick, Emil Mittag, Debra J. Searles, and Denis J. Evans. Physical Review Letters 89 (2002) の話。

関連

• 2008-10-12 - たけをの日記＠天竺から帰ってきたよ

λ. うみねこ×汝は人狼なりや？〜序章〜‐ニコニコ動画(秋)

人狼のなく頃にとは (ジンロウノナクコロニとは) - ニコニコ大百科 より。 「人狼のなく頃に」とは言っても、ゲームのひぐらし人狼ではなくて、「うみねこのなく頃に」の舞台で人狼をやる動画。 「ちょっwww、その展開はねーよwww」とは思うものの、面白い。

• マイリスト 人狼のなく頃に‐ニコニコ動画(秋)

λ. SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values

SmallCheck and Lazy SmallCheck: automatic exhaustive testing for small values. Colin Runciman, Matthew Naylor and Fredrik Lindblad. in Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell

を読んだ。

QuickCheck がランダムテストなのに対して、SmallCheck は指定した上限までの範囲の網羅的な検査を行う*1。 QuickCheckでは値が適切に分散するように値の生成機を書くのは簡単ではないが、SmallCheckでは確率を考えながらパラメータをいじったりする必要がない。 また、QuickCheckでは発見された反例は最小のものとは限らないが、SmallCheckは小さいものからテストするので常に最小の反例が見つかる。

SmallCheck は網羅的なテストであるためあまり深い範囲の検査は難しいという問題がある。プロパティの持つ非正格性を利用してそれを解決しようとしているのが Lazy SmallCheck で、データ構造の一部に⊥を含む値をテストの入力として与える。結果がTrueやFalseであれば、⊥の部分を具体的な値にrefineしてもその結果は変わらないはずなので、多くの値に対するテストを省略できる。結果が未定義(エラー)であれば、⊥の部分をより具体的な値にrefineしていく。

それから、Lazy SmallCheck はプロパティの条件部に使うために並列論理積(parallel conjunction)を提供しているのが面白かった。条件部で通常の論理積の代わりに並列論理積を使うことで、生成された値に対する条件の検査結果を未定義(エラー)からFalseにすることが出来場合があり、その場合にはその値をrefineするような値の生成を省略することが出来る。

関連

• <URL:http://www-users.cs.york.ac.uk/~mfn/lazysmallcheck/>
• <URL:http://video.google.com/videoplay?docid=8540922190337591178>
• <URL:http://jp.citeulike.org/user/msakai/article/3406980>

λ. 帰りに泳……がずに帰る

帰りに泳いで帰ろうと思ったら、点検中だか工事中だかでプールが閉まっていた。しょぼーん。

λ. Planarity

久しぶりにPlanarityやった。 懐かしい。

λ. Jerry needs no help playing with his ball.

SFC CLIP: 「パブロフの犬」もIT革命の時代 (2008年10月17日) より。 かわゆす。

λ. ウォンテッド

映画のウォンテッド観てきた。期待していたすごい動きをする弾丸とかはあんまし無かったけど、アクションは良かったし、Danny Elfman の音楽がいい味を出していた。

λ. 建碑法要など

小雨(?)の中、建碑法要。 ビストロ ラ・シャンソン デリカテッセン デリシューで昼食。 プールで1km泳いでから帰る。

λ. Seven Trees やっと解けた

一部で流行っていた Seven Trees の問題。 乗り遅れてしまって、等式変形をどうやるのか一人寂しく悩んでいたのだけど、Tⁿ + Tⁿ⁺³ = T^m + T^m+3 が成り立つことに気づいて、ようやく等式変形が出来た。

• 1 + T³ = 1 + T² + T⁴ = T + T⁴ = T(1 + T³)
• 帰納法により 1 + T³ = Tⁿ + Tⁿ⁺³
• よって Tⁿ + Tⁿ⁺³ = 1 + T³ = T^m + T^m+3 for all n, m
• ゆえに T = T⁰+T² = T⁰+(T¹+T³) = T¹+(T⁰+T³) = T¹+(T⁴+T⁷) = (T¹+T⁴)+T⁷ = (T⁶+T⁹)+T⁷ = T⁶+(T⁷+T⁹) = T⁶+T⁸ = T⁷

等式変形が出来たら、同型の証明をAgdaで書こうと思ってたのだけど、関数として書くのが案外面倒そうなので、なんだかもういいやという気分になってしまった。 しかし、中野さんの5種類のパターンの分岐で定義ってのは分からなくて、気になるなぁ。

関連

• Seven Trees：解答のトラックバック受け付け所

λ. Seven Trees 問題を定理自動証明器を使って解く

Seven Trees 問題を解くときに、一階述語論理の定理自動証明器を使って解けないか試していた。 そのためには、以下の等式を公理として、T = T⁷ を証明させれば良い。

1. x+y = y+x
2. x+(y+z) = (x+y)+z
3. x×y = y×x
4. x×(y×z) = (x×y)×z
5. x×(y+z) = (x×y)+(x×z)
6. 1×x = x
7. T = 1+T×T

最初にSPASSで試したのが 7trees.dfg だけど、これは止まらなかった。 可換性と結合性を直接サポートしていないのが不味いのではないかと思い、The E Equational Theorem Prover で試してみたのが 7trees.lop で、これもやっぱり止まらなかった。 あと、EQPなんかも試してみたが、これは使い方がいまいち良くわからなかった*1。

ここで諦めて結局手で解いてしまったのだけど、ふと思いついて以下のような公理(を途中で打ち切ったもの)から T1 = T7 を証明させてみたところ、うまくいった。

1. x+y = y+x
2. x+(y+z) = (x+y)+z
3. T1 = T0+T2
4. T2 = T1+T3
5. …

これはいわば全て展開した多項式だけを対象にすることにしたもの。 ここで T^k+1 = T^k + T^k+2 は最初の公理系の定理なので、Tk を T^k で解釈すれば、この公理系における証明から最初の公理系における証明が得られる*2。 で、実行してみたところ、SPASSでもEでも一瞬で証明できた。 出てきた証明は、「Seven Trees やっと解けた」で手で導出したものと、ほぼ同じもの。

• 7trees2.dfg
• 7trees2.lop

人の目から見るとどっちの公理系も同じようなものだけど、ちょっと工夫して問題を変形してやるだけで自動定理証明には劇的な効果がある、というのが面白かった。

【2009-02-15追記】 さらに、他の定理証明器として Prover9 と Equinox でも試してみた。

• Prover9は既に試した定理証明器と同じく、元の問題7trees.inは止まらず、単純化した問題7trees2.inは一瞬で解けた。
• Equinoxは残念ながら元の問題7trees.tptpでも単純化した問題7trees2.tptpでも止まらなかった。

λ. 水泳1km

今日も帰りに1km泳いできた。 かかる時間はちょっとずつ短くなって、今日は1kmで25分くらい。

λ. 【金融危機】日銀、利下げも検討　急激な円高・株安を懸念

「金融緩和を検討する」と言いつつ、実際には「日銀は独自の施策として、金融機関が日銀に預けている当座預金に利子を付ける方針」という、まるで正反対のことをしてるのね。 意味不明すぎる。 これが日銀クオリティwww