日々の流転

λ. こともなし

λ. ミクロ経済Ⅲ

テスト大失敗。なんだか頭がボーっとして、集中できなかった。落ち着いて考えれば解ける問題だけに悔しい。悩みが「A欲しいなぁ」から「単位くるかなぁ」に変わってしまった。(T_T)

λ. friday_noon

……頓挫。中村さんにミスドでドーナツをおごってもらう。

λ. friday_night

friday_noonのはずだったのに、いつの間にかfriday_nightに...

まずは、藤沢ボウルでボーリング。1ゲーム目は「100点以下の人は (100-得点) 本の論文を書く」、2ゲーム目は「合計得点が250点以下の人は、(250-得点)×100 行のコードを書く」という、良く分からんペナルティを設定してみた。ペナルティを設定したら、とたんにみんなストライクを出したりして、「そんなに論文書きたくないのかっ(笑)」とか言いあってみたり。

その後、Jパスタで夕食。「チキンのカリビアントマトソーススパゲティ」他。

λ. 『マンガ嫌韓流』

とりあえず予約。割とお勧め。韓国への反発を煽るつもりはないけど、韓国には「韓流」として喧伝されているような面だけでなく、こういった面もあるということは知っておくべきだと思う。まあ、まともな知識があったり、あるいはハン板やNAVERを見ている人には不要だろうけど。

FAR EAST -極東-

作者のサイト

晋遊舎ONLINE: マンガ嫌韓流

出版社による公式サイト

脱・マンガ嫌韓流

-

「嫌韓流」を韓国人が斬る・・・　斬り!! :今だからこそ・・・　韓国斬り　!!

-

MyWiki.jp - マンガ嫌韓流のここがデタラメのここがデタラメ

「コモンズ社発行の『マンガ嫌韓流のここがデタラメ』に記載されている内容の間違いを指摘する為のページ」

λ. 某F氏の机の本

トポスとかの本と、コーポレートファイナンスが並んでるのが素敵。

λ. Otter で 3 not problem を解く

20080716#p02で紹介したように、3 not problemを定理証明機のOtterに解かせる例が <URL:http://www-unix.mcs.anl.gov/AR/otter/examples33/program/two_inv.in> にあるので、実際に実行してみた。以下ネタバレ注意!!

• 実行ログ
• 証明から抽出した回路をGraphvizで適当に整形したPNG (.dot)

今だと25秒で解けているが、当時の486マシンで40分かかったそうで、大体100倍高速化した計算か。

Otterの入力ファイルをまじめに読んだのは初めてだったのだけど、Prologみたいに結構汚いことが出来るのね。$VARなんてPrologのvarメタ述語そのものじゃないか。そして、汚いけど、このリソースの扱い方は非常に巧妙で感心した。 記述する論理を線形一階述語論理にすれば、もっと素直に書けるだろうとも思うが、そういえば線形論理の定理証明機とかってあまり聞かないな。 線形一階述語論理に基づいた線形論理プログラミングよりも更に聞かないけど、なんでなんだろうね。

ついでに、Otterの後継のProver9でも試そうと思ったのだけど、Prover9はOtterよりも純粋な定理証明機のようで、同じテクニックは使えなさそうだった。うーむ。

λ. 日本Ruby会議2009 2日目

後で書く

Ruby 1.8 のゆくえ / 卜部 昌平

クリスマスリリースの制約がなくなったため(?)、1.8系のリリース間隔は伸びている。 Joe Damato の提案している インラインアセンブラを使ったパッチ(Fixing Threads in Ruby 1.8: A 2-10x performance boost)があって、自前でスタック確保して切り替えをするので2-10倍くらい早くなる。1.8.9 は多分無い。 質問を受けるだけで、答えるのはircとかまつもとさんとかという素敵なシステム。

Ruby 1.9.2ロードマップ / Yugui - 園田 裕貴

バージョン番号をけちる文化。拡張ライブラリの互換性。RSTRING_PTR / RSTRING_LEN などを使う必要がある。rb_str_newで文字列をつくるとバイト列としての文字列になるので、ちゃんとエンコーディング情報を指定して作る必要がある(rb_usascii_str_newなど)。 はやくパッチをマージしてください。 1.9にしたくて、ライブラリに片っ端からパッチを送ってる。Rubyは正論の通るコミュニティなので、不満はパッチに。

静的コード解析統合環境の試作 / 勝間 友久

静的コード解析ということで coverity 的なものを期待して行ったら、古典的なメトリクスの測定とlint的なソースコードの検査の話だったのでちょっとがっかり。 利用しているエンジンについてはranhaさんが書いているInfoQ: 静的解析ツールの総まとめ：Roodi、Rufus、Reek、Flayに簡単な紹介がある。 Ruby固有の問題や知見について質問してみたが、それはまだまだこれからのようだった。

基調講演 / まつもとゆきひろ

席にいくつかnilがはいってるのでArray#compactしてください(by 角谷さん)。lvar_propagateとか面白そう。

Lightning Talks

斉藤ただしさんのDecimalの話が面白かった。

分散並列処理フレームワークfairyと分散オブジェクトシステムDeepConnect / 石塚 圭樹、増田 創

.

偉大なBigTableとぼくのおもちゃ / 関 将俊

.

concov: 時系列に注目したテストカバレッジビューア / 遠藤 侑介

遠藤さんの発表はconconvの話も面白かったが、後半のあまった時間で関係ないことをしゃべりまくるフリーダムな感じが面白かった。

RubyのGC改善による私のエコライフ 〜レジ袋は結構ですよ(2009夏)〜 / nari

NODEを長寿命オブジェクトとして世代別GCをするとう話だったが、RubyKaigi直前にささださんがNODEをGC対象でなくてしてしまって涙目という話。 私が「GCはよくわかってないんですが」といって世代別GCの基本的なことについて質問したら、その後の質問者がみんな同じような聞き方をしていてうけた。 それから、去年のRubyKaigiで発表していたLazySweepの話はどうなったのか質問してみた。Rejectされたと思っていたら、自分でRejectしてたらしいw　 それにしても、nariさんは愛されてるなぁ。

お昼はranhaさん、soutaroさんと、ろしあ亭というところに。

λ. IDPで 3 not problem を解けなかった

以前に

• 3 not problem - ヒビルテ(2008-07-16)
• Alloy で 3 not problem を解く - ヒビルテ(2008-07-16)
• Otter で 3 not problem を解く - ヒビルテ(2008-07-18)

辺りで書いた 3 not problem (別名: The 2-inverter puzzle) を、IDP (Inductive Definition Programming) で解いてみようとした。 が、うまくいかなかったという話。

回路の構成自体を解として直接求めるのは、Alloyや他のソルバーでうまくいってなかったので、Otterの場合と同じく、notを使う箇所だけを解として求めることにした。 具体的には「notを適用する真理値表Inv1,Inv2が与えられた時に真理値表xsが計算可能である」ことを表す述語P(xs)を帰納的に定義して、出力となる真理値表がこの述語を満たすときのInv1,Inv2の値を解として求める。 一階述語論理の普通のモデル発見器では帰納的な定義ができないので、こういうやり方を出来るのは、IDPとかASPくらいのはず。

定式化自体は two_inv.idp.gz のように非常に簡単にできた。ただ、ビット演算のやり方が分からないので、そこは定数とテーブルを自前で用意することで対処した。その辺りのつまらない部分を省略したものを以下に示す。

Given:
  type BV8 = {
B00000000;
B00000001;
〜(中略)〜
B11111111;
} 
  BIT_NOT (BV8) : BV8
  BIT_AND (BV8,BV8) : BV8
  BIT_OR (BV8,BV8) : BV8

Find:
  Inv1 : BV8
  Inv2 : BV8

Declare:
  P (BV8)

Satisfying:
  { P(B00001111). // input 1
    P(B00110011). // input 2
    P(B01010101). // input 3
    P(BIT_AND(x,y))  <- P(x) & P(y).
    P(BIT_OR(x,y))   <- P(x) & P(y).
    P(BIT_NOT(Inv1)) <- P(Inv1).
    P(BIT_NOT(Inv2)) <- P(Inv2).
  }
  P(B11110000). // output 1
  P(B11001100). // output 2
  P(B10101010). // output 3

Data:
  BIT_NOT = { 
B00000000 -> B11111111;
〜(中略)〜
B11111111 -> B00000000;
}

  BIT_AND = {
B00000000,B00000000 -> B00000000;
B00000000,B00000001 -> B00000000;
〜(中略)〜
B11111111,B11111111 -> B11111111;
}

  BIT_OR = {
B00000000,B00000000 -> B00000000;
B00000000,B00000001 -> B00000001;
〜(中略)〜
B11111111,B11111111 -> B11111111;
}

だけど、実際に gidl.exe two_inv.idp | midl.exe と実行してみたら、midl.exe が「This application has requested the Runtime to terminate it in an unusual way. Please contact the application's support team for more information.」で落ちた。残念。

関連

• IDPで数独を解く - ヒビルテ(2009-03-04)
• The IDP framework for declarative problem solving - ヒビルテ(2009-08-13)

λ. ASPで 3 not problem を解いた

IDP (Inductive Definition Programming) でダメなら、解集合プログラミング(Answer Set Programming, ASP)でということで、やってみた。 ソルバには例によって、Potasscoで配布されているclingoを利用。入力は以下のようにした(two_inv.lp)。IDPの場合と違って、ASPの場合はプログラム全体が帰納的定義になっていて、欲しい結果がpに含まれない場合を一貫性制約(integrity constraint)を使って弾いている。

% domain predicate
bv8(0..255).

% inv(X)を満たすbv8(X)はたかだか2つ
0{inv(X) : bv8(X)}2.

p(15). % input 1 (15 = 0b00001111)
p(51). % input 2 (51 = 0b00110011)
p(85). % input 3 (85 = 0b01010101)
p(X & Y) :- p(X), p(Y), bv8(X), bv8(Y).
p(X ? Y) :- p(X), p(Y), bv8(X), bv8(Y).
p(~X & 255) :- p(X), inv(X), bv8(X).

% integrity constraint
:- not p(240). % output 1 (240 = 0b11110000)
:- not p(204). % output 2 (204 = 0b11001100)
:- not p(170). % output 3 (170 = 0b10101010)

これを clingo-2.0.3-win32.exe -n 0 two_inv.lp として実行した結果が two_inv_asp.txt 。オプションの -n 0 はモデルを全て列挙するという指定で、出力から inv(23), inv(105) なるモデルが唯一のモデルであることがわかる。 このnotを使う箇所は当然ながらOtterが見つけたものと同じものになっている。 このモデルから直接分かるのは、2つのnotを使う箇所だけだけど、ここから回路全体を構成するのは難しくない。

ASPすごいな、と初めて思ったよ。

関連

• ASPで数独を解く - ヒビルテ(2009-04-21)

λ. 何故ASPがすごいと思ったか補足

なんでASPがすごいかと思ったかというと、Pが帰納的(最小)であるという制約を除いたものを、有名なSMTソルバーであるYices(1.0.28)とCVC3(2010-07-11)に食わせてみて、ぜんぜん答えが出なかったので。

• test-yices.ys
• test-cvc3.cvc