第20章

Countdown 問題

(やさしい版) Pearls of Functional Algorithm Design(関数プログラミングによるアルゴリズム設計の真珠)

どんな問題?

Countdown(カウントダウン)は、イギリスの人気テレビ番組で行われる算数ゲームの名前です。フランスでは Le Conte est Bon と呼ばれています。ルールはこうです。

元の数が [1, 3, 7, 10, 25, 50]、目標が 831 のとき、ぴったりの解はありません。惜しいものとしては 7 + (1 + 10) × (25 + 50) = 832 があります。

この章のねらいは、Countdown を解く関数型プログラムを、素朴な版から高速な版へと少しずつ改良していくことです。どの版も全部の候補を調べる「全探索」がベースですが、無駄な計算をどう減らすかで速度が大きく変わります。空間と時間のトレードオフを比べるのにちょうど良い題材です。

単純なプログラム

全体の流れ

まず、素直に書いたプログラムを見てみましょう。

countdown1 :: Int → [Int] → (Expr, Value) countdown1 n = nearest n · concatMap mkExprs · subseqs
Dart // 3段構成: 部分列を作る → 各部分列で式を全列挙 → 目標に一番近いものを選ぶ (Expr, int) countdown1(int n, List<int> xs) { final all = <(Expr, int)>[ for (final ys in subseqs(xs)) ...mkExprs(ys), ]; return nearest(n, all); }

やっていることは 3 段階です。

  1. subseqs:元の数のリストから、空でない部分列(=どの数字を使うかの選び方)をすべて作る。
  2. mkExprs:各部分列に対して、それらの数から作れるすべての「妥当な」算術式を、値付きで列挙する。
  3. nearest n:全部つなげたリストの中から、値が目標 n に一番近いものを 1 つ選ぶ。

元の数はリストとして与えられ、順序自体は問題になりませんが、重複は意味を持ちます。ここでは元のリストは昇順にそろっていることを仮定します(あとで役立つ性質です)。

部品①:subseqs(部分列を全部作る)

空でないリストの、空でない部分列を全部返す関数です。

subseqs [x] = [[x]] subseqs (x : xs) = xss ++ [x] : map (x :) xss where xss = subseqs xs
Dart // xs が [x] のときは [[x]]。それ以外は先頭 x を「使わない/単独/前置」の3パターン。 // 「xs が ys の部分列なら xs の方が先」の順で並ぶよう構築する。 List<List<int>> subseqs(List<int> xs) { if (xs.length == 1) return [[xs.first]]; final x = xs.first; final xss = subseqs(xs.sublist(1)); return [ ...xss, [x], for (final ys in xss) [x, ...ys], ]; }

部品②:式と値の型

式は「数」または「演算子で 2 つの式を結んだもの」で表します。

data Expr = Num Int | App Op Expr Expr data Op = Add | Sub | Mul | Div type Value = Int
Dart // Dart 3 の sealed class + パターンマッチで代数的データ型を表す。 enum Op { add, sub, mul, div } sealed class Expr { const Expr(); } class Num extends Expr { final int x; const Num(this.x); } class App extends Expr { final Op op; final Expr e1, e2; const App(this.op, this.e1, this.e2); } // Value は int の別名として扱う。

式の値は次のように計算できます。

value :: Expr → Value value (Num x) = x value (App op e1 e2) = apply op (value e1) (value e2)
Dart int value(Expr e) => switch (e) { Num(:final x) => x, App(:final op, :final e1, :final e2) => apply(op, value(e1), value(e2)), }; int apply(Op op, int v1, int v2) => switch (op) { Op.add => v1 + v2, Op.sub => v1 - v2, Op.mul => v1 * v2, Op.div => v1 ~/ v2, };

ここで apply Add = (+)apply Sub = (−) のように、演算子タグを実際の演算に対応づけます。

部品③:どんな式が「妥当」か

Countdown ではすべての式が使えるわけではありません。途中の値も正の整数である必要があるからです。

legal :: Op → Value → Value → Bool legal Add v1 v2 = True legal Sub v1 v2 = (v2 < v1) legal Mul v1 v2 = True legal Div v1 v2 = (v1 mod v2 == 0)
Dart bool legal(Op op, int v1, int v2) => switch (op) { Op.add => true, Op.sub => v2 < v1, Op.mul => true, Op.div => v1 % v2 == 0, };

部品④:mkExprs(部分列から式を全列挙)

与えられた部分列を左右に分け、それぞれの側で作れる式を再帰的に列挙し、演算子で結合します。

mkExprs :: [Int] → [(Expr, Value)] mkExprs [x] = [(Num x, x)] mkExprs xs = [ev | (ys, zs) ← unmerges xs, ev1 ← mkExprs ys, ev2 ← mkExprs zs, ev ← combine ev1 ev2]
Dart List<(Expr, int)> mkExprs(List<int> xs) { if (xs.length == 1) return [(Num(xs.first), xs.first)]; return [ for (final (ys, zs) in unmerges(xs)) for (final ev1 in mkExprs(ys)) for (final ev2 in mkExprs(zs)) ...combine(ev1, ev2), ]; }

ここで登場するのが unmerges です。順序付きリスト xs について、yszs を混ぜ合わせると xs になるような、空でない組 (ys, zs) をすべて返します。

unmerges :: [a] → [([a], [a])] unmerges [x, y] = [([x], [y]), ([y], [x])] unmerges (x : xs) = [([x], xs), (xs, [x])] ++ concatMap (add x) (unmerges xs) where add x (ys, zs) = [(x : ys, zs), (ys, x : zs)]
Dart // xs を、混ぜ合わせると xs になるような空でない (ys, zs) 全通りに分ける。 List<(List<int>, List<int>)> unmerges(List<int> xs) { if (xs.length == 2) { final a = xs[0], b = xs[1]; return [([a], [b]), ([b], [a])]; } final x = xs.first; final rest = xs.sublist(1); return [ ([x], rest), (rest, [x]), for (final (ys, zs) in unmerges(rest)) ...[ ([x, ...ys], zs), (ys, [x, ...zs]), ], ]; }

combine は、2 つの (式, 値) の組から、4 種類の演算子で結合してできる妥当な式を全部返します。

combine :: (Expr, Value) → (Expr, Value) → [(Expr, Value)] combine (e1, v1) (e2, v2) = [(App op e1 e2, apply op v1 v2) | op ← ops, legal op v1 v2]
Dart const ops = Op.values; // [add, sub, mul, div] List<(Expr, int)> combine((Expr, int) ev1, (Expr, int) ev2) { final (e1, v1) = ev1; final (e2, v2) = ev2; return [ for (final op in ops) if (legal(op, v1, v2)) (App(op, e1, e2), apply(op, v1, v2)), ]; }

ここで ops = [Add, Sub, Mul, Div] です。

部品⑤:nearest(一番近い式を選ぶ)

目標 n との差が最小のものを 1 つ選びます。差 0 の式(ぴったり)を見つけたら、そこで打ち切ります。

nearest n ((e, v) : evs) = if d == 0 then (e, v) else search n d (e, v) evs where d = abs (n − v) search n d ev [] = ev search n d ev ((e, v) : evs) | d' == 0 = (e, v) | d' < d = search n d' (e, v) evs | d' ≥ d = search n d ev evs where d' = abs (n − v)
Dart // 差 0 が見つかった時点で打ち切る早期リターン付きの最小差探索。 (Expr, int) nearest(int n, List<(Expr, int)> evs) { var best = evs.first; var d = (n - best.$2).abs(); if (d == 0) return best; for (var i = 1; i < evs.length; i++) { final ev = evs[i]; final dp = (n - ev.$2).abs(); if (dp == 0) return ev; if (dp < d) { best = ev; d = dp; } } return best; }

実測結果

GHCi(バージョン 6.8.3、2394 MHz の Windows XP ノート)で動かすと、こうなります。

> display (countdown1 831 [1,3,7,10,25,50]) (7+((1+10)*(25+50))) = 832 (42.28 secs, 4198816144 bytes) > length $ concatMap mkExprs $ subseqs [1,3,7,10,25,50] 4672540
実測結果 約 450 万個の式を 42 秒で処理(毎秒 10 万式ペース)。 Countdown の制限時間 30 秒には収まらず、これでは足りません。

2 つの最適化

最適化①:無駄な式を作らない(強い妥当性テスト)

6 個の数から作れる式は約 3300 万個、そのうち妥当なものは 400 万〜500 万個ほどあります。でも、その中には本質的に同じ式がたくさん含まれています。たとえば次の対はどれも同じ意味です。

x + y と y + x, x ∗ y と y ∗ x, (x − y) + z と (x + z) − y

そこで、妥当性テストを次のように強化します。

legal Add v1 v2 = (v1 ≤ v2) legal Sub v1 v2 = (v2 < v1) legal Mul v1 v2 = (1 < v1) ∧ (v1 ≤ v2) legal Div v1 v2 = (1 < v2) ∧ (v1 mod v2 == 0)
Dart // 可換演算は小→大の順に制限。1 との積/商は無意味なので禁止。 bool legalStrong(Op op, int v1, int v2) => switch (op) { Op.add => v1 <= v2, Op.sub => v2 < v1, Op.mul => 1 < v1 && v1 <= v2, Op.div => 1 < v2 && v1 % v2 == 0, };

これだけで、妥当な式は 300 万 → 約 30 万に減ります(10 倍改善)。

最適化②:unmerges の重複を止める

もとの unmerges(ys, zs)(zs, ys) を両方返していて、二重に働いていました。片方だけを返すよう定義を変えます。

unmerges [x, y] = [([x], [y])] unmerges (x : xs) = [([x], xs)] ++ concatMap (add x) (unmerges xs) where add x (ys, zs) = [(x : ys, zs), (ys, x : zs)]
Dart // 二重の (ys, zs)/(zs, ys) を止め、片側だけ返すよう改良。 List<(List<int>, List<int>)> unmerges2(List<int> xs) { if (xs.length == 2) return [([xs[0]], [xs[1]])]; final x = xs.first; final rest = xs.sublist(1); return [ ([x], rest), for (final (ys, zs) in unmerges2(rest)) ...[ ([x, ...ys], zs), (ys, [x, ...zs]), ], ]; }

これに合わせて combine は両向きを試すように書き換えます。

combine (e1, v1) (e2, v2) = [(App op e1 e2, apply op v1 v2) | op ← ops, legal op v1 v2] ++ [(App op e2 e1, apply op v2 v1) | op ← ops, legal op v2 v1]
Dart // unmerges を片側だけにした分、combine で両向きを試す。 List<(Expr, int)> combineBoth((Expr, int) ev1, (Expr, int) ev2) { final (e1, v1) = ev1; final (e2, v2) = ev2; return [ for (final op in ops) if (legalStrong(op, v1, v2)) (App(op, e1, e2), apply(op, v1, v2)), for (final op in ops) if (legalStrong(op, v2, v1)) (App(op, e2, e1), apply(op, v2, v1)), ]; }

まとめて速くする:combine に判定を埋め込む

さらに速い方法として、強化した妥当性テストを combine の中に直接書いてしまいます。値の大小で 3 通りに分岐します。

combine (e1, v1) (e2, v2) | v1 < v2 = comb1 (e1, v1) (e2, v2) | v1 == v2 = comb2 (e1, v1) (e2, v2) | v1 > v2 = comb1 (e2, v2) (e1, v1)
Dart // 判定を combine に埋め込み、値の大小で 3 分岐する版。 List<(Expr, int)> combine2((Expr, int) ev1, (Expr, int) ev2) { final v1 = ev1.$2, v2 = ev2.$2; if (v1 < v2) return comb1(ev1, ev2); if (v1 == v2) return comb2(ev1, ev2); return comb1(ev2, ev1); }

comb1 は v1 < v2 のとき、comb2 は v1 == v2 のときに使います。中身は図 20.1 のとおりです。

comb1 (e1, v1) (e2, v2) = [(App Add e1 e2, v1 + v2), (App Sub e2 e1, v2 − v1)] ++ if 1 < v1 then [(App Mul e1 e2, v1 ∗ v2)] ++ [(App Div e2 e1, q) | r == 0] else [] where (q, r) = divMod v2 v1 comb2 (e1, v1) (e2, v2) = [(App Add e1 e2, v1 + v2)] ++ if 1 < v1 then [(App Mul e1 e2, v1 ∗ v2), (App Div e1 e2, 1)] else []
Dart // v1 < v2 の前提。Add/Sub は常に、Mul/Div は v1 > 1 のときだけ。 List<(Expr, int)> comb1((Expr, int) ev1, (Expr, int) ev2) { final (e1, v1) = ev1; final (e2, v2) = ev2; final q = v2 ~/ v1; final r = v2 % v1; return [ (App(Op.add, e1, e2), v1 + v2), (App(Op.sub, e2, e1), v2 - v1), if (1 < v1) ...[ (App(Op.mul, e1, e2), v1 * v2), if (r == 0) (App(Op.div, e2, e1), q), ], ]; } // v1 == v2 の前提。等しいので Sub と Div (=1 以外) は無意味。 List<(Expr, int)> comb2((Expr, int) ev1, (Expr, int) ev2) { final (e1, v1) = ev1; final (e2, v2) = ev2; return [ (App(Op.add, e1, e2), v1 + v2), if (1 < v1) ...[ (App(Op.mul, e1, e2), v1 * v2), (App(Op.div, e1, e2), 1), ], ]; }
図 20.1 comb1 と comb2 の定義

この改良版を countdown2 と呼びます。実測すると、

> display (countdown2 831 [1,3,7,10,25,50]) (7+((1+10)*(25+50))) = 832 (1.77 secs, 168447772 bytes) > length $ concatMap mkExprs $ subseqs [1,3,7,10,25,50] 240436
実測結果 約 25 万個の式を 1.77 秒で処理。42 秒 → 2 秒未満と大幅改善! でも、まだ改善の余地があります。

さらに強い妥当性テスト

「正規形」を決めて重複を減らす

もっと候補を絞るために、式の正規形(normal form)を定義します。式が正規形であるとは、次の形の「和 − 和」であるときと決めます。

[(e1 + e2) + · · · + em] − [(f1 + f2) + · · · + fn]

ここで m ≥ 1、n ≥ 0 で、ei や fi はすべて値の昇順に並んでいます。さらに各 ei, fi は次の形の「積 / 積」です。

[(g1 ∗ g2) ∗ · · · ∗ gp]/[(h1 ∗ h2) ∗ · · · ∗ hq]

ここでも p ≥ 1、q ≥ 0、gi, hi は昇順で、gi, hi は単一の数か、または正規形の式です。

なぜ効くのか 各式は、同じ値の部分式の並べ替えを除けばただ 1 つの正規形を持ちます。先ほど 30 万個あった妥当な式のうち、正規形は約 3 万〜7 万まで減ります。

ただし、正規形でも重複はゼロにはなりません。たとえば 2 + 5 + 72 ∗ 7 はどちらも値 14 ですが、後者は前者の数字の部分集合から作れています。本当に必要な式だけに絞り込む「間引き(thinning)」もありますが、判定のコストが節約分を上回るため、ここでは採用しません。

実装:non と新しい legal

今度は値だけでなく式そのものを見る必要があります。まず、式のトップにある演算子が op と一致しないことを判定する non を定義します。

non :: Op → Expr → Bool non op (Num x) = True non op1 (App op2 e1 e2) = op1 ≠ op2
Dart // 式のトップの演算子が op と一致しないかを判定する。 bool non(Op op, Expr e) => switch (e) { Num() => true, App(op: final op2) => op != op2, };

そして強化された妥当性テストは次のようになります。

legal :: Op → (Expr, Value) → (Expr, Value) → Bool legal Add (e1, v1) (e2, v2) = (v1 ≤ v2) ∧ non Sub e1 ∧ non Add e2 ∧ non Sub e2 legal Sub (e1, v1) (e2, v2) = (v2 < v1) ∧ non Sub e1 ∧ non Sub e2 legal Mul (e1, v1) (e2, v2) = (1 < v1 ∧ v1 ≤ v2) ∧ non Div e1 ∧ non Mul e2 ∧ non Div e2 legal Div (e1, v1) (e2, v2) = (1 < v2 ∧ v1 mod v2 == 0) ∧ non Div e1 ∧ non Div e2
Dart // 正規形(和−和 / 積÷積 のネスト)に限る強化版妥当性テスト。 bool legalNF(Op op, (Expr, int) ev1, (Expr, int) ev2) { final (e1, v1) = ev1; final (e2, v2) = ev2; return switch (op) { Op.add => v1 <= v2 && non(Op.sub, e1) && non(Op.add, e2) && non(Op.sub, e2), Op.sub => v2 < v1 && non(Op.sub, e1) && non(Op.sub, e2), Op.mul => 1 < v1 && v1 <= v2 && non(Op.div, e1) && non(Op.mul, e2) && non(Op.div, e2), Op.div => 1 < v2 && v1 % v2 == 0 && non(Op.div, e1) && non(Op.div, e2), }; }

これを comb1 と comb2 に組み込んだのが図 20.2 です。

comb1 (e1, v1) (e2, v2) = (if non Sub e1 ∧ non Sub e2 then [(App Add e1 e2, v1 + v2) | non Add e2] ++ [(App Sub e2 e1, v2 − v1)] else []) ++ (if 1 < v1 ∧ non Div e1 ∧ non Div e2 then [(App Mul e1 e2, v1 ∗ v2) | non Mul e2] ++ [(App Div e2 e1, q) | r == 0] else []) where (q, r) = divMod v2 v1 comb2 (e1, v1) (e2, v2) = [(App Add e1 e2, v1 + v2) | non Sub e1, non Add e2, non Sub e2] ++ (if 1 < v1 ∧ non Div e1 ∧ non Div e2 then [(App Mul e1 e2, v1 ∗ v2) | non Mul e2] ++ [(App Div e1 e2, 1)] else [])
Dart // 正規形制約を comb1/comb2 に埋め込んだ、countdown3 の中核。 List<(Expr, int)> comb1NF((Expr, int) ev1, (Expr, int) ev2) { final (e1, v1) = ev1; final (e2, v2) = ev2; final q = v2 ~/ v1; final r = v2 % v1; return [ if (non(Op.sub, e1) && non(Op.sub, e2)) ...[ if (non(Op.add, e2)) (App(Op.add, e1, e2), v1 + v2), (App(Op.sub, e2, e1), v2 - v1), ], if (1 < v1 && non(Op.div, e1) && non(Op.div, e2)) ...[ if (non(Op.mul, e2)) (App(Op.mul, e1, e2), v1 * v2), if (r == 0) (App(Op.div, e2, e1), q), ], ]; } List<(Expr, int)> comb2NF((Expr, int) ev1, (Expr, int) ev2) { final (e1, v1) = ev1; final (e2, v2) = ev2; return [ if (non(Op.sub, e1) && non(Op.add, e2) && non(Op.sub, e2)) (App(Op.add, e1, e2), v1 + v2), if (1 < v1 && non(Op.div, e1) && non(Op.div, e2)) ...[ if (non(Op.mul, e2)) (App(Op.mul, e1, e2), v1 * v2), (App(Op.div, e1, e2), 1), ], ]; }
図 20.2 comb1 と comb2 の新しい定義

この版を countdown3 と呼びます。

> display (countdown3 831 [1,3,7,10,25,50]) (7+((1+10)*(25+50))) = 832 (1.06 secs, 88697284 bytes) > length $ concatMap mkExprs $ subseqs [1,3,7,10,25,50] 36539
実測結果 約 3.6 万個の式を 1.06 秒で処理。countdown2 のおよそ 2 倍速です。

メモ化

なぜ計算が重複するのか

正規形でも冗長性が残る話とは別に、部分列ごとに独立して計算しているため、同じ計算が何度も繰り返されています。

たとえば元の数が [1..6] のとき、基底が [1..5] の式は 2 回計算されます(部分列 [1..5][1..6] のとき)。基底が [1..4] の式は次の 4 つの部分列ごとに、合わせて 4 回計算されます。

[1, 2, 3, 4], [1, 2, 3, 4, 5], [1, 2, 3, 4, 6], [1, 2, 3, 4, 5, 6]

一般に、n 個の元の数から k 個を基底とする式は 2nkも計算されます。もったいない!

メモ化の設計

そこで mkExprs の結果をメモテーブルに保存し、次回からは再計算せず取り出すようにします。次の操作を持つデータ型 Memo を用意します。

empty :: Memo fetch :: Memo → [Int] → [(Expr, Value)] store :: [Int] → [(Expr, Value)] → Memo → Memo
Dart // メモ操作の抽象インターフェース(実装は trie で後述)。 // Memo empty(); // List<(Expr, int)> fetch(Memo m, List<int> xs); // Memo store(List<int> xs, List<(Expr, int)> evs, Memo m);

mkExprs はメモテーブルを引数に取る形に書き換えます。

mkExprs :: Memo → [Int] → [(Expr, Value)] mkExprs memo [x] = [(Num x, x)] mkExprs memo xs = [ev | (ys, zs) ← unmerges xs, ev1 ← fetch memo ys, ev2 ← fetch memo zs, ev ← combine ev1 ev2]
Dart // メモ付き mkExprs:部分列 ys, zs の結果は必ずメモ済みという前提で取り出す。 List<(Expr, int)> mkExprsMemo(Memo memo, List<int> xs) { if (xs.length == 1) return [(Num(xs.first), xs.first)]; return [ for (final (ys, zs) in unmerges2(xs)) for (final ev1 in fetch(memo, ys)) for (final ev2 in fetch(memo, zs)) ...combine2(ev1, ev2), ]; }
大事な前提 この定義は、部分列 xs を処理する時点で、そのあらゆる分割 (ys, zs) について yszs の結果がすでにメモにあることを仮定しています。
幸い、先の subseqs は「xsys の部分列なら xs の方が先に出る」順で並べてくれるので、この前提は自然に成り立ちます。

全体は次のように書けます。

countdown4 :: Int → [Int] → (Expr, Value) countdown4 n = nearest n · extract · memoise · subseqs
Dart (Expr, int) countdown4(int n, List<int> xs) { final memo = memoise(subseqs(xs)); return nearest(n, extract(memo)); }
memoise :: [[Int]] → Memo memoise = foldl insert empty insert memo xs = store xs (mkExprs memo xs) memo
Dart // 各部分列を昇順(=短い部分列が先)でメモに畳み込んでいく。 Memo memoise(List<List<int>> xss) { var memo = empty(); for (final xs in xss) { memo = store(xs, mkExprsMemo(memo, xs), memo); } return memo; }

Memo の中身:trie(トライ木)

メモテーブルの実装として、枝に整数ラベルが付いた trie(トライ木)を使います。

data Trie a = Node a [(Int, Trie a)] type Memo = Trie [(Expr, Value)]
Dart // 枝に整数ラベルを持つ trie。ノードは値 a と (Int, Trie a) の列を保持。 class Trie<A> { final A value; final List<(int, Trie<A>)> children; const Trie(this.value, this.children); } typedef Memo = Trie<List<(Expr, int)>>;

空のメモは empty = Node [] [] です。検索は枝ラベルをたどるだけ。

fetch :: Memo → [Int] → [(Expr, Value)] fetch (Node es xms) [] = es fetch (Node es xms) (x : xs) = fetch (follow x xms) xs follow :: Int → [(Int, Memo)] → Memo follow x xms = head [m | (x', m) ← xms, x == x']
Dart Memo empty() => const Trie<List<(Expr, int)>>([], []); List<(Expr, int)> fetch(Memo m, List<int> xs) { var cur = m; for (final x in xs) { cur = follow(x, cur.children); } return cur.value; } Memo follow(int x, List<(int, Memo)> xms) { for (final (xp, m) in xms) { if (xp == x) return m; } throw StateError('trie: label $x not found'); }

登録は次のとおり。既存のエントリの後ろに新規エントリを追加します。

store :: [Int] → [(Expr, Value)] → Memo → Memo store [x] es (Node fs xms) = Node fs ((x, Node es [ ]) : xms) store (x : xs) es (Node fs xms) = Node fs (yms ++ (x, store xs es m) : zms) where (yms, (z, m) : zms) = break (equals x) xms equals x (z, m) = (x == z)
Dart // パスを辿りつつ、末端では新しい子として (x, Node es []) を先頭に付加する。 Memo store(List<int> xs, List<(Expr, int)> es, Memo m) { final fs = m.value; final xms = m.children; if (xs.length == 1) { final x = xs.first; return Trie(fs, [(x, Trie(es, const [])), ...xms]); } final x = xs.first; final rest = xs.sublist(1); // 一致する子を探して差し替える(見つからない前提はない)。 final newChildren = <(int, Memo)>[ for (final (z, child) in xms) if (z == x) (z, store(rest, es, child)) else (z, child), ]; return Trie(fs, newChildren); }

そして、メモテーブル全体から式を取り出す関数。

extract :: Memo → [(Expr, Value)] extract (Node es xms) = es ++ concatMap (extract · snd) xms
Dart // メモ木を丸ごと平坦化する。 List<(Expr, int)> extract(Memo m) => [ ...m.value, for (final (_, child) in m.children) ...extract(child), ];

実行結果はこうです。

> display (countdown4 831 [1,3,7,10,25,50]) (10*((1+7)+(3*25))) = 830 (0.66 secs, 55798164 bytes)
実測結果 0.66 秒まで縮みました(countdown3 の約半分)。 返ってきた式は違いますが(解析順が異なるため)、いずれも「831 との差 1」で、目標に一番近い答えです。

骨格木(Skeleton trees)

メモ化の弱点

ただし、メモ化には代償があります。メモテーブルは非常に大きくなるので、ヒープを圧迫し、ガーベジコレクション(GC)に時間を取られるのです。メモ化の利点を残したまま、空間の使用を抑えられないでしょうか?

アイデア:まず括弧の形だけ数える

式の中の演算子を無視して、括弧の構造だけに注目してみましょう。すると、6 個の数からできる方向付き二分木(oriented binary tree)は、なんとたった 1881 個しかありません(方向付き=部分木の順序を区別しない)。この木を骨格木(skeleton tree)と呼びます。

順序としては、まず骨格木を全部作ってからメモ化し、あとで演算子を挿入するのが省エネです。

実装:Tree 型と mkTrees

先端に整数ラベルの付いた二分木を使います。

data Tree = Tip Int | Bin Tree Tree
Dart sealed class Tree { const Tree(); } class Tip extends Tree { final int x; const Tip(this.x); } class Bin extends Tree { final Tree t1, t2; const Bin(this.t1, this.t2); }

メモの中身も式ではなく木にします。

type Memo = Trie [Tree]
Dart // 骨格木版のメモは Tree のリストを保持する(式ではなく形だけ)。 typedef TreeMemo = Trie<List<Tree>>; TreeMemo emptyTree() => const Trie<List<Tree>>([], []); // fetch/store/extract は先の trie 実装をジェネリックに読み替えれば同じ。

木の構築は、式の構築とまったく同じ形で行えます。

mkTrees :: Memo → [Int] → [Tree] mkTrees memo [x] = [Tip x] mkTrees memo xs = [Bin t1 t2 | (ys, zs) ← unmerges xs, t1 ← fetch memo ys, t2 ← fetch memo zs]
Dart // 演算子を無視して二分木の形だけを構築する。 List<Tree> mkTrees(TreeMemo memo, List<int> xs) { if (xs.length == 1) return [Tip(xs.first)]; List<Tree> fetchT(List<int> k) { var cur = memo; for (final x in k) { for (final (xp, m) in cur.children) { if (xp == x) { cur = m; break; } } } return cur.value; } return [ for (final (ys, zs) in unmerges2(xs)) for (final t1 in fetchT(ys)) for (final t2 in fetchT(zs)) Bin(t1, t2), ]; }

その後、木を式に変換するときに、あらゆる妥当な演算子を挿入します。

toExprs :: Tree → [(Expr, Value)] toExprs (Tip x) = [(Num x, x)] toExprs (Bin t1 t2) = [ev | ev1 ← toExprs t1, ev2 ← toExprs t2, ev ← combine ev1 ev2]
Dart // 骨格木に、可能なあらゆる演算子を挿入して式へ展開する。 List<(Expr, int)> toExprs(Tree t) => switch (t) { Tip(:final x) => [(Num(x), x)], Bin(:final t1, :final t2) => [ for (final ev1 in toExprs(t1)) for (final ev2 in toExprs(t2)) ...combine2(ev1, ev2), ], };

全体はこうなります。

countdown5 n = nearest n · concatMap toExprs · extract · memoise · subseqs
memoise :: [[Int]] → Memo memoise = foldl insert empty insert memo xs = store xs (mkTrees memo xs) memo

いつもの例で実行:

> display (countdown5 831 [1,3,7,10,25,50]) (10*((1+7)+(3*25))) = 830 (1.06 secs, 88272332 bytes)

おや、これだけを見ると、骨格木のメモ化は式のメモ化ほど良くないように見えます……。でも状況をもう少しよく調べてみましょう。

もう少し詳しい実験

5 つの countdown を、GHC 6.8.3 の -O2 でコンパイルして比較しました。ランタイムのオプション -s で統計を取ります。ファイルは d6、d7、d8 の 3 つで、それぞれ元の数が 6、7、8 個です。どれも厳密解が存在しないようにして、全空間を探索させました。

ファイル countdown1 countdown2 countdown3 countdown4 countdown5
TotalGC TotalGC TotalGC TotalGC TotalGC
d61.560.780.190.080.090.050.080.020.050.00
d777.636.92.031.190.440.090.530.300.330.02
d899.857.213.87.3016.99.027.220.31
図 20.3 元の数が 6, 7, 8 個の場合の countdown 実行時間(秒)

countdown1 は d8 では時間がかかりすぎるため実行していません。

結論
Dart // Expr を簡易的に文字列化 String showExpr(Expr e) => switch (e) { Num(:final x) => '$x', App(:final op, :final e1, :final e2) => '(${showExpr(e1)} ${switch (op) { Op.add => '+', Op.sub => '-', Op.mul => '*', Op.div => '/' }} ${showExpr(e2)})', }; // 動作確認: 定番のテストケース (Hutton 2002) void main() { final nums = [1, 3, 7, 10, 25, 50]; const target = 831; // countdown1 は素朴版、countdown4 は正規形+剪定版。どちらも (Expr, int) を返す。 final (e1, v1) = countdown1(target, nums); print('countdown1: ${showExpr(e1)} = $v1'); final (e4, v4) = countdown4(target, nums); print('countdown4: ${showExpr(e4)} = $v4'); // どちらも v == 831(正解が存在)を返す。 }

結び

本章は Bird and Mu (2005) をもとに、内容を抜粋・改変してまとめたものです。同論文では、Countdown の仕様を「関係」の枠組みで書き下し、fold と unfold の代数法則を使って、いくつかのプログラムを計算的に導いています(本章では計算の詳細は省略)。

Countdown はさらに古い章 (Hutton, 2002) でも扱われており、そこでは「関数プログラムが仕様を満たすことをどう証明するか」の題材として使われました。Hutton の目的は最良のアルゴリズムを導くことではなく、単純な帰納法だけで正当性が示せる例を提示することでした。実質的には、Hutton は countdown2 の正当性を扱っています。

参考文献

Bird, R. S. and Mu, S.-C. (2005). Countdown: a case study in origami programming. Journal of Functional Programming 15 (6), 679–702.

Hutton, G. (2002). The Countdown problem. Journal of Functional Programming 12 (6), 609–16.

1論理的には、値は式から計算できるので、両方を返す必要はありません。ただし、章「Making a century」(Pearl 6)で見たとおり、同じ値を何度も計算しないようにするのは良い設計です。ここでも最初からこの最適化を取り入れています。