You selected ck01.pl
headline:-
write('% --------------------------------------------------------- %'),nl,
write('% common knowledge : 3 children puzzle.'),nl,
write('% created: 13-15 Jan 2003.'),nl,
write('% author: Kenryo INDO (Kanto Gakuen University) '),nl,
write('% url: http://www.us.kanto-gakuen.ac.jp/indo/front.html'),nl,
write('% --------------------------------------------------------- %'),nl.
references:-
write('% references:'),nl,
write('% [1] Aumann, R. J. (1976). Agreeing to disagree.'),nl,
write('% Annals of Statistics 4: 1236-1239.'),nl,
write('% [2] Geanakoplos, J. (1992). Common knowledge.'),nl,
write('% Journal of Economic Perspective 6: 53-82.'),nl,
write('% also in R. J. Aumann and S. Hart (eds.),'),nl,
write('% Handbook of Game Theory 2: 1437-1496, 1994.'),nl.
:- dynamic true_state/1.
:- dynamic said/3.
:- dynamic said/4.
:- headline.
:- write(' said/4 to simulate the message procces.'),nl.
:- write(' for example, ?- said(I,T, [r,r,r], Y).'),nl.
:- write(' make_public/0 to assert the impossibility of www.'),nl.
%
% ------------------------------------------------- %
% state, agent, information (partition),
% and possibility relation
% ------------------------------------------------- %
true_state([r,r,r]).
agent(1).
agent(2).
agent(3).
state([r,r,r]).
state([r,r,w]).
state([r,w,r]).
state([w,r,r]).
state([r,w,w]).
state([w,r,w]).
state([w,w,r]).
state([w,w,w]).
partition(1,[r,r,r],[[r,r,r],[w,r,r]]).
partition(1,[r,r,w],[[r,r,w],[w,r,w]]).
partition(1,[r,w,r],[[r,w,r],[w,w,r]]).
partition(1,[w,r,r],[[w,r,r],[r,r,r]]).
partition(1,[r,w,w],[[r,w,w],[w,w,w]]).
partition(1,[w,r,w],[[w,r,w],[r,r,w]]).
partition(1,[w,w,r],[[w,w,r],[r,w,r]]).
partition(1,[w,w,w],[[w,w,w],[r,w,w]]).
partition(2,[r,r,r],[[r,r,r],[r,w,r]]).
partition(2,[r,r,w],[[r,r,w],[r,w,w]]).
partition(2,[r,w,r],[[r,w,r],[r,r,r]]).
partition(2,[w,r,r],[[w,r,r],[w,w,r]]).
partition(2,[r,w,w],[[r,w,w],[r,r,w]]).
partition(2,[w,r,w],[[w,r,w],[w,w,w]]).
partition(2,[w,w,r],[[w,w,r],[w,r,r]]).
partition(2,[w,w,w],[[w,w,w],[w,r,w]]).
partition(3,[r,r,r],[[r,r,r],[r,r,w]]).
partition(3,[r,r,w],[[r,r,w],[r,r,r]]).
partition(3,[r,w,r],[[r,w,r],[r,w,w]]).
partition(3,[w,r,r],[[w,r,r],[w,r,w]]).
partition(3,[r,w,w],[[r,w,w],[r,w,r]]).
partition(3,[w,r,w],[[w,r,w],[w,r,r]]).
partition(3,[w,w,r],[[w,w,r],[w,w,w]]).
partition(3,[w,w,w],[[w,w,w],[w,w,r]]).
all_agnets(Is):- findall(J,agent(J),Is).
all_states(O):- findall(S,state(S),O).
think(J,S,is_impossible(O)):-
agent(J),
state(S),
state(O),
\+ think(J,S,is_possible(O)).
think(J,S,is_possible(O)):-
agent(J),
state(S),
partition(J,S,H),
member(O,H),
\+ said(public,0,is_impossible(O)).
think(J,S,K):-
K = think(_J1,O,_O1),
think(J,S,is_possible(O)),
K.
test_think:-
think(3, [r,r,r],
think(2, [r,r,w],
think(1, [r,w,w],
is_possible([w,w,w])
)
)
).
%
% ------------------------------------------------- %
% event, (static) knowledge, and reachability
% ------------------------------------------------- %
event(E):-
all_states(O),
subset_of(E,_N,O).
know(J,S,E):-
agent(J),
state(S),
partition(J,S,H1),
remove_impossible_states(J,S,H1,H),
event(E),
subset(H,E).
remove_impossible_states(J,S,E,H):-
event(E),
findall(X,
think(J,S,is_impossible(X)),
D),
subtract(E,D,F),
sort(F,H).
rimps(J,S,E,H):-
remove_impossible_states(J,S,E,H).
%
cyclic(J/Y,S/T):-
nth1(K,Y,J),
nth1(K,T,S).
is_reachable(S,S1,[J],[S]):-
state(S),
agent(J),
partition(J,S,H),
member(S1,H),
S1 \= S.
is_reachable(S1,S,[J|Y],[S|T]):-
is_reachable(S1,S2,Y,T),
agent(J),
partition(J,S,H),
\+ cyclic(J/Y,S/T),
member(S2,H).
%
test_reachability(S,S1,Y):-
(is_reachable(S,S1,_,_)->Y=yes;Y=no).
test_reachability(S,H):-
state(S),
findall(S1,
(
state(S1),
test_reachability(S,S1,yes)
),
H).
%
% ------------------------------------------------- %
% common knowledge via meet of partitions
% ------------------------------------------------- %
meet_of_partitions([J],[S],H):-
partition(J,S,H).
meet_of_partitions([J|Js],[S|Ss],M):-
meet_of_partitions(Js,Ss,M1),
partition(J,S,H),
\+ cyclic(J/Js,S/Ss),
\+ subset(H,M1),
intersection(M1,H,H12),
H12 \= [],
union(H,M1,M2),
sort(M2,M).
mops(Js,Ss,M):-
meet_of_partitions(Js,Ss,M).
% it is relatively difficult to find a path of enumerating states.
test_mops(B,C,N):-
mops([1,2,3,1,2,3,1],B,C),
length(C,N).
%
%-----------------------------------------------
/* time and act of agent : message process */
%-----------------------------------------------
time(0/N):- last_time(N).
time(T/N):- last_time(N),length(L,N), nth1(T,L,T).
last_time(7).
move(J,0/N,no):-
time(0/N),
agent(J).
move(J,T/N,yes):-
time(T/N),
T > 0,
T1 is T - 1,
agent(J),
J is T1 mod 3 + 1.
make_public:-
assert(said(public,0,is_impossible([w,w,w]))).
said(public,0,void).
said(J,T,S,Reply):-
state(S),
time(T/N),
T > 0,
T1 is T - 1,
agent(J),
move(J,T/N,yes),
(
know(J,T1/N,S,[S])
->
Reply=know
;
Reply=dk
).
%
%-----------------------------------------------
/* dynamic knowledge updated by messages */
%-----------------------------------------------
know(J,T/N,S,E):-
time(T/N),
agent(J),
state(S),
partition(J,T/N,S,H),
% remove_impossible_states(J,T/N,S,E,H),
(length(H,1)->E=H;true),
event(E),
subset(H,E).
%
remove_impossible_states(J,T/N,S,E,H):-
time(T/N),
agent(J),
state(S),
event(E),
findall(X,
think(J,T/N,S,is_impossible(X)),
D),
subtract(E,D,F),
sort(F,H).
rimps(J,T/N,S,E,H):-
remove_impossible_states(J,T/N,S,E,H).
%
partition(J,T/N,S,H):-
time(T/N),
partition(J,S,H1),
remove_impossible_states(J,T/N,S,H1,H).
%
think(J,T/N,S,is_impossible(O)):-
agent(J),
time(T/N),
state(S),
state(O),
\+ think(J,T/N,S,is_possible(O)).
%
think(J,0/N,S,is_possible(O)):-
time(0/N),
think(J,S,is_possible(O)).
think(J,T/N,S,is_possible(O)):-
time(T/N),
T \= 0,
T1 is T - 1,
think(J,T1/N,S,is_possible(O)),
is_consistent_with_information(T,S,O).
%
%-----------------------------------------------
/* the supporting evidence of state */
%-----------------------------------------------
is_consistent_with_information(T,S,O):-
time(T/_N),
state(S),
state(O),
agent(J),
said(J,T,S,Reply), % real.
said(J,T,O,Reply). % expected.
icwi(T,S,O):-
is_consistent_with_information(T,S,O).
% subset_of/3 : subset-enumeration
% ----------------------------------------------------------- %
subset_of(A,N,As):-
length(As,L),
length(D,L),
list_projection(D,As,B),
length(B,N),
sort(B,A).
% a sequence of binary choice for a list:
%--------------------------------------------------
list_projection([],[],[]).
list_projection([X|Y],[_A|B],C):-
X = 0,
list_projection(Y,B,C).
list_projection([X|Y],[A|B],[A|C]):-
X = 1,
list_projection(Y,B,C).
% sum
% ----------------------------------------------------------- %
sum([],0).
sum([X|Members],Sum):-
sum(Members,Sum1),
%number(X),
Sum is Sum1 + X.
%
% product
% ----------------------------------------------------------- %
product([],1).
product([X|Members],Z):-
product(Members,Z1),
%number(X),
Z is Z1 * X.
%
% ------------------------------------------------- %
% Apendix: a generalization
% ------------------------------------------------- %
/*
color_of_hat(J,C):-
agent(J),
member(C,[w,r]).
state(S):-
bagof(I,agent(I),Is),
maplist(color_of_hat,Is,S).
state0(S):-
bag0(S,[w,r],3).
bag0([],_A,0).
bag0([C|B],A,N):-
length([C|B],N),
bag0(B,A,_N1),
member(C,A).
partition(J,S,H):-
agent(J),
state(S),
setof(O,
S^(
think_possible(J,S,O)
),
H).
can_see(J,S,H):-
agent(J),
state(S),
length(S,N),
length(H,N),
bagof(P,
K^X^(
nth1(K,S,X),
(K\=J -> P=X; P=_var)
),
H).
*/
%end
return to front page.