:-T='Arrovian possibility theorem by prolog '
,N='(swf_a.pl, 5-7,21,25 Feb 2006)'
,H='----------------------------------------'
,forall(member(X,[H,T,N,H]),(nl,write(X))),nl.

% References:
% [1] Arrow, K. (1951/1963). 
%  Social Choice and Individual Values.
%  Cowles Foundation Monograph 12.
% [2] Sen, A. (1995). 
%  Rationality and social choice.
%  American Economic Review 85(1):1-24. 

% Definitions
%-------------------------------------------------
% A: a set of social states(alternatives of social choice), 
% N=[1,2,,...,n] : a set of agents(the members of the society). 
% R=[r(1),r(2),...,r(n)]: a profile of weak orderings of individual agents. 

% Def. (unristricted domain; UD)
%   None of the logically possible orderings may be excluded. 
% Def. (social welfare function; SWF) 
%   f: profiles of weak orderings R^n over A -> weak orderings R over A.
% Def. (decisiveness of a group G over (x,y)
%   A subset G of N is decisive if for a pair (x,y) in A^2,
%   the swf r=f(R)is such that r(X,Y)<->r(G,X,Y) for (X,Y) is (x,y) or (y,x).  
% Def. (decisiveness of G)
%   A subset G of N is decisive if for any pair (x,y) in A^2,
%   decisive(G,x,y). 
% Def. (Pareto principle)  N is decisive.
% Def. (dictatorship)  For a member J in N, [J] is decisive.
% Def. (independence of irrelevant alternatives;IIA)
%   If r(x,y) is not depend on any r(j,A,B)
%   such that (A,B) is neither (x,y) or (y,x).

% Theorem(Arrow). Suppose UD and IIA. Then decisive(N)->decisive([J]).
% Lemma. subset(G,N),decisive(G,X,Y)-> decisive(G).
% Lemma. decisive(G)->(partition(G1,G2,G),member(A,[G1,G2]),decisive(A)). 


% 2 person 3 alternatives example
%-------------------------------------------------

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

agent(1).
agent(2).

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

group([1]).
group([2]).
group([1,2]).

counter_group(G,H):-
   set_of_agents(N),
   group(G),
   subtract(N,G,H).


% modeling the weak orderings
% of the 2x3 unrestricted domain
%-------------------------------------------------
% In favor of brevity,
% we will concentrate on the strict part of it. 

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]).


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

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

maximal_element( X, R):-
   possible_preference_ordering( R,[X|_O]).


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

possible_preference_of_group( G, R, O):-
   group(G),
   possible_preference_of_group_1( G, R, O).

possible_preference_of_group_1( [], [], []).
possible_preference_of_group_1( [J|G], [R1|R], [(J,R1)|P]):-
   possible_preference_of_group_1( G, R, P),
   possible_preference_of_agent( J, R1, _).


possible_preference_pair( urd(2,3), (R1, R2),(O1,O2)):-
   possible_preference_of_group( [1,2], [R1,R2], [O1,O2]).



/*

?- setof(J,A^B^C^D^possible_preference_pair( H, (r(J),r(K)),_),
L),nl,write(H;K;L),fail.

urd(2, 3);1;[1, 2, 3, 4, 5, 6]
urd(2, 3);2;[1, 2, 3, 4, 5, 6]
urd(2, 3);3;[1, 2, 3, 4, 5, 6]
urd(2, 3);4;[1, 2, 3, 4, 5, 6]
urd(2, 3);5;[1, 2, 3, 4, 5, 6]
urd(2, 3);6;[1, 2, 3, 4, 5, 6]

No
?- 

*/


% pattern of preferences on binary comparisons
%-------------------------------------------------

bit_profile_of_preference_on_pair(_, [],[]).
bit_profile_of_preference_on_pair((X,Y), [Rj|R],[Bj|B]):-
   bit_profile_of_preference_on_pair((X,Y),R,B),
   (strictly_prefer_to(X,Y,Rj)->Bj=1;Bj=0).



% group/social choice set
%-------------------------------------------------
% It would be used for satisfies_Pareto_principle_2/2 below.

social_preference_profile(N, Rn, On):-
   set_of_agents(N), 
   possible_preference_of_group( N, Rn, On).

socially_choosing_maximals(R,Rn,C,Cn):-
   social_preference_profile(N, Rn,_),
   group_choice_set(N, Rn,Cn),
   possible_preference_ordering(R,_),
   group_choice_set(_,[R],C),
   subset(C,Cn).

group_choice_set(G,Rn,Cn):-
   % group(G) both in full or not.
   (\+ var(Rn) ->true
     ;possible_preference_of_group( G, Rn, _)
   ),
   findall( X,
    (
     member( Ra, Rn),
     maximal_element( X, Ra)
    ),
   Cn0),
   sort(Cn0,Cn).

/*

?- is_socially_choosing_maximals(R,Rn,C,Cn),Cn=[a],
nl,write(R;Rn;C;Cn),fail.

r(1);[r(1), r(1)];[a];[a]
r(2);[r(1), r(1)];[a];[a]
r(1);[r(2), r(1)];[a];[a]
r(2);[r(2), r(1)];[a];[a]
r(1);[r(1), r(2)];[a];[a]
r(2);[r(1), r(2)];[a];[a]
r(1);[r(2), r(2)];[a];[a]
r(2);[r(2), r(2)];[a];[a]

No
?- 

*/



% sample SWF for the unrestricted domain
%-------------------------------------------------

%social_welfare_function( urd(2,3), swf(auto)).
social_welfare_function( urd(2,3), swf(1)).
social_welfare_function( urd(2,3), swf(2)).
social_welfare_function( urd(2,3), swf(3)).

social_welfare_function( urd(2,3), swf(1),[r(J),R2]->r(J)):-
   possible_preference_of_group( [1,2], [r(J),R2], _).
social_welfare_function( urd(2,3), swf(2),[R1,r(K)]->r(K)):-
   possible_preference_of_group( [1,2], [R1,r(K)], _).
social_welfare_function( urd(2,3), swf(3),[r(J),r(K)]->r(L)):-
   possible_preference_of_group( [1,2], [r(J),r(K)], _),
   L is (K+J) mod 5 + 1.



% unanimity within a group
%-------------------------------------------------

solid_support_by_group( G, (X > Y), Rz):-
   support_members_in_group( G, G, (X > Y), Rz).

support_members_in_group( G, S, (X > Y), Rz):-
   group(G),
   alternative(X),
   alternative(Y),
   findall( J,
    (
     member(J,G),
     member((J,R),Rz),
     strictly_prefer_to(X,Y, R)
    ),
   S).

distinct_pair_of_alternatives(X,Y):-
   alternative(X),
   alternative(Y),
   X \= Y.


%  decisiveness for pair of alternatives
%-------------------------------------------------

is_decisive( urd(2,3), G, (X > Y), swf(K)):-
   social_welfare_function( urd(2,3), swf(K)),
   group(G),
   distinct_pair_of_alternatives(X,Y),
   forall(
    ( 
     social_welfare_function( urd(2,3), swf(K), [R1,R2]->R),
     solid_support_by_group( G, (X > Y), [(1,R1),(2,R2)])
    ),
    (
     strictly_prefer_to(X,Y, R)
    )
   ).

is_decisive( urd(2,3), G, (X, Y), swf(K)):-
   is_decisive( urd(2,3), G, (X > Y), swf(K)),
   is_decisive( urd(2,3), G, (Y > X), swf(K)).

/*

?- is_decisive( urd(2,3), [1,2], X, swf(1)),
X=(_,_),tab(2),write([X]),fail.
  [ (a, b)]  [ (a, c)]  [ (b, a)]  [ (b, c)]  [ (c, a)]  [ (c, b)]

No
?- is_decisive( urd(2,3), [1], X, swf(1)),
X=(_>_),tab(2),write([X]),fail.
  [a>b]  [a>c]  [b>a]  [b>c]  [c>a]  [c>b]

No
?- is_decisive( urd(2,3), [1], X, swf(1)),
X=(_,_),tab(2),write([X]),fail.
  [ (a, b)]  [ (a, c)]  [ (b, a)]  [ (b, c)]  [ (c, a)]  [ (c, b)]

No
?- is_decisive( urd(2,3), [2], X, swf(1)).

No
?-

*/

%  decisiveness of group
%-------------------------------------------------

is_decisive( urd(2,3), G, swf(K)):-
   group(G),
   social_welfare_function( urd(2,3), swf(K)),
   forall(
    (
     distinct_pair_of_alternatives(X,Y)
    ),
    (
     is_decisive( urd(2,3),G, (X, Y), swf(K))
    )
   ).

/*

?- is_decisive( urd(2,3), G, Swf).

G = [1]
Swf = swf(1) ;

G = [2]
Swf = swf(2) ;

G = [1, 2]
Swf = swf(1) ;

G = [1, 2]
Swf = swf(2) ;

No
?-

*/


%  dictatorship as decisiveness of singlton
%-------------------------------------------------

dictator_for_swf(Domain, Swf, J):-
   is_decisive( Domain, [J], Swf). 


%  the Pareto principle as decisiveness of everyone
%-------------------------------------------------

satisfies_Pareto_principle( Domain, Swf):-
   set_of_agents(N),
   is_decisive( Domain, N, Swf). 


/*

?- dictator_for_swf(Domain, swf(K), J).

Domain = urd(2, 3)
K = 1
J = 1 ;

Domain = urd(2, 3)
K = 2
J = 2 ;

No
?- satisfies_Pareto_principle( Domain, swf(K)).

Domain = urd(2, 3)
K = 1 ;

Domain = urd(2, 3)
K = 2 ;

No
?-

*/

%  another definition for the Pareto principle :
%  restriction to the socially maximal set
%-------------------------------------------------

satisfies_Pareto_principle_2( Domain, Swf):-
   social_welfare_function( Domain, Swf),
   forall(
    (
     possible_preference_pair( urd(2,3), (R1, R2),_)
    ),
    (
     social_welfare_function( Domain, Swf, [R1,R2]->R),
     is_subset_of_maximals( [R1,R2]->R)
    )
   ).


is_subset_of_maximals( Rn->R):-
   socially_choosing_maximals(R,Rn,_,_).


/*

?- satisfies_Pareto_principle( Domain, swf(K)),
\+ satisfies_Pareto_principle_2( Domain, swf(K)).

No
?- satisfies_Pareto_principle_2( Domain, swf(K)),
\+ satisfies_Pareto_principle( Domain, swf(K)).

No
?-

*/



% independent from irrelevant alternatives (IIA)
%-------------------------------------------------

iia_condition_of_swf(Swf,(X,Y)):-
   social_welfare_function( urd(2,3), Swf),
   distinct_pair_of_alternatives(X,Y),
   findall(B,
    (
     social_welfare_function( urd(2,3), Swf,R->F),
     bit_profile_of_preference_on_pair( (X,Y),[F|R],B)
    ),
   Lb),
   \+ \+ setof(Bf, member( [Bf|_],Lb),[_]).


iia_condition_of_swf(Swf):-
   social_welfare_function( urd(2,3), Swf),
   forall(
    (
     distinct_pair_of_alternatives(X,Y)
    ),
    (
     iia_condition_of_swf(Swf,(X,Y))
    )
   ).


/*

?- iia_condition_of_swf(Swf).

Swf = swf(1) ;

Swf = swf(2) ;

No
?- iia_condition_of_swf(swf(3),(X,Y)).

No
?- 

*/



%  automated designing SWFs recursively for the 2x3 
%  unrestricted domain with the IIA condition 
%-------------------------------------------------

:- dynamic auto_swf_0/4.

all_preference_pairs_in_urd23( Poss):-
   findall([R1,R2],
     possible_preference_pair( urd(2,3), (R1, R2),_),
   Poss).

auto_swf( urd(2,3), FL,Property):-
   abolish(auto_swf_0/4),
   all_preference_pairs_in_urd23( L),
   auto_swf( urd(2,3), FL, L, Property).

auto_swf( _, [],[], _).

auto_swf( Domain, [R->F | H], [R|Q], free):-
   auto_swf( Domain, H,Q,free),
   possible_preference_ordering(F, _).

auto_swf( Domain, [R->F | H], [R|Q], pareto):-
   auto_swf( Domain, H,Q,pareto),
   possible_preference_ordering(F, _),
   is_subset_of_maximals( R->F).

auto_swf( Domain, [R->F | H], [R|Q], iia(1)):-
   auto_swf( Domain, H,Q,iia(1)),
   possible_preference_ordering(F, _),
   \+ violates_iia( R->F, H, _).

auto_swf( Domain, H, [R], iia(2)):-
   auto_swf( Domain, H,[R],pareto).

auto_swf( Domain, [R->F | H], [R|Q], iia(2)):-
   auto_swf( Domain, H,Q,iia(2)),
   Q\=[],
   possible_preference_ordering(F, _),
   \+ violates_iia( R->F, H, _).

auto_swf( Domain, H, [R], iia(3)):-
   auto_swf( Domain, H,[R],pareto).

auto_swf( Domain, [R->F | H], [R|Q], iia(3)):-
   auto_swf( Domain, H,Q,iia(3)),
   Q\=[],
   possible_preference_ordering(F, _),
   is_subset_of_maximals( R->F),
   \+ violates_iia( R->F, H, _).

auto_swf( Domain, H, [R], iia(4)):-
   auto_swf( Domain, H,[R],pareto),
   assert( auto_swf_0(Domain,H,[R],iia(4))).

auto_swf( Domain, [R->F | H], [R|Q], iia(4)):-
   auto_swf( Domain, H,Q,iia(4)),
   Q\=[],
   possible_preference_ordering(F, _),
   is_subset_of_maximals( R->F),
   %is_weak_Paretian( R->F ),
   \+ violates_iia( R->F, H, _),
   assert( auto_swf_0(Domain,[R->F|H],[R|Q],iia(4))).


is_weak_Paretian( [R1,R2]->R):-
   set_of_agents(N),
   forall(
    (
     distinct_pair_of_alternatives(X,Y),
     solid_support_by_group( N, (X > Y), [(1,R1),(2,R2)])
    ),
     strictly_prefer_to(X,Y, R)
   ).

violates_iia( R->F, H, [(X,Y), B, B1]):-
   distinct_pair_of_alternatives(X,Y),
   bit_profile_of_preference_on_pair( (X,Y),[F|R],[B|Br]),
   member( R1->F1, H),
   bit_profile_of_preference_on_pair( (X,Y),[F1|R1],[B1|Br]),
   B  \= B1.

/*

?- auto_swf( Domain, H, free),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=3;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=4;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=5;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=6;[r(1), r(1), r(1), r(1), r(1), r(1)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] 

Yes
?- auto_swf( Domain, H, pareto),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=3;[r(1), r(1), r(3), r(3), r(3), r(3)]
row=4;[r(1), r(1), r(3), r(3), r(3), r(3)]
row=5;[r(1), r(1), r(3), r(3), r(5), r(5)]
row=6;[r(1), r(1), r(3), r(3), r(5), r(5)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] 

Yes
?- auto_swf( Domain, H, iia(1)),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=3;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=4;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=5;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=6;[r(1), r(1), r(1), r(1), r(1), r(1)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] 

Yes
?- auto_swf( Domain, H, iia(3)),
display_auto_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(2), r(2), r(2), r(2), r(2), r(2)]
row=3;[r(3), r(3), r(3), r(3), r(3), r(3)]
row=4;[r(4), r(4), r(4), r(4), r(4), r(4)]
row=5;[r(5), r(5), r(5), r(5), r(5), r(5)]
row=6;[r(6), r(6), r(6), r(6), r(6), r(6)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(2)), ([r(3), r(1)]->r(3)), ([r(4), r(1)]->r(4)), ([r(5), r(1)]->r(5)), ([r(6), r(...)]->r(6)), ([r(...)|...]->r(1)), ([...|...]->r(...)), (... ->...)|...] ;

row=1;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=2;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=3;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=4;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=5;[r(1), r(2), r(3), r(4), r(5), r(6)]
row=6;[r(1), r(2), r(3), r(4), r(5), r(6)]

Domain = urd(2, 3)
H = [ ([r(1), r(1)]->r(1)), ([r(2), r(1)]->r(1)), ([r(3), r(1)]->r(1)), ([r(4), r(1)]->r(1)), ([r(5), r(1)]->r(1)), ([r(6), r(...)]->r(1)), ([r(...)|...]->r(2)), ([...|...]->r(...)), (... ->...)|...] ;

No
?- 

*/


%  displaying swfs
%-------------------------------------------------

preprocess_for_display_swf(Swf,F):-
   social_welfare_function( urd(2,3), Swf),
   findall(
     [r(J),r(K)]->C,
     social_welfare_function( urd(2,3), Swf,[r(J),r(K)]->C),
     F
   ).

display_swf(Swf):-
   preprocess_for_display_swf(Swf,F),
   display_auto_swf(F).

display_swf_n(Swf):-
   preprocess_for_display_swf(Swf,F),
   display_auto_swf_n(F).



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

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

/*

?- display_swf(H).

row=1;[r(1), r(1), r(1), r(1), r(1), r(1)]
row=2;[r(2), r(2), r(2), r(2), r(2), r(2)]
row=3;[r(3), r(3), r(3), r(3), r(3), r(3)]
row=4;[r(4), r(4), r(4), r(4), r(4), r(4)]
row=5;[r(5), r(5), r(5), r(5), r(5), r(5)]
row=6;[r(6), r(6), r(6), r(6), r(6), r(6)]

H = swf(1) 

Yes
?- 

*/



/*

?- auto_swf( Domain, H, iia(4)),
display_auto_swf(H).

...
?- [menu].
% menu compiled 0.02 sec, 18,120 bytes

Yes
?- tell_goal( 'swf_b.csv',(
auto_swf_0( Domain, [R->F|H], [R|Q],iia(4)),
R=[r(K),r(J)],F=r(W),length(Q,N),nl,write((N,K,J,W)),fail)).

Domain = _G168
R = _G157
F = _G158
H = _G161
Q = _G164
K = _G173
J = _G178

W = _G186
N = _G192 

Yes
?- findall(1,auto_swf( Domain, H,[R],pareto),L),length(L,N).

Domain = _G163
H = _G164
R = _G160
L = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 120 

Yes
?- findall((K,J,W),(H=[[r(K),r(J)]->r(W)|_],
auto_swf( Domain, H,[R],pareto)),L),nth1(Q,L,(6,6,6)).

K = _G163
J = _G160
W = _G161
H = _G184
Domain = _G190
R = _G187
L = [ (1, 1, 1), (2, 1, 1), (3, 1, 1), (4, 1, 1), (5, 1, 1), (6, 1, 1), (1, 2, 1), (2, ..., ...), (..., ...)|...]
Q = 120 

Yes


*/

% end of the program