You selected sged06.pl
/************************************************************
coalitions, simple games, essential decomposability
and transitivity of dominance relations: revised version
program: sged06.pl
language: prolog
date: 2006.12.26-31 & 2007.1.1,5-9,12.
last revision: 21:04 pm, 12 Jan 2007
creator: Kenryo INDO
************************************************************/
% load the ia-domain manager if oof/2 does not exist.
:- (\+ clause(mia_domain(_,_),_)->[drsc06];true).
% cumulative system list
sys_list([gprf06,cswf06,spcf06,dcdi06,drsc06,sged06]).
% override init_me/0
init_me:- sys_list(L),oof(P,L),nl,write(reload:P),[P],fail;true.
% override display_swf_header/0,1 in cswf06
display_swf_header:-
bagof(N,K^R^(id_r(K:N,R),r_j_admitted(2,R)),L),
nl,write('swf:row col |'),write_sequence(L).
display_swf_header(XY):- b(XY),
findall(T,(id_r(_,R),rb(T,XY,R),r_j_admitted(2,R)),L),
tab(1),XY=(X,Y),write(X),write(Y),write(|),write_sequence(L).
%-------------
% generating individual admissible domain
% mia_domain(L,Y) :- .. from drsc06.pl
%-------------
% logical implications
if(A,B):- \+ (A, \+ B). % if(A,B):- forall(A,B).
iff(A,B):- if(A,B),if(B,A).
if(A,B,fail):- A, \+ B.
if(A,B,true):- \+ if(A,B,fail).
only_if(A,B,fail):- \+ A, B.
only_if(A,B,true):- \+ only_if(A,B,fail).
iff(A,B,fail):- if(A,B,fail).
iff(A,B,fail):- only_if(A,B,fail).
iff(A,B,true):- \+ iff(A,B,fail).
%-------------
% list concatenate
l_concat([A],A).
l_concat([L|R],Z):- l_concat(R,Q),concat(L,Q,Z).
%-------------
% display each element in a list
display_each(W):- \+ var(W),forall(oof(X,W),(nl,write(X))).
%-------------
% coalitions and group structure
coalition(C):- c(C).
c(C):- agents(N),select_n(C,N,K),K>0.
all_coalitions(L):- findall(C,c(C),L).
supergroup(C,D):- c_sup(C,D).
subgroup(C,D):- c_sub(C,D).
complementary_group(C,D):- c_comp(C,D).
c_sup(C,D):- (var(C)->c(C);true),c(D),subset(C,D).
c_sub(C,D):- (var(C)->c(C);true),c(D),subset(D,C).
c_comp(C,D):- (var(C)->c(C);true),agents(N),subtract(N,C,D).
% revised: 5 Jan 2007
c_union([],[]).
c_union([C|D],E):-
c_union(D,F),(var(C)->c(C);true),union(C,F,G),sort(G,E).
% revised: 9 Jan 2007
c_meet([],[]).
c_meet([C],C).
c_meet([C|D],E):-
c_meet(D,F),D\=[],(var(C)->c(C);true),intersection(C,F,E).
%-------------
% simple game : a family of winning coalitions
:- dynamic win/2.
winning(C):- var(C),win(C,yes).
winning(C):- \+ var(C),sort(C,C1),win(C2,yes),sort(C2,C1).
loosing(C):- var(C),win(C,no).
loosing(C):- \+ var(C),sort(C,C1),win(C2,no),sort(C2,C1).
all_win(L):- findall(C,win(C,yes),L).
all_loose(L):- findall(C,win(C,no),L).
axioms_for_win([
monotonic:_,
proper:_,
strong:_,
'not weak':_,
essential:_
]).
antonym(monotonic,nonmonotonic).
antonym(proper,improper).
antonym(strong,'not strong').
antonym('not weak',weak(vetoers)).
antonym(essential,inessential(dictator)).
axiom_win(A):- axioms_for_win(X),oof(A:_,X).
verify_axiom_win(A):- \+ not_win(A).
% violations
not_win(monotonic:(C,D)):- winning(C),supergroup(C,D),loosing(D).
not_win(proper:C):- winning(C),c_comp(C,D),winning(D).
not_win(strong:C):- loosing(C),c_comp(C,D),loosing(D).
not_win('not weak':V):- setof(J,vetoer(J),V).
not_win(essential:J):- min_win([[J]]).
% THEOREM (Shapley,1952) No essential game is both weak and strong.
not_win(nondictatorial:J):- setof(J,vetoer(J),[J]).
vetoer(J):- j(J), \+ (win(C,yes), \+ oof(J,C)).
dictator(J):- vetoer(J), \+ (vetoer(K),K\=J).
all_supersets(C,L):- findall(D,supergroup(C,D),L).
seteq(A,B):- subset(A,B),subset(B,A).
% minimal winning coalitions
filter_win(M):- all_win(W),select_n(M,W,_), findall(D,
(oof(C,M),supergroup(C,D)), U), seteq(W,U).
all_filter_win(L):- findall(M,filter_win(M),L).
min_win(M):- all_filter_win(L),all_intersect(L,M).
all_intersect([],[]).
all_intersect([A],A).
all_intersect([A|L],M):- all_intersect(L,Y),intersection(A,Y,M).
dummy_j(J):- j(J),\+ (min_win(M),oof(C,M),oof(J,C)).
all_dummy(L):- findall(J,dummy_j(J),L).
%-------------
% inspecting properties of simple game
inspectall_win([M,P,S,W,E,D]):-
inspect_win(monotonic:M),
inspect_win(proper:P),
inspect_win(strong:S),
inspect_win('not weak':W),
inspect_win(essential:E),
(W=[J]->D=no(J);D=yes).
inspect_win(A:Z):- not_win(A:V),!,Z=no(V).
inspect_win(_:yes).
verify_win(T,F):-
findall(Y,(axiom_win(Y),inspect_win(Y:yes)),T),
findall(Z:P,(axiom_win(Y),antonym(Y,Z),inspect_win(Y:no(P))),F).
verify_win:- all_win(W),verify_win(T,F),
nl,write(game:W),nl,tab(1),write('+':T),nl,tab(1),write('-':F).
%-------------
% generating simple games
% initialize win/2
init_win(L):- abolish(win/2),(var(L)->all_coalitions(L);true),
forall(oof(C,[[]|L]),assert(win(C,no))).
nonempty_set_of_coalitions(W,LC):- select_n(W,LC,K),K>0.
gen_win(W):- gen_win(W,[]).
gen_win(W,CON):- all_coalitions(L),gen_win(W,L,CON).
gen_win(W,L,CON):-
axioms_for_win(Ax),subset(CON,Ax),init_win(L),
nonempty_set_of_coalitions(W,L),update_win(W),
\+ (oof(G:T,CON),\+ inspect_win(G:T)).
update_win(W):- forall(win(C,A),update_win(C,W,A->_)).
update_win(C,W,yes->yes):- oof(C,W).
update_win(C,W,no->no):- \+ oof(C,W).
update_win(C,W,no->yes):-
oof(C,W),retract(win(C,no)),assert(win(C,yes)).
update_win(C,W,yes->no):-
\+ oof(C,W),retract(win(C,yes)),assert(win(C,no)).
:- dynamic win_0/2.
% for rescue: reserve-and-restore
reserve_win:- abolish(win_0/2),forall(win(C,Y),assert(win_0(C,Y))).
restore_win:- forall(win_0(C,Y),assert(win(C,Y))).
display_win:- forall(winning(C),(write(C),write(;))).
% demo
/*
?- gen_win(W).
W = [[1, 2], [1], [2]]
Yes
?- display_win.
[1, 2];[1];[2];
Yes
?- gen_win(W),nl,write(g:W),findall(C,winning(C),L),tab(1),write(w:L),
findall(C,loosing(C),F),tab(1),write(l:F),fail.
g:[[1, 2], [1], [2]] w:[[1, 2], [1], [2]] l:[]
g:[[1, 2], [1]] w:[[1, 2], [1]] l:[[2]]
g:[[1, 2], [2]] w:[[1, 2], [2]] l:[[1]]
g:[[1, 2]] w:[[1, 2]] l:[[1], [2]]
g:[[1], [2]] w:[[1], [2]] l:[[1, 2]]
g:[[1]] w:[[1]] l:[[1, 2], [2]]
g:[[2]] w:[[2]] l:[[1, 2], [1]]
No
?- gen_win(W),nl,write(W),inspectall_win(S),write(S),fail.
[[1, 2], [1], [2]][yes, no([1]), yes, yes, yes]
[[1, 2], [1]][yes, yes, yes, no([1]), no((-weak, [1]))]
[[1, 2], [2]][yes, yes, yes, no([2]), no((-weak, [2]))]
[[1, 2]][yes, yes, no([1]), no([1, 2]), no((-strong, [1]))]
[[1], [2]][no(([1], [1, 2])), no([1]), yes, yes, yes]
[[1]][no(([1], [1, 2])), yes, yes, no([1]), no((-weak, [1]))]
[[2]][no(([2], [1, 2])), yes, yes, no([2]), no((-weak, [2]))]
No
?- gen_win(W,[]),min_win(M),all_dummy(D),nl,write(win:W-min:M:dummy:D),
fail.
win:[[1, 2], [1], [2]]-min:[[1], [2]]:dummy:[]
win:[[1, 2], [1], [2]]-min:[]:dummy:[]
win:[[1, 2], [1]]-min:[[1]]:dummy:[2]
win:[[1, 2], [1]]-min:[]:dummy:[2]
win:[[1, 2], [2]]-min:[[2]]:dummy:[1]
win:[[1, 2], [2]]-min:[]:dummy:[1]
win:[[1, 2]]-min:[[1, 2]]:dummy:[]
win:[[1, 2]]-min:[]:dummy:[]
win:[[1], [2]]-min:[]:dummy:[1, 2]
win:[[1]]-min:[]:dummy:[1, 2]
win:[[2]]-min:[]:dummy:[1, 2]
No
?- gen_win(W,[]),verify_win,fail.
game:[[1, 2], [1], [2]]
+ :[monotonic, strong, not weak, essential]
- :[improper:[1]]
game:[[1, 2], [1]]
+ :[monotonic, proper, strong]
- :[weak(vetoers):[1], inessential(dictator):1]
game:[[1, 2], [2]]
+ :[monotonic, proper, strong]
- :[weak(vetoers):[2], inessential(dictator):2]
game:[[1, 2]]
+ :[monotonic, proper, essential]
- :[not strong:[1], weak(vetoers):[1, 2]]
game:[[1], [2]]
+ :[not weak, essential]
- :[nonmonotonic: ([1], [1, 2]), improper:[1], not strong:[]]
game:[[1]]
+ :[proper, essential]
- :[nonmonotonic: ([1], [1, 2]), not strong:[], weak(vetoers):[1]]
game:[[2]]
+ :[proper, essential]
- :[nonmonotonic: ([2], [1, 2]), not strong:[], weak(vetoers):[2]]
No
?-
% THEOREM (Shapley,1952) No essential game is both weak and strong.
?- gen_win(W,['not weak':no(_),strong:yes]),verify_win,fail.
game:[[1, 2], [1]]
+ :[monotonic, proper, strong]
- :[weak(vetoers):[1], inessential(dictator):1]
game:[[1, 2], [2]]
+ :[monotonic, proper, strong]
- :[weak(vetoers):[2], inessential(dictator):2]
No
?-
% THEOREM (Wilson,1972; Arrow, 1963)
% No nondictatorial game is both proper and strong.
?- gen_win(W,[proper:yes,strong:yes]),verify_win,fail.
game:[[1, 2], [1]]
+ :[monotonic, proper, strong]
- :[weak(vetoers):[1], inessential(dictator):1]
game:[[1, 2], [2]]
+ :[monotonic, proper, strong]
- :[weak(vetoers):[2], inessential(dictator):2]
No
?-
*/
%-------------
% duality
dual_win(D):- findall(C,(win(L,no),c_comp(L,C)),D).
dual_win(W,D):- \+ var(W),
findall(C,((L=[];c(L)),\+ oof(L,W),c_comp(L,C)),D).
blocking(B):- loosing(C),c_comp(C,B),loosing(B).
minimal_blocking(B):- min_block(B).
min_block(B):- blocking(B),\+ (c_sub(B,D),\+ blocking(D)).
% THEOREM (Shapley,1952)
% (1) the dual of the dual of game W is W.
% (2) the dual of game W is proper iff W is strong.
% (3) the dual of game W is W iff W is strong and proper.
% demo
/*
% proof of (1)
?- gen_win(W,[]),dual_win(D),dual_win(D,DD),nl,
write(g:W:d:D:dd:DD),tab(1),(seteq(W,DD)->write(w=dd);true),fail.
g:[[1, 2], [1], [2]]:d:[[1, 2]]:dd:[[1], [1, 2], [2]] w=dd
g:[[1, 2], [1]]:d:[[1, 2], [1]]:dd:[[1], [1, 2]] w=dd
g:[[1, 2], [2]]:d:[[1, 2], [2]]:dd:[[1, 2], [2]] w=dd
g:[[1, 2]]:d:[[1, 2], [2], [1]]:dd:[[1, 2]] w=dd
g:[[1], [2]]:d:[[1, 2], []]:dd:[[1], [2]] w=dd
g:[[1]]:d:[[1, 2], [], [1]]:dd:[[1]] w=dd
g:[[2]]:d:[[1, 2], [], [2]]:dd:[[2]] w=dd
No
?-
% proof of (2)
?- gen_win(W,[]),inspect_win(strong:S),dual_win(D),nl,
write((g=W):(strong=S)),update_win(D),inspect_win(proper:P),
tab(1),write((dual=D):(proper=P)),fail.
(g=[[1, 2], [1], [2]]): (strong=yes) (dual=[[1, 2]]): (proper=yes)
(g=[[1, 2], [1]]): (strong=yes) (dual=[[1, 2], [1]]): (proper=yes)
(g=[[1, 2], [2]]): (strong=yes) (dual=[[1, 2], [2]]): (proper=yes)
(g=[[1, 2]]): (strong=no([1])) (dual=[[1, 2], [2], [1]]): (proper=no([1]))
(g=[[1], [2]]): (strong=no([])) (dual=[[1, 2], []]): (proper=no([]))
(g=[[1]]): (strong=no([])) (dual=[[1], [1, 2], []]): (proper=no([]))
(g=[[2]]): (strong=no([])) (dual=[[2], [1, 2], []]): (proper=no([]))
No
?-
% proof of (3)
?- gen_win(W,[proper:yes,strong:yes]),dual_win(D),
nl,write(g:W:d:D),tab(1),(seteq(W,D)->write(w=dual);true),fail.
g:[[1, 2], [1]]:d:[[1, 2], [1]] w=dual
g:[[1, 2], [2]]:d:[[1, 2], [2]] w=dual
No
?- gen_win(W,[]),
\+ (inspect_win(proper:yes),inspect_win(strong:yes)),dual_win(D),
nl,write(g:W:d:D),tab(1),(seteq(W,D)->write(w=dual);true),fail.
g:[[1, 2], [1], [2]]:d:[[1, 2]]
g:[[1, 2]]:d:[[1, 2], [2], [1]]
g:[[1], [2]]:d:[[1, 2], []]
g:[[1]]:d:[[1, 2], [], [1]]
g:[[2]]:d:[[1, 2], [], [2]]
No
?-
*/
% decisive set as xy-winning coalitions
%-------------
% The following program generates a collection of simple games
% for each pair of alternatives respectively
% (given a set of conditions).
all_d_pairs(L):- findall(XY,d_pair(XY),L).
all_dop(L):- findall(XY,dop(XY),L).
:- dynamic win_b/2.
gen_win_b(W):- gen_win_b(W,_,[]).
gen_win_b(W,D):- gen_win_b(W,D,[]).
gen_win_b(W,D,CON):-
axioms_for_win(A),subset(CON,A),
all_dop(ADP),(var(D)->D=ADP;subset(D,ADP)),
all_coalitions(LC),
gen_win_b_r(W,D,(LC,CON)).
gen_win_b_r([],[],_).
gen_win_b_r([XY:Wxy|WL],[XY|L],(LC,CON)):-
gen_win_b_r(WL,L,(LC,CON)),
gen_win(Wxy,CON).
update_win_b(W):- abolish(win_b/2),
forall(oof(XY:Wxy,W),assert(win_b(XY,Wxy))).
% demo
/*
?- gen_win_b(W,[proper:yes,strong:yes]),
forall(oof(X,W),(nl,write(X))),!,fail.
(a, b):[[1, 2], [1]]
(a, c):[[1, 2], [1]]
(b, c):[[1, 2], [1]]
(b, a):[[1, 2], [1]]
(c, a):[[1, 2], [1]]
(c, b):[[1, 2], [1]]
No
?-
*/
%-------------
% essential decomposability (See Blair and Muller (1983))
r_j_xy(J,R,XY):- dop(XY),r_j_admitted(J,R),r(XY,R).
p_j_xy(J,R,XY):- r_j_xy(J,R,XY),p(XY,R).
xy_winning((X,Y),C):- win_b((X,Y),Wxy), oof(C,Wxy).
% revised : 9 Jan 2007
% agreed preferences in a coalition at a profile
c_agree(C,XY,RC):- c(C),dop(XY),c_agree_r(C,C,XY,RC).
% dominative coalition at a profile
c_agree_rr(C,XY,RR):- agents(N),dop(XY),c_agree_r(N,C,XY,RR),C\=[].
% recursive construction for (maximal) agreed coalition
% revised: 7,10 Jan 2007
c_agree_r([],[],_,[]).
c_agree_r([J|N],[J|C],XY,[Q|R]):- c_agree_r(N,C,XY,R),p_j_xy(J,Q,XY).
c_agree_r([J|N],C,XY,[Q|R]):-
c_agree_r(N,C,XY,R),r_j_admitted(J,Q).%,\+ p_j_xy(J,Q,XY).
pivotal_j(J,(X,Y),C):- dop((X,Y)),
p_j_xy(J,_,(X,Y)),
p_j_xy(J,_,(Y,X)),
xy_winning((X,Y),C),subtract(C,[J],B),
\+ xy_winning((X,Y),B).
c_sub_inhibited_triple((X,Y,Z),C,B):- (var(C)->c(C);true),
findall(J,(oof(J,C),
\+ (p_j_xy(J,_Dj,(X,Y)),p_j_xy(J,_Dj,(Y,Z)))
),B).
% Definition: Assume strict orderings.
% A set of ordered pairs of alternatives D is said
% to be Essentially Decomposable w.r.t. a given profile P under
% the individual admissible domain Di if for every ordered pair
% (x,y) there exists a set of winning coalitions Wxy=W(x,y)
% which satisifies the set of conditions from (ED1) to (ED4)
% simultaneously.
% (ed 1). If for all coalition C,
% (for all i in C, Di contains xy)
% & (for all j in N-C, Dj contains yx)
% then Wxy contains C iff Wyx contains N-C.
% Condition ed 1 implies that the ASWF is asymmetric and complete.
not_ed(1,(X,Y),(C,B)):- dop((X,Y)),
c_comp(C,B),
\+ \+ c_agree(C,(X,Y),_),
\+ \+ c_agree(B,(Y,X),_),
\+ iff(xy_winning((X,Y),C),\+ xy_winning((Y,X),B)).
% (ed 2). Wxy is monotone.
% Condition ed 2 implies that the ASWF is monotonic.
not_ed(2,XY,V):-
win_b(XY,W),update_win(W),not_win(monotonic:V).
% (ed 3). for all individual i, there exists a pair of
% alternatives (xy) and a coalition C such that
% (Di contains both xy and yx) & (Wxy contains C)
% & (Wxy does not contain C-{i})
% Condition ed 3 implies that the ASWF is essential.
% And together with ed 2 and the nonemptiness of Wxy,
% it implies the Pareto condition.
not_ed(3,_,J):- j(J),\+ (dop(XY),pivotal_j(J,XY,_)).
% (ed 4). for all triple of alternative (x,y,z),
% if (Wxy contains C) & (Wyz contains B)
% & (for all i in C, Di contains xy)
% & (for all j in B, Dj contains yz)
% & (for all k in N-C-B, Dk contains zx)
% then Wxz contains a coalition which is
% the union of D,E, and meet(C,B), where
% D:= {i in C| Di does not contain zxy}, and
% E:= {j in B| Dj does not contain yzx}.
% Condition ed 4 implies that the ASWF is transitive.
not_ed(4,(X,Y),(Z,C,B,D,E,F)):- dot((X,Y,Z)),
xy_winning((X,Y),C),xy_winning((Y,Z),B),
\+ \+ c_agree(C,(X,Y),_),\+ \+ c_agree(B,(Y,Z),_),
c_union([C,B],U),c_comp(U,NCB),\+ \+ c_agree(NCB,(Z,X),_),
c_sub_inhibited_triple((Z,X,Y),C,D),
c_sub_inhibited_triple((Y,Z,X),B,E),
c_meet([C,B],CB),c_union([D,E,CB],F),
\+ (F\=[],xy_winning((X,Z),F)).
a_set_of_symmetric_dops(D):- all_d_pairs(L),select_n(P,L,_),
P\=[],findall(XY,(oof((X,Y),P),oof(XY,[(X,Y),(Y,X)])),D).
ed_win(W,D):- ed_win(W,D,[monotonic:yes]).
ed_win(W,D,CON):- (var(CON)->CON=[monotonic:yes];true),
% a_set_of_symmetric_dops(D),
% all_dop(L),select_n(D,L,_),
all_dop(D),
gen_win_b(W,D,CON),update_win_b(W),
\+ not_ed(_,_,_).
%-------------
% some test codes
% overlooking a set of conditions in a list L.
rlxd_ed_win(W,D,L):- \+ var(L), subset(L,[1,2,3,4]),
% a_set_of_symmetric_dops(D),
all_dop(D),
gen_win_b(W,D),update_win_b(W),
\+ (not_ed(K,_,_),\+ oof(K,L)).
/*
% a demo for relaxation
?- rlxd_ed_win(W,D,[1]),nl,write(D),display_win_xy(W).
[ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)]
(a, b):[[1, 2]]
(a, c):[[1, 2]]
(b, c):[[1, 2]]
(b, a):[[1, 2]]
(c, a):[[1, 2], [1], [2]]
(c, b):[[1, 2], [1], [2]]
W = [ (a, b):[[1, 2]], (a, c):[[1, 2]], (b, c):[[1, 2]], (b, a):[[1, 2]], (c, a):[[1, 2], [1], [...]], (c, b):[[1|...], [...]|...]]
D = [ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)]
Yes
?-
*/
%-------------
% the derived essential monotonic social ordering (EM-SWF) :
% xy iff Wxy contains coalition via which x dominates y.
em_swf([],[]).
em_swf([RR->Q|F],[RR|L]):- em_swf(F,L),axiom_em_swf(RR->Q).
em_swf(F):-all_rr(L),em_swf(F,L).
% axioms for em_swf
axiom_em_swf(RR->Q):- l(Q),\+ (c_agree(_,XY,RR),\+ p(XY,Q)).
%-------------
% generating xy-dominative coalitions as xy-minimal winning
% coalition based on an EM-SWF.
em_win_xy(XY,C,F):- (var(F)->em_swf(F);true),
dop(XY),oof(RR->R,F),p(XY,R),c_agree_rr(C,XY,RR).
gen_em_win_xy(XY,L,F):- em_swf(F),setof(C,E^(
em_win_xy(XY,E,F),c(C),subset(E,C)
),L1),
agents(N),
union(L1,[N],L).
gen_em_win(W,F):-
findall(XY:L,gen_em_win_xy(XY,L,F),W), update_win_b(W).
em_swf_1([],[]).
em_swf_1([RR->Q|F],[RR|L]):- em_swf_1(F,L),axiom_em_swf_1(RR->Q).
em_swf_1(F):-all_rr(L),em_swf_1(F,L).
axiom_em_swf_1(RR->Q):- l(Q),\+ (win_b(XY,C),c_agree(C,XY,RR),\+ p(XY,Q)).
% The following clause uses udrr/4 from spcf06.pl
% DEFINITION (Essential SWF):
% An swf f on a linear ordering individual admissible domain
% is essential iff for all agent i there exists a profile PP,
% permissible ordering Qi and a pair (x,y) of alternatives,
% such that f(PP) contains xy and f(PP/Qi) contains yx where
% PP/Qi denotes the unilateral deviated profile.
essential_swf(F):- if(j(J),essential_swf_j((J,_),_XY,F)).
essential_swf_j((J,P,Q,RR,RQ),(X,Y),F):- dop((X,Y)),
oof(RR->R,F),p((X,Y),R),
oof(RQ->S,F),p((Y,X),S),
udrr(RR,RQ,_,(J,P,Q)).
% pivotality is a similar concept (w.r.t. xy-decisive coalition).
% DEFINITION (Monotonic SWF):
% An swf f on a linear ordering individual admissible domain
% is monotonic iff for all pairs (x,y) of alternatives, and for
% all coalitions C, if for every profile PP at which
% x dominates y via C implies that f(PP) contains xy,
% then for any profile QQ at which x dominates y via D s.t.
% C is a subset of D implies f(QQ) still contains xy.
mono_swf([],[]).
mono_swf([RR->Q|F],[RR|L]):- mono_swf(F,L),axiom_mono_swf(RR->Q,F).
mono_swf(F):-all_rr(L),mono_swf(F,L).
% axioms for mono_swf
axiom_mono_swf(RR->Q,F):- l(Q),\+ not_monotonic(RR->Q,F,_).
not_monotonic(RR->Q,F,(XY,D,QQ->S)):-
c_agree_rr(C,XY,RR),p(XY,Q),oof(QQ->S,F),
c_agree_rr(D,XY,QQ),subset(C,D),D\=C,\+ p(XY,S).
not_monotonic(RR->Q,F,(XY,D,QQ->S)):-
c_agree_rr(C,XY,RR),\+ p(XY,Q),oof(QQ->S,F),
c_agree_rr(D,XY,QQ),p(XY,S),subset(D,C),D\=C.
% demo
/*
?- L=[[+,+,-]],R=[[-,-,-]],mia_domain([1:L,2:R],free).
L = [[+, +, -]]
R = [[-, -, -]]
Yes
?- F = [ ([[+, +, -], [-, -, -]]->[+, -, -])],
em_win_xy(XY,W,F),nl,write(XY;W),fail.
a, b;[1]
c, a;[2]
c, b;[1, 2]
No
?- F = [ ([[+, +, -], [-, -, -]]->[+, -, -])],
gen_em_win_xy(XY,W,F),nl,write(XY;W),fail.
a, b;[[1], [1, 2]]
c, a;[[2], [1, 2]]
c, b;[[1, 2]]
No
?- F = [ ([[+, +, -], [-, -, -]]->[+, -, -])],
gen_em_win(W,F),display_each(W),fail.
(a, b):[[1], [1, 2]]
(c, a):[[2], [1, 2]]
(c, b):[[1, 2]]
No
?- em_swf(F).
F = [ ([[+, +, -], [-, -, -]]->[+, +, -])] ;
F = [ ([[+, +, -], [-, -, -]]->[+, -, -])] ;
F = [ ([[+, +, -], [-, -, -]]->[-, -, -])] ;
No
?- em_swf(F),swf(F,arrow(l)),\+ dictator(_,F).
F = [ ([[+, +, -], [-, -, -]]->[+, -, -])] ;
No
?- c_agree(A,B,C),nl,write(A;B;C),fail.
[1, 2];c, b;[[+, +, -], [-, -, -]]
[1];a, b;[[+, +, -]]
[1];a, c;[[+, +, -]]
[1];c, b;[[+, +, -]]
[2];b, a;[[-, -, -]]
[2];c, a;[[-, -, -]]
[2];c, b;[[-, -, -]]
No
?- win_b(A,B),nl,write(A;B),fail.
a, b;[[1], [1, 2]]
c, a;[[2], [1, 2]]
c, b;[[1, 2]]
No
?- em_swf_1(F),nl,write(F),fail.
[ ([[+, +, -], [-, -, -]]->[+, +, +])]
[ ([[+, +, -], [-, -, -]]->[-, +, +])]
[ ([[+, +, -], [-, -, -]]->[-, -, +])]
[ ([[+, +, -], [-, -, -]]->[+, +, -])]
[ ([[+, +, -], [-, -, -]]->[+, -, -])]
[ ([[+, +, -], [-, -, -]]->[-, -, -])]
No
?- em_swf_1(F),
essential_swf_j((J,P,Q,RR,RQ),(X,Y),F).
No
?- L = [[+, +, -], [+, -, -]],R = [[+, -, -], [-, -, -]],
mia_domain([1:L,2:R],free).
L = [[+, +, -], [+, -, -]]
R = [[+, -, -], [-, -, -]]
Yes
?- swf(F,A), \+ mono_swf(F),display_swf_t2(F).
swf:row col |ZN ab|+- ac|-- bc|--
--------------------------------------------------
[+, +, -]=T |AC +|-+ +|++ -|++
[+, -, -]=Z |AC +|-+ -|++ -|++
F = [ ([[+, +, -], [+, -, -]]->[-, +, +]), ([[+, -, -], [+, -, -]]->[-, +, +]), ([[+, +, -], [-, -, -]]->[+, +, +]), ([[+, -, -], [-, -|...]]->[+, +, +])]
A = iia
Yes
?- mono_swf(F),swf(F,iia),display_swf_t2(F).
swf:row col |ZN ab|+- ac|-- bc|--
--------------------------------------------------
[+, +, -]=T |AA +|++ +|++ -|++
[+, -, -]=Z |AA +|++ -|++ -|++
F = [ ([[+, +, -], [+, -, -]]->[+, +, +]), ([[+, -, -], [+, -, -]]->[+, +, +]), ([[+, +, -], [-, -, -]]->[+, +, +]), ([[+, -, -], [-, -|...]]->[+, +, +])]
Yes
?- mono_swf(F),\+ swf(F,iia),display_swf_t2(F).
swf:row col |ZN ab|+- ac|-- bc|--
--------------------------------------------------
[+, +, -]=T |AT +|++ +|++ -|-+
[+, -, -]=Z |AA +|++ -|++ -|++
F = [ ([[+, +, -], [+, -, -]]->[+, +, -]), ([[+, -, -], [+, -, -]]->[+, +, +]), ([[+, +, -], [-, -, -]]->[+, +, +]), ([[+, -, -], [-, -|...]]->[+, +, +])]
Yes
?-
*/
%-------------
% proving Blair-Muller Theorem
% THEOREM (Blair and Muller,1983)
% The following three conditions are equivalent.
% (1) a set of distinct alternatives D is essentially
% decomposable wrt an individually admissible domain
% (2) There is an essential monotonic Arrovian swf.
% (3) There is a coalitional strategy-proof scf.
display_win_xy:- forall(win(XY,C),(nl,write(XY:C))).
display_win_xy(W):- \+ var(W),display_each(W).
% demo
/*
% -------------
% Proving Blair-Muller theorem (for 2-agent 3-alternative case)
% -------------
% setting the domain
?- [menu].
% menu compiled 0.00 sec, 18,696 bytes
Yes
?- display_domain.
current domain: ACITZN
[base domain=l:linear]
Yes
?- model(A,B).
A = states:[a, b, c]
B = agents:[1, 2]
Yes
?-
% Proving the equivalence for the Kalai-Muller theorem
% for common admissible domains (similarly to the way of dcdi06)
?- restricted_domain(L,l,N),
\+ iff(\+ ed_win(W,D),\+ (swf(F,arrow(l)),\+ dictator(_,F))).
No
?- restricted_domain(L,l,N),
\+ iff(\+ ed_win(W,D),\+ (swf(F,arrow(l)),\+ dictator(_,F),em_swf(F))).
No
?-
% a review of dcdi06.pl
?- restricted_domain(L,l,N),
\+ iff(\+ cdi_pairs(_,_),\+ (swf(F,arrow(l)),\+ dictator(_,F))).
No
?-
% -------------
% proof for diagonals :
% Another way to reproduce the Kalai-Muller theorem by
% generating (assymetric) individual admissible domains
% OBSERVATION. Assume symmetric admissible domains.
% A domain is essentially decomposable iff
% there exists a nondictatorial Arrovian SWF.
?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D),
\+ (swf(F,arrow(l)),\+ dictator(_,F))
));true,T).
% time elapsed (sec): 171.562
L = _G158
W = _G172
D = _G173
F = _G179
T = 171.562
Yes
% After revised c_meet/2
?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D),
\+ (swf(F,arrow(l)),\+ dictator(_,F))
));true,T).
% time elapsed (sec): 164.625
L = [[+, +, +], [-, +, +], [-, -, +], [+, +, -], [+, -, -], [-, -, -]]
W = _G175
D = _G176
F = _G182
T = 164.625
Yes
?-
% OBSERVATION. For common admissible domains,
% essentiality is implied by nondictatorship.
% (Generally essentiality implies nondictatorship.)
?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D),
\+ (swf(F,arrow(l)),\+ dictator(_,F),essential_swf(F))
));true,T).
% time elapsed (sec): 171.61
L = _G158
W = _G172
D = _G173
F = _G179
T = 171.61
Yes
% OBSERVATION. For common (symmetric) admissible domains,
% every Arrovian SWF is monotonic.
?- stopwatch((mia_domain([1:L,2:L],free),
swf(F,arrow(l)),\+ mono_swf(F));true,T).
% time elapsed (sec): 116.25
L = _G158
F = _G174
T = 116.25
Yes
% OBSERVATION. Dominance-based SWF provide the equivalent results
% on behalf of the essentiality.
?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D),
\+ (swf(F,arrow(l)),\+ dictator(_,F),em_swf(F))
));true,T).
% time elapsed (sec): 172.218
L = _G161
W = _G175
D = _G176
F = _G182
T = 172.218
Yes
% OBSERVATION. Monotonicity implied by IIA-Pareto SWF
?- stopwatch((mia_domain([1:L,2:R],free),L@ (monotone) essential swf exists.
?- stopwatch((mia_domain([1:L,2:R],free),L@ nondictatorial swf exists
% In asymmetric admissible domains, essential decomposability
% is sufficient (but not necessary) for the exsistence of
% a non-dictatorial Arrovian SWF.
?- stopwatch((mia_domain([1:L,2:R],free),L@[+, -, -])]
Yes
% NOTE: Because of a violation to the 3rd condition under bi-singlton
% domain (L,R) above, it (F) can not be an essential swf.
% DEBUG. A counter example against that (e.d. <- essential swf)??
% ---the result below was caused by
% former codes of both c_agree_rr and c_meet/2.
% individual admissible domain consists of (or contains)
% two latin squares.
?- L = [[+, +, +], [-, -, +], [+, -, -]],
R = [[-, +, +], [+, +, -], [-, -, -]],
mia_domain([1:L,2:R],free),L@[+, +, +]), ([[-, -, +], [-, +, +]]->[-, +, +]), ([[+, -, -], [-, +, +]]->[+, +, +]), ([[+, +, +], [+, +|...]]->[+, +, +]), ([[-, -|...], [+|...]]->[+, +, +]), ([[+|...], [...|...]]->[+, +|...]), ([[...|...]|...]->[+|...]), ([...|...]->[...|...]), (... ->...)]
Yes
?-
% DEBUG. After correction for c_meet, the code below has intended
% to generate the xy-winning coalitions as the decisive set.
?- L = [[+, +, +], [-, -, +], [+, -, -]],
R = [[-, +, +], [+, +, -], [-, -, -]],
mia_domain([1:L,2:R],free),swf(F,arrow(l)),essential_swf(F),
gen_em_win(W,F),display_win_xy(W),!,fail.
1.(a, b):[[1], [2], [1, 2]]
2.(a, c):[[1], [2], [1, 2]]
3.(b, c):[[1], [2], [1, 2]]
4.(b, a):[[1], [2], [1, 2]]
5.(c, a):[[1], [2], [1, 2]]
6.(c, b):[[1], [2], [1, 2]]
No
?- not_ed(A,B,C).
A = 1
B = a, b
C = [1], [2]
Yes
?-
% DEBUG. before the revision, the following results has come
% by same code as above.
?- L = [[+, +, -], [+, -, -]],R = [[+, -, -], [-, -, -]],
mia_domain([1:L,2:R],free),
\+ (swf(F,arrow(l)),mono_swf(F),essential_swf(F)),
ed_win(W,D),display_win_xy(W),nl,write(D).
(a, b):[[1, 2], [2]]
(a, c):[[1, 2], [2]]
(b, c):[[1, 2], [1], [2]]
(b, a):[[1, 2], [1], [2]]
(c, a):[[1, 2], [1], [2]]
(c, b):[[1, 2], [1], [2]]
[ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)]
L = [[+, +, -], [+, -, -]]
R = [[+, -, -], [-, -, -]]
F = _G180
W = [ (a, b):[[1, 2], [2]], (a, c):[[1, 2], [2]], (b, c):[[1, 2], [1], [2]], (b, a):[[1, 2], [1], [2]], (c, a):[[1, 2], [1], [...]], (c, b):[[1|...], [...]|...]]
D = [ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)]
Yes
?- (...try and error, many times )
% ADDENDUM. proving for domains of equal-length (a result)
?- restricted_domain(L,l,2).
L = [[+, +, +], [-, +, +]]
Yes
?- stopwatch((mia_domain(L,len(N)),
\+ iff(\+ ed_win(W,D),\+ (swf(F,arrow(l)),\+ dictator(_,F))));true,T).
% time elapsed (sec): 93.188
L = _G159
N = _G157
W = _G162
D = _G163
F = _G169
T = 93.188
Yes
?-
*/
%-------------
% another derived social ordering (SWF) based on dominance relation :
% xy iff there is no Wxy which contains coalition via which y dominates x.
t_swf([],[]).
t_swf([RR->Q|F],[RR|L]):- t_swf(F,L),axiom_t_swf(RR->Q).
t_swf(F):-all_rr(L),t_swf(F,L).
% axioms for transitive swf
axiom_t_swf(RR->Q):- o(Q),
\+ (dop((X,Y)),\+ iff(\+ c_agree(_,(Y,X),RR),r((X,Y),Q))).
% demo
/*
?- t_swf(F),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
?-
*/
%-------------
% Necessary and sufficient condition of transitivity
% for dominance relations (See Kaneko(1975))
% DEF. For a triple t=(X,Y,Z), W_t (resp. k_t) is the collection
% of dominative coalitions (resp. dominance relations)
% for all pairs of X, Y, Z.
dop_in_triple((U,V),(X,Y,Z)):- dop((U,V)),subset([U,V],[X,Y,Z]).
d_pair_in_triple((U,V),(X,Y,Z)):- d_pair((U,V)),subset([U,V],[X,Y,Z]).
all_dop_in_triple(L,T):- dot(T),findall(U,dop_in_triple(U,T),L).
all_d_pairs_in_triple(L,T):- dot(T),findall(U,d_pair_in_triple(U,T),L).
% dominance relation 3: agreed preferences in a winning coalition
w_dom(C,(X,Y),RR,+):- c_agree_rr(C,(X,Y),RR),winning(C).
w_dom(C,(X,Y),RR,-):- w_dom(C,(Y,X),RR,+).
w_dom(C,(X,Y),RR):- w_dom(C,(Y,X),RR,+).
% transitivity of dominance relation w_dom
trans_w_dom(RR,B):-
rr(RR),findall(X>Y,w_dom(_,(X,Y),RR),B1),sort(B1,B),trans(B).
intrans_w_dom(RR,B,T):-
rr(RR),findall(X>Y,w_dom(_,(X,Y),RR),B1),sort(B1,B),intrans(T,B).
% derived preference relation
r_dom((X,Y),RR):- rr(RR),dop((X,Y)),\+ w_dom(_,(Y,X),RR,+).
% CLAIM.
% r_dom can be seen as a variant of Arrovian swf on admissible domains.
% And it is nondictatorial if \+ w_dom([J],XY,RR,+).
% transitivity of r_dom
trans_r_dom(RR,B):- rr(RR),findall(X>Y,r_dom((X,Y),RR),B),trans(B).
intrans_r_dom(RR,B,T):- rr(RR),findall(X>Y,r_dom((X,Y),RR),B),intrans(T,B).
w_t_r(_,_,[],[],[]).
w_t_r((X,Y,Z),R,[S:XY:C|K],W,[XY|L]):-
w_t_r((X,Y,Z),R,K,W0,L),w_dom(C,XY,R,S),
(oof(C,W0)->W=W0;W=[C|W0]).
w_t_r((X,Y,Z),R,K,W,[XY|L]):-
w_t_r((X,Y,Z),R,K,W,L),\+ w_dom(_,XY,R,_).
w_t(XYZ,R,K,W):- all_d_pairs_in_triple(L,XYZ),w_t_r(XYZ,R,K,W,L).
% demo
/*
?- init_me.
(...)
Yes
?- gen_win(W).
W = [[1, 2], [1], [2]]
Yes
?- w_t((a,b,c),R,K,W),length(W,N).
R = [[+, +, +], [+, +, +]]
K = [+ : (a, b):[1, 2], + : (a, c):[1, 2], + : (b, c):[1, 2]]
W = [[1, 2]]
N = 1 ;
R = [[+, +, +], [+, +, +]]
K = [+ : (a, b):[1], + : (a, c):[1, 2], + : (b, c):[1, 2]]
W = [[1], [1, 2]]
Yes
?- make_n_agents(3).
Yes
?- w_t((a,b,c),R,K,W),length(W,N).
R = [[+, +, +], [+, +, +], [+, +, +]]
K = [+ : (a, b):[1, 2], + : (a, c):[1, 2], + : (b, c):[1, 2]]
W = [[1, 2]]
N = 1 ;
R = [[+, +, +], [+, +, +], [+, +, +]]
K = [+ : (a, b):[1], + : (a, c):[1, 2], + : (b, c):[1, 2]]
W = [[1], [1, 2]]
N = 2 ;
Yes
% REMARK. W_t has at most three coalitions (Kaneko(1975), p.387)
?- w_t((a,b,c),R,K,W),length(W,N),N>3.
No
?-
*/
% DEF. For a triple t=(X,Y,Z),
% U_t is an empty set if W_t is a singlton set or an empty set;
% if W_t consists of two dominative coalitions, then the union;
% if W_t consists of three dominative coalitions, then the union of
% the meet of each pair of dominative coalitions.
u_t((T,RR,WL),WT,U):- w_t(T,RR,WL,WT),u_t_1(WT,U).
u_t_1([],[]).
u_t_1([_],[]).
u_t_1([S,T],U):- c_union([S,T],U).
u_t_1([S,T,V],U):-
c_meet([S,T],ST),c_meet([T,V],TV),c_meet([V,S],VS),
c_union([ST,TV,VS],U).
% Condition T (Condition 2.5 in Kaneko(1975)):
% for any distinct triple of alternatives t=(X,Y,Z), one of the
% following conditions is true for every agent in U_t.
% (1) Some A in {X,Y,Z} is not worst in the triple. That is one
% of the remaining two is strictly preferred to A.
% (2) Some A in {X,Y,Z} is not best in the triple. That is A
% is strictly preferred to one of the remaining two.
oof_triple(A,T):- dot(T),T=(X,Y,Z),oof(A,[X,Y,Z]).
% Condition T for the transitivity of dominance relations
% where value/4 from drsc06
t_value((RR,T,U),-Value,A):- u_t((T,RR,_),_,U),
oof(Value,[worst,best]),oof_triple(A,T),
\+ (oof(J,U),r_j(J,RR,R),value(Value:A,T,R)).
t_value(fail,(RR,T)):- rr(RR),d_triple(T),
\+ t_value((RR,T,_),_,_).
t_value(RR):- rr(RR),\+ t_value(fail,(RR,_)).
% THEOREM (Kaneko,1975).
% Assume a proper (monotone) simple game. The dominance relation
% (w_dom_rr in our implementation) is transitive
% iff Condition T holds.
% demo
/*
?- display_domain.
current domain: ACITZN
[base domain=l:linear]
Yes
?- make_n_agents(2).
Yes
?- init_r_admission.
Yes
?- r_j_admission(J,R),name_domain(S,R),nl,write(J:S),fail.
1:ACITZN
2:ACITZN
No
?- gen_win(W).
W = [[1, 2], [1], [2]]
Yes
?- trans_w_dom(RR,B),nl,write(RR:B),fail.
[[+, +, +], [+, +, +]]:[b>a, c>a, c>b]
[[-, +, +], [+, +, +]]:[b>a, c>a, c>b, a>b]
[[+, +, -], [+, +, +]]:[b>a, c>a, c>b, b>c]
[[-, -, -], [+, +, +]]:[b>a, c>a, c>b, a>b, a>c, b>c]
[[+, +, +], [-, +, +]]:[b>a, c>a, c>b, a>b]
[[-, +, +], [-, +, +]]:[c>a, c>b, a>b]
[[-, -, +], [-, +, +]]:[c>a, c>b, a>b, a>c]
[[+, -, -], [-, +, +]]:[b>a, c>a, c>b, a>b, a>c, b>c]
[[-, +, +], [-, -, +]]:[c>a, c>b, a>b, a>c]
[[-, -, +], [-, -, +]]:[c>b, a>b, a>c]
[[+, +, -], [-, -, +]]:[b>a, c>a, c>b, a>b, a>c, b>c]
[[-, -, -], [-, -, +]]:[c>b, a>b, a>c, b>c]
[[+, +, +], [+, +, -]]:[b>a, c>a, c>b, b>c]
[[-, -, +], [+, +, -]]:[b>a, c>a, c>b, a>b, a>c, b>c]
[[+, +, -], [+, +, -]]:[b>a, c>a, b>c]
[[+, -, -], [+, +, -]]:[b>a, c>a, a>c, b>c]
[[-, +, +], [+, -, -]]:[b>a, c>a, c>b, a>b, a>c, b>c]
[[+, +, -], [+, -, -]]:[b>a, c>a, a>c, b>c]
[[+, -, -], [+, -, -]]:[b>a, a>c, b>c]
[[-, -, -], [+, -, -]]:[b>a, a>b, a>c, b>c]
[[+, +, +], [-, -, -]]:[b>a, c>a, c>b, a>b, a>c, b>c]
[[-, -, +], [-, -, -]]:[c>b, a>b, a>c, b>c]
[[+, -, -], [-, -, -]]:[b>a, a>b, a>c, b>c]
[[-, -, -], [-, -, -]]:[a>b, a>c, b>c]
No
?- gen_win(W).
W = [[1, 2], [1], [2]] ;
W = [[1, 2], [1]]
Yes
?- trans_w_dom(RR,B),nl,write(RR:B),fail.
[[+, +, +], [+, +, +]]:[b>a, c>a, c>b]
[[-, +, +], [+, +, +]]:[c>a, c>b, a>b]
[[-, -, +], [+, +, +]]:[c>b, a>b, a>c]
[[+, +, -], [+, +, +]]:[b>a, c>a, b>c]
[[+, -, -], [+, +, +]]:[b>a, a>c, b>c]
[[-, -, -], [+, +, +]]:[a>b, a>c, b>c]
[[+, +, +], [-, +, +]]:[b>a, c>a, c>b]
[[-, +, +], [-, +, +]]:[c>a, c>b, a>b]
[[-, -, +], [-, +, +]]:[c>b, a>b, a>c]
[[+, +, -], [-, +, +]]:[b>a, c>a, b>c]
[[+, -, -], [-, +, +]]:[b>a, a>c, b>c]
[[-, -, -], [-, +, +]]:[a>b, a>c, b>c]
[[+, +, +], [-, -, +]]:[b>a, c>a, c>b]
[[-, +, +], [-, -, +]]:[c>a, c>b, a>b]
[[-, -, +], [-, -, +]]:[c>b, a>b, a>c]
[[+, +, -], [-, -, +]]:[b>a, c>a, b>c]
[[+, -, -], [-, -, +]]:[b>a, a>c, b>c]
[[-, -, -], [-, -, +]]:[a>b, a>c, b>c]
[[+, +, +], [+, +, -]]:[b>a, c>a, c>b]
[[-, +, +], [+, +, -]]:[c>a, c>b, a>b]
[[-, -, +], [+, +, -]]:[c>b, a>b, a>c]
[[+, +, -], [+, +, -]]:[b>a, c>a, b>c]
[[+, -, -], [+, +, -]]:[b>a, a>c, b>c]
[[-, -, -], [+, +, -]]:[a>b, a>c, b>c]
[[+, +, +], [+, -, -]]:[b>a, c>a, c>b]
[[-, +, +], [+, -, -]]:[c>a, c>b, a>b]
[[-, -, +], [+, -, -]]:[c>b, a>b, a>c]
[[+, +, -], [+, -, -]]:[b>a, c>a, b>c]
[[+, -, -], [+, -, -]]:[b>a, a>c, b>c]
[[-, -, -], [+, -, -]]:[a>b, a>c, b>c]
[[+, +, +], [-, -, -]]:[b>a, c>a, c>b]
[[-, +, +], [-, -, -]]:[c>a, c>b, a>b]
[[-, -, +], [-, -, -]]:[c>b, a>b, a>c]
[[+, +, -], [-, -, -]]:[b>a, c>a, b>c]
[[+, -, -], [-, -, -]]:[b>a, a>c, b>c]
[[-, -, -], [-, -, -]]:[a>b, a>c, b>c]
No
?- gen_win([[1]]).
Yes
?- trans_w_dom(RR,B),nl,write(RR:B),fail.
[[+, +, +], [+, +, +]]:[b>a, c>a, c>b]
[[-, +, +], [+, +, +]]:[a>b, c>a, c>b]
[[-, -, +], [+, +, +]]:[a>b, a>c, c>b]
[[+, +, -], [+, +, +]]:[b>a, b>c, c>a]
[[+, -, -], [+, +, +]]:[a>c, b>a, b>c]
[[-, -, -], [+, +, +]]:[a>b, a>c, b>c]
[[+, +, +], [-, +, +]]:[b>a, c>a, c>b]
[[-, +, +], [-, +, +]]:[a>b, c>a, c>b]
[[-, -, +], [-, +, +]]:[a>b, a>c, c>b]
[[+, +, -], [-, +, +]]:[b>a, b>c, c>a]
[[+, -, -], [-, +, +]]:[a>c, b>a, b>c]
[[-, -, -], [-, +, +]]:[a>b, a>c, b>c]
[[+, +, +], [-, -, +]]:[b>a, c>a, c>b]
[[-, +, +], [-, -, +]]:[a>b, c>a, c>b]
[[-, -, +], [-, -, +]]:[a>b, a>c, c>b]
[[+, +, -], [-, -, +]]:[b>a, b>c, c>a]
[[+, -, -], [-, -, +]]:[a>c, b>a, b>c]
[[-, -, -], [-, -, +]]:[a>b, a>c, b>c]
[[+, +, +], [+, +, -]]:[b>a, c>a, c>b]
[[-, +, +], [+, +, -]]:[a>b, c>a, c>b]
[[-, -, +], [+, +, -]]:[a>b, a>c, c>b]
[[+, +, -], [+, +, -]]:[b>a, b>c, c>a]
[[+, -, -], [+, +, -]]:[a>c, b>a, b>c]
[[-, -, -], [+, +, -]]:[a>b, a>c, b>c]
[[+, +, +], [+, -, -]]:[b>a, c>a, c>b]
[[-, +, +], [+, -, -]]:[a>b, c>a, c>b]
[[-, -, +], [+, -, -]]:[a>b, a>c, c>b]
[[+, +, -], [+, -, -]]:[b>a, b>c, c>a]
[[+, -, -], [+, -, -]]:[a>c, b>a, b>c]
[[-, -, -], [+, -, -]]:[a>b, a>c, b>c]
[[+, +, +], [-, -, -]]:[b>a, c>a, c>b]
[[-, +, +], [-, -, -]]:[a>b, c>a, c>b]
[[-, -, +], [-, -, -]]:[a>b, a>c, c>b]
[[+, +, -], [-, -, -]]:[b>a, b>c, c>a]
[[+, -, -], [-, -, -]]:[a>c, b>a, b>c]
[[-, -, -], [-, -, -]]:[a>b, a>c, b>c]
No
?- gen_win(W),nl,display_win,nl,
intrans_w_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail.
[1, 2];[1];[2];
IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN;
[1, 2];[1];
[1, 2];[2];
[1, 2];
[1];[2];
IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN;
[1];
[2];
No
?- gen_win(W,[proper:yes]),nl,display_win,nl,
intrans_w_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail.
[1, 2];[1];
[1, 2];[2];
[1, 2];
[1];
[2];
No
?- gen_win(W,[monotonic:yes,proper:yes]),nl,display_win,nl,
intrans_w_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail.
[1, 2];[1];
[1, 2];[2];
[1, 2];
No
?- mia_domain([1:L,2:R],free),
gen_win(W,[proper:yes]),\+ intrans_r_dom(_,_,_).
L = [[-, -, -]]
R = [[-, -, -]]
W = [[1, 2], [1]]
Yes
?- t_value(fail,_).
No
?- mia_domain([1:L,2:R],free),L@=c, b>c]
A = _G196
Yes
?- mia_domain([1:L,2:R],free),L@=c, b>c]
A = _G196
B = _G200
No
?-
*/
% An additional observation of transitivity.
/*
?- L = [[+, +, -]],R = [[-, -, -]],W = [[1, 2], [1]],
mia_domain([1:L,2:R],free),L@= Condition T.
?- stopwatch((
mia_domain([1:L,2:R],free),L@=b, a>c, b>a, b>c, c>a]
XYZ = [c, a, b]
Time = 1.344
Yes
?- W = [[1, 2, 3], [1, 2], [1], [2]],
gen_win(W,[monotonic:yes,proper:yes]).
No
?-
% a proof of only-if paet when n=3
%(12 Jan 2007. I used a relatively slow machine in the experiment.)
?- stopwatch((
mia_domain([1:L,2:R,3:S],free),L@= Condition T.
?- stopwatch((
mia_domain([1:L,2:R],free),L@=b, a>c, b>a, c>a, c>b]
XYZ = [b, a, c]
T = 0.0469999
Yes
?- w_dom(C,X,L,+).
C = [1, 2]
X = c, b
L = [[+, +, -], [-, -, -]] ;
No
?- stopwatch((
mia_domain([1:L,2:R],free),L@=b, a>c, b>a, c>a, c>b]
XYZ = [b, a, c]
T = 0.0469999
Yes
?- w_dom(C,X,L,+).
C = [1, 2]
X = c, b
L = [[+, +, -], [-, -, -]] ;
No
?- w_t((a,b,c),R,K,W),length(W,N).
R = [[+, +, -], [-, -, -]]
K = [- : (b, c):[1, 2]]
W = [[1, 2]]
N = 1 ;
No
?- u_t(((a,b,c),R,K),W,U).
R = [[+, +, -], [-, -, -]]
K = [- : (b, c):[1, 2]]
W = [[1, 2]]
U = []
Yes
?- gen_win(W),nl,display_win,nl,
intrans_r_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail.
[1, 2];[1];[2];
[1, 2];[1];
[1, 2];[2];
[1, 2];
TN;
[1];[2];
[1];
[2];
No
?-
*/
% Other observations about r_dom and its transitivity
/*
?- init_r_admission.
Yes
?- display_win.
[1, 2];[1];[2];
Yes
?- trans_r_dom(RR,B),nl,write(RR:B),fail.
[[+, +, +], [+, +, +]]:[a>b, a>c, b>c]
[[-, +, +], [+, +, +]]:[a>c, b>c]
[[-, -, +], [+, +, +]]:[b>c]
[[+, +, -], [+, +, +]]:[a>b, a>c]
[[+, -, -], [+, +, +]]:[a>b]
[[-, -, -], [+, +, +]]:[]
[[+, +, +], [-, +, +]]:[a>c, b>c]
[[-, +, +], [-, +, +]]:[a>c, b>c, b>a]
[[-, -, +], [-, +, +]]:[b>c, b>a]
[[+, +, -], [-, +, +]]:[a>c]
[[+, -, -], [-, +, +]]:[]
[[-, -, -], [-, +, +]]:[b>a]
[[+, +, +], [-, -, +]]:[b>c]
[[-, +, +], [-, -, +]]:[b>c, b>a]
[[-, -, +], [-, -, +]]:[b>c, b>a, c>a]
[[+, +, -], [-, -, +]]:[]
[[+, -, -], [-, -, +]]:[c>a]
[[-, -, -], [-, -, +]]:[b>a, c>a]
[[+, +, +], [+, +, -]]:[a>b, a>c]
[[-, +, +], [+, +, -]]:[a>c]
[[-, -, +], [+, +, -]]:[]
[[+, +, -], [+, +, -]]:[a>b, a>c, c>b]
[[+, -, -], [+, +, -]]:[a>b, c>b]
[[-, -, -], [+, +, -]]:[c>b]
[[+, +, +], [+, -, -]]:[a>b]
[[-, +, +], [+, -, -]]:[]
[[-, -, +], [+, -, -]]:[c>a]
[[+, +, -], [+, -, -]]:[a>b, c>b]
[[+, -, -], [+, -, -]]:[a>b, c>a, c>b]
[[-, -, -], [+, -, -]]:[c>a, c>b]
[[+, +, +], [-, -, -]]:[]
[[-, +, +], [-, -, -]]:[b>a]
[[-, -, +], [-, -, -]]:[b>a, c>a]
[[+, +, -], [-, -, -]]:[c>b]
[[+, -, -], [-, -, -]]:[c>a, c>b]
[[-, -, -], [-, -, -]]:[b>a, c>a, c>b]
No
?- trans_r_dom(RR,[]),!,w_dom(C,XY,RR,+),nl,write(RR:C:XY),fail.
[[-, -, -], [+, +, +]]:[2]: (a, b)
[[-, -, -], [+, +, +]]:[2]: (a, c)
[[-, -, -], [+, +, +]]:[2]: (b, c)
[[-, -, -], [+, +, +]]:[1]: (b, a)
[[-, -, -], [+, +, +]]:[1]: (c, a)
[[-, -, -], [+, +, +]]:[1]: (c, b)
No
?- trans_r_dom(RR,[]),!,c_agree_rr(C,XY,RR),nl,write(RR:XY:C),fail.
[[-, -, -], [+, +, +]]: (a, b):[2]
[[-, -, -], [+, +, +]]: (a, c):[2]
[[-, -, -], [+, +, +]]: (b, c):[2]
[[-, -, -], [+, +, +]]: (b, a):[1]
[[-, -, -], [+, +, +]]: (c, a):[1]
[[-, -, -], [+, +, +]]: (c, b):[1]
No
?- intrans_r_dom(RR,B,V),name_domain(S,RR),nl,write(S:V),fail.
No
?- gen_win(W),nl,display_win,nl,
intrans_r_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail.
[1, 2];[1];[2];
[1, 2];[1];
[1, 2];[2];
[1, 2];
IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN;
[1];[2];
[1];
[2];
No
?- gen_win(W,[proper:yes]),nl,display_win,nl,
intrans_r_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail.
[1, 2];[1];
[1, 2];[2];
[1, 2];
IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN;
[1];
[2];
No
?- mia_domain([1:L,2:R],free),
gen_win(W,[proper:yes]),\+ intrans_r_dom(_,_,_).
L = [[-, -, -]]
R = [[-, -, -]]
W = [[1, 2], [1]]
Yes
?- t_value(fail,_).
No
?- mia_domain([1:L,2:R],free),L@=
return to front page.