Dynamic Epistemic Logic: solving the puzzles from Hans van Ditmarsch's tutorial course on Dynamic Epistemic Logic, NASSLLI 2010, June 20, 2010. See also

Dynamic Epistemic Logic and Knowledge Puzzles H.P. van Ditmarsch, W. van der Hoek, and B.P. Kooi http://www.csc.liv.ac.uk/~wiebe/pubs/Documents/iccs.pdf

Epistemic Puzzles Hans van Ditmarsch http://www.cs.otago.ac.nz/staffpriv/hans/cosc462/logicpuzzlesB.pdf

We encode the statement of the problem as a filter on possible worlds. The possible worlds consistent with the statement of the problem are the solutions.

"Agent A does not know proposition phi" is interpreted

as the statement that for all worlds consistent with the propositions A currently knows, phi is true in some but false in the others.

- type P1World = (Int, Int)
- p1_anne :: P1World -> Int
- p1_bill :: P1World -> Int
- p1worlds :: MonadPlus m => m P1World
- prob1 :: [P1World]
- prob1a :: [P1World]
- prob1a' :: [[P1World]]
- type P2World = (Int, Int, Int)
- p2_anne :: P2World -> Int
- p2_anne_keys :: P2World -> [P2World]
- p2_bill :: P2World -> Int
- p2_bill_keys :: P2World -> [P2World]
- p2_cath :: P2World -> Int
- p2_cath_keys :: P2World -> [P2World]
- p2worlds :: MonadPlus m => m P2World
- prob2 :: [P2World]
- choose :: MonadPlus m => [a] -> m a
- nat :: MonadPlus m => m Int
- iota :: MonadPlus m => Int -> m Int
- nonunique :: Ord key => (w -> [key]) -> [w] -> [w]
- unique :: Ord key => (w -> [key]) -> (key -> Bool) -> [w] -> [w]

# Documentation

type P1World = (Int, Int)Source

Problem 1 Anne and Bill each privately receive a natural number. Their numbers are consecutive. The following truthful conversation takes place:

Anne: I don't know your number Bill: I don't know your number either Anne: I know your number. Bill: I know your number too.

If Anne has received the number 2, what was the number received by Bill? This puzzle is also known as `Conway paradox': it appears that Anne and Bill have truthfully made contradictory statements.

A possible world for a problem 1: numbers received by Anne and Bill

Encoding the statement of the problem: the conversation steps. The remaining possible world gives us the solution.

A variation of the problem: Assuming the numbers don't exceed 100, what are the numbers received by Anne and Bill? Again, the possible worlds consistent with the statement of the problem are the solutions.

type P2World = (Int, Int, Int)Source

Problem 2

Anne, Bill and Cath each have a positive natural number written on their foreheads. They can only see the foreheads of others. One of the numbers is the sum of the other two. All the previous is common knowledge. The following truthful conversation takes place:

Anne: I don't know my number. Bill: I don't know my number. Cath: I don't know my number. Anne: I now know my number, and it is 50.

What are the numbers of Bill and Cath? Math Horizons, November 2004. Problem 182.

A possible world for a problem 1: numbers received by Anne, Bill, and Cath

p2_anne_keys :: P2World -> [P2World]Source

If Anne sees the number x on Bill's forehead and the number y on Cath's forehead, what numbers could be on Anne's forehead? In other words, compute the set of possible worlds that are indistinguishable from the world w as far as Anne is concerned.

p2_bill_keys :: P2World -> [P2World]Source

Which worlds Bill can't distinguish

p2_cath_keys :: P2World -> [P2World]Source

Ditto for Cath

p2worlds :: MonadPlus m => m P2WorldSource

An initial stream of possible worlds for problem 2. The code is naive but hopefully obviously correct as it clearly corresponds to the statement of the problem.

Encoding the statement of the problem: the conversation steps. The remaining possible world gives us the solution.

nonunique :: Ord key => (w -> [key]) -> [w] -> [w]Source

Filter a set of possible worlds Given a proj function (yielding a set of keys for a world w), return a stream of worlds that are not unique with respect to their keys. That is, there are several worlds with the same key. Our state is a set of quarantined worlds. When we receive a world whose key we have not seen, we quarantine it. We release from the quarantine when we encounter the same key again. Our function is specialized to the List monad. In general, we need MonadMinus (see the LogicT paper), of which List is an instance.

unique :: Ord key => (w -> [key]) -> (key -> Bool) -> [w] -> [w]Source

Given a proj function (yielding a set of keys for a world w), return a stream of worlds that are unique with respect to their keys. That is, there is only one world for the key. We accept a termination criterion. We terminate the stream once we have received the key for which the criterion returns true. When we receive a world whose key we have not seen, we quarantine it. We release from the quarantine when the stream is terminated.