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