LogicT

Backtracking, Interleaving, and Terminating Monad Transformersを紹介します。

Abstract

任意のモナドでバックトラッキングを可能にするモナドトランスフォーマーを設計、実装します。

このライブラリは次のような操作を提供します。

これらはmsplitという一つプリミティブで実装することができます。

また、次の2つの実装を紹介します。

1. Introduction

モナドは計算の観念を一般化します。

モナドプラスには実践的な応用があります。

Hinzeのバックトラッキングモナドトランスフォーマーは非決定的選択とProlog-likeなcutをサポートします。

これを含めた多くのバックトラッキングモナドトランスフォーマーには3つの欠点があります。

一番目は不公平による終わらない解の探索です。これは公平な選言と連言を実装することで解決されます。

二番目はcutを実装することによる否定と枝刈りの混同です。これはソフトカットとコミットチョイスに分離することで解決されます。

三番目は最終的な結果を得る機能が限定的であることです。これは表現力のある実行インターフェースを提供することで解決されます。

ストリームベースの実装に加えてCPSとControl-channelの二つの実装を示します。

CPSに基づく実装は成功と失敗の継続を使います。パターンマッチは行われず継続が実行されるだけです。このため、決定的なコードは高速に実行されます。

Control-channelに基づく実装は限定継続を使います。これはより洗礼された探索戦略で拡張可能です。

これら二つの実装に対してmsplitを定義します。

msplit :: (Monad m, LogicT t, MonadPlus (t m)) => t m a -> t m (Maybe (a, (t m a)))

msplitは最初の解を計算し残りの計算を停止します。

mは任意の作用を提供するモナドで、tはここで設計し実装されるモナド変換子です。

2. Basic Backtracking Computation: MonadPlus

mplusは選言を、mzeroは失敗を意味します。

class Monad m => MonadPlus m where
  mzero :: m a
  mplus :: m a -> m a -> m a

モナドプラスは次のような法則を満たすべきです。

-- 定義 2.1
mplus a mzero === a
mplus mzero a === a
mplus a (mplus b c) === mplus (mplus a b) c
mzero >>= k === mzero
(mplus a b) >>= k === mplus (a >>= k) (b >>= k)

連言>>=はゴールを左から右に評価します。

t1, t2, t3 :: MonadPlus m => m Int
t1 = mzero
t2 = return 10 `mplus` return 20 `mplus` return 30
t3 = msum (map return [10, 20, 30])

t1は失敗を表現し、t2t3は同一で3つの選択肢を表現します。

リストモナドはモナドプラスの適切な実装です。

複数の選択により生成された解はストリームに変換可能です。

runList :: [a] -> [a]
runList = id

リストモナドは決定的計算でオーバーヘッドがあります。

また、次のプログラムは全ての解の列挙にn^2時間掛かります。

( ... (return 1 `mplus` return 2) `mplus` ... return n)

効率的な実装には二継続モデルと限定継続を使います。

コンビネータを定義した後個々の実装に立ち戻ります。

3. A More Expressive Interface

4つのコンビネータでモナドプラスを拡張します。

最初にrunListをリスト以外のモナドへ一般化します。

3.1 Running Computations

さしあたり次ような関数runLを考えます。

runL :: Maybe Int -> L a -> [a]

Lはバックトラッキングモナドです。

引数がNothingのときすべての解が生成されます。

引数がJust nのとき多くともnだけ解が生成されます。

3.2 Interleaving (Fair Disjunction)

プログラムは潜在的に無限の非決定的選択を作ります。

odds :: MonadPlus m => m Int
odds = (return 1) `mplus` (odds >>= \a -> return (2 + a))

runL (Just 5) odds[1,3,5,7,9]を返します。

oddsは単純には他の計算と合成できません。

runL (Just 1) (do x <- odds `mplus` t3
                  if even x then return x else mzero)

odds `mplus` t3t3を決して考慮しません。

しかし、10と20と30は解として返すことが可能です。

そこで新しいプリミティブinterleaveがあると便利です。

runL (Just 10) (odds `interleave` t3)

これは[1,10,3,20,5,30,7,9,11,13]を返します。

interleaveは次の例を可能にします。

runL (Just 1) (do x <- odds `interleave` t3
                  if even x then return x else mzero)

これは答え10を返します。

3.3 Fair Conjunction

不公平な選言は不公平な連言を引き起こします。

let oddsPlus n = odds >>= \a -> return (a + n)
in runL (Just 1)
        (do x <- (return 0 `mplus` return 1) >>= oddsPlus
            if even x then return x else mzero)

return 1 >>= oddsPlusがあるにも関わらず発散します。

公平なmplusに加えて公平な>>=が必要です。

>>-を使うことで次のプログラムは2を生成します。

let oddsPlus n = odds >>= \a -> return (a + n)
in runL (Just 1)
        (do x <- (return 0 `mplus` return 1) >>- oddsPlus
            if even x then return else mzero)

3.4 Laws of interleave and >>-

interleave>>-mplus>>=のアナロジーです。

非決定性計算はmzeroreturn a `mplus` mで表現できます。

-- 定義 3.1
interleave mzero m === m
interleave (return a `mplus` m1) m2 === return a `mplus` (interleave m2 m1)
mzero >>- k === mzero
(mplus (return a) m) >>- k === interleave (k a) (m >>- k)

interleave>>-の主な用途は発散を回避することです。

解の順序を考慮しなければmplus>>=に等しいです。

3.5 Soft cut (Conditional)

条件分岐は他の計算に依存する計算を表現できます。

次の例は他の数値で割り切れる奇数を生成します。

iota n = msum (map return [1..n])
test_oc = runL (Just 10)
               (do n <- odds
                   guard (n > 1)
                   d <- iota (n - 1)
                   guard (d > 1 && n `mod` d == 0)
                   return n)

この結果は[9,15,15,21,21,25,27,27,33,33]です。

奇素数の生成には"有限失敗による否定"が必要です。

ifte t th elは論理条件分岐演算です。

  1. 計算tを実行します
  2. 一つでも結果があれば全体はt >>= thと等価です
  3. さもなければ全体の計算はelと等価です

これは次の法則が得られます。

-- 定義 3.2
ifte (return a) th el === th a
ifte mzero th el === el
ifte (return a `mplus` m) th el === th a `mplus` (m >>= th)

ifteは"失敗の説明"に便利で、静かな失敗を回避します。

ifteを使って奇素数を生成することができます。

-- 例 3.1
test_op = runL (Just 10)
               (do n <- odds
                   guard (n > 1)
                   ifte (do d <- iota (n - 1)
                            guard (d > 1 && n `mod` d == 0))
                        (const mzero)
                        (return n))

結果は[3, 5, 7, 11, 13, 17, 19, 23, 29, 31]です。

3.6 Pruning (Once)

ifteはある意味で枝刈りのプリミティブです。

別の重要な枝刈りのプリミティブにonceがあります。

これはただ一つの解を選択します。

"どれでもよい非決定性"の表現に重要です。

onceのための簡単な例を示します。

bogosort l = do p <- permute l
                if sorted p then return p else mzero

sorted (e1:e2:r) = e1 <= e2 && sorted (e2:r)
sorted _ = True

permute [] = return []
permute (h:t) = do { t' <- permute t; insert h t' }

insert e [] = return [e]
insert e l@(h:t) = return (e:l) `mplus` do { t' <- insert e t; return (h:t') }

生成し、検査する手法は論理プログラミング特有です。

bogosortは要素が重複するとき複数の解を持ちます。

runL Nothing (bogosort [5,0,3,4,0,1])

これは[[0,0,1,3,4,5],[0,0,1,3,4,5]]を生成します。

しかし、明らかに解のどれか一つだけを必要とします。

bogosortを次のように変更することで表現できます。

bogosort' l = once (do p <- permute l
                       if sorted p then return p else mzero)

例3.1では素数の検査で全ての因数を計算します。

任意の因数があればそれ以上探索することは不要です。

test_op' = runL (Just 10)
                (do n <- odds
                    guard (n > 1)
                    ifte (once (do d <- iota (n - 1)
                                   guard (d > 1 && n `mod` d == 0)))
                         (const mzero)
                         (return n))

ifteonceで"失敗による否定"が実装できます。

gnot :: (Monad m, LogicT t, MonadPlus (t m)) => t m a -> t m ()
gnot m = ifte (once m) (const mzero) (return ())

mが成功するならばgnot mは失敗し、mが失敗するならばgnot mは成功します。

4. Splitting Computations

interleave>>-ifteoncemsplitで実装可能です。

msplitでインスタンス化できる型クラスを定義します。

4.1 The Monad LogicM

LogicMは前のセクションのインターフェースを持ちます。

これはmsplitを使ったデフォルト実装を含みます。

class MonadPlus m => LogicM m where
  msplit :: m a -> m (Maybe (a, m a))
  interleave :: m a -> m a -> m a
  interleave sg1 sg2 =
    do r <- msplit sg1
       case r of
         Nothing -> sg2
         Just (sg11, sg12) -> (return sg11) `mplus` (interleave sg2 sg12)
  (>>-) :: m a -> (a -> m b) -> m b
  sg >>- g =
    do r <- msplit
       case r of
         Nothing -> mzero
         Just (sg1, sg2) -> interleave (g sg1) (sg2 >>- g)
  ifte :: m a -> (a -> m b) -> m b -> m b
  ifte t th el =
    do r <- msplit t
       case r of
         Nothing -> el
         Just (sg1, sg2) -> (th sg1) `mplus` (sg2 >>= th)
  once :: m a -> m a
  once m =
    do r <- msplit m
      case r of
        Nothing -> mzero
        Just (sg1, _) -> return sg1

msplitは次の二つの法則を持ちます。

msplit mzero === return Nothing
msplit (return a `mplus` m) === return (Just (a, m))

デフォルト実装から公理を確かめることができます。

    ifte (return a) th el
=== do r <- msplit (return a)
       case r of
         Nothing -> el
         Just (sg1, sg2) -> (th sg1) `msplit` (sg2 >>= th)
=== do r <- msplit (return a `mplus` mzero)
       case r of
         Nothing -> el
         Just (sg1, sg2) -> (th sg1) `msplit` (sg2 >>= th)
=== do r <- return (Just (a, mzero))
       case r of
         Nothing -> el
         Just (sg1, sg2) -> (th sg1) `msplit` (sg2 >>= th)
=== case Just (a, mzero) of
       Nothing -> el
       Just (sg1, sg2) -> (th sg1) `msplit` (sg2 >>= th)
=== (th a) `mplus` (mzero >>= th)
=== th a

4.2 Implementing msplit Using Lists

この論文では継続モナドに対してmsplitを実装します。

リストモナドの場合はmsplitの実装が素直です。

newtype SSG a = Stream [a]
unSSG (Stream str) = str

instance Monad SSG where
  return e = Stream [e]
  (Stream es) >>= f = Stream (concat (map (unSSG . f) es))

instance MonadPlus SSG where
  mzero = Stream []
  (Stream es1) `mplus` (Stream es2) = Stream (es1 ++ es2)

instance LogicM SSG where
  msplit (Stream []) = return Nothing
  msplit (Stream (h:t)) = return (Just (h, Stream t))

4.3 The Monad Transformer LogicT

任意のモナドにバックトラッキングを加えるため、モナドトランスフォーマーを使います。

class MonadTrans t where
  lift :: Monad m => m a -> t m a

liftは次の法則を満たします。

lift . return === return
lift (m >>= k) === lift m >>= lift . k

これは基底のモナドmt mに持ち上げます。

LogicMに型変数を加えることでLogicTに一般化できます。

class MonadTrans t => LogicT t where
  msplit :: (Monad m, MonadPlus (t m)) => t m a -> t m (Maybe (a, t m a))
  interleave :: (Monad m, MonadPlus (t m)) => t m a -> t m a -> t m a
  (>>-) :: (Monad m, MonadPlus (t m)) => t m a -> (a -> t m b) -> t m b
  ifte :: (Monad m, MonadPlus (t m)) => t m a -> (a -> t m b) -> t m b -> t m b
  once :: (Monad m, MonadPlus (t m)) => t m a -> t m a

MonadTransを継承することでLogicTもまたliftすることができます。

lift (putStrLn "text") >> mzero

これは副作用を実行した後失敗する計算を表現します。

定義4.1は"持ち上げ"を制御することで一般化されます。

一番目の法則はlift m >> mzeroを考慮すべきで、二番目の法則はlift m `mplus` tm1を考慮すべきです。

tm1は型t m aを持ち、msplitは型t m (Maybe (a, t m a))を持ちます。

これらの関係を表すために次の関数を定義します。

reflect :: (Monad m, LogicT t, MonadPlus (t m)) => Maybe (a, t m a) -> t m a
reflect r = case r of
  Nothing -> mzero
  Just (a, tmr) -> return a `mplus` tmr

rr tm = msplit tm >>= reflect

rr tmtmと同じ型を持ち、reflectはモナドの計算値に作用しません。

一般化された法則を示します。

-- 定義 4.2
rr (lift m >> mzero) === lift m >> mzero
rr (lift m `mplus` tma) === lift m `mplus` (rr tma)

5. Implementations of LogicT

ここではLogicTの実装に注目し、継続とコントロールオペレータの2つの実装を与えます。

5.1 CPS Implementation

CPS実装は成功と失敗の継続を持つSFKTを導入します。

newtype SFKT m a = SFKT (forall ans. SK (m ans) a -> FK (m ans) -> m ans)
unSFKT (SFKT a) = a

type FK ans = ans
type SK ans a = a -> FK ans -> ans

SFKT mMonadかつMonadPlusで、SFKTはモナドトランスフォーマーです。

instance Monad m => Monad (SFKT m) where
  return e = SFKT (\sk fk -> sk e fk)
  m >>= f = SFKT (\sk -> unSFKT m (\a -> unSFKT (f a) sk))

instance Monad m => MonadPlus (SFKT m) where
  mzero = SFKT (\_ fk -> fk)
  m1 `mplus` m2 = SFKT (\sk fk -> unSFKT m1 sk (unSFKT m2 sk fk))

instance MonadTrans SFKT where
  lift m = SFKT (\sk fk -> m >>= (\a -> sk a fk))

"コンテキストパッシング"実装は項の解釈を除きます。

継続の抽象表現を維持しmsplitをサポートします。

instance LogicT SFKT where
  msplit tma = lift (unSFKT tma ssk (return Nothing))
    where ssk a fk = return (Just (a, (lift fk >>= reflect)))

成功と失敗の継続を与えることでtmaを分割します。

  1. 失敗したらlift (return Nothing)を返します
  2. 成功したらaと停止状態を返します

5.2 Implementation Using Delimited Control

コントロールオペレータ実装は限定継続を利用します。

これは限定継続計算CCとデリミタPromptを提供します。

最初にCCをモナドトランスフォーマーに拡張し、次のコントロールオペレータを定義します。

promptP :: Monad m => (Prompt r a -> CC r m a) -> CC r m a
abortP :: Monad m => Prompt r a -> CC r m a -> CC r m b
shiftP :: Monad m => Prompt r b -> ((CC r m a -> CC r m b) -> CC r m b) -> CC r m a

PromptCCのcontrol regionはrでパラメタ化されます。

型変数rは次の関数を使ってカプセル化されます。

runCC :: Monad m => (forall r. CC r m a) -> m a
runIdentity (runCC (promptP $ \p ->
                    do x <- shiftP p (\k -> k (k (return 2)))
                       return (x + 1)))

上の式は次のように進行します。

  1. プロンプトを作りスタックにプッシュします
  2. コンテキストdo{ }をスタックにプッシュします
  3. shiftPpまでの継続を保存します
  4. 継続に2を二回適用します

CCを使ってLogicTのインスタンスSRを定義します。

newtype SR r m a = SR (forall ans. ReaderT (Prompt r (Tree r m ans)) (CC r m) a)
unSR (SR f) = f

data Tree r m a = HZero | HOne a | HChoice a (CC r m (Tree r m a))

計算はReaderTの環境で実行されます。

次の型を持つask関数で環境にアクセスできます。

ReaderT (Prompt r (Tree r m ans)) (CC r m) (Prompt r (Tree r (Tree r m ans)))

SR r mは二継続モデルのダイレクトスタイル版です。

成功継続は値だけでなく継続を取り実行します。

二継続モデルでは決定的計算の特別な表現はありません。

このモデルではTree r m aで決定的な結果を区別します。

SR r mMonadのインスタンスを示します。

instance Monad m => Monad (SR r m) where
  return e = SR (return e)
  (SR m) >>= f = SR (m >>= (unSR . f))

決定的計算は基底モナドmを"普通に"実行します。

SR r mMonadPlusのインスタンスを示します。

instance Monad m => MonadPlus (SR r m) where
  mzero =
    SR (ask >>= \pr -> lift (abortP pr (return HZero)))
  m1 `mplus` m2 =
    SR (ask >>= \pr ->
        lift $ shiftP pr $ \sk ->
        do f1 <- sk (runReaderT (unSR m1) pr)
           let f2 = sk (runReaderT (unSR m2) pr)
           compose_trees f1 f2)

compose_trees HZero r = r
compose_trees (HOne a) r = return $ HChoice a r
compose_trees (HChoice a r') r =
  return $ HChoice a $ r' >>= (\v -> compose_trees v r)

mzeroは結果HZeroでデリミタを中断します。

mplusはより複雑です。

  1. デリミタまでの継続skを保存します
  2. 選択肢m1は継続で実行されます
  3. 選択肢m2は一時停止されます
  4. compose_treesTreeを構築します
    • 最初の結果と停止状態を結合します

msplitに必要な関数を検討します。

reifyはデータ型でバックトラッキングを表現します。

reify :: Monad m => SR r m a -> CC r m (Tree r m a)
reify m = promptP (\pr -> runReaderT (unSR m) pr >>= (return . HOne))

次の例は計算mmplus m1 m2の場合です。

reify (m0 >>= (\x -> k1 x `mplus` k2 x) >>= k3)

この例は次に等しいです。

do HOne x <- reify m0
   f1val <- reify (k1 x >>= k3)
   let f2comp = reify (k2 x >>= k3)
   compose_trees f1val f2comp

ここでm0は決定的計算です。

f1valは一番目の選択肢の結果です。

f2compは二番目の選択肢に対応する計算です。

compose_treesは選択点の制御を柔軟にします。

(odds >> mzero) `mplus` mで発散を回避できます。

SR rmsplitを実装します。

instance MonadTrans (SR r) where
  lift m = SR (lift (lift m))

instance LogicT (SR r) where
  msplit m = SR (lift (reify m >>= (return . reflect_sr)))
    where reflect_sr HZero = Nothing
          reflect_sr (HOne a) = Just (a, mzero)
          reflect_sr (HChoice a r1) =
            Just (a, SR (lift r1) >>= (return . reflect_sr) >>= reflect)

ダイレクトスタイルのためのLogicTを実装しました。

SR r m aは先進的なシステムの実装に適しています。

6. Running Computations

解のリストを結果とするrunLを実装します。

単純な方法はSFKTなどにsolve関数を定義することです。

solve :: (Monad m) => SFKT m a -> m [a]
solve (SFKT m) = m (\a fk -> fk >>= (return . (a:))) (return [])

しかし、この関数では十分ではありません。

これはmが非正格なときだけ動作します。

mが正格なときSFKT m aの全ての解が集められます。

無限の解を持つSFKT IO aへのsolveの適用は発散します。

runLは観測したい数だけの答えを返し、それ以上のバックトラッキングは行われません。

従って、runLは正格なモナドの上でも計算を安全に扱えます。

SFKTを実行するとき継続を通す必要があります。

次の関数は最初の解を返した後に継続を無視します。

observe :: Monad m => SFKT m a -> m a
observe (SFKT m) = m (\a fk -> return a) (fail "no anser")

fkを実行することでsolveのように全ての解を得ます。

しかし、一定の回数だけfkを実行する方法が見えません。

msplitを使うことでrunLを実装します。

これはより一般的な操作bagofNunfoldを実装することが可能です。

bagofNはバックトラッキングの実装に依存しません。

Prologのbagofはリストにゴールの全ての解を集めますが、bagofNは望まれる数だけの解を得ます。

bagofN :: (Monad m, LogicT t, MonadPlus (t m)) => Maybe Int -> t m a -> t m [a]
bagofN (Just n) _ | n <= 0 = return []
bagofN n m = msplit m >>= bagof N'
  where bagofN' Nothing = return []
        bagofN' (Just (a, m')) = bagofN (fmap pred n) m' >>= (return . (a:))

最初の引数がJust nなら多くともnだけ解を選択します。

bagofNの結果はt m [a]で、mに戻すにはobserveが必要です。

観測関数には明確なバックトラッキング実装が必要です。

SRモナドでは次のようになります。

observe_sr :: Monad m => (forall r. SR r m a) -> m a
observe_sr m = runCC (reify m >>= pick1)
  where pick1 HZero = fail "no answer"
        pick1 (HOne a) = return a
        pick1 (HChoice a r) = return a

計算mTree r m aにreifyし最初の解を取り出します。

observeによりrunL関数を書くことができます。

type L a = forall r. SR r Identity a
runL :: Maybe Int -> L a -> [a]
runL n m = runIdentity (observe_sr (bagofN n m))

恒等モナド上のSR rはバックトラッキングモナドLです。

SFKTでも実行可能です。

例3.1を変更します。

test_opio = print =<< observe (bagofN (Just 10))
              do n <- odds
                 guard (n > 1)
                 ifte (do d <- iota (n - 1)
                          guard (d > 1 && n `mod` d == 0)
                          liftIO (print d))
                      (const mzero)
                      (return n)

IOモナドは中間結果をプリントします。

このアプローチはDebug.Traceを使うよりロバストです。

例3.1と比較しても大部分は同じコードです。

9. Conclusion

バックトラッキングモナドの次の機能を紹介しました。

次のトランスフォーマーの実装を説明しました。

msplitでバックトラッキングオペレータが実装されます。

これはストリームとしてトランスフォーマーを扱えます。

ダイレクトスタイルを使うことで、洗礼されたバックトラッキングを実装できます。