Implementation in DEMO
To generate the worlds and to check the model, an implementation in DEMO was used. The following lists the entire program. We'll go trough this step by step, but you can download the code here.module TNP
where
import DEMO
--Uses DEMO, Dynamic Epistemic MOdelling Tools, developed by Jan van Eijck
DEMO[2] is a toolkit, developed by Prof. Dr. D.J.N. van Eijck and written in Haskell, to check dynamic epistemic models. It therefore is useful when checking the models for the three number problem and the Sum & Product problem.
One useful, if not important, feature of DEMO is its ability to create output that can be interpreted by dot from the Graphviz toolkit which can generate graphs in numerous ways.
--This program implements the three-number-problem in DEMO
--There are three agents (A, B and C) who are assigned three numbers (x, y and z)
--Written by Chris Janssen, Maarten van Grootel, Selwin van Dijk
--Each pair in the set consists of three number between 0 and 10,
-- one of which is the sum of the other two
pairs :: [(Int,Int,Int)]
pairs = [(x,y,z)| x<-[0..10], y<-[0..10], z<-[0..10],
(x+y==z || x+z==y || y+z==x)]
--The number of the possible worlds (i.e. pairs)
numpairs =llength(pairs)
--returns the number of elements in the list
llength [] =0
llength (x:xs) = 1+ llength xs
--gives an index to the worlds.
ipairs = zip [0..numpairs-1] pairs
--The model
tnpm :: EpistM
tnpm = (Pmod [0..numpairs-1] val acc [0..numpairs-1])
where
val = [(w,[P x, Q y, R z]) | (w,(x,y,z)) <- ipairs]
Here the valuation of the model is created, which are all possible worlds automatically constricted by the constrainst that x,y,z < 10 and one is the sum of the remaining two. The accessibility (Agent,World,Valuation) is given such that for all Worlds w, a Validation v exists for Agents a,b or c.
acc = [(a,w,v)| (w,(x1,y1,z1)) <- ipairs,
(v,(x2,y2,z2)) <- ipairs, y1==y2, z1==z2]++
[(b,w,v)| (w,(x1,y1,z1)) <- ipairs,
(v,(x2,y2,z2)) <- ipairs, x1==x2, z1==z2]++
[(c,w,v)| (w,(x1,y1,z1)) <- ipairs,
(v,(x2,y2,z2)) <- ipairs, x1==x2, y1==y2]
These accessability relations state that in every world in which an agent sees two particular numbers, he will keep all other worlds possible in which he sees the same two numbers. This means that the agent, in any specific situation, holds at most two worlds possible: one where his number is the sum of the others, and one where his number with one of the others sums to the last.
--Agent A says he does not know his number
aA = Conj [(Disj[Neg (Prop (P x)), Neg (K A ( Prop (P x))) ] )|x <- [0..10]]
annA = public (aA)
The agents announce their ingorance with the line,
Disj[Neg (Prop (P x)), Neg (K A ( Prop (P x)))].
This states the agent is not assigned number x or it does not know what the number is, or in the form of an implication: "if i've got a number, I don't know it". Though the problem description has the agents state that they do not know all the numbers, we only have them state ignorance of their own number. This leads to a big decrease in computation time while returning the same result, this is because it decreases the search space.
The less efficiënt line would read:
Conj [(Disj[Neg (Conj [
Prop (P x),Prop (Q y),Prop (R z)]),
Neg (K A (Conj [Prop (P x),Prop (Q y),Prop (R z)]))
] ) |(x,y,z)<-pairs]
Given the accessibility statement given earlier, the agent already knows y and z. If something is always true, checking if its conjunction is false is useless, and thus can be left out. We can therefore simply say Agent A only doesn't know his own number.
In a similar way, the statements of agents B and C are formalised.
--Agent B says he does not know his number either
aB = Conj [(Disj[Neg (Prop (Q y)), Neg (K B ( Prop (Q y))) ] )|y <- [0..10]]
annB = public (aB)
--Agent C says he does not know his number either
aC = Conj [(Disj[Neg (Prop (R z)), Neg (K C ( Prop (R z) )) ] )|z <- [0..10]]
annC = public (aC)
--Show the possible solutions after all agents have made their announcements
solution = showM (upds tnpm [annA, annB, annC])
--Agent A says he now knows his number.
--This announcement does not change any of the agents' knowledge
aA2 = Conj [(Disj[Neg (Prop (P x)), K a (Prop (P x)) ] )|x<-[0..10]]
annA2 = public (aA2)
--gives same solution as first solution
solution2 = showM (upds tnpm [annA, annB, annC, annA2])
The 'solution'-statement applies the three agents' statements sequentially. When finished the set of possible worlds has been reduced to the four mentioned in the 'solution' section of this webpage. When adding the utterance of A ('solution2' in the program) that he now knows his number is rather unnecessary as it already was common knowledge that A knows his number after the three previous statements.
Running the program (with the GHC compiler of Haskell 98) would normally look like this:
___ ___ _
/ _ \ /\ /\/ __(_)
/ /_\// /_/ / / | | GHC Interactive, version 6.4.2, for Haskell 98.
/ /_\\/ __ / /___| | http://www.haskell.org/ghc/
\____/\/ /_/\____/|_| Type :? for help.
Loading package base-1.0 ... linking ... done.
Prelude> :load TNP
Compiling DPLL ( ./DPLL.hs, interpreted )
Compiling DEMO ( ./DEMO.hs, interpreted )
Compiling TNP ( ./tnp.hs, interpreted )
Ok, modules loaded: TNP, DEMO, DPLL.
*SNP> solution
==> [0,1,2,3]
[0,1,2,3]
(0,[p1,q3,r2])(1,[p1,q3,r4])(2,[p2,q1,r1])(3,[p2,q1,r3])
(a,[[0],[1],[2],[3]])
(b,[[0],[1],[2],[3]])
(c,[[0,1],[2,3]])
*SNP>
In this output we can see the four solutions numbered 0 to 3. We also see that in each of these worlds both agents A and B hold only that world possible. However, when in world 0 or 1, agent C cannot decide in which one he is. Similarly he can't choose between worlds 2 and 3 when he is in one of those. This can be seen in the last line of output, where agent C has accessibility relations between worlds 0 and 1 and between 2 and 3.