/************************************************************
  (resolute) strategy proof social choices and decisions
  program: spcf06.pl
  language: prolog
  date: 2006.12.20-26.
  revised: 2009.9.3-4. ( corrections for the Pareto conditions)
  creator: Kenryo INDO
************************************************************/
% load the profile generator if rr/1 does not exist.
:- (\+ clause(rr(_),_)->[cswf06];true).

% agenda for choice
agenda(A):- var(A),alternatives(A).
agenda(A):- \+ var(A),alternatives(B),subset(A,B).

% one of them
oof(A,B):- member(A,B).
xof(Y,A):- agenda(A), oof(Y,A).

% best alternative (among a set A)
best(X,Q):- x(X), \+ (x(Y),\+ r((X,Y),Q)).
best(X,A,Q):- xof(X,A),\+ (xof(Y,A),\+ r((X,Y),Q)).

% worst alternative (among a set A)
worst(X,Q):- x(X), \+ (x(Y),\+ r((Y,X),Q)).
worst(X,A,Q):- xof(X,A),\+ (xof(Y,A),\+ r((Y,X),Q)).

% middle alternatives
medium(X,Q):- x(X),\+ worst(X,Q),\+ best(X,Q).
medium(X,A,Q):- xof(X,A),\+ worst(X,A,Q),\+ best(X,A,Q).

% social decision function
sdf_1([],[],_).
sdf_1([RR->C|F],[RR->R|W],A):- sdf_1(F,W,A),best(C,A,R).
sdf(F,X,W,A):- swf(W,X),sdf_1(F,W,A).
sdf(F,X,W):- alternatives(A),sdf(F,X,W,A).

% social choice function
scf([],[],_).
scf([RR->C|F],[RR|L],X):- scf(F,L,X),axiom_scf(X,RR->C,F).
scf(F,X):-all_rr(L),scf(F,L,X).

% axioms for scf
axiom_scf(d(J,A),RR->C,_):- xof(C,A),dictatorial_scf(J,A,[RR->C]).
axiom_scf(d(J),RR->C,_):- x(C),dictatorial_scf(J,[RR->C]).
axiom_scf(p(A),RR->C,_):- xof(C,A),pareto_scf(A,[RR->C]).
axiom_scf(p,RR->C,_):- x(C),pareto_scf([RR->C]).
axiom_scf(sp(A),RR->C,F):- xof(C,A),spx(A,[RR->C|F]).
axiom_scf(sp,RR->C,F):- x(C),spx([RR->C|F]).
axiom_scf(mm(A),RR->C,F):- xof(C,A),mmx(A,[RR->C|F]).
axiom_scf(mm,RR->C,F):- x(C),mmx([RR->C|F]).
% for a debug
axiom_scf(xp,RR->C,_):- x(C),xp1([RR->C]).

%
agree_to_prefer((X,Y),PP,strict):- x(X),x(Y),\+ ( oof(Q,PP), \+ p((X,Y),Q) ).
agree_to_prefer((X,Y),PP,weak):- x(X),x(Y),\+ ( oof(Q,PP), \+ r((X,Y),Q) ).

% properties of scf 

% the weak Pareto condition (corrected )
pareto_scf(F):- weak_pareto(F).
weak_pareto(F):-
   \+ (oof(PP->C,F), agree_to_prefer((_,C),PP,strict) ).
strict_pareto(F):-
   \+ (oof(PP->C,F), agree_to_prefer((B,C),PP,weak), r_j(_,PP,P), p((B,C),P) ).

pareto_scf(A,F):- agenda(A),
   \+ (oof(PP->C,F), oof(B,A), agree_to_prefer((B,C),PP,strict) ).

% (I screwed up.)
xp1(F):-
   \+ (oof(PP->C,F), \+ (j(J), r_j(J,PP,P), best(C,P))).
xp2(F):-
   \+ (oof(PP->C,F), \+ (r_j(_,PP,P),\+ best(B,P)),C\=B).
xp3(F) :- agenda(A),
   \+ (oof(PP->C,F), \+ (r_j(_,PP,P),\+ best(B,A,P)),C\=B).

/*

?- dp_mode(I).
I = 2.

?- rr(P),scf(F,[P],x),\+ scf(F,[P],xp).
false.

?- rr(P),scf(F,[P],xp),\+ scf(F,[P],p),nl,write(F),fail.

[ ([[+, -, -], [-, +, +]]->c)]
[ ([[-, +, -], [+, -, +]]->a)]
[ ([[+, +, -], [-, -, +]]->b)]
[ ([[-, -, +], [+, +, -]]->b)]
[ ([[+, -, +], [-, +, -]]->a)]
[ ([[-, +, +], [+, -, -]]->c)]
false.
?- 

*/

% other properties of scf
dictatorial_scf(J,F):- j(J),
   \+ (oof(PP->C,F),r_j(J,PP,P),\+ best(C,P)).
dictatorial_scf(J,A,F):- j(J),agenda(A),
   \+ (oof(PP->C,F),r_j(J,PP,P),\+ best(C,A,P)).
cs_scf(F):- \+ (x(X),\+ oof(_->X,F)).
cs_scf(A,F):- \+ (xof(X,A),\+ oof(_->X,F)).
sp(F):- \+ manipulable(_,_,_,F).
sp(A,F):- \+ manipulable(A,_,_,_,F).
manipulable(J,PP->X,QQ->Y,F):- dop((X,Y)),oof(QQ->Y,F),
   udrr(PP,QQ,_,(J,P,_)),oof(PP->X,F),p((Y,X), P).
manipulable(A,J,PP->X,QQ->Y,F):-
   xof(X,A),xof(Y,A),
   manipulable(J,PP->X,QQ->Y,F).
spx([W|F]):-
   \+ manipulable(_,W,_,[W|F]),
   \+ manipulable(_,_,W,[W|F]).
spx(A,[W|F]):-
   \+ manipulable(A,_,W,_,[W|F]),
   \+ manipulable(A,_,_,W,[W|F]).

% unilaterally deviated profile (udrr)
udrr([],[],[],[],non).
udrr([J|N],[P|PP],[Q|PP],L,(J,P,Q)):-
   r(P),r(Q), P \= Q,
   udrr(N,PP,PP,L,non).
udrr([_|N],[P|PP],[P|QQ],[P|L],D):-
   udrr(N,PP,QQ,L,D).
udrr(PP,QQ,L,(J,P,Q)):-
   agents(N),udrr(N,PP,QQ,L,(J,P,Q)).

%udrr(PP,QQ,L,(J,P,_)):-
%   r_j(-J,PP,P,L),r_j(-J,QQ,_,L),

% downward shift of ranking
depreciate((X,Y),P->Q):- r((X,Y),P),\+ r((X,Y),Q).

% monotonocity in Maskin's sense.
mm(F):- \+ nonmonotonic(_,_,_,F).
mm(A,F):- \+ nonmonotonic(A,_,_,_,F).

mmx([W|F]):-
   \+ nonmonotonic(_,W,_,[W|F]),
   \+ nonmonotonic(_,_,W,[W|F]).
mmx(A,[W|F]):-
   \+ nonmonotonic(A,_,W,_,[W|F]),
   \+ nonmonotonic(A,_,_,W,[W|F]).

nonmonotonic(J,PP->X,QQ->Y,F):- oof(PP->X,F),
   oof(QQ->Y,F),Y \= X, \+ ( r_j(J,PP,P),
   r_j(J,QQ,Q),depreciate((X,Y),P->Q)).

nonmonotonic(A,J,PP->X,QQ->Y,F):-
   nonmonotonic(J,PP->X,QQ->Y,F),
   xof(X,A),xof(Y,A).

% display (1): a simple table
%-------------------
 
display_scf(F):-show_scf(F).
display_scf_t1(F):-show_scf(F).

show_scf(F):-
   \+ var(F),agents([1,2]),
   display_scf_header,hr(20),
   forall( id_r(_:I,P),
    (
     an_scf_line(L,P,F),
     nl,write(P=I),tab(2),write_sequence(L)
    )
   ).

display_scf_header:-
   bagof(N,K^R^id_r(K:N,R),L),
   nl,write('swf:row  col '),write_sequence(L).

an_scf_line(L,P,F):-
   bagof(C, Q^oof([P,Q]->C,F),L).

% display (2): lines
%-------------------
display_scf_l(F):-show_scf_l(F).

rr_0([R|Q],[_|N],T):- rr_0(Q,N,T),B=..[T,R],B.
rr_0([],[],_).
rr_0(QQ,T):- model(_,_:N),r_type(T:_),rr_0(QQ,N,T).
r_j_0(J,PP,P,T):- rr_0(PP,T), nth1(J,PP,P).

show_scf_hl(T):-
   forall(j(J),(
     nl,write(pref:j=J),write(:),
     forall(r_j_0(J,_,P,T),(id_r(_:S,P,_),write(S)))
   )), 
   forall(j(J),(
     nl,write(best:j=J),write(:),
     forall(r_j_0(J,_,P,T),(best(A,P),write(A)))
   )).
show_scf_l(F,T):-
   show_scf_hl(T),
   show_scf_l0(F,T).
show_scf_l0(F,T):-
   nl,write(scf),write(:),tab(5),
   forall(rr_0(PP,T),((oof(PP->A,F)->B=A;B='-'),write(B))).


%---------
% demo

% proof(1): Strategy-proof + citizen's sovereignty -> dictatorial
% (the Gibbard-Satterthwaite theorem)

/*

?- stopwatch((scf(F,sp([a,b,c])),cs_scf(F),display_scf(F),fail;true),T).

swf:row  col ACITZN
--------------------
[+, +, +]=A  aaaaaa
[-, +, +]=C  bbbbbb
[-, -, +]=I  bbbbbb
[+, +, -]=T  aaaaaa
[+, -, -]=Z  cccccc
[-, -, -]=N  cccccc
swf:row  col ACITZN
--------------------
[+, +, +]=A  abbacc
[-, +, +]=C  abbacc
[-, -, +]=I  abbacc
[+, +, -]=T  abbacc
[+, -, -]=Z  abbacc
[-, -, -]=N  abbacc
% time elapsed (sec): 0.344

F = _G168
T = 0.344 

Yes
?- A=[a,c],stopwatch((scf(F,sp(A)),cs_scf(A,F),display_scf(F),fail;true),T).

swf:row  col ACITZN
--------------------
[+, +, +]=A  aaaaaa
[-, +, +]=C  aaaaaa
[-, -, +]=I  aacacc
[+, +, -]=T  aaaaaa
[+, -, -]=Z  aacacc
[-, -, -]=N  aacacc
swf:row  col ACITZN
--------------------
[+, +, +]=A  aaaaaa
[-, +, +]=C  aaaaaa
[-, -, +]=I  cccccc
[+, +, -]=T  aaaaaa
[+, -, -]=Z  cccccc
[-, -, -]=N  cccccc
swf:row  col ACITZN
--------------------
[+, +, +]=A  aacacc
[-, +, +]=C  aacacc
[-, -, +]=I  aacacc
[+, +, -]=T  aacacc
[+, -, -]=Z  aacacc
[-, -, -]=N  aacacc
swf:row  col ACITZN
--------------------
[+, +, +]=A  aacacc
[-, +, +]=C  aacacc
[-, -, +]=I  cccccc
[+, +, -]=T  aacacc
[+, -, -]=Z  cccccc
[-, -, -]=N  cccccc
% time elapsed (sec): 0.125

A = [a, c]
F = _G168
T = 0.125 

Yes
?-

*/

% proof(2): Strategy-proof scf <-> Maskin monotonic scf
%( the Muller-Satterthwaite theorem)
/*
?- scf(F,sp),\+ scf(F,mm),display_scf(F).

No
?- scf(F,mm),\+ scf(F,sp),display_scf(F).

No
?-

*/

% proof(3): Strategy-proof -> Pareto optimal
/*
?- scf(F,sp),\+ scf(F,p),display_scf(F).

No
?-
*/



%---- end