module CAIA where
import Data.List
-- Section 13.7
data Agent = A | B | C | D | E deriving (Eq,Ord,Enum)
-- Sample agents
a,alice, b,bob, c,carol, d,dave, e,ernie :: Agent
a = A; alice = A
b = B; bob = B
c = C; carol = C
d = D; dave = D
e = E; ernie = E
instance Show Agent where
show A = "a"; show B = "b";
show C = "c"; show D = "d";
show E = "e"
-- As before propositions are letter with subscript
data Prop = P Int | Q Int | R Int deriving (Eq,Ord)
instance Show Prop where
show (P 0) = "p"; show (P i) = "p" ++ show i
show (Q 0) = "q"; show (Q i) = "q" ++ show i
show (R 0) = "r"; show (R i) = "r" ++ show i
-- model of epistemic logic. Note use of record syntax in Haskell
data EpistM state = Mo {
dom :: [state], -- set of worlds
agents :: [Agent], -- set of agents
valuation :: [(state,[Prop])], -- formulas true for each world
rels :: [(Agent,state,state)], -- accessibility for each agent
actual :: [state] -- real world is one of these based on current knowledge
} deriving (Eq,Show)
-- Can access agents by exampleModel.agents
exampleModel :: EpistM Integer
exampleModel =
Mo [0..3]
[a..c]
[(0,[]),(1,[P 0]),(2,[Q 0]),(3,[P 0, Q 0])]
([ (a,x,x) | x <- [0..3] ] ++
[ (b,x,x) | x <- [0..3] ] ++
[ (c,x,y) | x <- [0..3], y <- [0..3] ])
[1]
type Rel a = [(a,a)]
-- is xs a subset of ys
containedIn :: Eq a => [a] -> [a] -> Bool
containedIn xs ys = all (\ x -> elem x ys) xs
-- reverse a relation
cnv :: Rel a -> Rel a
cnv r = [ (y,x) | (x,y) <- r ]
infixr 5 @@
-- r@@s composes the relations r and s (& throws away dups)
(@@) :: Eq a => Rel a -> Rel a -> Rel a
r @@ s = nub [ (x,z) | (x,y) <- r, (w,z) <- s, y == w ]
-- checks if r is reflexive relation on xs
reflR :: Eq a => [a] -> Rel a -> Bool
reflR xs r = [(x,x) | x <- xs] `containedIn` r
-- checks if r is symmetric relation on xs
symmR :: Eq a => Rel a -> Bool
symmR r = cnv r `containedIn` r
-- checks if r is transitive relation on xs
transR :: Eq a => Rel a -> Bool
transR r = (r @@ r) `containedIn` r
-- checks if r is equivalence relation on xs
isS5 :: Eq a => [a] -> Rel a -> Bool
isS5 xs r = reflR xs r && transR r && symmR r
-- extracts accessibility relation for agent a from model
rel :: Agent -> EpistM a -> Rel a
rel a model = [ (x,y) | (b,x,y) <- rels model, a == b ]
-- Uses equivalence relation a to form partition.
-- returns list of all equivalence classes for r
rel2partition :: Ord a => [a] -> Rel a -> [[a]]
rel2partition [] r = []
rel2partition (x:xs) r = xclass : rel2partition (xs\\xclass) r
where xclass = x : [ y | y <- xs, (x,y) `elem` r ]
-- displays model whose accessibility relations are equivalence classes
-- by displaying accessibility for each agent as a partition
showS5 :: (Ord a,Show a) => EpistM a -> [String]
showS5 m = show (dom m)
: show (valuation m)
: map show [ (a,(rel2partition (dom m)) (rel a m))
| a <- (agents m)]
++ [show (actual m)]
-- even nicer display of model with line breaks
displayS5 :: (Ord a,Show a) => EpistM a -> IO()
displayS5 = putStrLn . unlines . showS5
-- create new model in which there is a world for every assignment of
-- truth values for the propositions and each agent has each of them
-- accessible. Thus each agent is blissfully ignorant of the real state
-- of the world
initM :: [Agent] -> [Prop] -> EpistM Integer
initM ags props = (Mo worlds ags val accs points)
where worlds = [0..(2^k-1)]
k = length props
val = zip worlds (sortL (powerList props))
accs = [ (ag,st1,st2) | ag <- ags,
st1 <- worlds,
st2 <- worlds ]
points = worlds
-- generate list of all sublists of xs
powerList :: [a] -> [[a]]
powerList [] = [[]]
powerList (x:xs) = (powerList xs) ++ (map (x:) (powerList xs))
-- lexicographic sort of list of lists
sortL :: Ord a => [[a]] -> [[a]]
sortL = sortBy (\ xs ys -> if length xs < length ys
then LT
else if length xs > length ys
then GT
else compare xs ys)
-- compute least fixed point of f
lfp :: Eq a => (a -> a) -> a -> a
lfp f x | x == f x = x
| otherwise = lfp f (f x)
-- compute reflexive transitive closure of r over xs
rtc :: Ord a => [a] -> Rel a -> Rel a
rtc xs r = lfp (\ s -> (sort.nub) (s ++ (r@@s))) i
where i = [ (x,x) | x <- xs ]
-- formulas phi
data Form = Top
| Prop Prop
| Neg Form
| Conj [Form]
| Disj [Form]
| K EE Form -- [alpha]P
| PA Form Form -- [!P]Q
| PC [(Prop,Form)] Form -- change
deriving (Eq,Ord)
-- accessibility relations alpha
data EE = Agent Agent
| Test Form -- [?P]
| Cmp EE EE -- a;b
| Sum [EE] -- a U b
| Star EE -- a*
deriving (Eq,Ord)
p = Prop (P 0) -- formula P0
q = Prop (Q 0) -- formula Q0
instance Show Form where
show Top = "T"
show (Prop p) = show p
show (Neg f) = '-':(show f)
show (Conj fs) = '&': show fs
show (Disj fs) = 'v': show fs
show (K e f) = '[':show e ++"]"++show f
show (PA f1 f2) = '[':'!': show f1 ++"]"++show f2
show (PC s f) = show s ++ show f
instance Show EE where
show (Agent a) = show a
show (Test f) = '?': show f
show (Cmp e1 e2) = show e1 ++ ";" ++ show e2
show (Sum es) = 'U': show es
show (Star e) = '(': show e ++ ")*"
-- it is common knowledge among ags that f is true
ck :: [Agent] -> Form -> Form
ck ags f = K (Star (Sum [Agent a | a <- ags])) f
-- look up value of prop in world
apply :: Eq a => [(a,b)] -> a -> b
apply [] _ = error "argument not in list"
apply ((x,z):xs) y | x == y = z
| otherwise = apply xs y
rightS :: Ord a => a -> Rel a -> [a]
rightS x r = (sort.nub) [ z | (y,z) <- r, x == y ]
-- isTrueAt m w phi -- tells whether phi true in world w of model m
isTrueAt :: Ord state => EpistM state -> state -> Form -> Bool
isTrueAt m w Top = True
isTrueAt m w (Prop p) = p `elem` (concat
[ ps | (w',ps) <- valuation m, w'==w])
isTrueAt m w (Neg f) = not (isTrueAt m w f)
isTrueAt m w (Conj fs) = and (map (isTrueAt m w) fs)
isTrueAt m w (Disj fs) = or (map (isTrueAt m w) fs)
-- checks if f true in all worlds accessible from e
isTrueAt m w (K e f) = and (map (flip (isTrueAt m) f)
(rightS w (evalEE m e)))
-- checks if f2 is true in universe restricted to worlds where
-- f1 is known to be true
isTrueAt m w (PA f1 f2) = not (isTrueAt m w f1)
|| isTrueAt m' w f2
where m' = upd_pa m f1
isTrueAt m w (PC s f) = isTrueAt (upd_pc m s) w f
-- evaluate epistemic expressions to get worlds
evalEE :: Ord state => EpistM state -> EE -> Rel state
evalEE m (Agent a) = rel a m -- accessibility relation for agent a
evalEE m (Test f) = [(w,w) | w <- dom m, isTrueAt m w f] -- ?f
evalEE m (Cmp e1 e2) = (evalEE m e1) @@ (evalEE m e2) -- e1;e2
evalEE m (Sum (es)) = (sort.nub) (concat (map (evalEE m) es)) -- e1 U e2
evalEE m (Star e) = rtc (dom m) (evalEE m e) -- e*
test1 = isTrueAt (initM [a..c] [P 0]) 0
(ck [a..c] (Neg (K (Agent a) p)))
-- is f true in all actual worlds in m
isTrue :: Ord state => EpistM state -> Form -> Bool
isTrue m f = and [ isTrueAt m s f | s <- actual m ]
test2 = isTrue (initM [a..c] [P 0])
(ck [a..c] (Neg (K (Agent a) p)))
-- restrict m to worlds in which f is true
upd_pa :: Ord state => EpistM state -> Form -> EpistM state
upd_pa m@(Mo states agents val rels actual) f =
(Mo states' agents val' rels' actual')
where
states' = [ s | s <- states,
isTrueAt m s f ]
val' = [ (s,p) | (s,p) <- val,
s `elem` states' ]
rels' = [ (a,x,y) | (a,x,y) <- rels,
x `elem` states',
y `elem` states' ]
actual' = [ s | s <- actual,
s `elem` states' ]
type Subst = [(Prop,Form)]
upd_pc :: Ord state => EpistM state -> Subst -> EpistM state
upd_pc m@(Mo worlds agents val acc points) subst =
(Mo worlds agents val' acc points)
where
val' = [ (w,[p | p <- ps, isTrueAt m w (liftS subst p)])
| w <- worlds ]
ps = (sort.nub) (concat (map snd val))
liftS :: Subst -> Prop -> Form
liftS [] p = Prop p
liftS ((x,z):xs) y | x == y = z
| otherwise = liftS xs y
m0 = initM [a..c] [P 0,Q 0]
-- renumbers states so no gaps: [0,1,...,n]
convert :: Eq state => EpistM state -> EpistM Integer
convert (Mo states agents val rels actual) =
Mo states' agents val' rels' actual'
where
states' = map f states
val' = map (\ (x,y) -> (f x,y)) val
rels' = map (\ (x,y,z) -> (x,f y,f z)) rels
actual' = map f actual
f = apply (zip states [0..])
-- get generated submodel containing only those states accessible from points
gsm :: Ord state => EpistM state -> EpistM state
gsm (Mo states ags val rel points) =
Mo states' ags val' rel' points
where
states' = closure rel ags points
val' = [(s,ps) | (s,ps) <- val,
s `elem` states' ]
rel' = [(ag,s,s') | (ag,s,s') <- rel,
s `elem` states',
s' `elem` states' ]
-- finds accessible states (helper for gsm)
closure :: Ord state => [(Agent,state,state)] ->
[Agent] -> [state] -> [state]
closure rel agents xs = lfp f xs where
f = \ ys -> (nub.sort) (ys ++ (expand rel agents ys))
-- add new relations and agents (helper for closure)
expand :: Ord state => [(Agent,state,state)] ->
[Agent] -> [state] -> [state]
expand rel agents ys = (nub.sort.concat)
[ alternatives rel ag state | ag <- agents,
state <- ys ]
-- returns set of accessible states for agent (helper for expand)
alternatives :: Eq state => [(Agent,state,state)] ->
Agent -> state -> [state]
alternatives rel ag current = [ s' | (a,s,s') <- rel,
a == ag, s == current ]
-- Muddy children example. pi says child i's face is muddy
p1, p2, p3, p4 :: Form
p1 = Prop (P 1); p2 = Prop (P 2)
p3 = Prop (P 3); p4 = Prop (P 4)
-- compute accessible states for each child. They don't know their own state.
computeAcc :: Agent -> [Integer] -> [Prop] -> [(Integer,[Prop])]
-> [(Agent,Integer,Integer)]
computeAcc ag states props val =
[ (ag,x,y) | x <- states, y <- states,
apply val x \\ props == apply val y \\ props ]
initMuddy :: EpistM Integer
initMuddy = Mo states
[a..d]
valuation
(computeAcc a states [P 1] valuation ++
computeAcc b states [P 2] valuation ++
computeAcc c states [P 3] valuation ++
computeAcc d states [P 4] valuation)
[7]
where states = [0..15]
valuation = zip states (powerList [P 1,P 2,P 3,P 4])
m1 = convert (upd_pa initMuddy (Disj [p1,p2,p3,p4]))
aK = Disj [K (Agent a) p1, K (Agent a) (Neg p1)]
bK = Disj [K (Agent b) p2, K (Agent b) (Neg p2)]
cK = Disj [K (Agent c) p3, K (Agent c) (Neg p3)]
dK = Disj [K (Agent d) p4, K (Agent d) (Neg p4)]
m2 = convert (upd_pa m1 (Conj [Neg aK,Neg bK,Neg cK,Neg dK]))
m3 = convert (upd_pa m2 (Conj [Neg aK,Neg bK,Neg cK,Neg dK]))
m4 = convert (upd_pa m3 (Conj [Neg aK, bK, cK, dK]))