You selected cswf08.pl
/************************************************************
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)
revised: 2013.8.9. (debug: rr_cube_first_select/2 and display_swf_header/1 )
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
% debug 9 Aug 2013 (to prevent unintended backtrack in collecting profile domain)
rr_cube_first_select([],0).
rr_cube_first_select(M,1):- hyper_plane_cube(M).
rr_cube_first_select(M,2):- rr_cube_first(1,M). % slower
rr_cube_first_select(M,3):- rr_cube_first(M). % slower
rr_cube_first_select(M,4):- rr_cube_first(M).
/*
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('|'), % debug 9 Aug '13 miss-quot ''
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
return to front page.