You selected spcf06.pl
/************************************************************
(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
return to front page.