Documentation

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

The number Anne received in the world w

The number Bill received in the world w

An initial stream of possible worlds for problem 1

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.

Spelling out the unique condition, to demonstrate what it means

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

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.

Reverse application

A stream of naturals

A stream of integers starting with n

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.

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.