2009-02-02 [長年日記]
λ. pure crisis :)
haskell-cafe の pure crisis :) というスレッドがちょっと面白い。「pure functional denotation for crisis: (_|_)」に対する、「Thus, when people try to evaluate the amount of savings they have left, their behavior frequently becomes _undefined_ :)」とか。
2009-02-03 [長年日記]
λ. 『奥様はネットワーカ』 森 博嗣
読了。
昔、ダ・ヴィンチで時々読んでたけど単行本になってたんだねぇ。
詩的な文章とコジマケン氏のイラストがマッチした、この独特の雰囲気はやっぱりいいなぁ。
昔読んだときは、それほど面白いとは思わなかったけど、改めて通して読んだら、とても面白かった。
Quotation
p.14 より。
私の今の本名は三枝智佳なんだけど、これもここで使うことは滅多にない。旧姓の内野という名前で私はずっと呼ばれている。それに、ネットではスージィがハンドル。つまり、耳なら「内野」、目なら「スージィ」に反応する習慣。
洋侑さんが、私をどう呼ぶのかは、秘密にしておこう(今、私、笑ったわよ。可愛いんだ)。それは、子供にだって教えられないことかもね。
2009-02-07 [長年日記]
λ. 権利者団体が補償金制度に対し会見--Blu-ray課金を機に適正な見直しを
ブルーレイが補償金制度の対象になること自体は割とどうでも良いのだけど、「デジタル私的録画問題に関する権利者会議（Culture First推進91団体）」による声明「ブルーレイディスクの早期指定を求めます」にちょっと「アレ?」と思うところがあった。
なお、昨年6月に経産、文科両大臣の合意が発表され、またダビング10も実施されながら、約7カ月間も指定が実行されていないことについては、極めて異常な事態と言わざるを得ません。仄聞するところによれば、今回の政令案策定に関する経産、文科両省の調整過程において、「現行の録画補償金はアナログ放送の録画に限定したものである」との解釈が述べられ、その解釈に基づく制約を政令案に付すべきとの主張がされたようです。しかしながら、経産、文科両大臣の合意においては、今回の指定が、デジタル放送のコピールールであるダビング10の早期実現のための環境整備であるとのことがすでに明言されており、このような主張が行われること自体あり得ないことです。よって、今回文化庁から示された政令案につきましては、関係者が速やかに合意されるものと確信しております。
経産・文科両大臣の合意を理由に「このような主張が行われること自体あり得ないこと」と言われてもなぁ。
というのも、両大臣の合意がダビング10の早期実現のための環境整備であるのはその通りなのだけど、その合意についての平成20年6月17日大臣会見概要を読むと、あくまで暫定的措置としてブルーレイを私的録画補償金制度の対象に追加するというだけでしかなく、そのこと自体がデジタル放送の録画が本来補償金制度の対象であるか否かを含意することは無いように思えるので。
大体、2008年6月17日（火）デジタル私的録画問題に関する権利者会議28団体と社団法人日本芸能実演家団体協議会加盟61団体（賛同団体）自身が「ブルーレイディスクを現行補償金制度の対象とすることについて」への声明文発表では「デジタル放送に着目したものであるか明確でない」と言ってたわけで。
2009-02-08 [長年日記]
λ. 第四十九回圏論勉強会
今日は圏論勉強会だった(写真)。 今回は、かがみさん、nucさん、Mさんにお会いすることが出来た。
前回で、S. Abramsky "Temperley-Lieb algebra: From knot theory to logic and computation via quantum mechanics" が終わったので今回から新しいテキスト。 新しいテキストは Peter Selinger による絵算のサーベイ論文“A survey of graphical languages for monoidal categories”で、今回は圏とモノイダル圏の定義とそれらに対応する図形言語(p.10 の Graphical language の前まで)。
p.57 の Table 9: Summary of monoidal notions and their graphical languages が楽しいな。
圏を導入するところで「For a gentler introduction, with more details and examples, see e.g. Mac Lane[23].」(強調酒井)と書いてあって、「そうか、あれはgentleだったのかー」などと思う。 「やさしい Haskell 入門 (バージョン98)」(A Gentle Introduction to Haskell, Version 98)が全然やさしくないと感じるのと同じような感覚だろうか。
ボックスの左上の黒い四角は誤植か何かかと思っていたら、後から「Remark 2.2. We have equipped wires with a left-to-right arrow, and boxes with a marking in the upper left corner. These markings are of no use at the moment, but will become important as we extend the language in the following sections.」と書いてあった。
数式や射を表す式の中に現れる変数について、「シンボル」「任意の値を表すプレイスホルダー」「任意の項を表すプレイスホルダー」の三つの見方があると明示的に説明していたのは良かったな。
(後で書く)
飲み会で、限定継続(delimited continuation)の話が出たので、 call/ccによるshift/resetの表現 - ヒビルテ(2003-05-03) で書いたような例で説明してみる。
帰りに、かがみさんに Snake lemma というものを教えてもらった。 それから、有理数から実数の埋め込みは位相空間の圏で全射だそうだ(c.f. Rng で「monoかつepiであって同型射でないもの」)。 昔[mixi] 圏論勉強会 | 質問とかしてみるトピで話していた、epi but not surjective な例を少し思い出す。
2009-02-22 竹島の日 [長年日記]
λ. Paradoxで数独を解く
ふと、一階述語論理のモデル発見器であるParadoxを使って、数独を解いてみた。
Paradox
Paradoxは等号付き一階述語論理の有限モデルを探してくれるツールで、一階述語論理の問題を一連のSAT問題に変換して、SATソルバを使うことでモデルを探してくれている。実装にはHaskellが使われていて、SATソルバにはMiniSatが使われている。
入力ファイル sudoku.tptp
% 数の定義 (Paradoxは数をサポートしていないので、単に項として扱う) fof( dom1, axiom, ![X] : (X=1 | X=2 | X=3 | X=4 | X=5 | X=6 | X=7 | X=8 | X=9) ). fof( dom2, axiom, 1!=2 & 1!=3 & 1!=4 & 1!=5 & 1!=6 & 1!=7 & 1!=8 & 1!=9 & 2!=3 & 2!=4 & 2!=5 & 2!=6 & 2!=7 & 2!=8 & 2!=9 & 3!=4 & 3!=5 & 3!=6 & 3!=7 & 3!=8 & 3!=9 & 4!=5 & 4!=6 & 4!=7 & 4!=8 & 4!=9 & 5!=6 & 5!=7 & 5!=8 & 5!=9 & 6!=7 & 6!=8 & 6!=9 & 7!=8 & 7!=9 & 8!=9 ). % 範囲の定義 fof( r1, axiom, ![X] : (r1(X) <=> (X=1 | X=2 | X=3))). fof( r2, axiom, ![X] : (r2(X) <=> (X=4 | X=5 | X=6))). fof( r3, axiom, ![X] : (r3(X) <=> (X=7 | X=8 | X=9))). % 全ての数が全ての行および列に存在する fof( rule1, axiom, ![N,X] : ?[Y] : N=a(X,Y) ). fof( rule2, axiom, ![N,Y] : ?[X] : N=a(X,Y) ). % 全ての数が任意のブロックに存在する fof( rule3, axiom, ![N] : ( (?[X,Y] : (r1(X) & r1(Y) & N=a(X,Y))) & (?[X,Y] : (r1(X) & r2(Y) & N=a(X,Y))) & (?[X,Y] : (r1(X) & r3(Y) & N=a(X,Y))) & (?[X,Y] : (r2(X) & r1(Y) & N=a(X,Y))) & (?[X,Y] : (r2(X) & r2(Y) & N=a(X,Y))) & (?[X,Y] : (r2(X) & r3(Y) & N=a(X,Y))) & (?[X,Y] : (r3(X) & r1(Y) & N=a(X,Y))) & (?[X,Y] : (r3(X) & r2(Y) & N=a(X,Y))) & (?[X,Y] : (r3(X) & r3(Y) & N=a(X,Y))) )). % 既知のマスの定義 fof( given, axiom, a(1,1)=1 & a(1,4)=2 & a(1,7)=3 & a(2,2)=2 & a(2,5)=3 & a(2,8)=4 & a(3,3)=3 & a(3,6)=4 & a(3,9)=5 & a(4,1)=6 & a(4,4)=4 & a(4,7)=5 & a(5,2)=7 & a(5,5)=5 & a(5,8)=6 & a(6,3)=8 & a(6,6)=6 & a(6,9)=7 & a(7,1)=8 & a(7,4)=9 & a(7,7)=7 & a(8,2)=9 & a(8,5)=1 & a(8,8)=8 & a(9,3)=1 & a(9,6)=2 & a(9,9)=4 ).
fofは一階の論理式(first order formula)を追加するためのキーワードで、引数は「名前」「種類」「論理式」という順番になっている。ここでは「種類」としてはaxiomしか用いていないけど、他にもconjectureとかがある。 論理式については、感嘆符(!)が全称量化を表し、疑問符(?)は存在量化を表していることを除けば、普通に読めるのではないかと思う。
実行例
このsudoku.tptpをparadoxに喰わせると、小さなモデルから順に探査していき、領域のサイズが9になったところでモデルが発見される。
% time paradox3 --model sudoku.tptp Paradox, version 3.0, 2008-07-29. +++ PROBLEM: sudoku.tptp Reading 'sudoku.tptp' ... OK +++ SOLVING: sudoku.tptp domain size 1 domain size 2 domain size 3 domain size 4 domain size 5 domain size 6 domain size 7 domain size 8 domain size 9 +++ BEGIN MODEL % domain size is 9 〜中略〜 a(!1,!1) = !1 a(!1,!2) = !4 a(!1,!3) = !5 a(!1,!4) = !2 a(!1,!5) = !8 a(!1,!6) = !9 a(!1,!7) = !3 a(!1,!8) = !7 a(!1,!9) = !6 a(!2,!1) = !7 a(!2,!2) = !2 〜中略〜 +++ END MODEL +++ RESULT: Satisfiable paradox3 --model sudoku.tptp 0.01s user 0.00s system 0% cpu 3.583 total %
これを表の形にすると以下のようになる。とりあえずあってるかな。
179|632|845 428|175|693 563|948|271 ---+---+--- 257|413|968 836|259|417 914|786|352 ---+---+--- 381|594|726 742|361|589 695|827|134
最適化
論理的には上に書いた制約で十分だけど、このままだと既知のマスが少ないときに解を発見するのに時間がかかってしまう。 これは多分、上の規則だけだと一つの行か列かブロックのマスを全部埋めてからでないと矛盾を発見できず、早い段階で枝刈りを行えていないため。 そこで、各行、各列、各ブロックの中に数字が重複して現れないことを表す公理を追加したら、既知のマスが少ない場合でもあまり時間がかからないようになった。
% 各行、各列、各ブロックの中に数字が重複して現れない fof( rule1b, axiom, ![X,Y,Z] : (a(X,Y)=a(X,Z) => Y=Z) ). fof( rule2b, axiom, ![X,Y,Z] : (a(X,Y)=a(Z,Y) => X=Z) ). fof( rule3b, axiom, ![X,Y,Z,W] : ( ((r1(X) & r1(Y) & r1(Z) & r1(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r1(X) & r2(Y) & r1(Z) & r2(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r1(X) & r3(Y) & r1(Z) & r3(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r2(X) & r1(Y) & r2(Z) & r1(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r2(X) & r2(Y) & r2(Z) & r2(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r2(X) & r3(Y) & r2(Z) & r3(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r3(X) & r1(Y) & r3(Z) & r1(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r3(X) & r2(Y) & r3(Z) & r2(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) & ((r3(X) & r3(Y) & r3(Z) & r3(W) & a(X,Y)=a(Z,W)) => (X=Z & Y=W)) )).
まとめ
Paradoxには、Alloyのような便利な集合・関係演算や、SMTのような便利なセオリーは無いけれど、こういった組み合わせ的な問題なら特に問題は無いな。速度的にも、直接SATを使うのに比べたら劣るとは思うが、最適化を入れた後は悪くない速度で動いていると思う。 Alloyと比べると、変なクセのない標準的な一階述語論理で書けるのは一応メリットかも。
- 入力ファイル sudoku-paradox.tptp
- ログ sudoku-paradox.txt
参考
2009-02-23 [長年日記]
λ. Darwinで数独を解く
Paradoxで数独を解いてみたので、そのついでにDarwinでも試してみた。 Paradoxが既存のSATソルバを利用していたのに対して、DarwinはSATソルバの基本アルゴリズムであるDPLLアルゴリズムの一階述語論理版として Model Evolution Calculus というのを考えて、それを使っているとか。 ただ、実際に試してみると、Paradoxより随分時間がかかるようだ。 これは等号に直接対応していないため?
- 入力ファイル sudoku-darwin.tptp
- ログ sudoku-darwin.txt
ψ 竹内 [ParadoxとDarwin、 面白そうですね。僕は相変わらず遅いままの Prologプログラムで数独作ってます。(..]
ψ さかい [この手のツールは結構あるので、色々試してみると面白いと思いますよ。 > 話は変わりますが4月からまたしばらく神奈川..]
ψ とおる。 [ぼくもまえに MEPHISTO の制約システムで数独ソルバーを作ってみました。一階述語論理じゃないので、限界があるん..]
ψ さかい [おお。やっぱり視覚化されてると、見てて楽しいですね。 > 一階述語論理じゃないので、限界があるんですけど。 一階..]
ψ とおる。 [うん。でも、一階述語論理の場合は、可能な値を列挙できるようにルールを与えるものですよね？ 逆にほかの制約解消アルゴリ..]
ψ さかい [うーん。 ParadoxやDarwinで値の列挙が可能なのは、これらのアルゴリズムが有限のサイズのモデルしか探さない..]
ψ とおる。 [ああなるほど。一階述語論理＝有限だと思い込んでました。勉強になりました。]
