/************************************************************ common admissible domain, closedness under decisiveness implicature, and decomposability: proving Kalai-Muller theorem program: dcdi06.pl language: prolog date: 2006.12.22-23,25-26,31 & 2007.1.5-6. creator: Kenryo INDO ************************************************************/ % load the social choice analyzer if oof/2 does not exist. :- (\+ clause(oof(_,_),_)->[spcf06];true). init_me:-init_me(4). init_me(K):- L=[gprf06,cswf06,spcf06,dcdi06], nth1(J,L,P),J=retract(O);true),assert(r_j_admission(J,L)). init_r_admission:- domain_type(T:_),all_r(L,T),update_r_admission(L). init_r_j_admission(J):- j(J), r_admission(L), forall(clause(r_j_admission(J,_),_),update_r_j_admission(J,L)). r_admit(Q):- domain_type(T:_),r_admission(L),R=..[T,Q],R,member(Q,L). % override r/1 (to update domain with r_admit and affect rr/1,3). r_admit_domain:- abolish(r/1),forall(r_admit(Q),assert(r(Q))). % override chdom/1 to initialize r_admission/1. chdom(A->A):- \+ var(A),domain_type(A). chdom(A->B):- domain_type(A),r_type(B),B\=A, update_domain(B),init_r_admission. :- init_r_admission. % override rr/2 (to affect rr/1,3). rr([],[]). rr([Q|R],[J|N]):- rr(R,N),r_j_admitted(J,Q). r_j_admitted(J,Q):- j(J),clause(r_j_admission(J,L),_),r(Q,_,_),oof(Q,L). r_j_admitted(J,Q):- j(J),\+ clause(r_j_admission(J,_),_), r(Q). % generating common admissible domain % specified with type T and length N restricted_domain(L,T,N):- all_r(A,T), (var(L)->select_n(L,A,N);(subset(L,A),length(L,N))), L\=[],update_r_admission(L). select_n([],[],0). select_n([R|Q],[R|S],A):-select_n(Q,S,B), A is B + 1. select_n(Q,[_|S],B):-select_n(Q,S,B). % omission for current domain (added: 31 Dec2006) restricted_domain(L):- domain_type(T:_),restricted_domain(L,T,_). display_domain(L):- (var(L)->r_admission(L);true),forall(oof(R,L),(id_r(_:S,R,_),write(S))). % a experiment of existence of the strategy-proof scf. /* ?- show_scf_hl(l), stopwatch((restricted_domain(L,l,N),\+ \+ (scf(F,sp),cs_scf(F), show_scf_l0(F,l),tab(2),display_domain(L)),fail;true),Time). pref:j=1:ACITZNACITZNACITZNACITZNACITZNACITZN pref:j=2:AAAAAACCCCCCIIIIIITTTTTTZZZZZZNNNNNN best:j=1:abbaccabbaccabbaccabbaccabbaccabbacc best:j=2:aaaaaabbbbbbbbbbbbaaaaaacccccccccccc scf: abbaccabbaccabbaccabbaccabbaccabbacc ACITZN scf: abbaa-bbbbb-bbbbb-abbaa-abbac------- ACITZ scf: aaaa-aabba-babba-baaaa-a------abba-c ACITN scf: abb-ccabb-ccabb-cc------abb-ccabb-cc ACIZN scf: abb-a-bbb-b-bbb-b-------abb-c------- ACIZ scf: aaa--aabb--babb--b------------abb--c ACIN scf: aa-aaaab-aab------aa-aaaaa-accab-acc ACTZN scf: aa-aa-ab-aa-------aa-aa-aa-ac------- ACTZ scf: aa-a-aab-a-b------aa-a-a------ab-a-c ACTN scf: aa--aaab--ab------------aa--ccab--cc ACZN scf: aa--a-ab--a-------------aa--c------- ACZ scf: aa---aab---b------------------ab---c ACN scf: a-bacc------a-bacca-bacca-bacca-bacc AITZN scf: a-baa-------b-bbb-a-baa-a-bac------- AITZ scf: a-aa-a------a-ba-ba-aa-a------a-ba-c AITN scf: a-aa--------b-bc--a-aa-------------- AIT scf: a-b-cc------a-b-cc------a-b-cca-b-cc AIZN scf: a-b-a-------b-b-b-------a-b-c------- AIZ scf: a-a--a------a-b--b------------a-b--c AIN scf: a--a-b------------a--a-c------a--a-c ATN scf: a---ab------------------a---cca---cc AZN scf: a----b------------------------a----c AN scf: -------bbacc-bbacc-bbacc-bbacc-bbacc CITZN scf: -------bbbb--bbbb--bbaa--bbac------- CITZ scf: -------bba-b-bba-b-aaa-a-------bba-c CITN scf: -------bba---bbc---aaa-------------- CIT scf: -------bb-a--bb-c--------bb-c------- CIZ scf: -------b-aab-------a-aaa-a-acc-b-acc CTZN scf: -------b-aa--------a-aa--a-ac------- CTZ scf: -------b-a-b-------a-a-a-------b-a-c CTN scf: -------b--ab-------------a--cc-b--cc CZN scf: -------b--a--------------a--c------- CZ scf: --------------bacc--bacc--bacc--bacc ITZN scf: --------------bbb---baa---bac------- ITZ scf: --------------ba-b--aa-a--------ba-c ITN scf: --------------bc----aa-------------- IT % time elapsed (sec): 3.531 No ?- show_scf_hl(l),stopwatch((restricted_domain(L,l,N), \+ \+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F), show_scf_l0(F,l),tab(2),display_domain(L)),fail;true),Time). pref:j=1:ACITZNACITZNACITZNACITZNACITZNACITZN pref:j=2:AAAAAACCCCCCIIIIIITTTTTTZZZZZZNNNNNN best:j=1:abbaccabbaccabbaccabbaccabbaccabbacc best:j=2:aaaaaabbbbbbbbbbbbaaaaaacccccccccccc scf: abbaa-bbbbb-bbbbb-abbaa-abbac------- ACITZ scf: aaaa-aabba-babba-baaaa-a------abba-c ACITN scf: abb-abbbb-bbbbb-bb------abb-ccbbb-cc ACIZN scf: abb-a-bbb-b-bbb-b-------abb-c------- ACIZ scf: aaa--aabb--babb--b------------abb--c ACIN scf: aa-aaaab-aab------aa-aaaaa-accab-acc ACTZN scf: aa-aa-ab-aa-------aa-aa-aa-ac------- ACTZ scf: aa-a-aab-a-b------aa-a-a------ab-a-c ACTN scf: aa--aaab--ab------------aa--ccab--cc ACZN scf: aa--a-ab--a-------------aa--c------- ACZ scf: aa---aab---b------------------ab---c ACN scf: a-aaaa------a-bacca-aaaaa-cacca-cacc AITZN scf: a-baa-------b-bbb-a-baa-a-bac------- AITZ scf: a-aa-a------a-ba-ba-aa-a------a-ba-c AITN scf: a-aa--------b-bc--a-aa-------------- AIT scf: a-b-ab------b-b-bb------a-b-ccb-b-cc AIZN scf: a-b-a-------b-b-b-------a-b-c------- AIZ scf: a-a--a------a-b--b------------a-b--c AIN scf: a--a-b------------a--a-c------a--a-c ATN scf: a---ab------------------a---cca---cc AZN scf: a----b------------------------a----c AN scf: -------bbbbb-bbbbb-bbacc-bbccc-bbccc CITZN scf: -------bbbb--bbbb--bbaa--bbac------- CITZ scf: -------bba-b-bba-b-aaa-a-------bba-c CITN scf: -------bba---bbc---aaa-------------- CIT scf: -------bb-a--bb-c--------bb-c------- CIZ scf: -------b-aab-------a-aaa-a-acc-b-acc CTZN scf: -------b-aa--------a-aa--a-ac------- CTZ scf: -------b-a-b-------a-a-a-------b-a-c CTN scf: -------b--ab-------------a--cc-b--cc CZN scf: -------b--a--------------a--c------- CZ scf: --------------bacc--aaaa--cacc--cacc ITZN scf: --------------bbb---baa---bac------- ITZ scf: --------------ba-b--aa-a--------ba-c ITN scf: --------------bc----aa-------------- IT % time elapsed (sec): 5.297 L = _G159 N = _G161 F = _G163 Time = 5.297 ?- */ %------------------------------------------------- % decomposability (Kalai and Muller, 1977) % trivial/nontrivial ordered pair dop_trivial((X,Y)):- dop((X,Y)),\+ (r(P),p((X,Y),P),r(Q),p((Y,X),Q)). dop_ntr((X,Y)):- dop((X,Y)),\+ dop_trivial((X,Y)). % closed under decisiveness implicature cdi_pairs(D,Tb):- select_ntr(D,Tb),\+ not_cdi(_,_,D). acyclic_cdi_pairs(D,Tb):- cdi_pairs(D,Tb),\+ circulate(_,D). circulate((X,Y),B):- oof((X,Y),B),oof((Y,X),B). circulate((X,Y),B):- oof((X,Y),B),oof((Y,Z),B),oof((Z,X),B). select_ntr(D,Tb):- findall(B,dop(B),Tb), select_ntr(D,Tb,K),D\=Tb,K>0. select_ntr([],[],0). select_ntr([R|D],[R|S],K):- select_ntr(D,S,K),dop_trivial(R). select_ntr([R|D],[R|S],M):- select_ntr(D,S,K),dop_ntr(R),M is K + 1. select_ntr(D,[R|S],K):- select_ntr(D,S,K),dop_ntr(R). not_cdi((V,C),(X,Y,Z),D):- dot((X,Y,Z)), dop_ntr((X,Y)),dop_ntr((X,Z)),not_cdi(V,(X,Y,Z),C,D). not_cdi((1,A), (X,Y,Z),[(P,Q)],D):- rr([P,Q]), r((X,Y),P),r((Y,Z),P),r((Y,Z),Q),r((Z,X),Q),not_cdi_1(A, (X,Y,Z),D). not_cdi((2,A), (X,Y,Z),[R], D):- r(R), r((X,Y),R),r((Y,Z),R),not_cdi_2(A, (X,Y,Z),D). not_cdi_1(a,(X,Y,Z),D):- oof((X,Y),D),\+ oof((X,Z),D). not_cdi_1(b,(X,Y,Z),D):- oof((Z,X),D),\+ oof((Y,X),D). not_cdi_2(a,(X,Y,Z),D):- oof((X,Y),D),oof((Y,Z),D),\+ oof((X,Z),D). not_cdi_2(b,(X,Y,Z),D):- oof((Z,X),D),oof((Y,X),D),oof((Z,Y),D). not_cdi_2(c,(X,Y,Z),D):- oof((Z,X),D),\+ oof((Y,X),D),\+ oof((Z,Y),D). % decomposability decomposable_domain(L,T,N):- restricted_domain(L,T,N),\+ \+ cdi_pairs(_,_). acyclic_decomposable_domain(L,T,N):- restricted_domain(L,T,N),\+ \+ acyclic_cdi_pairs(_,_). %----------- % demos % the verification of Kalai-Muller Theorem 2 and Theorem 3. % Assuming liner common admmisible domain, % there exists a set of cdi-pairs(cdi-triple) i.e., decomposable domain % <-> there exists an arrovian swf on liner common admmisible domain ...[A] % <-> there exists an exists an scf which satisfies SP + ND ...[B] /* proof:[A] ?- nl,restricted_domain(L,l,N),\+ cdi_pairs(_,_), \+ \+ (swf(F,arrow(l)),\+ dictator(_,F)). No ?- decomposable_domain(L,l,N), \+ (swf(F,arrow(l)),\+ dictator(_,F)). No ?- % addeundum for proving [A]: two latin squares are both decomposable but % there are only Arrovian SWFs using the inadmissible rankings. ?- decomposable_domain(L,l,N), \+ (swf(F,arrow),\+ dictator(_,F)), nl,display_domain(L),write(:),write(L),fail. AIZ:[[+, +, +], [-, -, +], [+, -, -]] CTN:[[-, +, +], [+, +, -], [-, -, -]] No ?- proof:[B] ?- restricted_domain(L,l,N),\+ cdi_pairs(_,_), \+ \+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F)). No ?- decomposable_domain(L,l,N), \+ (scf(F,sp),\+ dictatorial_scf(_,F)). No ?- */ % the verification of an extension of Kalai-Muller Theorem 2 and Theorem 3. % Assuming liner common admmisible domain, % there exists a noncircular set of cdi-pairs(cdi-triple) % i.e., acyclically decomposable domain % <-> there exists an scf which satisfies SP + ND + SC unless it cannot choose best alternative...[B] % <-> there exists an arrovian swf with SC condition ...[A] /* proof:[B] ?- restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_), \+ \+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F)). No ?- acyclic_decomposable_domain(L,l,N), \+ (scf(F,sp),cs_scf(F),\+ dictatorial_scf(_,F)), nl,display_domain(L),tab(1), forall(oof(R,L),(best(A,R),write(A))),fail. ACIT abba ATZN aacc CIZN bbcc No ?- demo_r(l). 1:[+, +, +]:A 3:[-, +, +]:C 9:[-, -, +]:I 19:[+, +, -]:T 25:[+, -, -]:Z 27:[-, -, -]:N Yes ?- */ /* proof:[A] % acyclically decomposable domain -> ND swf ?- acyclic_decomposable_domain(L,l,N), \+ (swf(F,arrow(l)),\+ dictator(_,F)),nl,display_domain(L),fail. No ?- % NOT (ND swf -> acyclically decomposable domain) ?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_), (\+ \+ (swf(F,arrow(l)),\+ dictator(_,F))), display_domain(L),write(;),fail. ACI;ACT;AC;AI;ATZ;AT;AZ;CIN;CI;CT;CN;IZN;IZ;IN;TZN;TZ;TN;ZN; No ?- % ND + CS swf -> acyclically decomposable domain ?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_), (\+ \+ (swf(F,arrow(l)),\+ dictator(_,F),cs(F))). No ?- */ % addendum (admissible domain valued swf) /* ?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_), (\+ \+ (swf(F,arrow),\+ dictator(_,F),cs(F))). No ?- acyclic_decomposable_domain(L,l,N), display_domain(L),write(;), \+ (swf(F,arrow),\+ dictator(_,F)),nl,display_domain(L),fail. AIZ CTN No ?- ?- nl,restricted_domain(L,l,N),\+ acyclic_cdi_pairs(_,_), \+ \+ (swf(F,arrow(l)),\+ dictator(_,F),display_swf_t2(F)), nl,display_domain(domain:L). swf:row col |ACI ab|+-- ac|++- bc|+++ -------------------------------------------------- [+, +, +]=A |AAA +|+++ +|+++ +|+++ [-, +, +]=C |ACC -|+-- +|+++ +|+++ [-, -, +]=I |ACI -|+-- -|++- +|+++ domain:ACI L = [[+, +, +], [-, +, +], [-, -, +]] N = 3 F = _G171 ; swf:row col |ACT ab|+-+ ac|+++ bc|++- -------------------------------------------------- [+, +, +]=A |AAA +|+++ +|+++ +|+++ [-, +, +]=C |AAC -|+-+ +|+++ +|+++ [+, +, -]=T |AAT +|+++ +|+++ -|++- domain:ACT L = [[+, +, +], [-, +, +], [+, +, -]] N = 3 F = _G171 ; swf:row col |AC ab|+- ac|++ bc|++ -------------------------------------------------- [+, +, +]=A |AA +|++ +|++ +|++ [-, +, +]=C |AC -|+- +|++ +|++ domain:AC L = [[+, +, +], [-, +, +]] N = 2 F = _G171 Yes ?- */ %---- end