Thinking Functionally with Haskell勉強メモ: 第５章２ 確定したマスの情報をベースにフィルタ

非常に非効率だが問題文に誠実に宣言的に書いているので正しさが（ほぼ）自明なプログラムに対して、ここから成り立つと証明できる法則を使って、結果が同一なことを担保しつつ効率が上がるような変換を行っていく。

前回の数独ソルバーは9^81-kものGridを一つ一つ作成してはルールに従ってフィルタしていくものだった。Grid作成過程でどうにかして作る数を減らさなければ、実際的な時間内で計算が終わらない。

今回はもっとも簡単なアイディアである「確定したマスの行、列、箱の他のマスが、確定した値を含まないようフィルタする」を実装し、それがもとのプログラムと同一の結果を返すことを証明する。

prune :: Matrix [Digit] -> Matrix [Digit]
filter valid . expand . choices = filter valid . expand . prune . choices

となるようなprune関数を求めたい。

Matrix Digit型の問題文をchoicesでMatrix [Digit]型の「各マスに入る可能性のあるDigitのリストのMatrix」に変換したわけだが、その「入る可能性のあるDigit」をexpandする前に減らしておく、という戦略である。

pruneRow関数

まずRowに対してフィルタするpruneRowを考えてみる。

pruneRow :: Row [Digit] -> Row [Digit]
pruneRow row = map (remove fixed) row
               where fixed = [d | [d] <- row]

この定義、とくにfixedの部分が面白い。[d | [d] <- row]でrowの中身に対してパターンマッチを行っていて、要素１のリストだけをフィルタしてその要素を摘出している。too cleverな気もするけど・・・

remove :: [Digit] -> [Digit]
remove _ [x] = [x]
remove ds xs = filter (`notElem` ds) xs

[x]な（つまり確定している）マス以外は、確定した値を含まないようフィルタする。remove _ [x] = [x]がないと確定したマスが空になってしまう。

とここで

The function pruneRow satisfies the equation

filter nodups . cp = filter nodups . cp . pruneRow

とさらっと書いてあって、「自明か？自明なのか？」と数学書でおなじみのアレになる。いや、やっていることを考えれば成り立つとは思うんだけど証明しなくていいのか？

これから使う等式

さて、ここでいくつか他にも重要な等式を列挙しておこう。

rows, cols, boxsは対合

rows . rows = id
cols . cols = id
boxs . boxs = id

boxsケースの証明は意外と簡単。colsつまりtransposeは自明っぽいけど（transposeしてtransposeしたらもとに戻る）証明はTFwHのここまでの説明だけでは無理らしい。

group . ungroup = id --すでにgroupされているMatrixに対して
ungroup . group = id

まあ自明。これを使ってboxsの対合性を証明できる。

expandとrows...の関係

map rows . expand = expand . rows
map cols . expand = expand . cols
map boxs . expand = expand . boxs

boxの定義上9x9のMatrixが引数な場合に限り、だと思う（本ではN^2xN2となっていたがその場合boxの定義も変える必要があるはず）

cpの特性

map (map f) . cp = cp . map (map f)
filter (all p) . cp = cp . map (filter p)

最初の式は自然変換。cpは要素に対してなにも働きかけないので、fを各要素に適用するのがcpの前か後かで結果は変わらない。

二番目の式はちょっとややこしい。

• 左辺は直積をとってできた[[a]]から、[a]の全要素がpを満たしているリストのみを摘出している
• 右辺は直積をとる前にそもそも[a]からpを満たさない要素を抜いている

その結果が等しいということは、直積する前にフィルタしてしまって効率化を図れるということ。

対合とfilter/map

-- f . f = idの場合
filter (p . f) = map f . filter p . map f
filter (p . f) . map f = map f . filter p

まあ自明。第４章ですべてのp, fにおいて

filter p . map f = map f . filter (p . f)

を証明したのを使えば楽に証明できる。

pruneRowの等価性の証明

以上の等式を使って、filter valid . expand . completions = filter valid . expand . prune . completionsが成り立つようなpruneをpruneRowを使って書けることを証明する。

まずfilter validを、validの定義から以下のように書き直す：

filter valid = filter (all nodups . rows) . filter (all nodups . cols) . filter (all nodups . boxs)

この変換も自明として扱われている。

p x = p1 x && p2 x
filter p = filter p1 . filter p2 = filter p2 . filter p1

が成り立つのは自明だろうか？直感的にはわかるが・・・

さて、これで

filter valid . expand = filter (all nodups . rows) . filter (all nodups . cols) . filter (all nodups . boxs) . expand

になるので

filter (all nodups . boxs) . expand
filter (all nodups . cols) . expand
filter (all nodups . rows) . expand

を一つ一つみていく（というのは嘘で最初のやつを解いたらまったく同じロジックであとの二つも解ける）。

filter (all nodups . boxs) . expand

= {filter (p . f) = map f . filter p . map f   -- f . f = id}
map boxs . filter (all nodups) . map boxs . expand

= {map boxs . expand = expand . boxs}
map boxs . filter (all nodups) . expand . boxs

= {expand = cp . map cp}
map boxs . filter (all nodups) . cp . map cp . boxs

= {filter (all p) . cp = cp . map (filter p)}
map boxs . cp . map (filter nodups) . map cp . boxs

= {functor law of map}
map boxs . cp . map (filter nodups . cp) . boxs

= {filter nodups . cp = filter nodups . cp . pruneRow}
map boxs . cp . map (filter nodups . cp . pruneRow) . boxs

ここまででpruneRowを等価な変換で登場させることに成功した。

あとは左側にfilter (all nodups . boxs) . expandが戻ってくるように逆変換していく：

map boxs . cp . map (filter nodups . cp . pruneRow) . boxs

= {functor law of map}
map boxs . cp . map (filter nodups) . map cp . map pruneRow . boxs

= {filter (all f) . cp = cp . map (filter f)}
map boxs . filter (all nodups) . cp . map cp . map pruneRow . boxs

= {expand = cp . map cp}
map boxs . filter (all nodups) . expand . map pruneRow . boxs

= {filter (p . f) . map f = map f . filter p  -- f . f = id}
filter (all nodups . boxs) . map boxs . expand . map pruneRow . boxs

= {map boxs . expand = expand . boxs}
filter (all nodups . boxs) . expand . boxs . map pruneRow . boxs

これで

filter (all nodups . boxs) . expand = filter (all nodups . boxs) . expand . boxs . map pruneRow . boxs

という等式が成り立つことが証明できた。まったく同じ理屈で

filter (all nodups . rows) . expand = filter (all nodups . rows) . expand . rows . map pruneRow . rows
filter (all nodups . cols) . expand = filter (all nodups . cols) . expand . cols . map pruneRow . cols

も成り立つ。

boxs . map pruneRow . boxsは、Matrixをまず3x3の区切りの集まりに変換し、各集まりに対して確定したマスの数を取り除くpruneRowを適用し、またboxを適用する。boxを適用したMatrixにboxを再度適用すると形はもとに戻るので、最終的には「3x3の区切りをただしくpruneしただけ」という結果が残る。

なのでpruneBy f = f . map pruneRow . fを定義して

• pruneBy boxsはMatrixの形を変えずにboxs単位で確定値をフィルタ
• pruneBy colsはMatrixの形を変えずにcols単位で確定値をフィルタ
• pruneBy rowsはMatrixの形を変えずにrows単位で確定値をフィルタ

とみなすことができる。

filter (all nodups . boxs) . expand = filter (all nodups . boxs) . expand . pruneBy boxs
filter (all nodups . rows) . expand = filter (all nodups . rows) . expand . pruneBy rows
filter (all nodups . cols) . expand = filter (all nodups . cols) . expand . pruneBy cols

とより簡単に表現できるようになる。

話をfilter valid . expandに戻すと：

filter valid . expand 

= {filter validの書き換え}
filter (all nodups . rows) . filter (all nodups . cols) . filter (all nodups . boxs) . expand

= {filter (all nodups . f) . expand = filter (all nodups . f) . expand . pruneBy f -- f in (rows, cols, boxs)}
filter (all nodups . rows) . filter (all nodups . cols) . filter (all nodups . boxs) . expand . pruneBy boxs

= {filter A . filter B = filter B . filter A}
filter (all nodups . rows) . filter (all nodups . boxs) . filter (all nodups . cols) . expand . pruneBy boxs

= {filter (all nodups . f) . expand = filter (all nodups . f) . expand . pruneBy f -- f in (rows, cols, boxs)}
filter (all nodups . rows) . filter (all nodups . boxs) . filter (all nodups . cols) . expand . pruneBy cols . pruneBy boxs

= {filter A . filter B = filter B . filter A}
filter (all nodups . cols) . filter (all nodups . boxs) . filter (all nodups . rows) . expand . pruneBy cols . pruneBy boxs

= {filter (all nodups . f) . expand = filter (all nodups . f) . expand . pruneBy f -- f in (rows, cols, boxs)}
filter (all nodups . cols) . filter (all nodups . boxs) . filter (all nodups . rows) . expand . pruneBy rows . pruneBy cols . pruneBy boxs

= {filter validの書き換え}
filter valid . expand . pruneBy rows . pruneBy cols . pruneBy boxs

と、filter valid . expandの後ろにrows/cols/boxsすべてのpruneBy fをつけても等価であることが証明できるので：

prune = pruneBy rows . pruneBy cols . pruneBy boxs

とpruneをpruneByを使って定義すれば：

filter valid . expand = filter valid . expand . prune
filter valid . expand . completions = filter valid . expand . prune . completions

を満たす。さらには：

filter valid . expand . completions = filter valid . expand . prune . prune . ... . prune . completions

とpruneを任意の回数入れても等価。pruneすることで確定したマスが出てきた場合、もう一度pruneすることでさらに絞り込みが可能になる場合も多い。

結果が変わらなくなるまでfを適用し続ける、という関数manyを

many :: (Eq a) => (a -> a) -> a -> a
many f x = if x == y then x else many y x
           where y = f x

と定義する。これを使えばsolveの定義を：

solve = filter . valid . expand . many prune . choices

と表現でき、これは

solve = filter . valid . expand . choices

と等価であることを証明できた。（manyの等価性担保は本当に自明か？）

まだ最適化の余地は大きい。次回はその話。