/************************************************************ Computing social welfare functions and distributing rights program: cswf08.pl language: prolog date: 2006.12.14.-21,24.( cswf06.pl) revised: 2007.10.29-31.( cswf07.pl) revised: 2008.5.7-14 & 19-25. & 6.5 & 22-27( cswf08.pl; minimal swf) revised: 2008.12.26. (debug: rr_cube_first_select/2) revised: 2010.3.21. (debug: rr_cube_first_select/2) creator: Kenryo INDO ************************************************************/ % to avoide multiplication on reload after model update. clear_agt:- (clause(agents(_),_)->abolish(agents/1);true). clear_trc:- (clause(track_arrow(_,_),_)->abolish(track_arrow/2);true). clear_cube:- (clause(cube_mode(_),_)->abolish(cube_mode/1);true). :- clear_agt,clear_trc,clear_cube. % load preference generator if r/1 does not exist. :- (\+ clause(r(_),_)->[gprf06];true). % set the initial domain. :- chdom(_->l:linear),display_domain. % members of society :- dynamic agents/1. agents([1,2]). j(X):- agents(N),member(X,N). make_n_agents(N):- clear_agt,length(L,N),findall(K,nth1(K,L,_),L),assert(agents(L)). model(states:A, agents:N):-alternatives(A),agents(N). model(states:A, agents:N,domain:D):-model(states:A, agents:N),domain_type(D). % possible types of swf values: % t(Q), l(Q), q(Q), a(Q), o(Q) in gprf06.pl. % profile : the domain of swf rr([R|Q],[_|N]):- rr(Q,N),r(R). rr([],[]). rr(QQ):- model(_,_:N),rr(QQ,N). r_j(J,PP,R):- rr(PP),j(J),nth1(J,PP,R). r_j(-J,PP,R,QL):- r_j(J,PP,R), findall(Q,(r_j(K,PP,Q),K\=J),QL). rr_b(_,[],[]). rr_b(XY,[A|B],[Q|R]):- rr_b(XY,B,R),rb(A,XY,Q). % rr/1: The list of all profiles :- dynamic all_rr/1,rrgrr_mode/0. clear_arr:- clause(all_rr(_),_),abolish(all_rr/1),fail. clear_arr. init_arr:- clear_arr, assert((all_rr(L):- \+ clause(rrgrr_mode,_),!,findall(QQ,rr(QQ),L))), assert((all_rr(L):- rrgrr_mode,rr_cube_first_all_rr(L))). :- init_arr. % rrgrr(on): accelarator for proving Arrow's theorem.(below) % SWF (Social Welfare Function, or Aggregated Social Ordering) swf([],[],_). swf([RR->Q|F],[RR|L],X):- swf(F,L,X),axiom_swf(X,RR->Q,F). swf(F,X):-all_rr(L),swf(F,L,X). save_trc:- tell_goal('trace_arrow_n.txt',forall,track_arrow(_,_)). % axioms for SWF % SWF is a function which decides a social ordering for each profile. % In Arrow's theorem, which derives only dictatorial rules, % the following conditions are assumed: % the iia condition and the Pareto condition, as well as % the tansitivity and unrestrictedness for orderings % both in the domain and region of SWF. And the theorems % which generalize Arrow's theorem modifies some of these conditions. axiom_swf(iia,RR->Q,F):- r(Q),iia(RR->Q,F). axiom_swf(pareto,RR->Q,_):- r(Q), pareto(RR->Q). axiom_swf(arrow,RR->Q,F):- r(Q),t(Q),pareto(RR->Q),iia(RR->Q,F). axiom_swf(wilson,RR->Q,F):- r(Q),t(Q),iia(RR->Q,F). axiom_swf(sen,RR->Q,F):- q(Q),pareto(RR->Q),iia(RR->Q,F). axiom_swf(iia(T),RR->Q,F):- r(Q,_,_,T), iia(RR->Q,F). axiom_swf(pareto(T),RR->Q,_):- r(Q,_,_,T), pareto(RR->Q). axiom_swf(arrow(T),RR->Q,F):- r(Q,_,_,T), pareto(RR->Q),iia(RR->Q,F). axiom_swf(wilson(T),RR->Q,F):- r(Q,_,_,T), iia(RR->Q,F). axiom_swf(bnom,RR->Q,_):- bnom(RR->Q). % a binominating rule. axiom_swf(olig(C),RR->Q,_):- q(Q), oligarchy(C,[RR->Q]). axiom_swf(decisive(B),RR->Q,_):- r(Q),decisive(B,RR->Q). axiom_swf(rights(B),RR->Q,_):- r(Q),rights(B,RR->Q). axiom_swf(rights_p(B),RR->Q,_):- r(Q),rights(B,RR->Q),pareto(RR->Q). axiom_swf(rights_i(B),RR->Q,F):- r(Q),rights(B,RR->Q),iia(RR->Q,F). axiom_swf(na_decisive(L),RR->Q,F):- r(Q),na_decisive(L,RR->Q,F). axiom_swf(majority_2,RR->Q,_):- agents([_,_]),majority_2(RR->Q). axiom_swf(majority,RR->Q,_):- majority(RR->Q). axiom_swf(dict(J),RR->Q,_):- r(Q),dictator(J,[RR->Q]). axiom_swf(sdict(J),RR->Q,_):- r(Q),dictator_s(J,[RR->Q]). axiom_swf(adict(J),RR->Q,_):- r(Q),ad(J,[RR->Q]). % added: 8 May 2008 for May(1952)'s theorem. axiom_swf(anonymous(T),RR->Q,F):- r(Q,_,_,T), anonymous(RR->Q,F). axiom_swf(neutral(T),RR->Q,F):- r(Q,_,_,T), neutral(RR->Q,F). axiom_swf(pos_res(T),RR->Q,F):- r(Q,_,_,T), positive_response(RR->Q,F). axiom_swf(may,RR->Q,F):- r_type(T:_),axiom_swf(may(T,_),RR->Q,F). axiom_swf(may(T),RR->Q,F):- axiom_swf(may(T,_),RR->Q,F). axiom_swf(may(T,XYZ),RR->Q,F):- r(Q,_,_,T), subset(XYZ,[p,n,a]),axiom_swf(may_r(XYZ),RR->Q,F). axiom_swf(may_r([]),_,_). axiom_swf(may_r([X|YZ]),RQ,F):- axiom_swf(may_r(YZ),RQ,F), axiom_swf(may_1(X),RQ,F). axiom_swf(may_1(p),RR->Q,F):- positive_response(RR->Q,F). axiom_swf(may_1(n),RR->Q,F):- neutral(RR->Q,F). axiom_swf(may_1(a),RR->Q,F):- anonymous(RR->Q,F). axiom_swf(neu+any(T),RR->Q,F):-r(Q,_,_,T), neutral(RR->Q,F),anonymous(RR->Q,F). axiom_swf(neu+iia(T),RR->Q,F):- r(Q,_,_,T), neutral(RR->Q,F),iia(RR->Q,F). % Conditions for SWF % revised: 29-31 Oct 2007; 7-9 May 2008 % dictatorship dictator(J,F):- j(J),\+ (member(PP->R,F),r_j(J,PP,P),P \= R). dictator_s(J,F):-j(J),\+ (member(PP->R,F),r_j(J,PP,P),opposite(_,_,[R,P])). % Pareto condition :- dynamic par_mode/1. par_mode(w). pareto(RR->S):- par_mode(T),pareto_rule(T,RR->S). % weak Pareto (unanimity) pareto_rule(w,RR->Q):- \+ (dop(XY),agree(s,XY,RR),\+ p(XY,Q) % ,assert(track_arrow(p,RR)) % trace backtracks ). pareto_rule(uv,RR->Q):- \+ (dop(XY),agree(-,XY,RR),r(XY,Q)). % veto by unanimity pareto_rule(ss,RR->Q):- \+ (dop(XY),agree(+,XY,RR),\+ r(XY,Q)). pareto_rule(s,RR->Q):- \+ (dop(XY),agree(+,XY,RR),anti_par(XY,RR->Q)). anti_par(XY,_->Q):- \+ r(XY,Q). anti_par((X,Y),RR->Q):- \+ agree(+,(Y,X),RR),\+ p((X,Y),Q). %anti_par(XY,RR->Q):- \+ \+ (member(R,RR),p(XY,R)),\+ p(XY,Q). % using different types of Pareto condition. chpar(A->B):- update_rule(par_mode,A->B,pareto_rule). % Independence of irrelevant alternatives (IIA) iia(RR->R,F):- \+ (member(QQ->Q,F),dop(XY), is_same_profile_for_dop(XY,RR,QQ),opposite(_,XY,[R,Q]) % ,assert(track_arrow(iia,RR)) % trace backtracks ). is_same_profile_for_dop(_,[],[]). is_same_profile_for_dop(XY,[R|P],[S|Q]):- is_same_profile_for_dop(XY,P,Q),\+ opposite(_,XY,[R,S]). debug_iia(RR->R,QQ->S,XY,A):- nl,write(RR->R;QQ->S;[XY];A). agree(_,_,[]). agree(s,XY,[Q|R]):- agree(s,XY,R),p(XY,Q). agree(+,XY,[Q|R]):- agree(+,XY,R),r(XY,Q). agree(-,XY,[Q|R]):- agree(-,XY,R),\+ r(XY,Q). %agree(0,XY,[Q|R]):- agree(0,XY,R),i(XY,Q). opposite(_,_,[]). opposite(A,XY,[Q|R]):- A==s,agree(s,XY,R),\+ p(XY,Q). opposite(+,XY,[Q|R]):- agree(+,XY,R),\+ r(XY,Q). opposite(-,XY,[Q|R]):- agree(-,XY,R),r(XY,Q). % deviator in almost unanimous profile opposite(+,J,XY,QQ):- agree(-,XY,QL),r_j(-J,QQ,R,QL),r(XY,R). opposite(-,J,XY,QQ):- agree(+,XY,QL),r_j(-J,QQ,R,QL),\+ r(XY,R). % Other important conditions for social orderings % citizen's sovereignty cs(F):- forall(dop(XY),(member(_->S,F),r(XY,S))). % anti-dictatorship ad(J,F):- j(J),\+ (member(PP->R,F),r_j(J,PP,P),agree(s,_,[R,P])). % bi-nominating rule bnom([[],[]]->[]). bnom([[B|P],[C|R]]->[A|Q]):- bnom([P,R]->Q), member((B,C,A),[(+,-,0),(-,+,0),(+,+,+),(-,-,-)]). % oligarchy, vetoers, decisive group oligarchy(_,[]). oligarchy(C,[RR->Q|F]):- oligarchy(C,F),vetoers(C,RR->Q), \+ (dop(XY),\+ decisive_group(C,XY,RR->Q)). vetoers([],_). vetoers([J|C],RR->Q):- vetoers(C,RR->Q),a_veoter(J,RR->Q). a_veoter(J,RR->Q):- r_j(J,RR,R),\+ (p((X,Y),R),p((Y,X),Q)). decisive_group(C,XY,RR->Q):- forall( forall((member(J,C),r_j(J,RR,R)),p(XY,R)), p(XY,Q) ). % decisiveness (at a profile) for pairs to an individual decisive([]->_,_). decisive([XY|E]->J,[P,Q]->S):- decisive(E->J,[P,Q]->S), member(J:R,[1:P,2:Q]), \+ opposite(_,XY,[R,S]). % distribution of rights among individuals rights([],_). rights([XY->J|E],[P,Q]->S):- rights(E,[P,Q]->S), member(J:R,[1:P,2:Q]), \+ opposite(_,XY,[R,S]). % almost decisiveness (with a detector) a_decisive(XY,J,[P,Q]->S):- member(J:R:U,[1:P:Q,2:Q:P]), (opposite(_,XY,[R,U])-> \+ opposite(_,XY,[R,S]);true). % deter the almost decisiveness na_decisive(L,RR->Q,F):- subset(L,[p,i]), \+ a_decisive(_,_,RR->Q), (member(p,L)->pareto(RR->Q);true), (member(i,L)->iia(RR->Q,F);true). % simple majority principle majority_2([[],[]]->[]). majority_2([[T|P],[T|Q]]->[T|R]):-majority_2([P,Q]->R). majority_2([[T|P],[F|Q]]->[0|R]):-majority_2([P,Q]->R),T\=F. majority(QQ->R):- findall(XY,d_pair(XY),L), majority(L,QQ->R). majority([],_->[]). majority([XY|L],QQ->[S|R]):- majority(L,QQ->R),majority(S,XY,QQ). % revised: 05 Jul 2007 majority(S,XY,QQ):- d_pair(XY),length(QQ,N), count_ballot(XY,QQ->S,M1), cop(XY,YX), count_ballot(YX,QQ->S,M2), sign_majority(S,N,M1,M2). sign_majority(+,N,M1,M2):- N < 2 * M1,N >= 2 * M2, !. sign_majority(-,N,M1,M2):- N >= 2 * M1,N < 2 * M2, !. sign_majority(0,_,_,_). count_ballot(_,[]->_,0). count_ballot(XY,[R|Q]->S,K):- count_ballot(XY,Q->S,M), (r(XY,R)->B=1;B=0), K is M + B. cop((X,Y),(Y,X)). % added: 8-11 May 2008 for axiom_swf(may) % anonymity, neutrality, and positive responsiveness (strict monotonicity): % May (1952)'s characterization for simple majority rule. % anonymity anonymous(R->Q,F):- \+ is_affected_by_voting_order(R->Q,_,_,F). is_affected_by_voting_order(R->Q,XC,P->S,F):- member(P->S,F),interchange_a_pair(R,(2,XC),P), Q \= S. %nl,write(R->Q;XC;P->S). % interchange_a_pair/3 % note: it is not equivalent to subset(R,P) & subset(P,R). interchange_a_pair([],non,[]). interchange_a_pair([J|R],A,[J|P]):- interchange_a_pair(R,A,P). interchange_a_pair([J|R],(1,J,K),[K|P]):- interchange_a_pair(R,non,P), J \= K. interchange_a_pair([K|R],(2,J,K),[J|P]):- interchange_a_pair(R,(1,J,K),P), J \= K. % neutrality neutral(R->Q,F):- is_odd_function(R->Q,F). % \+ is_affected_by_naming_of_alternatives(R->Q,_,_,F). is_odd_function(R->S,F):- \+ is_not_odd_function(R->S,_,_,F). % D(-A) = -D(A) is_not_odd_function(R->S,XY,Q->T,F):- member(Q->T, F),d_pair(XY), rr_b(XY,A,R),rr_b(XY,B,Q),reverse_signs_in_list(A,B), % \+ (d_pair(WV),WV\=XY,rr_b(WV,O,R),rb(WV,E,Q),O\=E), rb(U,XY,S),rb(V,XY,T),\+ reverse_sign(U,V). % ,nl,write('debug#':XY:R->S;Q->T) % ,nl,write('debug#':XY:A->U;B->V) % D(--A) = D(A) is_not_odd_function(R->S,XY,Q->T,F):- member(Q->T, F),d_pair(XY), rr_b(XY,A,R),rr_b(XY,A,Q),rb(U,XY,S),\+ rb(U,XY,T). reverse_signs_in_list([],[]). reverse_signs_in_list([A|R],[B|Q]):- reverse_signs_in_list(R,Q), reverse_sign(A,B). reverse_sign(+,-). reverse_sign(-,+). reverse_sign(0,0). % % another construction for neutrality: % is_affected_by_naming_of_alternatives/4 (under debugging) is_affected_by_naming_of_alternatives(R->Q,XY:Z,P->S,F):- member(P->S,F), dop(XY),interchange_alt_names(Z,XY,R,P), \+ interchange_alt_names(Z,XY,[Q],[S]). interchange_alt_names(-,XY,Q,R):- rr_b(XY,A,Q),rr_b(XY,A,R),!. interchange_alt_names(+,XY,Q,R):- rr_b(XY,A,Q),rr_b(XY,B,R),reverse_signs_in_list(A,B). % test code test_neutrality(P->S,Q->T,odd-naa(NAA)):- rr(P),!,rr(Q),P\=Q,r(S),r(T),F=[Q->T], is_odd_function(P->S,F), is_affected_by_naming_of_alternatives(P->S,NAA,Q->T,F). test_neutrality(P->S,Q->T,naa-odd(XY)):- rr(P),!,rr(Q),r(S),r(T),F=[Q->T], is_not_odd_function(P->S,XY,Q->T,F), \+ is_affected_by_naming_of_alternatives(P->S,_,Q->T,F). /* 686 ?- test_neutrality(R->Q,P->S,naa-CD). fail. 687 ?- test_neutrality(R->Q,P->S,odd-CD). fail. */ % positive responsiveness (strict monotonicity) % See Sen (1982), Chapter 8, Section 3. positive_response(R->Q,F):- \+ ( member(P->S,F), unilateral_change_in_rr(P,A->B,R), dop(XY), no_positive_response(XY,A,B,S,Q) % ,nl,write('debug#':XY:R->Q;P->S) ). % unilateral_change_in_rr/3 (debug 10 May 2008) unilateral_change_in_rr([],non,[]). unilateral_change_in_rr([A|R],A->B,[B|R]):- A\=B,!, unilateral_change_in_rr(R,non,R). unilateral_change_in_rr([A|R],C,[A|Q]):- unilateral_change_in_rr(R,C,Q). no_positive_response(XY,A,B,S,Q):- raise_vote_to_xy(XY,A->B),r(XY,S),\+ p(XY,Q). no_positive_response(XY,A,B,S,Q):- raise_vote_to_xy(XY,B->A),r(XY,Q),\+ p(XY,S). raise_vote_to_xy((X,Y),A->B):- i((X,Y),A), p((X,Y),B). raise_vote_to_xy((X,Y),A->B):- p((Y,X),A), r((X,Y),B). %----- % rrgrr: accelarator for proving Arrow's theorem % by re-arranging arguments the minimal profiles in all_rr/1. % (2008.5.11-21) % rrgrr(on): accelarator for proving Arrow's theorem for n=2 or more. % rrgrr(off): rrgrr_mode. rrgrr(off):- abolish(rrgrr_mode/0). rrgrr(on):- clause(rrgrr_mode,_),!. rrgrr(on):- assert(rrgrr_mode). % rrgrr mode: % realign all profile(rr/1)s so that each of which is a vertex of % the rr_cube, which is a minimal profiles of two-agent Arrow's SWF, % by means of simulating N-1 subgroup unanimity (sg_unan). rr_cube_first_all_rr(L):- cube_mode(N), rr_cube_first_select(M,N), findall(R,rr(R),L0),subtract(L0,M,P),append(P,M,L). :- dynamic cube_mode/1. cube_mode(1). cube_rule(4,intermediate_cube). cube_rule(1,hyper_plane_cube). cube_rule(2,unan_after_2). cube_rule(3,sort_by_cube). cube_rule(0,no_use). chcube(A->B):- rule_update(cube_mode,A->B,cube_rule/2). % versions rr_cube_first_select([],0). rr_cube_first_select(M,N):- (N=1-> hyper_plane_cube(M);true), % almost same (N=2-> rr_cube_first(1,M);true), % slower (N=3-> rr_cube_first(M);true), % slower % (N=4-> rr_cube_first(M);fail). % minimal % revised: 26 Dec 2008 (N=4-> rr_cube_first(M);true). % minimal % revised: 21 Mar 2010 % 21-22 May; 5 Jun 2008 hyper_plane_cube(M):- agents(N),hyper_plane_cube(N,M),!. hyper_plane_cube([],[]). hyper_plane_cube([J|N],M):- hyper_plane_cube(N,M0),rr_cube_first(J,Mj),union(M0,Mj,M). % revised: 6.27(6.22) added all_rr_cube/1 and modified rr_cube_first/1. all_rr_cube(C):- domain_type(Y:_), dp_mode(I), setof(K:X,rr_cube(dp(I,Y),K,X),L), findall(X,member(_:X,L),C). rr_cube_members(M,L):- dp_mode(I),domain_type(Y:_), findall([P,Q|R],(rr_cube(dp(I,Y),_,[P,Q]),member([P,Q|R],L)),M). rr_cube_first(M):- intermediate_cube_mode(4), all_rr_cube(M). rr_cube_first(M):- \+ intermediate_cube_mode(4), dp_mode(I),domain_type(Y:_), findall([P,Q|R],(rr_cube(dp(I,Y),_,[P,Q]),rr([P,Q|R])),M). % rr_cube_first(J,M):- dp_mode(I),domain_type(Y:_), findall((K,[P,Q]),(rr_cube(dp(I,Y),K,[P,Q])),L0), sort(L0,L), rr_cube_first(J,M,I,Y,L). rr_cube_first(_,[],_,_,[]). rr_cube_first(J,[RR|M],I,Y,[(_K,[P,Q])|L]):- rr_cube_first(J,M,I,Y,L), % rr_cube(dp(I,Y),K,[P,Q]), r(P),r(Q), rr_unan_except_for_j(J,P,RR,Q). rr_cube_first(J,M,I,Y,[(_,[P,Q])|L]):- rr_cube_first(J,M,I,Y,L), \+ (r(P),r(Q)). rr_unan_except_for_j(J,P,RR,Q):- r_j(-J,RR,P,QL),sort(QL,[Q]). % Vertex of the cube represention. % a minimal subset of profiles to prove Arrow's theorem. rr_cube(dp(2,l),1,[[-,+,+],[+,+,-]]). rr_cube(dp(2,l),2,[[-,-,+],[-,+,-]]). rr_cube(dp(2,l),3,[[+,-,+],[-,+,+]]). rr_cube(dp(2,l),4,[[+,-,-],[-,-,+]]). rr_cube(dp(2,l),5,[[+,+,-],[+,-,+]]). rr_cube(dp(2,l),6,[[-,+,-],[+,-,-]]). rr_cube(dp(2,Y),K,P):- Y\=l,rr_cube(dp(2,l),M,P),K is 2*(M-1)+1. rr_cube(dp(2,Y),0,P):- Y\=l,intermediate_cube_mode(5),rr_zero(P). rr_cube(dp(2,Y),K,R):- Y\=l,cube_mode(4), rr_cube(dp(2,l),M,P),L is mod(M,6)+1, rr_cube(dp(2,l),L,Q),rr_between(P,Q,R),K is 2*(M-1)+2. rr_cube(dp(1,Y),K,R):- rr_cube(dp(2,Y),K,P),convert_rr_cube_2_to_1(1:R,2:P). rr_zero([[0,0,0],[0,0,0]]). convert_rr_cube_2_to_1(Vertex_A,Vertex_B):- Vertex_A= 1:[[P,Q,R],[S,T,U]], Vertex_B= 2:[[P,R,V],[S,U,W]], reverse_sign(V,Q),reverse_sign(W,T). % chcube(_->4) is required. % :- dynamic intermediate_cube_mode/1. intermediate_cube_mode(3). between_rule(1). between_rule(2). between_rule(3). % both between_rule(4). % minimal between_rule(5). % zero + linear(-1sg_unan) chbetween(A->B):- rule_update(intermediate_cube_mode,A->B,between_rule/1). rr_between(P,Q,R):- rr_between_1(P,Q,R),R\=P.% It is not guaranteed that RR=[X,Y],r(X),r(Y). rr_between_1([[],[]],[[],[]],[[],[]]). rr_between_1([[X|P],[Y|Q]],[[Z|R],[W|S]],[[A|T],[B|U]]):- rr_between_1([P,Q],[R,S],[T,U]), r_between([X,Y],[Z,W],[A,B]). % r_between_1 is minimal. % r_between_2 is not minimal. % revised: 23-24 May 2008; 27(22) Jun 2008 r_between(A,_,A):- \+ (intermediate_cube_mode(I),I>3). % r_between(A,B,C):- intermediate_cube_mode(N),N>1,N=<3,r_between_2(a,A,B,C). % r_between(A,B,C):- \+ intermediate_cube_mode(2),r_between_1(a,A,B,C). % r_between(A,B,C):- intermediate_cube_mode(4),member(Y,[b,c]),r_between_1(Y,A,B,C). % r_between(A,B,C):- intermediate_cube_mode(5),member(Y,[b,c]),r_between_1(Y,A,B,C). % % minimal profiles (rule 1 with rr_zero) r_between_1(a,[X,Y],[X,Z],[X,0]):- Y\=Z. r_between_1(b,[X,Y],[X,Y],[X,Y]). r_between_1(c,[X,Y],[W,Y],[0,Y]):- X\=W. r_between_2(a,[X,Y],[X,Y],[0,Y]). %r_between_2(b,[X,Y],[X,Y],[0,0]). %r_between_2(c,[X,Y],[X,Y],[X,0]). %r_between_2(d,[X,Y],[Z,W],[X,Y]):- \+ (X=Z,Y=W). /* % 24 May 2008 ?- [menu,cswf08]. ?- chdom(_->t:_),chbetween(_->5),chcube(_->4). % %I = l:linear->t:transitive ?- rr_zero(Z),rr_cube_first(M),stopwatch((swf(F,[Z|M],arrow),display_swf_t6(F),fail);true,Time). a, b + 0 - + [+] [+] [+] 0 [0] [0] [0] - [-] [-] [-] a, c + 0 - + [+] [+] [+] 0 [0] [0] [0] - [-] [-] [-] b, c + 0 - + [+] [+] [+] 0 [0] [0] [0] - [-] [-] [-] ---end of swf --- a, b + 0 - + [+] [0] [-] 0 [+] [0] [-] - [+] [0] [-] a, c + 0 - + [+] [0] [-] 0 [+] [0] [-] - [+] [0] [-] b, c + 0 - + [+] [0] [-] 0 [+] [0] [-] - [+] [0] [-] ---end of swf --- % time elapsed (sec): 11.562 Z = [[0, 0, 0], [0, 0, 0]] M = [[[-, -, +], [+, +, +]], [[-, -, -], [-, +, +]], [[+, -, -], [-, -, +]], [[+, +, -], [-, -, -]], [[+, +, +], [+, -|...]], [[-, +|...], [+|...]], [[-|...], [...|...]], [[...|...]|...], [...|...]|...] F = _G167 Time = 11.562 Yes ?- */ %--------------- % recursive decomposition of SWF based on subgroup unanimity % virtually extendes 2-agent SWF up to N-agent SWF (or conversly reducing). % (2008.5.11-16,18-19) template_swf([],[]). template_swf([R->_|F],[R|L]):- template_swf(F,L). rdsu_swf(F,X):- all_rr(L),rdsu_swf(F,L,X). rdsu_swf(F,L,X):- agents(N),template_swf(F,L),rdsu_swf(F,X,N,[]). rdsu_swf(_,_,[],_). rdsu_swf(F,X,[J|N],M):- rdsu_swf(F,X,N,[J|M]), nl,write('challenge for sg unan':[J|M]), G=swf_sg_unan(F,X,[J|M]), stopwatch(G,_Time). % confined to subgroup unanimous profiles. rr_sg_unan([],_,_). rr_sg_unan([J|N],R,Q):-rr_sg_unan(N,R,Q),r_j(J,R,Q). %all_rr_sg_unan(+SubGroup,+AllProfiles,-UnanProfiles) all_rr_sg_unan(N,U):- all_rr(L),all_rr_sg_unan(N,L,U). all_rr_sg_unan([],U,U):- all_rr(U). %all_rr_sg_unan(N,L,U):- N\=[],findall(R,(r(Q),member(R,L),rr_sg_unan(N,R,Q)),U). all_rr_sg_unan(_,[],[]). all_rr_sg_unan(N,[R|L],[R|U]):- rr_sg_unan(N,R,_),all_rr_sg_unan(N,L,U). all_rr_sg_unan(N,[R|L],U):- \+ rr_sg_unan(N,R,_),all_rr_sg_unan(N,L,U). swf_sg_unan(F,X,[_]):- swf(F,X). swf_sg_unan(F,X,N):- N=[_,_|_], all_rr(L),agents(I),subset(N,I),swf_sg_unan(F,L,X,N). swf_sg_unan(F,L,X,M):- swf_sg_unan(F,L,X,M,_). swf_sg_unan(F,L,X,M,H):- all_rr_sg_unan(M,L,U),swf(H,U,X),ext_swf_dom(H,F). %ext_swf_dom_1(H,F):-ext_swf_dom(H,F),!. ext_swf_dom(_,[]). ext_swf_dom(H,[R->S|F]):- member(R->S,H),ext_swf_dom(H,F). ext_swf_dom(H,[R->S|F]):- \+ member(R->S,H),ext_swf_dom(H,F). % 25 May 2008 (ext_dom_swf/3 added) ext_swf_dom(_,[],[]). ext_swf_dom(H,[R|L],[R->S|F]):- member(R->S,H),ext_swf_dom(H,L,F). ext_swf_dom(H,[R|L],[R->S|F]):- \+ member(R->S,H),ext_swf_dom(H,L,F). /* 265 ?- ext_swf_dom([a->b,c->d],F,[a,b,c,d]). F = [ (a->b), (b->_G556), (c->d), (d->_G577)] . */ % displaying SWFs %------------------- % (1) simple table in symbols % changing default display of swf display_swf(F):-agents([_,_]),!,show_swf(F). display_swf(F):-agents([_,_,_|_]),!,display_swf_t6(F,v). show_swf(F):- \+ var(F),agents([1,2]), display_swf_header, hr(20), forall( id_r(_:I,P), ( an_swf_line(L,P,F), nl,write(P=I),tab(2),write('|'), write_sequence(L) ) ). display_swf_header:- bagof(N,K^R^id_r(K:N,R),L), nl,write('swf:row col |'), write_sequence(L). write_sequence(L):- forall(member(B,L),write(B)). hr(N):- length(L,N), nl, forall(member(_,L),write('-')). an_swf_line(L,P,F):- bagof(N, K^Q^R^B^( id_r(K:N,R,B), member([P,Q]->R,F) ),L). %------------------- % (2) a compound table in symbols + binaries display_swf_t2(F):- show_swf_ct(F). show_swf_ct(F):- \+ var(F),agents([1,2]), length(F,_), % bin_swf(Fxy,F), display_swf_header, forall(d_pair(XY),display_swf_header(XY)), hr(50), forall( ( id_r(_:I,P), an_swf_line(L,P,F), nl,write(P=I),write(' |'), write_sequence(L), d_pair(XY) ), display_swf_bb(XY,P,F) ). display_swf_header(XY):- b(XY), findall(T,(id_r(_,R),rb(T,XY,R)),L), tab(1),XY=(X,Y), write(X),write(Y),write(|), write_sequence(L). display_swf_bb(XY,P,F):- rb(T_row,XY,P), tab(2),write(T_row),write('|'), findall(T,( id_r(_,Q), member([P,Q]->R,F), rb(T,XY,R) ),L), write_sequence(L). %------------------- % (3) lined profiles in binaries display_swf_t3(F):-show_swf_l(F). display_swf_t3(XY,F):-show_swf_l(XY,F). show_swf_l(F):- \+ var(F), forall(j(J),write_component_wise_swf(_,[J],F)), write_component_wise_swf(_,soc,F). show_swf_l(XY,F):- \+ var(F), d_pair(XY), forall(j(J),write_component_wise_swf(XY,[J],F)), write_component_wise_swf(XY,soc,F). select_swf_component(_,[J],P,QQ->_):- r_j(J,QQ,P). select_swf_component(_,soc,P,_->P). write_component_wise_swf(XY,C,F):- forall(d_pair(XY),( nl,write(XY:C),write(:), forall(member(Element,F),( select_swf_component(XY,C,P,Element), rb(T,XY,P),write(T) )) )). %------------------- % (4) table for a pair in signs display_swf_t4(XY,F):-show_swf_b(XY,F). show_swf_b(XY,F):- \+ var(F),agents([1,2]), decompose_swf_into_tables(F,W), write_header_swf(XY,W,_), write_swf_contents(XY,W). decompose_swf_into_tables(F,W):- findall(J:L, bagof(C,K^member([J,K]->C,F),L),W). write_header_swf(XY,W,N):- length(W,N),length(H,N),d_pair(XY),nl,write(swf:wrt(XY)), tab(1),forall(nth1(K,H,_),(tab(2),write(r(K)))). write_swf_contents(XY,W):- d_pair(XY), forall(nth1(K,W,J:L),( nl,write(r(K)=J),write_each_swf_row_as_binary(XY,L) )). write_each_swf_row_as_binary(XY,L):- d_pair(XY), forall(member(R,L),(tab(5),rb(T,XY,R),write(T))). %------------------- % (5) lined profiles in alphabets ----vertical/horizontal display_swf_t5(F,v):-show_swf_v(F). display_swf_t5(F,l):-show_swf_la(F). show_swf_v(F):- \+ var(F),write('profile:'),tab(2), forall(j(J),(tab(2),write(J))),tab(2),write('swf'), write_profile_wise_swf(_,F),fail. show_swf_v(_):- nl,write('----'). write_profile_wise_swf(R->S,F):- member(R->S,F), nl,forall(member(P,R),(id_r(_:N,P),write(N))), id_r(_:N,S),tab(1),write('->'),write(N),write('.'). show_swf_la(F):- \+ var(F), forall(j(J),write_agent_wise_swf(_,[J],F)), write_agent_wise_swf(_,soc,F). write_agent_wise_swf(XY,C,F):- nl,write(C),write(:), forall(member(Element,F),( select_swf_component(XY,C,P,Element), id_r(_:N,P),write(N) )). %------------------- % (6) binary decomposition display_swf_t6(F):- decompose_swf(XY,F,Fxy), bagof(B,(U^V^sign_b(B,U,V),\+ \+ member([+,B]->C,Fxy)),COL), ROW=COL, nl,write(XY),forall(member(B,COL),(tab(4),write(B))), G1=member(B,COL), G2=member([A,B]->C,Fxy), member(A,ROW), nl,tab(4),write(A),forall(G1,(G2,tab(2),write(C))),fail. display_swf_t6(_):- nl,write('---end of swf ---'). display_swf_t6(F,v):- d_pair(XY),nl,write(XY), decompose_swf(XY,F,Fxy), member(G,Fxy),nl,write(G),fail. display_swf_t6(_,v):- nl,write('---end of swf ---'). % 24 May 2008 display_swf_t6(F,s) added. display_swf_t6(F,s):- findall(XY:R->S,( d_pair(XY),decompose_swf_1(XY,F,R->S) ),Fz), setof(R,XY^S^member(XY:R->S,Fz),Rz), findall(R->Sxy,XY^S^( member(R,Rz), findall(XY:S,(d_pair(XY),member(XY:R->S,Fz)),Sxy) ), Fxy), member(G,Fxy),nl,write(G),fail. display_swf_t6(_,s):- nl,write('---end of swf ---'). decompose_swf(XY,F,E):- % dop(XY), setof(C->H,decompose_swf_1(XY,F,C->H),E). decompose_swf_1(XY,F,C->H):- dop(XY), setof(B,Q^P^(member(P->Q,F),rr_b(XY,[B|C],[Q|P])),H). % bugfix of decompose_swf for n>= 3. (2008.5.19) /* decompose_swf(_,[],[]). decompose_swf(XY,[P->Q|F],E):- decompose_swf(XY,F,D), dop(XY),% d_pair(XY), rr_b(XY,[B|C],[Q|P]), % by d_pair add_to_decompose_swf(C->B,D,E). add_to_decompose_swf(C->B,D,D):- member(C->B,D),!. add_to_decompose_swf(C->B,D,E):- member(C->F,D),!, union(F,[B],G),subtract(D,[C->F],H),union([C->G],H,E). add_to_decompose_swf(C->B,D,E):- union([C->[B]],D,E). */ %----- % demo % impossibility theorems (Arrow-Wilson) and % a possibility theorem (Sen) /* ?- swf(F,dict(J)),nl,display_swf(F),fail. swf:row col |ACITZN -------------------- [+, +, +]=A |AAAAAA [-, +, +]=C |CCCCCC [-, -, +]=I |IIIIII [+, +, -]=T |TTTTTT [+, -, -]=Z |ZZZZZZ [-, -, -]=N |NNNNNN swf:row col |ACITZN -------------------- [+, +, +]=A |ACITZN [-, +, +]=C |ACITZN [-, -, +]=I |ACITZN [+, +, -]=T |ACITZN [+, -, -]=Z |ACITZN [-, -, -]=N |ACITZN No ?- swf(F,arrow),nl,display_swf(F),fail. swf:row col |ACITZN -------------------- [+, +, +]=A |AAAAAA [-, +, +]=C |CCCCCC [-, -, +]=I |IIIIII [+, +, -]=T |TTTTTT [+, -, -]=Z |ZZZZZZ [-, -, -]=N |NNNNNN swf:row col |ACITZN -------------------- [+, +, +]=A |ACITZN [-, +, +]=C |ACITZN [-, -, +]=I |ACITZN [+, +, -]=T |ACITZN [+, -, -]=Z |ACITZN [-, -, -]=N |ACITZN No ?- chdom(A). A = l:linear->t:transitive Yes ?- swf(F,dict(J)),nl,display_swf(F),fail. swf:row col |ABCFIJOSTWZnN -------------------- [+, +, +]=A |AAAAAAAAAAAAA [0, +, +]=B |BBBBBBBBBBBBB [-, +, +]=C |CCCCCCCCCCCCC [-, 0, +]=F |FFFFFFFFFFFFF [-, -, +]=I |IIIIIIIIIIIII [+, +, 0]=J |JJJJJJJJJJJJJ [0, 0, 0]=O |OOOOOOOOOOOOO [-, -, 0]=S |SSSSSSSSSSSSS [+, +, -]=T |TTTTTTTTTTTTT [+, 0, -]=W |WWWWWWWWWWWWW [+, -, -]=Z |ZZZZZZZZZZZZZ [0, -, -]=n |nnnnnnnnnnnnn [-, -, -]=N |NNNNNNNNNNNNN swf:row col |ABCFIJOSTWZnN -------------------- [+, +, +]=A |ABCFIJOSTWZnN [0, +, +]=B |ABCFIJOSTWZnN [-, +, +]=C |ABCFIJOSTWZnN [-, 0, +]=F |ABCFIJOSTWZnN [-, -, +]=I |ABCFIJOSTWZnN [+, +, 0]=J |ABCFIJOSTWZnN [0, 0, 0]=O |ABCFIJOSTWZnN [-, -, 0]=S |ABCFIJOSTWZnN [+, +, -]=T |ABCFIJOSTWZnN [+, 0, -]=W |ABCFIJOSTWZnN [+, -, -]=Z |ABCFIJOSTWZnN [0, -, -]=n |ABCFIJOSTWZnN [-, -, -]=N |ABCFIJOSTWZnN No ?- swf(F,arrow),nl,display_swf(F),fail. swf:row col |ABCFIJOSTWZnN -------------------- [+, +, +]=A |AAAAAAAAAAAAA [0, +, +]=B |BBBBBBBBBBBBB [-, +, +]=C |CCCCCCCCCCCCC [-, 0, +]=F |FFFFFFFFFFFFF [-, -, +]=I |IIIIIIIIIIIII [+, +, 0]=J |JJJJJJJJJJJJJ [0, 0, 0]=O |OOOOOOOOOOOOO [-, -, 0]=S |SSSSSSSSSSSSS [+, +, -]=T |TTTTTTTTTTTTT [+, 0, -]=W |WWWWWWWWWWWWW [+, -, -]=Z |ZZZZZZZZZZZZZ [0, -, -]=n |nnnnnnnnnnnnn [-, -, -]=N |NNNNNNNNNNNNN swf:row col |ABCFIJOSTWZnN -------------------- [+, +, +]=A |ABCFIJOSTWZnN [0, +, +]=B |ABCFIJOSTWZnN [-, +, +]=C |ABCFIJOSTWZnN [-, 0, +]=F |ABCFIJOSTWZnN [-, -, +]=I |ABCFIJOSTWZnN [+, +, 0]=J |ABCFIJOSTWZnN [0, 0, 0]=O |ABCFIJOSTWZnN [-, -, 0]=S |ABCFIJOSTWZnN [+, +, -]=T |ABCFIJOSTWZnN [+, 0, -]=W |ABCFIJOSTWZnN [+, -, -]=Z |ABCFIJOSTWZnN [0, -, -]=n |ABCFIJOSTWZnN [-, -, -]=N |ABCFIJOSTWZnN No ?- chdom(A). A = t:transitive->l:linear Yes ?- ?- [menu]. % menu compiled 0.00 sec, 0 bytes Yes ?- stopwatch((swf(F,arrow),nl,display_swf_t2(F),fail;true),T). swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ACITZN +|+--++- +|++-+-- +|+++--- [-, +, +]=C |ACITZN -|+--++- +|++-+-- +|+++--- [-, -, +]=I |ACITZN -|+--++- -|++-+-- +|+++--- [+, +, -]=T |ACITZN +|+--++- +|++-+-- -|+++--- [+, -, -]=Z |ACITZN +|+--++- -|++-+-- -|+++--- [-, -, -]=N |ACITZN -|+--++- -|++-+-- -|+++--- swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |AAAAAA +|++++++ +|++++++ +|++++++ [-, +, +]=C |CCCCCC -|------ +|++++++ +|++++++ [-, -, +]=I |IIIIII -|------ -|------ +|++++++ [+, +, -]=T |TTTTTT +|++++++ +|++++++ -|------ [+, -, -]=Z |ZZZZZZ +|++++++ -|------ -|------ [-, -, -]=N |NNNNNN -|------ -|------ -|------ % time elapsed (sec): 0.797 F = _G157 T = 0.797 Yes ?- stopwatch((swf(F,wilson),cs(F),nl,display_swf_t2(F),fail;true),T). swf:row col |ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ACITZN +|-++--+ +|--+-++ +|---+++ [-, +, +]=C |ACITZN -|-++--+ +|--+-++ +|---+++ [-, -, +]=I |ACITZN -|-++--+ -|--+-++ +|---+++ [+, +, -]=T |ACITZN +|-++--+ +|--+-++ -|---+++ [+, -, -]=Z |ACITZN +|-++--+ -|--+-++ -|---+++ [-, -, -]=N |ACITZN -|-++--+ -|--+-++ -|---+++ swf:row col |ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |NNNNNN +|------ +|------ +|------ [-, +, +]=C |ZZZZZZ -|++++++ +|------ +|------ [-, -, +]=I |TTTTTT -|++++++ -|++++++ +|------ [+, +, -]=T |IIIIII +|------ +|------ -|++++++ [+, -, -]=Z |CCCCCC +|------ -|++++++ -|++++++ [-, -, -]=N |AAAAAA -|++++++ -|++++++ -|++++++ swf:row col |ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |AAAAAA +|++++++ +|++++++ +|++++++ [-, +, +]=C |CCCCCC -|------ +|++++++ +|++++++ [-, -, +]=I |IIIIII -|------ -|------ +|++++++ [+, +, -]=T |TTTTTT +|++++++ +|++++++ -|------ [+, -, -]=Z |ZZZZZZ +|++++++ -|------ -|------ [-, -, -]=N |NNNNNN -|------ -|------ -|------ swf:row col |ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ACITZN +|+--++- +|++-+-- +|+++--- [-, +, +]=C |ACITZN -|+--++- +|++-+-- +|+++--- [-, -, +]=I |ACITZN -|+--++- -|++-+-- +|+++--- [+, +, -]=T |ACITZN +|+--++- +|++-+-- -|+++--- [+, -, -]=Z |ACITZN +|+--++- -|++-+-- -|+++--- [-, -, -]=N |ACITZN -|+--++- -|++-+-- -|+++--- % time elapsed (sec): 17.078 F = _G160 T = 17.078 Yes ?- stopwatch((swf(F,sen),nl,display_swf_t2(F),fail;true),T). swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ACITZN +|+--++- +|++-+-- +|+++--- [-, +, +]=C |ACITZN -|+--++- +|++-+-- +|+++--- [-, -, +]=I |ACITZN -|+--++- -|++-+-- +|+++--- [+, +, -]=T |ACITZN +|+--++- +|++-+-- -|+++--- [+, -, -]=Z |ACITZN +|+--++- -|++-+-- -|+++--- [-, -, -]=N |ACITZN -|+--++- -|++-+-- -|+++--- swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ABEJMO +|+00++0 +|++0+00 +|+++000 [-, +, +]=C |BCFKOP -|0--00- +|++0+00 +|+++000 [-, -, +]=I |EFIORS -|0--00- -|00-0-- +|+++000 [+, +, -]=T |JKOTWX +|+00++0 +|++0+00 -|000--- [+, -, -]=Z |MORWZn +|+00++0 -|00-0-- -|000--- [-, -, -]=N |OPSXnN -|0--00- -|00-0-- -|000--- swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |AAAAAA +|++++++ +|++++++ +|++++++ [-, +, +]=C |CCCCCC -|------ +|++++++ +|++++++ [-, -, +]=I |IIIIII -|------ -|------ +|++++++ [+, +, -]=T |TTTTTT +|++++++ +|++++++ -|------ [+, -, -]=Z |ZZZZZZ +|++++++ -|------ -|------ [-, -, -]=N |NNNNNN -|------ -|------ -|------ % time elapsed (sec): 3.75 F = _G157 T = 3.75 Yes ?- swf(F,bnom),display_swf_t2(F),fail. swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ABEJMO +|+00++0 +|++0+00 +|+++000 [-, +, +]=C |BCFKOP -|0--00- +|++0+00 +|+++000 [-, -, +]=I |EFIORS -|0--00- -|00-0-- +|+++000 [+, +, -]=T |JKOTWX +|+00++0 +|++0+00 -|000--- [+, -, -]=Z |MORWZn +|+00++0 -|00-0-- -|000--- [-, -, -]=N |OPSXnN -|0--00- -|00-0-- -|000--- No ?- */ % verify above result is the oligarchy. /* ?- member(G,[[1,2],[1],[2]]),swf(F,olig(G)),display_swf_t2(F),nl,fail. swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ABEJMO +|+00++0 +|++0+00 +|+++000 [-, +, +]=C |BCFKOP -|0--00- +|++0+00 +|+++000 [-, -, +]=I |EFIORS -|0--00- -|00-0-- +|+++000 [+, +, -]=T |JKOTWX +|+00++0 +|++0+00 -|000--- [+, -, -]=Z |MORWZn +|+00++0 -|00-0-- -|000--- [-, -, -]=N |OPSXnN -|0--00- -|00-0-- -|000--- swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |AAAAAA +|++++++ +|++++++ +|++++++ [-, +, +]=C |CCCCCC -|------ +|++++++ +|++++++ [-, -, +]=I |IIIIII -|------ -|------ +|++++++ [+, +, -]=T |TTTTTT +|++++++ +|++++++ -|------ [+, -, -]=Z |ZZZZZZ +|++++++ -|------ -|------ [-, -, -]=N |NNNNNN -|------ -|------ -|------ swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ACITZN +|+--++- +|++-+-- +|+++--- [-, +, +]=C |ACITZN -|+--++- +|++-+-- +|+++--- [-, -, +]=I |ACITZN -|+--++- -|++-+-- +|+++--- [+, +, -]=T |ACITZN +|+--++- +|++-+-- -|+++--- [+, -, -]=Z |ACITZN +|+--++- -|++-+-- -|+++--- [-, -, -]=N |ACITZN -|+--++- -|++-+-- -|+++--- No ?- */ % verify that above nondictatorship (origarchy) is the pairwise majority vote. /* ?- stopwatch((swf(F,majority),display_swf_t2(F),fail;true),T). swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ABEJMO +|+00++0 +|++0+00 +|+++000 [-, +, +]=C |BCFKOP -|0--00- +|++0+00 +|+++000 [-, -, +]=I |EFIORS -|0--00- -|00-0-- +|+++000 [+, +, -]=T |JKOTWX +|+00++0 +|++0+00 -|000--- [+, -, -]=Z |MORWZn +|+00++0 -|00-0-- -|000--- [-, -, -]=N |OPSXnN -|0--00- -|00-0-- -|000--- % time elapsed (sec): 0.0320001 F = _G160 T = 0.0320001 Yes ?- */ % verifying the decomposability of decisiveness % (or the possibility of distributing individual rights) /* ?- swf(F,rights([(a,b)->1,(a,c)->2])),display_swf_t2(F),!,fail. swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |AAAZZZ +|++++++ +|++-+-- +|++-+-- [-, +, +]=C |CCCIII -|------ +|++-+-- +|++++++ [-, -, +]=I |CCCIII -|------ -|++-+-- +|++++++ [+, +, -]=T |AAAZZZ +|++++++ +|++-+-- -|++-+-- [+, -, -]=Z |AAAZZZ +|++++++ -|++-+-- -|++-+-- [-, -, -]=N |CCCIII -|------ -|++-+-- -|++++++ No ?- swf(F,rights([(a,b)->1,(a,c)->J,(b,c)->K])),display_swf_t2(F),nl,write([J:K]),fail. swf: row col|ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |AAAAAA +|++++++ +|++++++ +|++++++ [-, +, +]=C |CCCCCC -|------ +|++++++ +|++++++ [-, -, +]=I |IIIIII -|------ -|------ +|++++++ [+, +, -]=T |TTTTTT +|++++++ +|++++++ -|------ [+, -, -]=Z |ZZZZZZ +|++++++ -|------ -|------ [-, -, -]=N |NNNNNN -|------ -|------ -|------ [1:1] No ?- chdom(A). A = l:linear->t:transitive Yes ?- swf(F,rights([(a,b)->1,(a,c)->2])),display_swf_t2(F),!,fail. swf:row col |ABCFIJOSTWZnN ab|+0---+0-+++0- ac|+++0-+0-+0--- bc|+++++000----- -------------------------------------------------- [+, +, +]=A |AAAAAAAAZZZZZ +|+++++++++++++ +|++++-++-++--- +|++++-++-++--- [0, +, +]=B |AAAAAAAAZZZZZ 0|+++++++++++++ +|++++-++-++--- +|++++-++-++--- [-, +, +]=C |CCCCCCCCIIIII -|------------- +|++++-++-++--- +|+++++++++++++ [-, 0, +]=F |CCCCCCCCIIIII -|------------- 0|++++-++-++--- +|+++++++++++++ [-, -, +]=I |CCCCCCCCIIIII -|------------- -|++++-++-++--- +|+++++++++++++ [+, +, 0]=J |AAAAAAAAZZZZZ +|+++++++++++++ +|++++-++-++--- 0|++++-++-++--- [0, 0, 0]=O |AAAAAAAAZZZZZ 0|+++++++++++++ 0|++++-++-++--- 0|++++-++-++--- [-, -, 0]=S |CCCCCCCCIIIII -|------------- -|++++-++-++--- 0|+++++++++++++ [+, +, -]=T |AAAAAAAAZZZZZ +|+++++++++++++ +|++++-++-++--- -|++++-++-++--- [+, 0, -]=W |AAAAAAAAZZZZZ +|+++++++++++++ 0|++++-++-++--- -|++++-++-++--- [+, -, -]=Z |AAAAAAAAZZZZZ +|+++++++++++++ -|++++-++-++--- -|++++-++-++--- [0, -, -]=n |AAAAAAAAZZZZZ 0|+++++++++++++ -|++++-++-++--- -|++++-++-++--- [-, -, -]=N |CCCCCCCCIIIII -|------------- -|++++-++-++--- -|+++++++++++++ No ?- */ % a proof of the Paretian-Liberal and the IIA-liberal for weak ordering /* ?- swf(F,rights([(a,b)->1,(a,c)->2,(b,c)->K])),display_swf_t2(F),nl,write([J:K]). No ?- chdom(K). K = l:linear->t:transitive Yes ?- swf(F,rights_i([(a,b)->1,(a,c)->2])). No % % The following query consumes time. % ?- swf(F,rights_p([(a,b)->1,(a,c)->2])). No ?- */ % an experimentation to deter the almost decisiveness % (earlier code has a bug) /* ?- swf(F,na_decisive([i])),display_swf_t2(F),fail. No ?- swf(F,na_decisive([p])),display_swf_t2(F),fail. No ?- */ % demo for the decomposed representaion (2008.5.8) /* ?- T=q,swf(F,arrow(T)),display_swf_t6(F),fail. a, b + - + [+] [+] - [-] [-] a, c + - + [+] [+] - [-] [-] b, c + - + [+] [+] - [-] [-] ---end of swf --- a, b + - + [+] [0] - [0] [-] a, c + - + [+] [0] - [0] [-] b, c + - + [+] [0] - [0] [-] ---end of swf --- a, b + - + [+] [-] - [+] [-] a, c + - + [+] [-] - [+] [-] b, c + - + [+] [-] - [+] [-] ---end of swf --- No ?- chdom(A). A = l:linear->t:transitive Yes ?- T=t,swf(F,arrow(T)),display_swf_t6(F),fail. a, b + 0 - + [+] [+] [+] 0 [0] [0] [0] - [-] [-] [-] a, c + 0 - + [+] [+] [+] 0 [0] [0] [0] - [-] [-] [-] b, c + 0 - + [+] [+] [+] 0 [0] [0] [0] - [-] [-] [-] ---end of swf --- a, b + 0 - + [+] [0] [-] 0 [+] [0] [-] - [+] [0] [-] a, c + 0 - + [+] [0] [-] 0 [+] [0] [-] - [+] [0] [-] b, c + 0 - + [+] [0] [-] 0 [+] [0] [-] - [+] [0] [-] ---end of swf --- No ?- % Arrow's theorem for n=3. ?- chdom(A). A = t:transitive->l:linear Yes ?- make_n_agents(3). Yes ?- swf(F,arrow),display_swf_t6(F,v). a, b [-, -, -]->[-] [+, -, -]->[+] [-, +, -]->[-] [+, +, -]->[+] [-, -, +]->[-] [+, -, +]->[+] [-, +, +]->[-] [+, +, +]->[+] b, c [+, +, +]->[+] [-, +, +]->[-] [+, -, +]->[+] [-, -, +]->[-] [+, +, -]->[+] [-, +, -]->[-] [+, -, -]->[+] [-, -, -]->[-] c, a [+, +, +]->[+] [-, +, +]->[-] [+, -, +]->[+] [-, -, +]->[-] [+, +, -]->[+] [-, +, -]->[-] [+, -, -]->[+] [-, -, -]->[-] ---end of swf --- a, b [-, -, -]->[-] [+, -, -]->[-] [-, +, -]->[+] [+, +, -]->[+] [-, -, +]->[-] [+, -, +]->[-] [-, +, +]->[+] [+, +, +]->[+] b, c [+, +, +]->[+] [-, +, +]->[+] [+, -, +]->[-] [-, -, +]->[-] [+, +, -]->[+] [-, +, -]->[+] [+, -, -]->[-] [-, -, -]->[-] c, a [+, +, +]->[+] [-, +, +]->[+] [+, -, +]->[-] [-, -, +]->[-] [+, +, -]->[+] [-, +, -]->[+] [+, -, -]->[-] [-, -, -]->[-] ---end of swf --- a, b [-, -, -]->[-] [+, -, -]->[-] [-, +, -]->[-] [+, +, -]->[-] [-, -, +]->[+] [+, -, +]->[+] [-, +, +]->[+] [+, +, +]->[+] b, c [+, +, +]->[+] [-, +, +]->[+] [+, -, +]->[+] [-, -, +]->[+] [+, +, -]->[-] [-, +, -]->[-] [+, -, -]->[-] [-, -, -]->[-] c, a [+, +, +]->[+] [-, +, +]->[+] [+, -, +]->[+] [-, -, +]->[+] [+, +, -]->[-] [-, +, -]->[-] [+, -, -]->[-] [-, -, -]->[-] ---end of swf --- No ?- T=q,swf(F,majority),display_swf_t6(F,v). a, b [-, -, -]->[-] [+, -, -]->[-] [-, +, -]->[-] [+, +, -]->[+] [-, -, +]->[-] [+, -, +]->[+] [-, +, +]->[+] [+, +, +]->[+] b, c [+, +, +]->[+] [-, +, +]->[+] [+, -, +]->[+] [-, -, +]->[-] [+, +, -]->[+] [-, +, -]->[-] [+, -, -]->[-] [-, -, -]->[-] c, a [+, +, +]->[+] [-, +, +]->[+] [+, -, +]->[+] [-, -, +]->[-] [+, +, -]->[+] [-, +, -]->[-] [+, -, -]->[-] [-, -, -]->[-] ---end of swf --- T = q F = [ ([[-, +, +], [-, +, +], [-, +, +]]->[-, +, +]), ([[+, -, +], [-, +, +], [-, +, +]]->[-, +, +]), ([[-, -, +], [-, +, +], [-, +|...]]->[-, +, +]), ([[+, +, -], [-, +|...], [-|...]]->[-, +, +]), ([[-, +|...], [-|...], [...|...]]->[-, +, +]), ([[+|...], [...|...]|...]->[-, +|...]), ([[...|...]|...]->[-|...]), ([...|...]->[...|...]), (... ->...)|...] Yes ?- T=q,swf(F,majority),swf(F,arrow(T)). No ?- T=q,swf(F,olig([1,3])),swf(F,arrow(T)),display_swf_t6(F,v). a, b [-, -, -]->[-] [+, -, -]->[0] [-, +, -]->[-] [+, +, -]->[0] [-, -, +]->[0] [+, -, +]->[+] [-, +, +]->[0] [+, +, +]->[+] b, c [+, +, +]->[+] [-, +, +]->[0] [+, -, +]->[+] [-, -, +]->[0] [+, +, -]->[0] [-, +, -]->[-] [+, -, -]->[0] [-, -, -]->[-] c, a [+, +, +]->[+] [-, +, +]->[0] [+, -, +]->[+] [-, -, +]->[0] [+, +, -]->[0] [-, +, -]->[-] [+, -, -]->[0] [-, -, -]->[-] ---end of swf --- */ %--------- % May(1952)'s Theorem (2008.5.9-11) % The one and only anonymous, neutral, and positively responsive % SDF (SWF) is pairwise majority rule. /* 703 ?- chdpm(A). A = (1->2) . 704 ?- display_domain. current domain: CGITVZ [base domain=l:linear] true . 705 ?- swf(F,may(o,[n,a,p])),display_swf(F),display_swf_t6(F,v),fail. swf:row col |CGITVZ -------------------- [-, +, +]=C |CEFKLO [+, -, +]=G |EGHMOQ [-, -, +]=I |FHIOPR [+, +, -]=T |KMOTUW [-, +, -]=V |LOPUVX [+, -, -]=Z |OQRWXZ a, b [-, -]->[-] [+, -]->[0] [-, +]->[0] [+, +]->[+] b, c [+, +]->[+] [-, +]->[0] [+, -]->[0] [-, -]->[-] c, a [+, +]->[+] [-, +]->[0] [+, -]->[0] [-, -]->[-] ---end of swf --- fail. 706 ?- % related results. % neutrality => iia 697 ?- swf(F,may(q,[n])),\+ swf(F,iia(q)),display_swf_t6(F,v),fail. fail. % iia & not neutral: a case 701 ?- swf(F,iia(q)),\+ swf(F,may(q,[n])),display_swf_t6(F,v),write(ok),!,fail. a, b [-, -]->[-] [+, -]->[-] [-, +]->[-] [+, +]->[-] b, c [+, +]->[+] [-, +]->[+] [+, -]->[+] [-, -]->[+] c, a [+, +]->[+] [-, +]->[+] [+, -]->[+] [-, -]->[+] ---end of swf ---ok fail. 703 ?- findall(1,swf(F,may(q,[n])),L),length(L,N). L = [1, 1, 1, 1, 1, 1, 1, 1, 1|...], N = 33. 696 ?- swf(F,may(q,[n])),decompose_swf(XY,F,Fa),sort(Fa,Fb),nl,write([XY]), forall(member(Y,Fb),(write(Y),write(;))),fail. [ (a, b)][+, +]->[-];[+, -]->[+];[-, +]->[-];[-, -]->[+]; [ (b, c)][+, +]->[-];[+, -]->[+];[-, +]->[-];[-, -]->[+]; [ (c, a)][+, +]->[-];[+, -]->[+];[-, +]->[-];[-, -]->[+]; ... [ (c, a)][+, +]->[+];[+, -]->[-];[-, +]->[+];[-, -]->[-]; fail. % n=3 : complete order is required because of Condorcet's cycle. 834 ?- member(X,[a,n,p]),swf(F,majority),swf(F,may(p,[X])). fail. 837 ?- swf(F,majority),swf(F,may(o,[a,n,p])). F = [ ([[-, +, +], [-, +, +], [-, +, +]]->[-, +, +]), ([[+, -, +], [-, +, +], [-, +, +]]->[-, +, +]), ([[-, -, +], [-, +, +], [-, +|...]]->[-, +, +]), ([[+, +, -], [-, +|...], [-|...]]->[-, +, +]), ([[-, +|...], [-|...], [...|...]]->[-, +, +]), ([[+|...], [...|...]|...]->[-, +|...]), ([[...|...]|...]->[-|...]), ([...|...]->[...|...]), (... -> ...)|...] . 838 ?- */ % Sen (1982), Chapter 8, Section 3, Proposition 3: % Originally, Mas-Colell and Sonnenschein (1972)'s theorem. % U, I, P and PR implies D on quasi-transitive-valued SDF (SWF), % if there are at least three agents. /* (1) all dictatorial swfs satisfy positive responsiveness. ?- T=q,swf(F,dict(J)),swf(F,arrow(T)),swf(F,pos_res(T)),write([J]:'yes!'),fail. [1]:yes![2]:yes![3]yes! No (2) all nondictatorial (oligarchy) swfs does not satisfy positive responsiveness. ?- member(C,[[1,2],[2,3],[1,3]]),T=q,swf(F,olig(C)),swf(F,arrow(T)),write(C:'yes!'),fail. [1, 2]:yes![2, 3]:yes![1, 3]:yes! No ?- member(C,[[1,2],[2,3],[1,3]]),T=q,swf(F,olig(C)),\+ swf(F,pos_res(T)),write(C:'no!'),fail. [1, 2]:no![2, 3]:no![1, 3]:no! No (3) There is no nondictatorial swf other than these swfs. ?- T=q,swf(F,arrow(T)),\+ swf(F,dict(J)),display_swf_t6(F,v),fail. ....This will work but take some hours. Please enter command only before bed. */ % demo of SWF for n=3, linear domain and values (2008.5.21) /* ?- [menu],[cswf08],chdpm(_->2),rrgrr(on). current domain: CGITVZ [base domain=l:linear] ?- stopwatch((T=q,swf(F,arrow(T)),display_swf(F),fail);true,Time). swf:row col |CGITVZ -------------------- [-, +, +]=C |CCCCCC [+, -, +]=G |GGGGGG [-, -, +]=I |IIIIII [+, +, -]=T |TTTTTT [-, +, -]=V |VVVVVV [+, -, -]=Z |ZZZZZZ swf:row col |CGITVZ -------------------- [-, +, +]=C |CEFKLO [+, -, +]=G |EGHMOQ [-, -, +]=I |FHIOPR [+, +, -]=T |KMOTUW [-, +, -]=V |LOPUVX [+, -, -]=Z |OQRWXZ swf:row col |CGITVZ -------------------- [-, +, +]=C |CGITVZ [+, -, +]=G |CGITVZ [-, -, +]=I |CGITVZ [+, +, -]=T |CGITVZ [-, +, -]=V |CGITVZ [+, -, -]=Z |CGITVZ % time elapsed (sec): 1.25 T = _G157 F = _G162 Time = 1.25 Yes ?- make_n_agents(3). ?- stopwatch((T=l,swf(F,arrow(T)),display_swf_t6(F,v),fail);true,Time). a, b [+, +, +]->[+] [+, +, -]->[+] [+, -, +]->[+] [+, -, -]->[+] [-, +, +]->[-] [-, +, -]->[-] [-, -, +]->[-] [-, -, -]->[-] b, c [+, +, +]->[+] [+, +, -]->[+] [+, -, +]->[+] [+, -, -]->[+] [-, +, +]->[-] [-, +, -]->[-] [-, -, +]->[-] [-, -, -]->[-] c, a [+, +, +]->[+] [+, +, -]->[+] [+, -, +]->[+] [+, -, -]->[+] [-, +, +]->[-] [-, +, -]->[-] [-, -, +]->[-] [-, -, -]->[-] ---end of swf --- a, b [+, +, +]->[+] [+, +, -]->[+] [+, -, +]->[-] [+, -, -]->[-] [-, +, +]->[+] [-, +, -]->[+] [-, -, +]->[-] [-, -, -]->[-] b, c [+, +, +]->[+] [+, +, -]->[+] [+, -, +]->[-] [+, -, -]->[-] [-, +, +]->[+] [-, +, -]->[+] [-, -, +]->[-] [-, -, -]->[-] c, a [+, +, +]->[+] [+, +, -]->[+] [+, -, +]->[-] [+, -, -]->[-] [-, +, +]->[+] [-, +, -]->[+] [-, -, +]->[-] [-, -, -]->[-] ---end of swf --- a, b [+, +, +]->[+] [+, +, -]->[-] [+, -, +]->[+] [+, -, -]->[-] [-, +, +]->[+] [-, +, -]->[-] [-, -, +]->[+] [-, -, -]->[-] b, c [+, +, +]->[+] [+, +, -]->[-] [+, -, +]->[+] [+, -, -]->[-] [-, +, +]->[+] [-, +, -]->[-] [-, -, +]->[+] [-, -, -]->[-] c, a [+, +, +]->[+] [+, +, -]->[-] [+, -, +]->[+] [+, -, -]->[-] [-, +, +]->[+] [-, +, -]->[-] [-, -, +]->[+] [-, -, -]->[-] ---end of swf --- % time elapsed (sec): 20.484 T = _G14 F = _G19 Time = 20.484 Yes ?- ?- make_n_agents(3). Yes ?- stopwatch((swf(F,arrow),display_swf_t6(F,s),fail);true,Time). [+, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, +, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, +, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] ---end of swf --- [+, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, +, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, -, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] ---end of swf --- [+, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, -, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, +, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] ---end of swf --- % time elapsed (sec): 18.265 F = _G157 Time = 18.265 Yes ?- chdom(_->t:_). ?- stopwatch((swf(F,arrow),display_swf_t6(F,s),fail);true,Time). [0, 0, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, 0, +]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, 0, -]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, +, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, +, +]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, +, -]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, -, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, -, +]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, -, -]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [+, 0, 0]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, 0, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, 0, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, 0]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, 0]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, 0, 0]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, 0, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, 0, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, +, 0]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, +, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, +, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, 0]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] ---end of swf --- [0, 0, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, 0, +]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, 0, -]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, +, 0]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [0, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [0, +, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [0, -, 0]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [0, -, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [0, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, 0, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [+, 0, +]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [+, 0, -]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [+, +, 0]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, 0]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, -, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, 0, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [-, 0, +]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [-, 0, -]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [-, +, 0]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, +, -]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, -, 0]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, +]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] ---end of swf --- [0, 0, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, 0, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [0, 0, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [0, +, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [0, +, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [0, -, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [0, -, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [0, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, 0, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [+, 0, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, 0, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, +, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [+, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, +, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [+, -, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [+, -, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [+, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, 0, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [-, 0, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, 0, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, +, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [-, +, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, +, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] [-, -, 0]->[ (a, b):[0], (a, c):[0], (b, c):[0]] [-, -, +]->[ (a, b):[+], (a, c):[+], (b, c):[+]] [-, -, -]->[ (a, b):[-], (a, c):[-], (b, c):[-]] ---end of swf --- % time elapsed (sec): 1661.11 F = _G14 Time = 1661.11 Yes ?- */ %---- end