liboleg-2010.1.9.0: An evolving collection of Oleg Kiselyov's Haskell modules

Logic.DynEpistemology

Description

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.

Synopsis

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

The number Anne received in the world w

The number Bill received in the world w

p1worlds :: MonadPlus m => m P1WorldSource

An initial stream of possible worlds for problem 1

prob1 :: [P1World]Source

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

prob1a :: [P1World]Source

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.

prob1a' :: [[P1World]]Source

Spelling out the `unique` condition, to demonstrate what it means

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

The number on Anne's forehead in the world w

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.

The number on Bill's forehead in the world w

Which worlds Bill can't distinguish

The number on Cath's forehead in the world w

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.

prob2 :: [P2World]Source

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

choose :: MonadPlus m => [a] -> m aSource

Reverse application

nat :: MonadPlus m => m IntSource

A stream of naturals

iota :: MonadPlus m => Int -> m IntSource

A stream of integers starting with n

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.