人気ブログランキング | 話題のタグを見る

All About Monads 読解 23

More examples with monad transformers の続き

StateT with List

前回の例では複合モナドの内側のモナドはいずれも IO モナドだった。今回の例は StateT モナド・トランスフォーマーとリスト・モナドを組み合わせて、不定数の変数を保持する状態を扱うプログラムを記述する。

この強力なモナドのコンビネーションを使って、制約充足問題を解く(この例の場合は論理パズル)。この問題では複数の変数と、それらが満たすべき複数の述語が必要になる。この種の問題では、現在の変数の値が状態を決定し、リスト・モナドの非決定性を利用して、全ての変数の組み合わせをテストする事ができる。

注:

このセクションでは、原著の記述とは順番を入れ替えて解読をする。このプログラム例で解かれる「制約充足問題」の性質を先に知っておいた方が、理解が容易になるからだ。

そこで、まず、このプログラムが解こうとしている「Kalotan (カロタン族)のパズル」について考えてみる。このパズルは Google で検索するとたくさんヒットするので有名なパズルのようだ。それは、次のような問題だ。
Kalotan 族は奇妙な習慣を持った種族だ。彼らの男性は皆本当のことしか言わない。しかし、かれらの女性は、本当のことも嘘も言う事ができるが、2回続けて本当の事を言う事もないし、2回続けて嘘をつくこともできない。

さて、人類学者 Worf は Kalotan 族のある夫婦と話していた。この夫婦には Kibi という子供がいる。Worf が子供に「君は男の子かい?」と話しかけたところ子供が Kalotan 語で答えた。残念ながら Worf は Kalotan 語が分からなかったので英語の分かる両親にこの子が何と答えたのか訪ねた。するとそのうちの一人は「Kibi は男の子だと言ったのだ。」と答えた。また別の一人は「Kibi は女の子だ。彼女は嘘を答えたのだ。」と言った。

さて、Kibi は一体男の子だったのだろうか、女の子だったのだろうか

これは、Kalotan 族の男性が嘘をつかないという特徴を捕まえると、簡単に解く事ができる。

最初に「Kibi は男の子だと言ったのだ」と言ったのが、父親の方だったとしよう。すると、父親は本当のことしか言わないのだから、Kibi は男の子だと言ったという事になる。そうすると、Kibi が「男の子だよ」と言ったのは真実である。しかし、かれが男の子であれば本当の事しか言わないので、彼は男の子だということになるが、Kibi が女の子であれば、本当の事を言ったのかうそを言ったのかはわからないので、Kibi の性別については依然わからない。

かりに Kibi が男の子であったとすれば、「Kibi は女の子だ、彼女は嘘を言ったのだ。」という言明は2つとも嘘になる。なぜなら、Kibi は男の子であるし、本当の事を言ったからだ。しかしながら、Kibi の母親は2回続けて嘘をつくことができない。したがって、Kibi が男の子であるとすると矛盾が生じてしまう。

それでは、Kibi が女の子であったらどうなるだろうか。この場合も「Kibi は女の子だ、彼女は嘘を言ったのだ。」という言明の前者も後者も本当の事であるから、Kibi の母親はやはりこの言明をすることはできない。

結局、Kibi の父親が「彼は男の子だと言った。」と仮定するとどちらも矛盾が生じる。

今度は、「Kibi は女の子だ、彼女は嘘を言ったのだ。」と言ったのが彼女の父親だったとしよう。この場合、Kibi は女の子で、嘘を言ったのだから彼女は「ぼくは、男の子だよ」といったことになる。この場合、Kibi の母親は「 Kibi は男の子だと言った。」という本当の言明をする事ができるので矛盾は生じない。

このパズルが複雑になったのは、事実の真偽と同時に、言明の真偽を問うているからだ。トリッキーでなかなか面白いパズルだが、解くよりは作る方が難しかっただろう。

しかし、これをプログラムに解かせるには一体どうすればいいのだろうか。

注終わり

example24.hs

example24.hs はコピペで動く。ただし、import の部分を次のように変更する必要がある。

import System.IO
import Control.Monad
import System.Environment
import Data.Maybe
import Control.Monad.State

実行例は次のようになる。子どもと両親の性別が特定されている。

Prelude> :e example24.hs
Prelude> :l example24.hs
[1 of 1] Compiling Main ( example24.hs, interpreted )
Ok, modules loaded: Main.
*Main> :main
Loading package transformers-0.3.0.0 ... linking ... done.
Loading package mtl-2.1.1 ... linking ... done.
Just [("child","female"),("parent2","male"),("parent1","female")]

原著の example24.hs の解説では、論理パスルを解くためにまず簡単な述語論理を記述する言語を作っている。

この言語の単語には Var 型と Value 型が定義されているが、いずれも String 型の別名だ。Var は「子供は女の子です。」という言明の主語にあたり、Value は女の子という補語を表している。

type Var = String
type Value = String

また、この言語の基本的な文は Is "child" "male" のように Predicate 型のデータだ。Predicate 型のデータは var (変数) と value (値) という2つのフィールドを持っている。Predicate 型のデータには次のような種類がある。

Is Var Value -- var has specific value
Equal Var Var -- vars have same (unspecified) value
And Predicate Predicate -- both are true
Or Predicate Predicate -- at least one is true
Not Predicate -- it is not true

上の Predicate 型のデータは ghci で試して見ることができる。

*Main> Is "child" "female"
Is "child" "female"

述語論理の言語を定義するプログラムにはこの他に Var と Value のペアのリストである Variables 型が定義されている。

type Variables = [(Var,Value)]

この言語には上の標準的な述語の他に、isNot、implies、orElse があり、それぞれ定義は次のようになっている。それぞれの意味は否定術後、含意、排他的論理和だ。

-- test for a variable NOT equaling a value
isNot :: Var -> Value -> Predicate
isNot var value = Not (Is var value)

-- if a is true, then b must also be true
implies :: Predicate -> Predicate -> Predicate
implies a b = Not (a `And` (Not b))

-- exclusive or
orElse :: Predicate -> Predicate -> Predicate
orElse a b = (a `And` (Not b)) `Or` ((Not a) `And` b)

最後に、これらの術後論理の真理値をチェックする check というプログラムが定義されている。check
の型は

check :: Predicate -> Variables -> Maybe Bool

なので、Predicate と Variables の (Var, Value) のペアを見比べて、Predicate が 真であれば Just True を、偽であれば Just False を返す。

-- Check a predicate with the given variable bindings.
-- An unbound variable causes a Nothing return value.
check :: Predicate -> Variables -> Maybe Bool
check (Is var value) vars = do
  val <- lookup var vars
  return (val == value)
check (Equal v1 v2) vars = do
  val1 <- lookup v1 vars
  val2 <- lookup v2 vars
  return (val1 == val2)
check (And p1 p2) vars = liftM2 (&&) (check p1 vars) (check p2 vars)
check (Or p1 p2) vars = liftM2 (||) (check p1 vars) (check p2 vars)
check (Not p) vars = liftM (not) (check p vars)

注:
liftM, liftM2 関数は普通の関数をモナド値を引数とする関数に変換する関数だ。たとえば (*2) は 引数を2倍にして返す関数だが、liftM (*2) とするとモナド値 m 3 を2倍にして m 6 を返す。

Prelude> import Control.Monad
Prelude Control.Monad> (*2) 3
6
Prelude Control.Monad> liftM (*2) (Just 3)
Just 6

liftM2 は liftM とおなじ機能だが、変数が2つの場合に使う。

Prelude Control.Monad> liftM2 (+) (Just 2) (Just 3)
Just 5

注終わり

check 関数を ghci でテストしてみた。

*Main> check (Is "child" "female") [("father", "male"), ("mother", "female"),("child", "female")]
Just True
*Main> check (Is "child" "male") [("father", "male"), ("mother", "female"),("child", "female")]
Just False

次にやることは、この述語論理言語を利用して制約充足問題を解くアルゴリズムを記述する事だ。ここで、複合モナドを定義して使うのだ。まず、論理パズルの問題のデータ型を定義する。ProblemState 型は、そのフィールドは変数リストと制約条件からなっている。

-- this is the type of our logic problem
data ProblemState = PS {vars::Variables, constraints::[Predicate]}

不定数の変数からなる状態を使うためにするために複合モナドを定義する。StateT モナド・トランスフォーマーとリスト・モナドとの複合モナドだ。NDS (non-deterministic computations with state) として定義する。

-- this is our monad type for non-determinstic computations with state
type NDS a = StateT ProblemState [] a

getVar 関数は Var 型の値を引数としてとり、状態のデータから同名の Var 型と Value 型のペアから対応する Value をとりだす。戻り値が NDS モナドなので、NDS モナド型の関数だ。

-- lookup a variable
getVar :: Var -> NDS (Maybe Value)
getVar v = do
  vs <- gets vars
  return $ lookup v vs

setVar 関数は Var と Value の2つを引数としてとり、状態のリストに追加する。この関数も NDS 型なので、NDS モナド型の関数だ。

-- set a variable
setVar :: Var -> Value -> NDS ()
setVar v x = do
  st <- get
  vs' <- return $ filter ((v/=).fst) (vars st)
  put $ st {vars=(v,x):vs'}

isConsitent 関数は、状態の vars フィールドの (Var, Value) のペアのリストが、constraints フィールドの述語のリストを満たすかどうかを検査し、満たせば NDS True を返す。isConsistent の引数は Bool 値で部分的なマッチでも True が返るかどうかの可否を指定する。引数が False の場合は全ての constraints の要件が成立する事が要求される。プログラムの constraints、vars はそれぞれ PS 型のデータのフィールドのアクセサだ。isConsistent 関数も戻り値は NDS 型なので、NDS モナド型の関数だ。

-- Check if the variable assignments satisfy all of the predicates.
-- The partial argument determines the value used when a predicate returns
-- Nothing because some variable it uses is not set. Setting this to True
-- allows us to accept partial solutions, then we can use a value of
-- False at the end to signify that all solutions should be complete.
isConsistent :: Bool -> NDS Bool
isConsistent partial = do
  cs <- gets constraints
  vs <- gets vars
  let results = map (\p->check p vs) cs
 nbsp;return $ and (map (maybe partial id) results)

getFinalVars 関数は、状態の vars フィールドの (Var, Value) リストが constraints フィールドの要件を全て満たしたときに vars フィールドのリストを戻す。

-- Return only the variable bindings that are complete consistent solutions.
getFinalVars :: NDS Variables
getFinalVars = do
  c <- isConsistent False
  guard c
&bsp; gets vars

getSolution 関数は最初の解答を取り出す関数だ。第1引数は NDS モナドの初期値、第2引数は PS 型のデータで戻り値は Maybe 型の解答のデータだ。

-- Get the first solution to the problem, by evaluating the solver computation with
-- an initial problem state and then returning the first solution in the result list,
-- or Nothing if there was no solution.
getSolution :: NDS a -> ProblemState -> Maybe a
getSolution c i = listToMaybe (evalStateT c i)

getAllSolution 関数は全ての解答を求める関数だ。

-- Get a list of all possible solutions to the problem by evaluating the solver
-- computation with an initial problem state.
getAllSolutions :: NDS a -> ProblemState -> [a]
getAllSolutions c i = evalStateT c i

次の3つの関数 said、saidBoth、lied は「Kalotan のパズル」を解くための複合命題だ。たとえば said v p は 「v が male であれば p は正しい」という意味だ。

-- if a male says something, it must be true
said :: Var -> Predicate -> Predicate
said v p = (v `Is` "male") `implies` p

また、saidBoth v p1 p2 は「v が male あれば p1 と p2 は正しい、かつ、v が female であれば、p1 か p2 のどちらかが正しい」という意味だ。

-- if a male says two things, they must be true
-- if a female says two things, one must be true and one must be false
saidBoth :: Var -> Predicate -> Predicate -> Predicate
saidBoth v p1 p2 =
  And ((v `Is` "male") `implies` (p1 `And` p2))
      ((v `Is` "female") `implies` (p1 `orElse` p2))

さらに、lied v p は 「v が p と言ったが p ではなかった、または、v が p ではないと言ったが p であったかどちらか一方が正しい」という意味になる。

-- lying is saying something is true when it isn't or saying something isn't true when it is
lied :: Var -> Predicate -> Predicate
lied v p = ((v `said` p) `And` (Not p)) `orElse` ((v `said` (Not p)) `And` p)

tryAllValues 関数は、var が mail のときと var が female の時の環境の条件について論理的整合性をチェックする (isConsistent)。

-- Test consistency over all allowed settings of the variable.
tryAllValues :: Var -> NDS ()
tryAllValues var = do
  (setVar var "male") `mplus` (setVar var "female")
  c <- isConsistent True
  guard c

最後に残っているのは、パズルの問題をこの述語論議言語で記述し、その全ての述語を満たす解答を得ることだ。

-- Define the problem, try all of the variable assignments and print a solution.
main :: IO ()
main = do
  let variables = []
      constraints = [ Not (Equal "parent1" "parent2"),
        "parent1" `said` ("child" `said` ("child" `Is` "male")),
        saidBoth "parent2" ("child" `Is` "female")
          ("child" `lied` ("child" `Is` "male")) ]
      problem = PS variables constraints
  print $ (`getSolution` problem) $ do
    tryAllValues "parent1"
    tryAllValues "parent2"
    tryAllValues "child"
    getFinalVars

おのおのの tryAllValues では "parent1" などの主語に "male" という補語と "female" という補語が割り当てられ、それぞれがパズルの全ての命題を満たすかどうかを調べる。条件に合わなかった変数は guard 関数でブロックされる。最後に呼ばれる getFinalVars 関数は再度 guard 関数によって条件に合わなかった変数を除外し、最終的な解答を返す。

前へ 目次 次へ
by tnomura9 | 2013-08-11 10:47 | Haskell | Comments(0)
<< All About Mona... All About Monad... >>