2002-02-22
λ. SF-ADJUSTMENT
いっちーさんが書いているように、どうやらカットアンドペーストのミスが原因だったらしい。おいおい……
λ. 不良債権処理
大手銀行13行の今期の処理額は7兆5000億円前後だそうだ。ところで、デフレが1%進むと不良債権が8兆円くらい増えると何かで見たことがあるんだけど……何で見たかは忘れてしまったので、その辺りの試算とか知ってたら教えてもらえると助かるっす。
ところで、公明党は「不良債権処理を１年で」なんて無責任な事言ってるのね……
2005-02-22
λ. When is a function a fold or an unfold?, Jeremy Gibbons, Graham Hutton, and Thorsten Altenkirch
を読んだ。集合の圏の場合の、関数がfold/unfoldの形で書けるための必要十分条件を与えている。証明は集合論的かつ選択公理を使っているので、構成的な関数の圏に一般化することは出来ない。条件とその証明は非常にシンプルなんだけど、具体例はちょっと不思議な感じもする。
- (∃g:FA->A. h = fold g) ⇔ ker(Fh)⊆ker(h ∘ in) *1
- (∃g:A->FA. h = unfold g) ⇔ img(Fh)⊇img(out ∘ h)
*1 ker(f) = {(a,b) | f(a)=f(b) }
λ. Constructively Characterizing Fold and Unfold, Tjark Weber and James Caldwell
.
2006-02-22
λ. 不動点はたくさん有る?
[haskell-jp:781]の話。(N->N)->(N->N) という型の関数として考えるなら不動点はただ一つと書いたが、もし (Int->Int)->(Int->Int) という型の関数として考えるなら、次のような関数も不動点になっている。
f3(x) :=
if (x == 0) -> 1
else if (x < 0) -> 0
else x * f3(x-1)
2007-02-22 竹島の日
λ. スキー三日目
今日はいきなりエコーコース〜スイングコースというルートに連れて行かれたのだが、スイングコースの28°の斜面が怖すぎる。
メルヘンコース、ファミリーコースは問題なく滑れるようになった。 今日はメルヘンコースを滑るのに大体20分弱。
夜
開拓屋というところへジンギスカンを食べに行った。
![[開拓屋]](./images/20070222_0.jpg)
Wiiで「エキサイトトラック」と「みんなのWii」をやった。
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
