はてな記法
いままで使ってなかった。。。。
ちょっとはてな固有でやだけど楽にハイライトできるから使ってみるかな。。。
-- Simple example for Bang-Patterns leak import Control.Monad import Data.Foldable ( foldr' ) import System.IO main :: IO () main = do result <- takeStat (return 100) 10000000 print $ "result is " ++ show result takeStat :: IO Int -> Int -> IO Int takeStat io count = foldr' (liftM2 (+)) (return 0) $ replicate count io
でも未だGist埋め込みと迷っている。。。。
世界一難しい数独＠Alloy(cont'd)
下記のような記事を見つけた。
なんと以前の記事を見てdisktnkさんという方が「遅すぎる」と検証してくださったようだ。。。
Lets's Compare!
ぼくの実行結果
Executing "Run run$1 for 13" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 77305 vars. 2201 primary vars. 146903 clauses. 3635ms. . found. Predicate is consistent. 82243ms.
disktnkさんの実行結果
Executing "Run game" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2725 vars. 729 primary vars. 3303 clauses. 508ms. . found. Predicate is consistent. 2681ms.
なんだこの複雑度の差は、、、、述語数が30～40倍くらいちがう。僕の実行環境がNetbookでバカ遅いという状況をはるかに超えている。。。たしかに余計な述語が多かったんだよな。
精進します。
入門 Verilog
長らく堪えていたが、耐え切れなくなってポチってしまった。夏休みの積ん読リスト入り。
世界一難しい数独、Alloyで解いてみたよ(RocketNews24から)
RocketNews24さんで 本当に解ける人いるの？ フィンランド人数学者が作った “世界一難しい数独” が発表されるという記事があったんで以前のAlloyの記事で使ったモデルを流用して解いてみた。
about alloy Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.
- 結論：
- 実は自分は数独のルールをわかっていなかった。
- 前回より工夫したところ：
- 数字をOne,Twoといったような表記ではなく、C01とか数字が入った表現にした。
- 数独って、9x9の枠の中でカブっちゃいけない、ってルールがあったんだ。。。。ということに気づいてルールを追加した。orz
では、以前のモデルを一部流用して解いてみます。
↓9x9のグルーピングを追加
abstract sig Index {}
sig Col extends Index {
cell : Index -> Index
}
abstract sig G01,G02,G03 extends Col {}
one sig C01,C02,C03 extends G01{}
one sig C04,C05,C06 extends G02{}
one sig C07,C08,C09 extends G03{}
縦、横の重複禁止ルールの他に9x9の重複禁止ルールを追加
// 縦横の禁止
fact{
all c:Col, r1,r2:Index | (r1=r2)or(not(cell[c,r1]=cell[c,r2]))
}
fact{
all c1,c2:Col, r:Index | (c1=c2)or(not(cell[c1,r]=cell[c2,r]))
}
// 9x9の重複禁止
fact{
all c1,c2:G01, r1,r2:G01 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
fact{
all c1,c2:G01, r1,r2:G02 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
:
実際に解かせてみると。。。。
Executing "Run run$1 for 13" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 77305 vars. 2201 primary vars. 146903 clauses. 3635ms. . found. Predicate is consistent. 82243ms.
82秒。
チェック結果掲載できてませんが、解答ページを見てみるとちゃんとあっていました。
ちなみに、標準的な問題を解かせてみると。。。
Executing "Run run$1 for 13" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 77309 vars. 2201 primary vars. 146933 clauses. 3712ms. . found. Predicate is consistent. 49608ms.
50秒。
つまり、世界一難しい問題は、SATソルバからみると60～70%程度難しい問題だってことがわかりました。
いずれにせよ、Alloyって戦略を明示しなくてもいいのにコレぐらいの時間で数独が解けてしまいます。数独はAlloyがとても良くハマる問題だといえるのではないかと思います。
追記： 2012/07/04 回答の図をアップしました。あと、Alloyの説明をちょっと追加。
Control.DeepSeqを使って正格評価(訂正版)
何が酷いって、記事を見なおしてみたらfoldrとfoldlのロジックを間違えてる。コレは死ねる。。。ただ、Bangについてはそれでもちょっと怪しいので訂正版の記事を作り直したいと思います。
古い記事 は自戒の意味も込めて残しておきます。(なんの意味があるのかは不明)
モンテカルロ法で円周率を計算するために多数のIOから取り出した結果の集計を行おうとした。
しかし未評価thunkによるメモリオーバーフローが発生し、インスタンス数を増やせなかった。途中でわざとprintを行なって未評価thunkを潰してメモリリークを防いでいたのだがもちろんこれは本質的な解決ではない。
また、Bang-Patternを使用して未評価thunkを潰そうとしたが、どうもthunkが潰れてくれない。
調べてみたところ、厳密な正格評価にはControl.DeepSeqが使用できることがわかったので試して見ることにした。
まず、リークを起こすコードの説明から。
main :: IO ()
main = do
(count,total) Int -> IO Stat
takeStat func count =
foldLN1 sum_stat (liftM point_to_stat func) count (0,0)
foldLN1 :: (a->b->a) -> IO b -> Int -> a -> IO a
foldLN1 folder m count init =
let foldLN_sub folder m count v = if count == 0
then v
else let v' = unsafePerformIO m
in foldLN_sub folder m (count -1) $! folder v v'
in return $ foldLN_sub folder m count init
だいぶ端折っているが、foldLN1という関数で$!の形でBang-Patternを使用している。にもかかわらず、実行するとメモリオーバーフローで落ちる。(どうやら、folder関数のthunkが潰れ切らないらしい) そこで、DeepSeqを使用したコードに修正する。
foldLN1 :: (NFData a) => (a->b->a) -> IO b -> Int -> a -> IO a
foldLN1 folder m count init =
let foldLN_sub folder m count v = if count == 0
then v
else let v' = unsafePerformIO m
in foldLN_sub folder m (count -1) $!! folder v v'
in return $ foldLN_sub folder m count init
NFDataクラスはDeepSeqモジュールの正格評価を適用できるデータのクラス。$!!はBang-Patternsにおける$!に相当する。引数を(Bang PatternsにおけるWHNFではなく、)値になるまで評価する。
そもそも、unsafePerformIO使っているし、foldを自分で書くクソダサさと、無茶しまくっている、、、 でも、確かにコレで落ちない。
ちなみに、DeepSeqを使用しなくても下記のように時々thunkを潰すような処理を入れてあげると上手く回る。
foldLN2 :: (Show a) =>(a->b->a) -> IO b -> Int -> a -> IO a
foldLN2 folder m count init =
let foldLN_sub folder m count v = if count == 0
then v
else let v' = unsafePerformIO $ do
when (count `mod` 100000 == 0) $ print_stat v count
m
in foldLN_sub folder m (count -1) $! folder v v'
in return $ foldLN_sub folder m count init
コード： Recursion2.hs
参考：
- 【まとめ】Haskellでの正格評価とWHNF
- http://kamonama.blogspot.jp/2011/04/haskellwhnf.html
- shelarcyさんの説明
- http://www.sampou.org/cgi-bin/haskell.cgi?shelarcy
補足：
$ ghc --version The Glorious Glasgow Haskell Compilation System, version 7.4.1 $ ghc -O Recursion.hs [1 of 1] Compiling Main ( Recursion.hs, Recursion.o ) Linking Recursion.exe ...
Control.DeepSeq を使用して正格評価
本記事はfoldのアルゴリズムに対する理解がめちゃくちゃだったんで修正記事作りました。(2012/06/25)
モンテカルロ法で円周率を計算するために多数のIOから取り出した結果の集計を行おうとした。
しかし未評価thunkによるメモリオーバーフローが発生し、インスタンス数を増やせなかった。途中でわざとprintを行なって未評価thunkを潰してメモリリークを防いでいたのだがもちろんこれは本質的な解決ではない。
また、Bang-Patternを使用して未評価thunkを潰そうとしたが、どうもthunkが潰れてくれない。
調べてみたところ、厳密な正格評価にはControl.DeepSeqが使用できることがわかったので試して見ることにした。
まず、リークを起こすコードの説明から。
-- Simple example for Bang-Patterns leak import Control.Monad import Data.Foldable ( foldr' ) import System.IO main :: IO () main = do result <- takeStat (return 100) 10000000 print $ "result is " ++ show result takeStat :: IO Int -> Int -> IO Int takeStat io count = foldr' (liftM2 (+)) (return 0) $ replicate count io
実行するとメモリオーバーフローで落ちる。 そこで、DeepSeqを使用したコードに修正する。
takeStat :: IO Int -> Int -> IO Int
takeStat io count =
foldr'' (liftM2 (+)) (return 0) $ replicate count io
instance NFData a => NFData (IO a) where
rnf x = rnf $ unsafePerformIO x
foldr'' :: NFData b => (a->b->b) -> b-> [a] -> b
foldr'' folder init = init
foldr'' folder init (head:tail) =
(foldr'' folder $!! (folder head init)) tail
NFDataクラスはDeepSeqモジュールの正格評価を適用できるデータのクラス。$!!はBang-Patternsにおける$!に相当する。引数を(Bang PatternsにおけるWHNFではなく、)値になるまで評価する。
foldを自分で書くクソダサさとIOを今更(しかも無理に)インスタンス化したり、無茶しまくっている、、、 でも、確かにコレで落ちない。
Bang Pattern的には下記なら大丈夫な感じがしてしまうが、やっぱりメモリ不足でおちちゃう。なぜダメなんだろうなぁ。
takeStat :: IO Int -> Int -> IO Int
takeStat io count =
return $ foldr' (+).unsafePerformIO 0 $ replicate count $ unsafePerformIO io
- 参考：【まとめ】Haskellでの正格評価とWHNF
- http://kamonama.blogspot.jp/2011/04/haskellwhnf.html
補足：
$ ghc --version The Glorious Glasgow Haskell Compilation System, version 7.4.1 $ ghc -O Recursion.hs [1 of 1] Compiling Main ( Recursion.hs, Recursion.o ) Linking Recursion.exe ...
追記：
IOをインスタンス化するのはやっぱ嫌なのでどうせunsafePerformIOつかうなら下記がいいかな、、、
takeStat :: IO Int -> Int -> IO Int
takeStat io count =
return $ foldr'' ((+).unsafePerformIO) 0 $ replicate count io
foldr'' :: NFData b => (a->b->b) -> b-> [a] -> b
foldr'' folder init = init
foldr'' folder init (head:tail) =
(foldr'' folder $!! folder head init) tail
追記２：
foldr'の根本にforceを挿してみたがこれもダメ。Bang Patternsがちゃんと動いていないのでは？
takeStat :: IO Int -> Int -> IO Int
takeStat io count =
return $ (foldr' . force) ((+).unsafePerformIO) 0 $ replicate count io
正格評価がうまく動かない？
モンテカルロ法で円周率計算、みたいな話がちょろっと降ってきたので任意精度で計算できるようなコードをHaskellで書いてみたのだがループの中でどうもスペースリークしている。もう少しいうと、集計用の畳み込み関数が未評価のまま残ってしまうようだ。
main :: IO ()
main = do
(count,total) Int -> IO Stat
takeStat func count =
let c = \(x1,y1)(x2,y2) -> (x1+x2,y1+y2)
f = \ (x,_) -> if x then (1,1) else (0,1)
in
foldRN c (liftM f func) count (0,0)
みたくして、foldRN関数を次のように。(unsafePerformIOは見逃してw)
foldRN :: (Show a)=> (a->a->a) -> IO a -> Int -> a -> IO a
foldRN folder m count init =
let foldRN_sub folder m count v
| count == 0 = v
| otherwise =
let r = unsafePerformIO $ do
when ((count `mod` 100000) == 0) $ do
putStrLn $ "v: " ++ show v ++ " count: " ++ show count
hFlush stdout
m
in
foldRN_sub folder m (count -1) $! folder v r
in return $ foldRN_sub folder m count init
これ、whenがないとスペースリークで死んでしまう。 再帰関数のtail-recursionでBangによってthunkを潰してるはずなのに。。。 なぜ、、、、 あとMonoid使わねーの？という指摘がありましたら甘んじて受けます。
