LogicT

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

Abstract

任意のモナドでバックトラッキングを可能にするモナド変換子を設計、実装します。

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

公平な選言: interleave
公平な連言: >>-
条件分岐: ifte
枝刈り: once

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

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

成功と失敗の継続を使ったもの
限定継続を使ったもの

1. Introduction

モナドを使ったプログラミングの利点は副作用や計算の観念を一般化して、非決定性やバックトラッキングのような評価モードをサポートします。

MonadPlus 型クラスには多くの実践的な応用があります。

非決定的な計算
トランザクション
パターンコンビネータ
エラーハンドリング

Hinze 氏のバックトラッキングモナド変換子は非決定的選択と Prolog-like なカットをサポートします。

これを含めた既存のバックトラッキングモナド変換子には以下の3つの欠点があります。

不公平さ
否定と枝刈りの混同
非決定性計算の最終的な結果を得る機能が限定的であること

1つ目の欠点は、ほとんどの MonadPlus で実装される単純な深さ優先探索が公平でないことです。

最初の選択肢が無限の解を提供するとき、2番目の選択肢は決して試みられないので、検索は不完全になります。

この問題はモナド変換子に公平な選言と連言を実装することで解決します。

2つ目の欠点は、Prolog のカットを採用していることです。これは、否定と枝刈りを混同させるものです。

このライブラリでは否定と枝刈りを独立させることで、論理プログラミングの表現力をより豊かにします。

3つ目の欠点は、無数の答えを返す可能性がある計算の実行と対話のインターフェースが貧弱であることです。

一般的な解決策は、必要に応じて消費または処理できるようなストリームを提供することです。しかし、モナド変換子の場合、この解決法はベースのモナドが正格でない場合のみ有効です。

別の解決方法として、リクエストに最大回答数を明示する方法があります。

このライブラリではこのインターフェースを一様に実装する方法を示します。

まとめると、公平な選言、公平な連言、soft-cut、once、そして表現力のあるインターフェースをもつバックトラッキングモナド変換子を実装します。

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

CPSに基づく実装は成功と失敗の継続を使います。これは2つの点で効率的です。

継続はパターンマッチが行われずそれらがただ呼び出されるだけ
direct-style の実装を CPS 変換した結果

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

これら2つの実装では msplit と呼ばれる単一の操作を要求することで、公平な選言と連言、否定、枝刈り、表現力のあるインターフェースを実現しています。

msplit は解をひとつ探すような操作です。

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

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

msplit は最初の解を計算し、残りの計算を中断します。

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は失敗を表現し、t2とt3は同一で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` t3はt3を決して考慮しません。

しかし、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と>>=のアナロジーです。

非決定性計算はmzeroかreturn 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は論理条件分岐演算です。

計算tを実行します
一つでも結果があれば全体はt >>= thと等価です
さもなければ全体の計算は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))

ifteとonceで”失敗による否定”が実装できます。

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と>>-とifteとonceはmsplitで実装可能です。

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

これは基底のモナドmをt 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 tmはtmと同じ型を持ち、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 mはMonadかつ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を分割します。

失敗したらlift (return Nothing)を返します
成功したら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

promptPはデリミタを作成します
abortPは実行を中断します
shiftPは継続を保存します

PromptとCCの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)))

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

プロンプトを作りスタックにプッシュします
コンテキストdo{ }をスタックにプッシュします
shiftPはpまでの継続を保存します
継続に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で決定的な結果を区別します。

決定的な結果はHOneを付けます
失敗はHZeroにより表現されます
選択はHChoice a rにより表現されます

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

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

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

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

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はより複雑です。

デリミタまでの継続skを保存します
選択肢m1は継続で実行されます
選択肢m2は一時停止されます
compose_treesはTreeを構築します
- 最初の結果と停止状態を結合します

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))

mが決定的に実行されるならHOne aを得ます
mが失敗するならHZeroを得ます

次の例は計算mがmplus 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は二番目の選択肢に対応する計算です。

f1valがHOne aならHChoice a f2compを結果とします
f1valがHChoice a r'ならr'とf2compを合成します

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

例えばf1valがHZeroであるとf2compを実行しない
f2compにIncompleteを付けて返す
- f2compを実行する
- 他の選択肢を試す

(odds >> mzero) `mplus` m

で発散を回避できます。

SR rにmsplitを実装します。

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を実装します。

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

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

計算mをTree 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

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

公平な連言と選言
論理的な条件分岐と枝刈り
任意個の解の選択

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

２継続のCPS
限定継続ライブラリを元にしたダイレクトスタイル

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

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

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