:-J=['% strategic manipulation by prolog'
,'%------------------------------------------------------'
,'% sproof.pl (12-3 Jan 2006 23:09)'
], forall(member(X,J),(nl,write(X))).

%  SP (strategy-proofness)
%  MM (Maskin monotonicity)
%  PE (Parato efficiency)

%  urd (unrestricted domain)
%  cs (citizen's sovereginty)

%  i=1, ..., n (agents) N=[1,..,n].
%  X=[a, b, ... ] (alternatives) #X=m.

%  Dict(i): the fact that agent i is a dictator.

% GS Theorem. Assume n>=2, m>=3, urd, cs. Then SP->Dict(i). 

% Lemma. SP --> MM (-->SP ).
% Lemma. SP -->PE. 


% 2 person 3 alternatives 
% example for Gibbard-Satterthwaite theorem
%-------------------------------------------------
  
% reference
% Ishii, Saijo, Shiozawa (1995). Introduction to Microeconomics. 
% Yuhikaku. (Japanese)

alternative(a).
alternative(b).
alternative(c).

agent(1).
agent(2).

set_of_alternatives([a,b,c]).
set_of_agents([1,2]).

possible_preference_ordering( r(1), [a,b,c]).
possible_preference_ordering( r(2), [a,c,b]).
possible_preference_ordering( r(3), [b,a,c]).
possible_preference_ordering( r(4), [b,c,a]).
possible_preference_ordering( r(5), [c,a,b]).
possible_preference_ordering( r(6), [c,b,a]).

strictly_prefer_to(A,B, R):-
   possible_preference_ordering( R, O),
   append( _,[A|C],O),
   member(B,C).

prefer_to(A,B, R):-
   alternative(A),
   alternative(B),
   \+ strictly_prefer_to(A,B, R).

indifferent_to(A,B, R):-
   prefer_to(B,A, R),
   prefer_to(A,B, R).



possible_preference_of_agent( J, R, O):-
   agent(J),
   possible_preference_ordering(R, O).


% 2 person 3 alternatives unrestricted domain
%-------------------------------------------------

preference_pair( urd(2,3), (1, R1,O1), (2, R2, O2)):-
   possible_preference_of_agent( 1, R1, O1),
   possible_preference_of_agent( 2, R2, O2).



% sample SCFs of unrestricted domain
%-------------------------------------------------

social_choice_function( urd(2,3), scf(1)).
social_choice_function( urd(2,3), auto(sp)).

social_choice_function( Domain, scf(1), (R1,R2)-> Win):-
   preference_pair( Domain, (1, R1,_), (2, R2,_)),
   majority_rule( (R1,R2), (X,Y), Tie, Win),
   tie_breaking(Tie, Win, [X,Y]).

social_choice_function( Domain, auto(sp), (R1,R2)-> Win):-
   clause(auto_scf_0( Domain, (R1,R2)-> Win,_,_),true).

majority_rule( (R1,R2), (X,X), decided, X):-
   possible_preference_ordering( R1, [X|_]),
   possible_preference_ordering( R2, [X|_]).

majority_rule( (R1,R2), (X,Y), tie, Z):-
   possible_preference_ordering( R1, [X|_]),
   possible_preference_ordering( R2, [Y|_]),
   X \= Y,
   member( Z, [X,Y]).

tie_breaking(decided, _, _).
tie_breaking(tie, Z, [X,Y]):-
   member( (Z,W),[(X,Y),(Y,X)]),
   strictly_prefer_to( Z, W, r(1)). 
   
% citizen's sovereignty.

taboo_alternative(Domain,SCR,A):-
   social_choice_function( Domain, SCR),
   alternative(A), 
   \+ social_choice_function( Domain, SCR, _R-> A).

no_taboo_alternatives(Domain, SCR):-
   social_choice_function( Domain, SCR),
   \+ taboo_alternative(Domain, SCR,_).


%  displaying scf 
%-------------------------------------------------

display_scf(Domain, Scf):-
   Warn=(nl,write('no such domain or scf. go ahead? ')),
   (
    social_choice_function( Domain, Scf)->true;
    (Warn,!,read(y))
   ),
   nl,
   write(domain:Domain),
   tab(1),
   write(scf:Scf),
   forall(
     bagof(C,
       B^social_choice_function( Domain, Scf, (A,B)->C),
     L),
    (
     nl,
     write(row=A),
     tab(1),
     write(L)
    )
   ).

/*

?- display_scf(A,B).

domain:urd(2, 3) scf:scf(1)
row=r(1) [a, a, a, a, a, a]
row=r(2) [a, a, a, a, a, a]
row=r(3) [a, a, b, b, b, b]
row=r(4) [a, a, b, b, b, b]
row=r(5) [a, a, b, b, c, c]
row=r(6) [a, a, b, b, c, c]

A = urd(2, 3)
B = scf(1) 

Yes
?- 

*/



%  Maskin monotonicity
%-------------------------------------------------

monotonic_scf( Domain, Scf):-
   social_choice_function( Domain, Scf),
   forall(
     social_choice_function( Domain, Scf, (R1,R2)-> X),
     \+ monotonicity( Domain, Scf, (R1,R2), _, X, no)
   ).

monotonicity( Domain, Scf, (R1,R2), (S1,S2), X, Chk):-
   social_choice_function( Domain, Scf, (R1,R2)-> X),
   monotonic_change( Domain, (R1,R2)-> (S1,S2), X),
   chk_monotonicity( Domain, Scf,(S1,S2), X, Chk).

monotonic_change( Domain, (R1,R2)-> (S1,S2), X):-
   preference_pair( Domain, (1, R1,_), (2, R2, _)),
   preference_pair( Domain, (1, S1,_), (2, S2, _)),
   (R1,R2)\=(S1,S2),
   is_not_depreciated( X, R1->S1),
   is_not_depreciated( X, R2->S2).

is_not_depreciated( X, R1->S1):-
   lower_contour_set(X, (R1,_), LccR1),
   lower_contour_set(X, (S1,_), LccS1),
   subset( LccR1,LccS1).

chk_monotonicity( Domain, Scf,(S1,S2), X, Chk):-
   social_choice_function( Domain,Scf, (S1,S2)-> X)
   -> Chk = yes 
   ; Chk = no.

lower_contour_set(X, (R,O), [X|Lcc]):-
   possible_preference_ordering( R, O),
   append( _,[X|Lcc],O).


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

/*

?- monotonicity( Domain, Scf, (R1,R2), (L1,L2), X,no).

No
?- monotonicity( Domain, Scf, (R1,R2), (L1,L2), X,yes).

Domain = urd(2,3)
Scf = scf(1)
R1 = r(1)
R2 = r(1)
L1 = r(1)
L2 = r(2)
X = a 

Yes
?- monotonic_scf( Domain ,Scf).

Domain = urd(2, 3)
Scf = auto(sp) ;

No
?- 

*/

%  strategic-proofness and manipulability
%-------------------------------------------------

is_manipulable( Domain ,Scf, agent(1), (R1->S1, R2),(X->Y)):-  
   social_choice_function( Domain, Scf, (R1,R2)-> X),
   social_choice_function( Domain, Scf, (S1,R2)-> Y),
   strictly_prefer_to( Y, X, R1). 

is_manipulable( Domain ,Scf, agent(2), (R1, R2->S2),(X->Y)):-  
   social_choice_function( Domain, Scf, (R1,R2)-> X),
   social_choice_function( Domain, Scf, (R1,S2)-> Y),
   strictly_prefer_to( Y, X, R2). 

strategy_proof( Domain ,Scf, (R1, R2)-> X):-  
   social_choice_function( Domain, Scf, (R1,R2)-> X),
   \+ is_manipulable( Domain ,Scf, agent(1), (R1->_, R2),(X->_)),  
   \+ is_manipulable( Domain ,Scf, agent(2), (R1, R2->_),(X->_)).

strategy_proof( Domain ,Scf):-  
   social_choice_function( Domain, Scf),
   \+ is_manipulable( Domain ,Scf, agent(_), _,_).

/*

?- is_manipulable( urd(2,3) ,scf(1), A,R,Y), 
    nl,write(A;R;Y),fail.

agent(1);r(5)->r(1), r(3);b->a
agent(1);r(5)->r(2), r(3);b->a
agent(1);r(5)->r(1), r(4);b->a
agent(1);r(5)->r(2), r(4);b->a
agent(2);r(3), r(5)->r(1);b->a
agent(2);r(3), r(5)->r(2);b->a
agent(2);r(4), r(5)->r(1);b->a
agent(2);r(4), r(5)->r(2);b->a

No
?- strategy_proof( Domain ,Scf).

Domain = urd(2, 3)
Scf = auto(sp) ;

No
?- 

*/


%  Pareto efficiency
%-------------------------------------------------

is_not_pareto_efficient( (R1, R2),X):-  
   strictly_prefer_to( Y, X, R1), 
   strictly_prefer_to( Y, X, R2). 

is_pareto_efficient( Domain, (R1, R2),X):-
   alternative(X),  
   preference_pair( Domain, (1, R1,_), (2, R2,_)),
   \+ is_not_pareto_efficient( (R1, R2),X).

is_not_pareto_efficient_scf( Domain, Scf, (R1,R2)-> X):-
   social_choice_function( Domain, Scf, (R1,R2)-> X),
   is_not_pareto_efficient( (R1, R2),X). 

is_pareto_efficient_scf( Domain, Scf, (R1,R2)-> X):-
   social_choice_function( Domain, Scf, (R1,R2)-> X),
   is_pareto_efficient( Domain, (R1, R2),X). 

is_pareto_efficient_scf( Domain, Scf):-
   social_choice_function( Domain, Scf),
   \+ \+ is_pareto_efficient( Domain, _,_). 

/*

?- is_pareto_efficient_scf( urd(2,3), Scf, (R1,R2)-> X).

Scf = scf(1)
R1 = r(1)
R2 = r(1)
X = a 

Yes
?- is_not_pareto_efficient_scf( Domain, Scf, (R1,R2)-> X).

No
?- is_pareto_efficient_scf( Domain, Scf).

Domain = urd(2, 3)
Scf = scf(1) ;

Domain = urd(2, 3)
Scf = auto(sp) ;

No
?-

*/


%  dictatorship
%-------------------------------------------------

dictator_for_scf(Domain, Scf,J):-
   social_choice_function( Domain, Scf),
   agent(J),
   forall(
     preference_pair( Domain, (1, R1,_), (2, R2, _)),
     dictator_for_scf(Domain, Scf, (R1,R2),J)
   ).

dictator_for_scf(Domain, Scf, (R1,R2),J):-
   social_choice_function( Domain, Scf, (R1,R2)-> X),
   dictatorship(Domain, (R1,R2)->X, J).

dictatorship(Domain, (R1,R2)->X, 1):-
   preference_pair( Domain, (1, R1,[X|_]), (2, R2, _)).

dictatorship(Domain, (R1,R2)->X, 2):-
   preference_pair( Domain, (1, R1,_), (2, R2, [X|_])).

/*

?- dictator_for_scf(Domain, Scf,J).

Domain = urd(2, 3)
Scf = scf(1)
J = 1 ;

Domain = urd(2, 3)
Scf = scf(1)
J = 2 ;

No
?- 
*/

%  automated construction of strategy-proof scf
%  by recursively propagating MM as the constraint 
%-------------------------------------------------

all_possible_preference_pair_n_domain( Domain, Poss):-
   setof((R1,R2),
     O1^O2^
       preference_pair( Domain, (1,R1,O1), (2,R2,O2)),
   Poss).

auto_scf( Domain, FL,Property):-
   all_possible_preference_pair_n_domain( Domain, L),
   auto_scf( Domain, FL, L, Property).

auto_scf( _, [],[], _).
auto_scf( Domain, [R-> X | H], [R|Q], pareto):-
   auto_scf( Domain, H,Q,pareto),
   is_pareto_efficient( Domain, R,X).

auto_scf( Domain, [R-> X | H], [R|Q], monotone):-
   auto_scf( Domain, H,Q,monotone),
   alternative(X),
   \+ (
     member( (S->Y), H),
     monotonic_change( Domain, S->R, Y),
     X \= Y
   ),
   \+ (
     monotonic_change( Domain, R->S, X),
     member( (S->Y), H),
     X \= Y
   ).

display_auto_scf(F):-
   forall(
     setof((K,C),member((r(J),r(K))->C,F),L),
     (nl,write(row=J;L))
   ).

display_auto_scf_nn(F):-
   \+ var(F),
   length(F,_),
   forall(
     bagof(C,K^member((r(J),r(K))->C,F),L),
     (nl,write(row=J;L))
   ).

/*

?- auto_scf( Domain,F, Property), display_auto_scf(F).

row=1;[ (1, a), (2, a), (3, a), (4, a), (5, a), (6, a)]
row=2;[ (1, a), (2, a), (3, a), (4, a), (5, a), (6, a)]
row=3;[ (1, a), (2, a), (3, b), (4, b), (5, a), (6, b)]
row=4;[ (1, a), (2, a), (3, b), (4, b), (5, b), (6, b)]
row=5;[ (1, a), (2, a), (3, a), (4, b), (5, c), (6, c)]
row=6;[ (1, a), (2, a), (3, b), (4, b), (5, c), (6, c)]

Domain = urd(2, 3)
F = [ (r(1), r(1)->a), (r(1), r(2)->a), (r(1), r(3)->a), (r(1), r(4)->a), (r(1), r(5)->a), (r(1), r(6)->a), (r(...), r(...)->a), (..., ... ->a), (... ->...)|...]
Property = pareto 

Yes
?- auto_scf( Domain,F, Property),
display_auto_scf_nn(F).

row=1;[a, a, a, a, a, a]
row=2;[a, a, a, a, a, a]
row=3;[a, a, b, b, a, b]
row=4;[a, a, b, b, b, b]
row=5;[a, a, a, b, c, c]
row=6;[a, a, b, b, c, c]

Domain = urd(2, 3)
F = [ (r(1), r(1)->a), (r(1), r(2)->a), (r(1), r(3)->a), (r(1), r(4)->a), (r(1), r(5)->a), (r(1), r(6)->a), (r(...), r(...)->a), (..., ... ->a), (... ->...)|...]
Property = pareto 

Yes
?- 

*/


%  generating script for strategic-proof scf.
%-------------------------------------------------

:- dynamic auto_scf_0/4.

% for iteration by fail operator.

generate_cs_scf( Domain, Property, Name):-
   generate_scf( Domain, Property, Name),
   no_taboo_alternatives( Domain, Name).

generate_scf( Domain, Property, Name):-
   generate_scf_init( Domain, Property,Name),
   generate_scf_gen( Domain, Property, Name,_FL),
   generate_scf_count( Domain, Property, Name,_Q),
   generate_scf_fin( Domain, Property, Name,_L,_M).

generate_scf_init( Domain, _Property,Name):-
   abolish(auto_scf_0/4),
   (var(Domain)->Domain = urd(2,3);true),
   (var(Name)->Name=auto(sp);assert(scf(Domain,Name))).

generate_scf_gen( Domain, Property, Name,FL):-
   auto_scf(Domain, FL, Property),
   update_auto_scf(Domain, FL, Property, Name).

update_auto_scf(Domain, FL, Property, Name):-
   Body = auto_scf_0(Domain,F,Property,Name),
   forall( clause( Body,true),retract( Body)),
   forall(member(F,FL),assert(Body)).

generate_scf_count( Domain, Property, Name,Q):-
   findall( 1,
    (
     auto_scf_0(Domain,_->_,Property,Name)
    ),
   P),
   length(P, Q),
   nl,
   write(Q/36),
   write( ' patterns have been generated.').

generate_scf_fin( Domain, Property, Name,L,M):-
   findall( (R1,R2),
    (
     preference_pair( Domain, (1,R1,_), (2,R2,_)),
     \+ auto_scf_0(Domain,(R1,R2)->_,Property,Name)
    ),
   L),
   length( L, M),
   nl,
   write( M),
   write( ' patterns are missing.'),
   nl,
   write( L).


:- abolish( auto_scf_0/3).


/*

?- generate_scf(A,monotone,C),
display_scf(A,C).

36/36 patterns have been generated.
0 patterns are missing.
[]
domain:urd(2, 3) scf:auto(sp)
row=r(1) [a, a, a, a, a, a]
row=r(2) [a, a, a, a, a, a]
row=r(3) [a, a, a, a, a, a]
row=r(4) [a, a, a, a, a, a]
row=r(5) [a, a, a, a, a, a]
row=r(6) [a, a, a, a, a, a]

A = urd(2, 3)
C = auto(sp) ;

36/36 patterns have been generated.
0 patterns are missing.
[]
domain:urd(2, 3) scf:auto(sp)
row=r(1) [a, a, a, a, a, a]
row=r(2) [a, a, a, a, a, a]
row=r(3) [a, a, b, b, a, b]
row=r(4) [a, a, b, b, a, b]
row=r(5) [a, a, a, a, a, a]
row=r(6) [a, a, b, b, a, b]

A = urd(2, 3)
C = auto(sp) 

Yes
?- generate_cs_scf(A,monotone,C),
display_scf(A,C),
dictator_for_scf(A, C,J).

(...)
36/36 patterns have been generated.
0 patterns are missing.
[]
domain:urd(2, 3) scf:auto(sp)
row=r(1) [a, a, b, b, c, c]
row=r(2) [a, a, b, b, c, c]
row=r(3) [a, a, b, b, c, c]
row=r(4) [a, a, b, b, c, c]
row=r(5) [a, a, b, b, c, c]
row=r(6) [a, a, b, b, c, c]

A = urd(2, 3)
C = auto(sp) 
J = 2 ;

(...)
36/36 patterns have been generated.
0 patterns are missing.
[]
domain:urd(2, 3) scf:auto(sp)
row=r(1) [a, a, a, a, a, a]
row=r(2) [a, a, a, a, a, a]
row=r(3) [b, b, b, b, b, b]
row=r(4) [b, b, b, b, b, b]
row=r(5) [c, c, c, c, c, c]
row=r(6) [c, c, c, c, c, c]

A = urd(2, 3)
C = auto(sp)
J = 1 ;

(...)
No
?- 

*/

return to front page.