{- |
This module implements an alternative representation of the Muddy Children, as proposed in:

- Nina Gierasimczuk, Jakub Szymanik (2011):
  /A note on a generalization of the Muddy Children puzzle/.
  <https://doi.org/10.1145/2000378.2000409>

The main idea is to not distinguish individual children who are in the same state which also means that their observations are the same.
Sections of Pascal's triangle can then be used to solve the Muddy Children puzzle in a Kripke model with less worlds than needed in the classical analysis, namely \(2n+1\) instead of \(2^n\) for \(n\) children.

-}
module SMCDEL.Other.MCTRIANGLE where

-- |A child can be muddy or clean.
data Kind = Muddy | Clean

-- | States are pairs of integers indicating how many children are (clean,muddy).
type State = (Int,Int)

-- | A muddy children model consists of three things: A list of observational states, a list of factual states and a current state.
data McModel = McM [State] [State] State deriving Int -> McModel -> ShowS
[McModel] -> ShowS
McModel -> String
(Int -> McModel -> ShowS)
-> (McModel -> String) -> ([McModel] -> ShowS) -> Show McModel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> McModel -> ShowS
showsPrec :: Int -> McModel -> ShowS
$cshow :: McModel -> String
show :: McModel -> String
$cshowList :: [McModel] -> ShowS
showList :: [McModel] -> ShowS
Show

-- | Create a muddy children model
mcModel :: State -> McModel
mcModel :: State -> McModel
mcModel cur :: State
cur@(Int
c,Int
m) = [State] -> [State] -> State -> McModel
McM [State]
ostates [State]
fstates State
cur where
  total :: Int
total   = Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m
  ostates :: [State]
ostates = [ ((Int
totalInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m',Int
m') | Int
m'<-[Int
0..(Int
totalInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ] -- observational states
  fstates :: [State]
fstates = [ (Int
totalInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m',    Int
m') | Int
m'<-[Int
0..Int
total    ] ] -- factual states

-- | Get the available successors of a state in a model
posFrom :: McModel -> State -> [State]
posFrom :: McModel -> State -> [State]
posFrom (McM [State]
_ [State]
fstates State
_) (Int
oc,Int
om) = (State -> Bool) -> [State] -> [State]
forall a. (a -> Bool) -> [a] -> [a]
filter (State -> [State] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [State]
fstates) [ (Int
ocInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
om), (Int
oc,Int
omInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ]

-- | Get the observational state of an agent
obsFor :: McModel -> Kind -> State
obsFor :: McModel -> Kind -> State
obsFor (McM [State]
_ [State]
_ (Int
curc,Int
curm)) Kind
Clean = (Int
curcInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
curm)
obsFor (McM [State]
_ [State]
_ (Int
curc,Int
curm)) Kind
Muddy = (Int
curc,Int
curmInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

-- | Get all states deemed possible by an agent
posFor :: McModel -> Kind -> [State]
posFor :: McModel -> Kind -> [State]
posFor McModel
m Kind
status = McModel -> State -> [State]
posFrom McModel
m (State -> [State]) -> State -> [State]
forall a b. (a -> b) -> a -> b
$ McModel -> Kind -> State
obsFor McModel
m Kind
status

{- |
Note that instead of naming or enumerating agents we only distinguish two
Kind`s, the muddy and non-muddy ones, represented by Haskells constants
Muddy` and Clean` which allow pattern matching.
-}


-- | Quantifiers on the number triangle, e.g. `some`.
type Quantifier = State -> Bool

-- | The "some" quantifier.
some :: Quantifier
some :: State -> Bool
some (Int
_,Int
b) = Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0

-- | The paper does not give a formal language definition, so here is our suggestion:
-- \[ \phi ::= \lnot \phi \mid  \bigwedge \Phi  \mid  Q  \mid  K_b \mid \overline{K}_b \]
-- where $\Phi$ ranges over finite sets of formulas, $b$ over $\{0,1\}$ and $Q$
-- over generalized quantifiers.
-- Note that when there are no agents of kind ``b`, the formulas
-- `KnowSelf b` and `NotKnowSelf b` are both true.
-- Hence `Neg (KnowSelf b)` and `NotKnowSelf b` are not the same!
data McFormula = Neg McFormula    -- negations
               | Conj [McFormula] -- conjunctions
               | Qf Quantifier    -- quantifiers
               | KnowSelf Kind    -- all b agents DO    know their status
               | NotKnowSelf Kind -- all b agents DON'T know their status

-- | Formula for ``Nobody knows their own state.''
nobodyknows :: McFormula
nobodyknows :: McFormula
nobodyknows   = [McFormula] -> McFormula
Conj [ Kind -> McFormula
NotKnowSelf Kind
Clean, Kind -> McFormula
NotKnowSelf Kind
Muddy ]

-- | Formula for ``Everybody knows their own state.''
everyoneKnows :: McFormula
everyoneKnows :: McFormula
everyoneKnows = [McFormula] -> McFormula
Conj [    Kind -> McFormula
KnowSelf Kind
Clean,    Kind -> McFormula
KnowSelf Kind
Muddy ]

{- |
Note that in contrast to the standard DEL language the formulas are
independent of how many children there are. This is due to our identification
of agents with the same state and observations.
-}

-- | The semantics for the minimal language.
-- The four nullary knowledge operators can be thought of as
--   ``All agents who are (not) muddy do (not) know their own state.''
-- Hence they are vacuously true whenever there are no such agents.
-- If there are, the agents do know their state iff they consider only one
-- possibility (i.e. their observational state has only one successor).
eval :: McModel -> McFormula -> Bool
eval :: McModel -> McFormula -> Bool
eval McModel
m (Neg McFormula
f)          = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ McModel -> McFormula -> Bool
eval McModel
m McFormula
f
eval McModel
m (Conj [McFormula]
fs)        = (McFormula -> Bool) -> [McFormula] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (McModel -> McFormula -> Bool
eval McModel
m) [McFormula]
fs
eval (McM [State]
_ [State]
_ State
s) (Qf State -> Bool
q) = State -> Bool
q State
s
eval m :: McModel
m@(McM [State]
_ [State]
_ (Int
_,Int
curm)) (KnowSelf    Kind
Muddy) = Int
curmInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 Bool -> Bool -> Bool
|| [State] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (McModel -> Kind -> [State]
posFor McModel
m Kind
Muddy) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
eval m :: McModel
m@(McM [State]
_ [State]
_ (Int
curc,Int
_)) (KnowSelf    Kind
Clean) = Int
curcInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 Bool -> Bool -> Bool
|| [State] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (McModel -> Kind -> [State]
posFor McModel
m Kind
Clean) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
eval m :: McModel
m@(McM [State]
_ [State]
_ (Int
_,Int
curm)) (NotKnowSelf Kind
Muddy) = Int
curmInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 Bool -> Bool -> Bool
|| [State] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (McModel -> Kind -> [State]
posFor McModel
m Kind
Muddy) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
eval m :: McModel
m@(McM [State]
_ [State]
_ (Int
curc,Int
_)) (NotKnowSelf Kind
Clean) = Int
curcInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 Bool -> Bool -> Bool
|| [State] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (McModel -> Kind -> [State]
posFor McModel
m Kind
Clean) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2

-- | Update models with a formula:
mcUpdate :: McModel -> McFormula -> McModel
mcUpdate :: McModel -> McFormula -> McModel
mcUpdate (McM [State]
ostates [State]
fstates State
cur) McFormula
f =
  [State] -> [State] -> State -> McModel
McM [State]
ostates' [State]
fstates' State
cur where
    fstates' :: [State]
fstates' = (State -> Bool) -> [State] -> [State]
forall a. (a -> Bool) -> [a] -> [a]
filter (\State
s -> McModel -> McFormula -> Bool
eval ([State] -> [State] -> State -> McModel
McM [State]
ostates [State]
fstates State
s) McFormula
f) [State]
fstates
    ostates' :: [State]
ostates' = (State -> Bool) -> [State] -> [State]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (State -> Bool) -> State -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [State] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([State] -> Bool) -> (State -> [State]) -> State -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. McModel -> State -> [State]
posFrom ([State] -> [State] -> State -> McModel
McM [] [State]
fstates' State
cur)) [State]
ostates

-- | Compute the n-th step of the puzzle, given an actual state.
step :: State -> Int -> McModel
step :: State -> Int -> McModel
step State
s Int
0 = McModel -> McFormula -> McModel
mcUpdate (State -> McModel
mcModel State
s) ((State -> Bool) -> McFormula
Qf State -> Bool
some)
step State
s Int
n = McModel -> McFormula -> McModel
mcUpdate (State -> Int -> McModel
step State
s (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) McFormula
nobodyknows

-- | Show all steps of the puzzle, given an actual state.
showme :: State -> IO ()
showme :: State -> IO ()
showme s :: State
s@(Int
_,Int
m) = (Int -> IO ()) -> [Int] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Int
n -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ McModel -> String
forall a. Show a => a -> String
show (State -> Int -> McModel
step State
s Int
n)) [Int
0..(Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]

{- |
==== __Examples__

>>> showme (1,2)
m0: McM [(2,0),(1,1),(0,2)] [(2,1),(1,2),(0,3)] (1,2)
m1: McM [(1,1),(0,2)] [(1,2),(0,3)] (1,2)
-}