4パターンマッチ指向プログラミングの効果

本章の目的は，パターンマッチ指向プログラミングがどのような場面でどのように役に立つか明確にすることである．前章までの例は，すべて単一のmatchAllやmatchで記述した例ばかりを紹介してきたが，本章ではより大きなプログラムの記述の中でEgisonのパターンマッチがどのような役割を果たすのかみていく．

4.1SATソルバーの実装

ある程度大きなプログラムを書く中で，パターンマッチ指向プログラミングの効果をみるために，SATソルバーを実装する． SATソルバーは，与えられた命題論理式が真になる論理変数の割り当てが存在するかどうか判定するプログラムである． SATソルバーが入力にとる論理式は，連言標準形（conjunctive normal form）であることが多い．論理式が連言標準形であるとは，論理式がリテラル（literal）の選言からなる節の連言になっていることをいう．リテラルとは， $$p$$ または $\neg p$ という形をした論理式のことをいう．たとえば， $(p \lor q) \wedge (\neg p \lor r) \wedge (\neg p \lor \neg r)$ は， $p = \texttt{False}$ ， $q = \texttt{True}$ ， $r = \texttt{True}$ という割り当てをすれば真になる連言標準形の論理式である．

4.1.1Davis-Putnamアルゴリズム

ここではDavis-Putnamアルゴリズム[3]という，SAT問題を解くアルゴリズムのなかでもシンプルなアルゴリズムを実装する．本節の実装では，連言標準形の命題論理式をリテラルのコレクションのコレクションとして表現する． $\wedge$ と $\lor$ は可換な演算子であるため，このコレクションのコレクションは，リテラルの多重集合の多重集合としてパターンマッチできる．さらに，リテラルを整数として表現し， $$p$$ の形のリテラルは正整数， $\neg p$ の形のリテラルは $$p$$ に対応する正整数の $$-1$$ 倍の負整数となるようにする．

そうすると，これらの論理式に対するマッチャーはmultiset (multiset integer)と定義できる．以下のプログラムは，Davis-Putnamアルゴリズムの核の実装である． dp関数は，論理変数のリストと論理式を引数にとり，解がある場合はTrueを，そうでない場合はFalseを返す．型注釈により，dp関数が整数のリスト（論理変数）と整数のリストのリスト（論理式）を受け取り，Boolを返すことを示している．

def dp (vars: [Integer]) (cnf: [[Integer]]) : Bool :=
  match (vars, cnf) as (multiset integer, multiset (multiset integer)) with
  | (_, []) -> True
  | (_, [] :: _) -> False
  -- 1-literal rule
  | (_, ($l :: []) :: _) -> dp (delete (abs l) vars) (assignTrue l cnf)
  -- pure literal rule (positive)
  | ($v :: $vs, !((#(neg v) :: _) :: _)) -> dp vs (assignTrue v cnf)
  -- pure literal rule (negative)
  | ($v :: $vs, !((#v :: _) :: _)) -> dp vs (assignTrue (neg v) cnf)
  -- otherwise
  | ($v :: $vs, _) ->
    dp vs
       ((resolveOn v cnf) ++ (deleteClausesWith v (deleteClausesWith (neg v) cnf)))

1つ目のマッチ節（3行目）は，入力された論理式が空だった場合，解を持つことを表現している． 2つ目のマッチ節（4行目）は，入力された論理式が空節を含んでいた場合，解が存在しないことを表現している． 3つ目のマッチ節（6行目）は，1-リテラル・ルール（1-literal rule）というルールを表現している．入力の論理式が1つのリテラルからなる節を持つとき，そのリテラルがTrueになる割り当てを即座にできる． 4つ目のマッチ節（8行目）は，ある論理変数の否定がリテラルとして全く現れない場合，その論理変数に即座にTrueを割り当てることができることを表現している．たとえば， $(p \lor q) \wedge (\neg p \lor r) \wedge (\neg p \lor \neg r)$ は論理変数 $$q$$ の否定を含まないため， $$q$$ にTrueを割り当てることができる． 5つ目のマッチ節（10行目）は，4つ目のマッチ節と逆のことを表現している．このマッチ節は，ある論理変数の否定のみが入力の論理式に含まれる場合，その論理変数にFalseを割り当てることができることを表現している．最後のマッチ節（12-14行目）は導出原理（resolution principle）を適用している．このマッチ節は， $p \lor C$ と $\neg p \lor D$ という形のすべての節のペアを列挙し（ $$C$$ と $$D$$ はリテラルの選言とする）， $C \lor D$ という形の節を生成する．

上記のdpの定義は，入力の論理式を簡約するためのすべてのルールを多重集合に対するパターンマッチをいかして記述している．同様のことをするために，伝統的な関数型プログラミングでは，複数のライブラリ関数を組み合わせたり，補助関数を定義する必要がある． Davis-PutnamアルゴリズムのOCamlによる実装は[3]でみることができる．

4.1.2導出原理

本節は，resolveOn関数の実装を紹介する．まずは，ナイーブな実装を紹介するところからはじめる． resolveOn関数は，matchAll式を使って以下のように定義できる．型注釈により，resolveOn関数が整数vと論理式cnfを受け取り，導出された節のリストを返すことを示している．

def resolveOn (v: Integer) (cnf: [[Integer]]) : [[Integer]] := matchAll cnf as multiset (multiset integer) with
| (#v :: $xs) :: (#(negate v) :: $ys) :: _ -> unique (filter (\c -> not (tautology c)) (xs ++ ys))

$p \lor C$ と $\neg p \lor D$ の形の節のペアを列挙するパターンは，多重集合の多重集合に対するパターンマッチにより記述できる．ただし，これだけでは， $C \lor D$ がトートロジーな節である場合（ $$C$$ がリテラル $$q$$ を含みかつ $$D$$ がリテラル $\neg q$ を含む場合そうなる）にもマッチしてしまう．そのために，filter関数とtautology関数を使って，そのような節を取り除いている．シーケンシャル・notパターン（第3章3.3節）を使ってresolveOn関数を定義すると，パターンにそのような操作を取り込める．

def resolveOn (v: Integer) (cnf: [[Integer]]) : [[Integer]] :=
  matchAll cnf as multiset (multiset integer) with
  | {(#v :: (@ & $xs)) :: (#(neg v) :: (@ & $ys)) :: _,
     !($l :: _, #(neg l) :: _)}
    ->  unique (xs ++ ys)

4.22種類のループの分離

4.1節で実装したSATソルバーは，パターンマッチ指向プログラミングによって取りのぞけないループを含んでいた．そのループとは，dp関数の再帰である．この再帰は，SAT問題を解くための探索空間を狭めるために本質的なループである．この探索空間の縮小は，単純なバックトラッキング・アルゴリズムでは不可能なものである．たいして，その他のバックトラッキングにより実装できるループはすべてパターンの中に押し込められている．伝統的な関数型プログラミングでは，これら2種類のループのどちらも再帰を使って記述する必要があった．パターンマッチ指向プログラミングは，バックトラッキングにより実装できるループをパターンに閉じ込めることにより，時間的計算量を減らすための本質的なループのみの記述にプログラマが注力できるようにする．これにより，プログラムの記述しやすさ・読解しやすさが向上する．