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で提供されているany
やall
と大体同じものです。
さらに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
から巧妙にx
とy
それぞれを評価する関数を作り出しているのが分かると思います。この実装を利用して、同じ型にはなってしまいますが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))
otimes
はx
の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]
となりエイト・クイーンを解くことができました
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)
これだけです!overline
もotimes
も必要なくモナドを使うと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モナドこれから流行るといいですね!