2001-08-26
λ. 頭痛。
λ. 20歳
あと約一ヵ月で20歳か。子供のころは、この下らない世の中に自分が20歳まで生きているなんて、考えたことすらなかった。しかし、不思議なものだなぁ。やはり涙が出るのではあるけれど…
2002-08-26
λ. 本田孝好 「FIREFLY (MOMENT ACT.3)」
一人で暮らすにはこの世界は広すぎる。広すぎる空間は、たった一人の存在の意味なんて、簡単に貶め、押し潰してしまう。そこに確かな痕跡を残すには、僕ら一人一人の力はあまりにか弱く、頼りない。
λ. 夢
中国へツアー旅行で行く夢。何故かドブ川に飛込んで泳いだり。なんか、妙に疲れる夢だった。
λ. freemail
昔作ったfreemailのアカウントを削除。全然使ってなかったし。
λ. Bugzilla
gnome.orgのBugzillaで、Short Summaryに書いた「<」や「>」がエスケープされていない事に気が付いた。これっていわゆるXSS?
2003-08-26
λ. 東方妖々夢
霊夢と咲夜はなんとかクリア出来たんだが、魔理沙がなかなかクリア出来ない。あ、ノーマルの話ね。Extraとか???とかの話じゃないよ。
λ. enum/flags class for Ruby-GNOME2
Ruby-GNOME2の列挙型とフラグ型の扱いを変更して、整数ではなく、固有のクラスのインスタンスとして扱うことにした(変更作業はまだ全部は終わってないけど)。利点は
- 分かりやすさ。例えば Gtk::Label#justify が整数の0を返しても意味は分かりにくいけど、返ってくるのが固有のクラスのインスタンスならば、inspectすれば誰にでも意味が分かる。(今はinspectのフォーマットは「#<Gtk::Justification left>」みたいな感じ。フォーマットは変更するかも)
- 型安全。「Gtk::Label.new.justify = Gtk::Window::TOPLEVEL」とかはTypeErrorになる。
といったところ。
ただ、flagsのクラスのAPIでいくつか悩んでいる。 悩みの1つはフラグをテストするAPIで、 以下の3つを実験的にすべて実装してあるのだけど、 どれを推奨するのが良いかなぁ。
- 「flags & Gtk::Dialog::MODAL != 0」 (これまで通り。でも「!= 0」というのはやはり野暮ったいなぁ)
- 「flags >= Gtk::Dialog::MODAL」 (ビットの集合として考えた時の包含関係で比較演算子を定義してあるので、 最初のコードとは若干意味が異なるけど、これでもテスト出来る)
- 「flags.modal?」(これが一番Rubyっぽい?)
λ. 最近読んだ漫画
λ. Topology Via Logic 進捗
滞ってる。ようやくScott位相がでてくるあたりまでは進んだ。
2004-08-26
λ. Jan-Åke Hedström, "RubySharp - a Ruby to CIL Compiler", [PDF]
Matzにっき (2004-08-20) より。ささださんも書いてるけど「ちょっとなぁ」って感じ。
λ. Anders Alexandersson, "RubyComp - a Ruby-to-LLVM Compiler Prototype", [PDF]
同じくMatzにっき (2004-08-20) より。
2006-08-26
λ. LL Ring
に行ってきた。
sumiiさん、 lethevertさん、 hyoshiokさん、 木山真人さん、 タナカコウイチロウさんに初めてお会いした。 (追記:タナカコウイチロウさんにお会いしたのは初めてではありませんでした。すみません)
到着
Language Update
Haskell の Language Update の発表資料はこちら(PPT, PDF)。
(追記: ソースコードのUnicodeサポートで「λ」に対応しているかのように書いてあるが、実際に試したところうまく動作しなかった。GHC 6.6 のソース中では予約された記号のテーブルに「λ」も登録されているが、実際には「λ」は記号ではなくアルファベットなので、そもそもそのテーブルは参照されないっぽ。GHC 6.6.1 ではテーブルからも削除された)
(2008-11-22追記: kazu-yamamotoさんの GHC でλが使えない理由 - あどけない話 で同じことについて触れられている)
soutaroさんのラクダのマスクは面白かったけど、やはり山羊だと思われていたようだ。予想通り(笑)。
LLで関数プログラミング
lethevertさんも指摘していたが、関数型言語での並列処理の話ではErlangに言及すべきだったと思う。それはそれとして、OCamlでは複数のネイティブスレッドが同時に走らないとか、「今のCleanはConcurrentじゃなかったり」とかの話を比較すると、Haskellは関数型言語の中では並列/並行処理のために頑張っている言語と言えるかも。「Software Transaction Memory」という便利な同期機構があるし、開発版にはSMPサポートも入っているしね。
日本語の扱いは、Haskellは結構嫌な状態にある。Char型はUCS4なのだけど、Hugs以外では外部エンコーディングとの変換が実装されていないため、入出力ではバイトがそのままCharに入ってしまったりする。Gtk2Hsは自前でCharとUTF-8の変換を行っているので一応日本語を表示できる。wxHaskellは、以前に試したときは、Charに外部エンコーディングのバイト列をつっこんでやらないと、正しく表示することが出来なかったと思う。
対戦「じゃんけん2.0」
これはこれで面白かったが、ゲームの戦略のようなものを各言語でどのように記述するかといった話も聞きたかった。
キミならどう書く
睡眠不足のため眠気のピークに。意識が半分飛んでいた。
Ruby on Rails チームで、「モデリングはしっかりやってる」的な話になったときに、「まさか複式?」と思ったら、本当に複式だったので爆笑。
LL Gong
非常に面白かった。眠気が吹っ飛んだ。
ただ、shelarcyさんの「HaskellでGUI」は、スライドすら用意していない のは余りにもあんまりだろうと思った。まあ、私も人のことはあまり言えないけど。
終了後
眠かったし、時間も時間なので、飲み会には参加せず帰宅。
ψ hyoshiok [どうもでした。トップバッターは緊張気味でしたね。 あれ、ラクダだったんですか?馬かと思いましたよ。 しかし、おじ..]
ψ さかい [どうもです。 いやー、あれは緊張しました(^^; > あれ、ラクダだったんですか?馬かと思いましたよ。 そうですよ..]
ψ osiire(通りすがり) [あれ? OCaml の複数のネイティブスレッドが同時に走らないっていうのは、そうなんでしょうか? VM-level ..]
ψ さかい [「複数のネイティブスレッドが同時に走らない」ではなく「同時にOCamlのコードを実行できるネイティブスレッドは一つだ..]
ψ カトウ [Haskell の発表良かったですよ。酒井さんってあの酒井さんだよなー、と思いながら見てました。]
ψ さかい [> Haskell の発表良かったですよ。 ありがとうございます。 そう言ってもらえるとうれしいです。 > 酒井さ..]
2007-08-26
λ. 旅行 二日目
白川郷。「そういえばひぐらしの雛見沢のモデルだっけ」と思い、舞台となった場所を少し探してみたが、あまり見つからず。一応、朝にみょふ〜会の雛見沢村聖地巡礼・小野さん捜索編を簡単に見てはいたのだけど、オチに地図が載っているのを見落としてた……残念。
2008-08-26
λ. QMLからIsometryへの変換
量子テレポーテーションの行列計算 で、ヒープの初期化を扱うためには、射 f : A→B をユニタリ変換からisometryに一般化した圏を考える必要があるらしいということを書いた。
isometryとは
isometryって何かと思ったけど、QML: A functional quantum programming language の 5.4.1 FQC° as isometric operations (p.87) によれば、以下のようなものだそう。
An isometry is a completely positive, distance preserving isomorphism between metric spaces. In the case of strict quantum computations the mapping is between pure quantum states, represented in the usual way as complex-valued vectors. The distance function in quantum mechanics is given by the inner-product.
……単に距離を保存する写像くらいに思ったら、意外と条件が多いのね。
completely positive については Choi's theorem on completely positive maps に説明がある。エルミート行列でかつ固有値が非負なのが positive maps で、id⊗M が常に positive map になる M が completely positive maps 。
しかし、ヒープの生成・初期化というある意味非可逆な操作を実現するために導入したいものなのに、同型だとかエルミートだとかいうのは異様に強い条件で、明らかに変だ。
というか、どうもQMLの文脈では、単に距離を保存する線形写像という意味で使われているように思える。
コンパイル例
例によって、量子テレポーテーションのプログラム
-- The Teleport algorithm Tele (a,qb) |- let (b,c) = Epr () in let f = Bnmeas (a,b) in U (c,f) :: qb;
をコンパイルしてみると以下のようになる。
Prelude QML> runI "teleport.qml" "Tele" OK (2, Isom input = 1, Isom output = 3, ([True],[True,True,True],0.4999999999999999 :+ 0.0) ([True],[True,True,False],0.4999999999999999 :+ 0.0) ([True],[True,False,True],0.4999999999999999 :+ 0.0) ([True],[True,False,False],0.4999999999999999 :+ 0.0) ([False],[False,True,True],0.4999999999999999 :+ 0.0) ([False],[False,True,False],0.4999999999999999 :+ 0.0) ([False],[False,False,True],0.4999999999999999 :+ 0.0) ([False],[False,False,False],0.4999999999999999 :+ 0.0))
これを行列で書くと以下のようになる。
これは量子テレポーテーションの行列計算で得られたユニタリー変換Uに、ヒープの生成・初期化に相当するisometry -⊗|00〉 : Q2 → Q2⊗Q2 を結合したisometry になっている。
まとめ
Q2⊗Q2⊗Q2→Q2⊗Q2⊗Q2 から、 Q2→Q2⊗Q2⊗Q2 になって、id : Q2→Q2⊗Q2 にちょっと近づいた。後はsuperoperatorの圏に移れば、Q2→Q2にすることが出来て、idと等しくなるはず……
2011-08-26
λ. “The worker/wrapper transformation” by Andy Gill and Graham Hutton
を読んだ。
GHCでお馴染みの worker-wrapper transformation についての論文。 私は worker-wrapper transformation というと非ボックス化(unboxing)のための手法という認識だったが、この論文では再帰する際の型を変更する変換として一般化して形式化しており、それを適用するための前提条件と、以下のような幾つかの例を紹介している。
- リストのreverseの素朴な再帰的定義から蓄積変数を利用する定義への変換
- 階乗を計算する関数の非ボックス化
- フィボナッチ数列を計算する関数のメモ化
- 例外を持つ言語の評価機のタグレス化
非ボックス化以外の例を worker-wrapper transfomration として形式化できるだなんて、考えたことがなかったので、驚いた。 ただ、それらはコンパイラが自動的に行うのは難しく、むしろ人間が使うための推論規則ではあるのだけれど。
2012-08-26
λ. Tseitin encoding と pseudo boolean constraint
任意の命題論理式は Tseitin encoding というを使うと、元の論理式に対して線形サイズであるような equisatisfiable なCNFへと変形できる。
その際に、連言 l1∧…∧ln を表現するために、新たな変数cと ¬l1∨…∨¬ln∨c (すなわち l1∧…∧ln → c) および ¬c∨li (すなわち c→li) という形の節を導入し、もとの連言をcで置き換える。ただし、PB制約(Pseudo Boolean constraint)が使える場合には、後者の ¬c∨li という形のn個の節の代わりに n*c ≦ l1+…+ln という形の単一のPB制約を加えても良いことが知られている。
しかし、いずれの方法が効率が良いだろうか? DPLLで解くことを考えると、 制約数の増加はそれほど問題ではないので、unit propagation の効率から節を用いた方が良さそう。 一方、LP緩和と単体法を用いる場合、制約数の増加は結構問題になりそうなので、節にすることで緩和問題の実行可能領域が狭められるメリットと、制約数の増加のデメリットのトレードオフになりそう。
といっても、どれくらい狭まるのかピンとこなかったので、2つのリテラルの連言x∧yの場合について、Sageでプロットしてみた。 どちらの場合についても、新たに導入した変数の取りうる値の範囲は下に閉じていることは明らかなので、この変数の最大値を x, y に関してそれぞれプロットしている。それぞれ、色のついた面よりも下の部分が実行可能領域。
x, y = var('x,y,z') plot3d(x+y / 2, (x,0,1), (y,0,1))
plot3d(min_symbolic(x,y), (x,0,1), (y,0,1))
こうしてみると、確かに範囲は限定されているねぇ。どれくらいのメリットがあるかは分からないけれど……