Posted at

Selectionモナド入門

Selectionモナドは2010年にEscardóとOlivaによって"Selection Functions, Bar Recursion, and Backward Induction"で紹介されました。継続モナドによく似ていますが少し違っており、ゲーム理論の解法の一つである後ろ向き帰納法や探索アルゴリズムなど色んなパターンを取り扱うことができます。transformersというよく知られたライブラリではControl.Monad.Trans.Selectというモジュールとして実装が提供されています。

Selectionモナドの型を見てみましょう。

newtype Select r a = Select { runSelect :: (a -> r) -> a }

一方、継続モナドの型はこちらです。

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

どちらもaを取ってrを返す関数を引数に取る高階関数になっていますがその返り値がaなのかrなのかの違いがあります。実はSelectionモナドが与えられれば継続モナドを作ることができます。すなわちSelectionモナドから継続モナドへの自然変換を

selectToCont :: Select r a -> Cont r a

selectToCont (Select e) = Cont $ \p -> p (e p)

のように実装することができます。

この記事ではSelectionモナドを使ったいくつかの例と、Monadとしての実装を見ていきたいと思います。


Selection関数

それではSelectionモナドの具体例を見ていきましょう。この章では"What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common"を参考に手短に要約しながら解説していきたいと思います。

まずはモナドとしてではなく単なる関数(Selection関数)としての性質を見ていきたいと思います。そのため

type J r x = (x -> r) -> x

という形でSelection関数にJという名前をつけておきます。

例えばある実数値関数の最大値を与える点を探す問題

\underset{x}{\rm argmax}\ f(x)

を考えると${\rm argmax}$は$x$を受け取って実数を帰す関数$f$を受け取って$x$の値を返す関数と考えることができ、Selection関数と思うことができます。これを実装すると

argmax :: [x] -> J Int x

argmax [] p = undefined
argmax [x] p = x
argmax (x:y:zs) p = if p x < p y
then argmax (y:zs) p
else argmax (x:zs) p

argmin :: [x] -> J Int x
argmin xs p = argmax xs (\x -> - p x)

のようになり(あまり効率的な実装ではありませんが...)、評価関数の符号を入れ替えることでargminを実装することもできました。

他にも平均値の定理より実数関数$p$が与えられると

\int^1_0 p(x)dx = p(a)

を満たすような$a$が存在しますが、$p$が与えられたときにこの$a$を返すような操作はSelection関数と思うことができます。ただしこの関数を具体的に実装することは難しそうです。

また単純な検索関数

find :: [x] -> J Bool x

find [] p = undefined
find [x] p = x
find (x:xs) p = if p x then x else find xs p

もSelection関数を使って表すことができます。これを使えば

-- | 継続のパターン

type K r x = (x -> r) -> r

-- | Selection関数から継続のパターンへの変換
overline :: J r x -> K r x
overline e = \p -> p (e p)

forsome, forevery :: [x] -> K Bool x
forsome = overline . find
forevery xs p = not (forsome xs (not . p))

というように、リストのある値が条件を満たすかを調べる関数forsomeとリストの全ての値が条件を満たすかを調べる関数foreveryのような関数を実装することができます。HaskellのPreludeで提供されているanyallと大体同じものです。

さらに2変数の実数値関数$q(x, y)$があった時に上記2つを組み合わせて

\underset{x}{\rm argmax}\int^1_0q(x, y)dy

のような式を考えて適切な$x, y$を求める操作を考えることが出来ると思います。これは$argmax$と平均値の定理という2つのSelection関数の積を取るような操作だと考えることができるでしょう。この操作を具体的に実装してみましょう。

-- | 2つのSelection関数の積

times :: J r x -> (x -> J r y) -> J r (x, y)
times e0 e1 p = (a0, a1)
where
a0 = e0 (\x0 -> overline (e1 x0) (\x1 -> p (x0, x1)))
a1 = e1 a0 (\x1 -> p (a0, x1))

timesを眺めると(x, y)を評価する関数pから巧妙にxyそれぞれを評価する関数を作り出しているのが分かると思います。この実装を利用して、同じ型にはなってしまいますがn個のSelection関数の積を求める関数を実装してみましょう。

otimes :: J r x -> (x -> J r [x]) -> J r [x]

otimes e0 e1 p = a0 : a1
where
a0 = e0 (\x0 -> overline (e1 x0) (\x1 -> p (x0 : x1)))
a1 = e1 a0 (\x1 -> p (a0 : x1))

otimesxのSelection関数とxを受け取って[x]のSelection関数を返す関数を組み合わせて[x]のSelection関数で、一つ前のSelection関数の結果に依存しながらSelection関数の積を計算していくことができています。もっと発展させて一つ前まで全ての結果に依存しながらSelection関数の積を計算していく関数を定義してみましょう。

bigotimes :: [[x] -> J r x] -> J r [x]

bigotimes [] = \p -> []
bigotimes (e:es) = e [] `otimes` (\x -> bigotimes [\xs -> d (x:xs) | d <- es])

実はこのbigotimes関数は一つ前までの値への依存を無視すると[J r x] -> J r [x]という型になっており、J rすなわちSelect rがモナドであること知っていればsequence関数に対応していることが分かるかと思います。bitotimesはSelectionモナドを語る時には欠かせない重要な関数です。


エイト・クイーン

実際にSelection関数を使って問題を解いてみましょう。ここで解いてみる問題はエイト・クイーンです。



画像出典: エイト・クイーン - Wikipedia

チェスにおいてクイーンは縦・横・斜めの全ての方向の任意のマスに移動できるコマです。このクイーンを8個、互いに互いのコマを1手で取ることができないようにチェス盤に配置することが出来るかと言うのがエイト・クイーンという問題です。この問題は解くことができて解が全部で12個あることが知られています。

-- | n個のクイーンを配置することを考える

n = 8

-- | コマの縦もしくは横の位置
-- 横から何列目か、上から何行目かをIntで表す
type Coord = Int

-- | コマの座標(x, y)
type Pos = (Coord, Coord)

-- | 2つの座標が衝突していないことを検証する
attacks :: Pos -> Pos -> Bool
attacks (x, y) (a, b) =
x == a -- 縦がかぶっていないか
|| y == b -- 横がかぶっていないか
|| abs (x - a) == abs (y - b) -- 斜めがかぶっていないか

-- | 全ての座標が衝突していないことを検証する
valid :: [Pos] -> Bool
valid [] = True
valid (u : vs) = not (any (\v -> attacks u v) vs) && valid vs

まずはエイト・クイーンに固有な関数を実装していきました。次にこれまでに定義したSelection関数に関する関数を組み合わせてエイト・クイーンを解いてみましょう。

-- | 与えられた配置が衝突しているかどうかを返す

p :: [Coord] -> Bool
p ms = valid (zip ms [0..(n-1)])

-- | 既存の配置が与えられた時の新しいコマのSelection関数のリスト
epsilons :: [[Coord] -> J Bool Coord]
epsilons = replicate n epsilon
where
epsilon hs = find ([0..(n-1)] \\ hs)

-- | 最適なコマの配置
optimalPlay :: [Coord]
optimalPlay = bigotimes epsilons p

main :: IO ()
main = print optimalPlay

実行してみると

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

となりエイト・クイーンを解くことができました :clap:

Repl.it上で動作するコードはこちら

https://repl.it/@lotz84/GivingBewitchedCodec


三目並べ

三目並べは2人のプレイヤーが3×3マスの盤面に○と☓を交互に書いていき、先に縦・横・斜めに同じ記号が揃えられた方の勝ちというゲームです。



画像出典: Googleで「三目並べ」と検索した結果出てくるゲームより

三目並べは先手・後手ともに最善を尽くすと必ず引き分けとなることが知られていますが、エイト・クイーンのときと同じようにSelection関数を使って最善の手を計算し、引き分けになることを実際計算してみましょう。

-- | 2人のプレイヤー

data Player = X | O

-- | 評価関数の値
-- 以下のような値を取る
-- Xが勝ち: 1
-- Oが勝ち: -1
-- 引き分け: 0
type Result = Int

-- | 盤面上の位置
-- 0 | 1 | 2
-- -----------
-- 3 | 4 | 5
-- -----------
-- 6 | 7 | 8
type Pos = Int

-- | XとOが行ってきた手番の組
type Board = ([Pos], [Pos])

-- | 手番に勝ちパターンが含まれているか
-- 引数の手番のリストはソートされていることを仮定している
wins :: [Pos] -> Bool
wins ms = any (`isSubsequenceOf` ms)
[[0,1,2],[3,4,5],[6,7,8],[0,3,6]
,[1,4,7],[2,5,8],[0,4,8],[2,4,6]]

-- | 手番を評価する
value :: Board -> Result
value (x,o)
| wins x = 1
| wins o = -1
| otherwise = 0

-- | ソートされたリストに要素を追加する
insert :: Ord x => x -> [x] -> [x]
insert x [] = [x]
insert x (vs@(y : ys))
| x == y = vs
| x < y = x : vs
| otherwise = y : insert x ys

-- | 勝敗が決まるか手番がなくなるまでゲームを進行する
outcome :: Player -> [Pos] -> Board -> Board
outcome whoever [] board = board
outcome X (m : ms) (x, o) =
if wins o then (x, o)
else outcome O ms (insert m x, o)
outcome O (m : ms) (x, o) =
if wins x then (x, o)
else outcome X ms (x, insert m o)

まずは三目並べに固有な関数をざっと実装してみました。次にSelectionに関する関数を組み合わせて、今度は三目並べを解いてみましょう。

-- | 手番のリストから結果を返す

p :: [Pos] -> Result
p ms = value (outcome X ms ([],[]))

-- | これまでの手番から次の最適な手番を返す関数のリスト
-- 偶数番目はXにとって最善な手を、
-- 奇数番目はOにとって最善な手を計算していることに注意
epsilons :: [[Pos] -> J Result Pos]
epsilons = take 9 all
where
all = epsilonX : epsilonO : all
epsilonX h = argmax ([0..8] \\ h)
epsilonO h = argmin ([0..8] \\ h)

-- | 最善な手番
optimalPlay :: [Pos]
optimalPlay = bigotimes epsilons p

-- | 最善な手番の結果
optimalOutcome :: Result
optimalOutcome = p optimalPlay

main :: IO ()
main = do
putStrLn $ "最善な手番: " ++ show optimalPlay
putStrLn $ "最善な手番の結果: " ++ show optimalOutcome

実行してみると

最善な手番: [0,4,1,2,6,3,5,7,8]

最善な手番の結果: 0

となり最善な手番の結果、引き分けとなることがわかりました。

Repl.it上で動作するコードはこちら

https://repl.it/@lotz84/AdorableMediumTelephone

ちなみにこの計算、膨大なゲームの展開を計算していくため非常に時間がかかります。ローカルのPCで実行したときは結果が出るのに約1分20秒かかりました(Repl.it上だと終わりません…)。しかし重要なのはエイト・クイーンも三目並べも同じパターンを使って解けているということです。同じパターンを使って書けるということは抽象化の可能性を秘めており、本質的な構造が裏に隠されているはずです。(計算時間に関しても実装の工夫で改善の余地はありそうです)


Selectionモナド

実は(表題にもある通り)Selection関数はモナドのインスタンスにすることができます。

newtype Select r a = Select { runSelect :: (a -> r) -> a }

まずはFunctorのインスタンスを定義してみましょう。

instance Functor (Select r) where

fmap f (Select g) = Select $ \p ->
let p' = (. f) p
in f (g p')

難解に見えますが一つずつ型を見ていきましょう。

f        :: a -> b

(.) :: (b -> r) -> (a -> b) -> a -> r
(. f) :: (b -> r) -> a -> r
p :: b -> r
p' :: a -> r
g :: (a -> r) -> a
f (g p') :: b

合成関数演算子(.)を使ってa -> b(b -> r) -> a -> rに置き換えてるのがポイントですね。次にApplicativeのインスタンスを定義してみましょう。

instance Applicative (Select r) where

pure a = Select $ \_ -> a
Select gf <*> Select gx = Select $ \p -> do
let h f = f (gx (p . f))
f = gf (p . h)
in h f

また一つずつ型を見ていくと、

gf         :: ((a -> b) -> r) -> (a -> b)

gx :: (a -> r) -> a
p :: b -> r
p . f :: a -> r
gx (p . f) :: a
h :: (a -> b) -> b
p . h :: (a -> b) -> r
f :: a -> b

このようにうまく組み合わせることでbの値を計算しています。最後にMonadのインスタンスを定義してみましょう。

instance Monad (Select r) where

Select g >>= f = Select $ \p -> do
let h x = runSelect (f x) p
y = g (p . h)
in h y

これもまた一つずつ型を見ていくと、

g :: (a -> r) -> a

f :: a -> Select r b
p :: b -> r
h :: a -> b
p . h :: a -> r
y :: a

となりうまくbの値が計算できていることが分かるかと思います。

最後に実装したSelectモナドを使って前章で見たbitotimesもう一度実装してみましょう。

bigotimes :: [[x] -> Select r x] -> Select r [x]

bigotimes [] = pure []
bigotimes (e:es) = do
x <- e []
xs <- bigotimes es
pure (x:xs)

これだけです!overlineotimesも必要なくモナドを使うとbigotimesをスッキリと実装することができました。

参考までにSelectionモナドを使ったバージョンのエイト・クイーンのプログラムをこちらに載せておきました。

https://repl.it/@lotz84/EuphoricChocolateTaskscheduling

ちなみにここで紹介したSelectモナドはtransformersライブラリのControl.Monad.Trans.Selectで提供されています。Selectionモナドのトランスフォーマー版であるSelectTもあります。


まとめ

Selectionモナドの存在は2019/3/30に新宿で行われたGordon Plotkin先生に学ぶAlgebraic EffectでPlotkin先生に紹介されて初めて知りました。この記事で紹介した例だけでなく証明論への応用1だったり、計算機科学版のチコノフの定理を応用して(Int -> Bool) -> rのような型を持つ関数のEqインスタンスを定義できたり2Selection関数を尤度関数と絡めることで機械学習に応用できる可能性も秘めているようで、まだまだ面白い話はたくさんありそうです。Selectionモナドこれから流行るといいですね!